Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/.github/workflows/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 447 B image not shown  

Quelle  path_lems.prf   Sprache: unbekannt

 
(path_lems
 (Pigeon_hole 0
  (Pigeon_hole-1 nil 3507100594
   ("" (skosimp*)
    (("" (lemma "seq_pigeon_hole[T,(vert(GF!1))]")
      (("" (inst?)
        (("1" (assert)
          (("1" (skosimp*)
            (("1" (inst?)
              (("1" (inst 2 "j!1")
                (("1" (expand "finseq_appl")
                  (("1" (assert) nil)))))))))))
         ("2" (skosimp*)
          (("2" (hide 2)
            (("2" (typepred "x1!1")
              (("2" (typepred "w!1")
                (("2" (expand "walk?")
                  (("2" (flatten)
                    (("2" (expand "verts_in?")
                      (("2" (inst?) nil))))))))))))))))))))
    nil)
   ((Graph type-eq-decl nil graphs nil)
    (nonempty? const-decl "bool" sets nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil path_lems nil)
    (seq_pigeon_hole formula-decl nil seq_pigeon "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (verts_in? const-decl "bool" walks nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (below type-eq-decl nil naturalnumbers nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (GF!1 skolem-const-decl "Graph[T]" path_lems nil)
    (Walk type-eq-decl nil walks nil)
    (w!1 skolem-const-decl "Walk[T](GF!1)" path_lems nil))
   nil)))

100%


[ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ]