products/sources/formale Sprachen/PVS/digraphs image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Merge.thy   Sprache: Lisp

Untersuchung PVS©

(cycles
 (cycle?_TCC1 0
  (cycle?_TCC1-1 nil 3559643154 ("" (subtype-tcc) nil nil)
   ((T formal-type-decl nil cycles nil)
    (verts_in? const-decl "bool" walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (edge? const-decl "bool" digraphs nil)
    (walk? const-decl "bool" walks nil)
    (pre_circuit? const-decl "bool" circuits nil)
    (circuit? const-decl "bool" circuits nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (cycle?_TCC2 0
  (cycle?_TCC2-1 nil 3559643154 ("" (subtype-tcc) nil nil)
   ((T formal-type-decl nil cycles nil)
    (verts_in? const-decl "bool" walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (edge? const-decl "bool" digraphs nil)
    (walk? const-decl "bool" walks nil)
    (pre_circuit? const-decl "bool" circuits nil)
    (circuit? const-decl "bool" circuits nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (cycle_is_circuit 0
  (cycle_is_circuit-1 nil 3559643176
   ("" (skeep)
    (("" (expand "cycle?")
      (("" (expand "circuit?")
        (("" (flatten) (("" (assertnil nil)) nil)) nil))
      nil))
    nil)
   ((cycle? const-decl "bool" cycles nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (circuit? const-decl "bool" circuits nil))
   shostak))
 (circuit_subwalk_cycle_TCC1 0
  (circuit_subwalk_cycle_TCC1-1 nil 3564335113
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs 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)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks nil)
    (T formal-type-decl nil cycles nil)
    (verts_in? const-decl "bool" walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (edge? const-decl "bool" digraphs nil)
    (walk? const-decl "bool" walks nil)
    (pre_circuit? const-decl "bool" circuits nil)
    (circuit? const-decl "bool" circuits nil))
   nil))
 (circuit_subwalk_cycle 0
  (circuit_subwalk_cycle-1 nil 3564335167
   ("" (measure-induct+ "length(w)" "w")
    (("1" (skeep)
      (("1" (case "cycle?(G, x!1)")
        (("1" (hide -2)
          (("1" (inst 1 "x!1")
            (("1" (split)
              (("1" (expand "sub_walk?")
                (("1" (inst 1 "0" "length(x!1) - 1")
                  (("1" (decompose-equality)
                    (("1" (expand"^" "min"nil nil)
                     ("2" (decompose-equality)
                      (("2" (expand"^" "min"nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil)
         ("2" (expand "cycle?" 1)
          (("2" (prop)
            (("2" (skeep)
              (("2" (expand "finseq_appl")
                (("2" (case "i < j")
                  (("1" (inst -3 "x!1^(i, j)")
                    (("1" (inst -3 "G")
                      (("1" (expand "^" -3 1)
                        (("1" (expand"empty_seq" "min")
                          (("1" (assert)
                            (("1" (split -3)
                              (("1"
                                (skeep -1)
                                (("1"
                                  (inst 2 "w1")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (expand "sub_walk?")
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (typepred
                                           "i"
                                           "j"
                                           "i!1"
                                           "j!1")
                                          (("1"
                                            (inst
                                             2
                                             "i + i!1"
                                             "i + j!1")
                                            (("1"
                                              (replace -5 2 rl)
                                              (("1"
                                                (hide -5)
                                                (("1"
                                                  (decompose-equality
                                                   2)
                                                  (("1"
                                                    (expand*
                                                     "^"
                                                     "min"
                                                     "empty_seq")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (lift-if)
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (decompose-equality)
                                                    (("2"
                                                      (expand "^" 1 3)
                                                      (("2"
                                                        (lift-if)
                                                        (("2"
                                                          (prop)
                                                          (("1"
                                                            (expand*
                                                             "^"
                                                             "min")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand*
                                                             "^"
                                                             "min")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide-all-but (-1 -4 1))
                                              (("2"
                                                (expand "^")
                                                (("2"
                                                  (expand "min")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (hide-all-but (-1 -3 1))
                                              (("3"
                                                (expand"^" "min")
                                                (("3"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 3)
                                (("2"
                                  (expand*
                                   "circuit?"
                                   "pre_circuit?"
                                   "finseq_appl")
                                  (("2"
                                    (rewrite "walk?_caret")
                                    (("2"
                                      (expand"^" "min" "empty_seq")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide -2 -3 3)
                      (("2" (expand"^" "min" "empty_seq")
                        (("2" (assertnil nil)) nil))
                      nil))
                    nil)
                   ("2" (inst -2 "x!1^(j, i)")
                    (("1" (inst -2 "G")
                      (("1" (expand "^" -2 1)
                        (("1" (expand"min" "empty_seq")
                          (("1" (assert)
                            (("1" (split -2)
                              (("1"
                                (skeep -1)
                                (("1"
                                  (inst 3 "w1")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (hide -2)
                                      (("1"
                                        (expand "sub_walk?")
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (typepred
                                             "i"
                                             "j"
                                             "i!1"
                                             "j!1")
                                            (("1"
                                              (inst
                                               3
                                               "j + i!1"
                                               "j + j!1")
                                              (("1"
                                                (replace -5 3 rl)
                                                (("1"
                                                  (hide -5)
                                                  (("1"
                                                    (decompose-equality
                                                     3)
                                                    (("1"
                                                      (expand*
                                                       "^"
                                                       "min"
                                                       "empty_seq")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (lift-if)
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (decompose-equality
                                                       1)
                                                      (("2"
                                                        (expand
                                                         "^"
                                                         1
                                                         3)
                                                        (("2"
                                                          (lift-if)
                                                          (("2"
                                                            (prop)
                                                            (("1"
                                                              (expand*
                                                               "^"
                                                               "min")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand*
                                                               "^"
                                                               "min")
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide-all-but
                                                 (-2 -4 +))
                                                (("2"
                                                  (expand"^" "min")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (hide-all-but
                                                 (-2 -3 +))
                                                (("3"
                                                  (expand"^" "min")
                                                  (("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 4)
                                (("2"
                                  (expand*
                                   "circuit?"
                                   "pre_circuit?"
                                   "finseq_appl")
                                  (("2"
                                    (rewrite "walk?_caret")
                                    (("2" (expand"^" "min"nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand"^" "min") (("2" (assertnil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide-all-but (-1 1))
      (("2" (skeep)
        (("2" (expand"circuit?" "pre_circuit?" "finseq_appl")
          (("2" (assertnil nil)) nil))
        nil))
      nil)
     ("3" (hide-all-but (-1 1))
      (("3" (skeep)
        (("3" (expand"circuit?" "pre_circuit?" "finseq_appl")
          (("3" (assertnil nil)) nil))
        nil))
      nil))
    nil)
   ((empty_seq const-decl "finseq" finite_sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs nil)
    (j!1 skolem-const-decl "below(length(x!1 ^ (i, j)))" cycles nil)
    (i!1 skolem-const-decl "below(length(x!1 ^ (i, j)))" cycles nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (pre_circuit? const-decl "bool" circuits nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (walk?_caret formula-decl nil walks nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (j skolem-const-decl "below(length(x!1) - 1)" cycles nil)
    (i skolem-const-decl "below(length(x!1) - 1)" cycles nil)
    (x!1 skolem-const-decl "prewalk[T]" cycles nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (i!1 skolem-const-decl "below(length(x!1 ^ (j, i)))" cycles nil)
    (j!1 skolem-const-decl "below(length(x!1 ^ (j, i)))" cycles nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (^ const-decl "finseq" finite_sequences nil)
    (cycle? const-decl "bool" cycles nil)
    (sub_walk? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (edgetype type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (circuit? const-decl "bool" circuits nil)
    (walk? const-decl "bool" walks nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (prewalk type-eq-decl nil walks nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (T formal-type-decl nil cycles nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (measure_induction formula-decl nil measure_induction nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil))
   shostak))
 (cycle_prefix_TCC1 0
  (cycle_prefix_TCC1-1 nil 3579270878 ("" (subtype-tcc) nil nil)
   ((T formal-type-decl nil cycles nil)
    (verts_in? const-decl "bool" walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (edge? const-decl "bool" digraphs nil)
    (walk? const-decl "bool" walks nil)
    (pre_circuit? const-decl "bool" circuits nil)
    (circuit? const-decl "bool" circuits nil)
    (/= const-decl "boolean" notequal nil)
    (cycle? const-decl "bool" cycles nil)
    (O const-decl "finseq" finite_sequences nil))
   nil))
 (cycle_prefix 0
  (cycle_prefix-1 nil 3582385881
   ("" (auto-rewrite "finseq_appl")
    (("" (skeep)
      (("" (lemma "circuit_subwalk_cycle")
        (("" (inst -1 "G" "w")
          (("" (assert)
            (("" (skeep -1)
              (("" (expand "sub_walk?")
                (("" (skeep -1)
                  (("" (typepred "i" "j")
                    (("" (case "i = 0 AND j = length(w) - 1")
                      (("1" (flatten)
                        (("1" (replaces -1)
                          (("1" (replaces -1)
                            (("1" (hide-all-but (-3 -4 1))
                              (("1"
                                (case-replace "w1 = w")
                                (("1"
                                  (hide -2 2)
                                  (("1"
                                    (replace -1 1 rl)
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (decompose-equality)
                                        (("1"
                                          (expand"^" "min")
                                          nil
                                          nil)
                                         ("2"
                                          (decompose-equality)
                                          (("2"
                                            (typepred "x!1")
                                            (("2"
                                              (expand"^" "min")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (case "i > j")
                        (("1" (expand "^" -4)
                          (("1" (assert)
                            (("1" (hide-all-but (-4 -5))
                              (("1"
                                (expand"cycle?" "circuit?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (hide -2 -4)
                                    (("1"
                                      (expand "empty_seq")
                                      (("1" (assertnil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (case-replace "j = length(w) - 1")
                          (("1" (inst 4 "w1" "w^(1, i)")
                            (("1" (assert)
                              (("1"
                                (replace -4 4 rl)
                                (("1"
                                  (rewrite "commuted_circuit_is_eq")
                                  nil
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but (1 3))
                              (("2"
                                (expand"^" "min")
                                (("2" (assertnil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (case-replace "i = 0")
                            (("1" (hide -1 -2 3 4)
                              (("1"
                                (inst
                                 3
                                 "w1"
                                 "w^(j + 1, length(w) - 1)")
                                (("1"
                                  (assert)
                                  (("1"
                                    (case-replace
                                     "w1 o w ^ (1 + j, length(w) - 1) = w")
                                    (("1"
                                      (hide-all-but (-5 3))
                                      (("1"
                                        (rewrite
                                         "eq_circuit_reflexive")
                                        nil
                                        nil))
                                      nil)
                                     ("2"
                                      (replace -2 1 rl)
                                      (("2"
                                        (hide -2 -3 -4 3 4)
                                        (("2"
                                          (decompose-equality)
                                          (("1"
                                            (expand*
                                             "o"
                                             "^"
                                             "min"
                                             "empty_seq")
                                            nil
                                            nil)
                                           ("2"
                                            (decompose-equality)
                                            (("2"
                                              (typepred "x!1")
                                              (("2"
                                                (expand*
                                                 "o"
                                                 "^"
                                                 "min"
                                                 "empty_seq")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide - 3)
                                  (("2"
                                    (expand"^" "min")
                                    (("2" (assertnil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide -1 -5 4 5)
                              (("2"
                                (inst
                                 4
                                 "w1"
                                 "w^(j+1, length(w)-1) o w^(1, i)")
                                (("1"
                                  (assert)
                                  (("1"
                                    (rewrite "o_assoc")
                                    (("1"
                                      (replace -2 4 rl)
                                      (("1"
                                        (hide -2 -3)
                                        (("1"
                                          (case-replace
                                           "w^(i, j) o w^(1 + j, length(w) - 1) = w^(i, length(w) - 1)")
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (rewrite
                                               "commuted_circuit_is_eq")
                                              nil
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 5)
                                            (("2"
                                              (decompose-equality)
                                              (("1"
                                                (expand*
                                                 "o"
                                                 "^"
                                                 "min"
                                                 "empty_seq")
                                                nil
                                                nil)
                                               ("2"
                                                (decompose-equality)
                                                (("2"
                                                  (typepred "x!1")
                                                  (("2"
                                                    (expand*
                                                     "o"
                                                     "^"
                                                     "min"
                                                     "empty_seq")
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide -2 -3)
                                  (("2"
                                    (expand"o" "^" "min" "empty_seq")
                                    (("2" (assertnil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil cycles nil)
    (edgetype type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil 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)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (^ const-decl "finseq" finite_sequences nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (commuted_circuit_is_eq formula-decl nil circuits nil)
    (i skolem-const-decl "below(length(w))" cycles nil)
    (w skolem-const-decl "prewalk[T]" cycles nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs nil)
    (o_assoc formula-decl nil finite_sequences nil)
    (nat_min application-judgement "{k: nat | k <= i AND k <= j}"
     real_defs nil)
    (eq_circuit_reflexive formula-decl nil circuits nil)
    (O const-decl "finseq" finite_sequences nil)
    (j skolem-const-decl "below(length(w))" cycles nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (empty_seq const-decl "finseq" finite_sequences nil)
    (cycle? const-decl "bool" cycles nil)
    (circuit? const-decl "bool" circuits nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" 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)
    (below type-eq-decl nil naturalnumbers nil)
    (sub_walk? const-decl "bool" walks nil)
    (circuit_subwalk_cycle formula-decl nil cycles nil))
   shostak))
 (cycle_o_circuit_TCC1 0
  (cycle_o_circuit_TCC1-1 nil 3579270878 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs 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)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T formal-type-decl nil cycles nil)
    (verts_in? const-decl "bool" walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (edge? const-decl "bool" digraphs nil)
    (walk? const-decl "bool" walks nil)
    (pre_circuit? const-decl "bool" circuits nil)
    (circuit? const-decl "bool" circuits nil)
    (/= const-decl "boolean" notequal nil)
    (cycle? const-decl "bool" cycles nil)
    (rest const-decl "finseq" seq_extras "structures/")
    (O const-decl "finseq" finite_sequences nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (cycle_o_circuit 0
  (cycle_o_circuit-1 nil 3582583306
   ("" (auto-rewrite "finseq_appl")
    (("" (skeep)
      (("" (lemma "cycle_prefix")
        (("" (inst -1 "G" "w")
          (("" (assert)
            (("" (skeep)
              (("" (inst 2 "w1" "add_first(last(w1), w2)")
                (("1" (rewrite "rest_add_first")
                  (("1" (assert)
                    (("1" (expand "eq_circuit?")
                      (("1" (flatten)
                        (("1" (hide -2 -4 1)
                          (("1" (expand"circuit?" "pre_circuit?")
                            (("1" (assert)
                              (("1"
                                (flatten)
                                (("1"
                                  (split)
                                  (("1"
                                    (case
                                     "add_first(last(w1), w2) = (w1 o w2) ^ (length(w1) - 1, length(w1 o w2) -1)")
                                    (("1"
                                      (replaces -1)
                                      (("1"
                                        (rewrite "walk?_caret")
                                        (("1"
                                          (expand "o" 1)
                                          (("1" (assertnil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide-all-but (-3 1))
                                      (("2"
                                        (decompose-equality)
                                        (("1"
                                          (expand*
                                           "add_first"
                                           "insert?"
                                           "o"
                                           "^"
                                           "min")
                                          nil
                                          nil)
                                         ("2"
                                          (decompose-equality)
                                          (("2"
                                            (typepred "x!1")
                                            (("2"
                                              (expand*
                                               "add_first"
                                               "insert?"
                                               "o"
                                               "^"
                                               "min")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (expand "last")
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (lift-if)
                                                      (("2"
                                                        (ground)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("3" (assertnil nil))
                                    nil)
                                   ("2"
                                    (expand"add_first" "insert?")
                                    (("2"
                                      (expand "last")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "o" -2)
                                          (("2"
                                            (hide -1 -3)
                                            (("2"
                                              (expand*
                                               "cycle?"
                                               "circuit?"
                                               "pre_circuit?")
                                              (("2"
                                                (flatten)
                                                (("2"
                                                  (hide -2 -4 -5)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (hide-all-but 1)
                                    (("3"
                                      (expand"add_first" "insert?")
                                      (("3" (assertnil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but 1)
                  (("2" (expand"add_first" "insert?")
                    (("2" (assertnil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil cycles nil)
    (edgetype type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil 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)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (rest_add_first formula-decl nil seq_extras "structures/")
    (eq_circuit? const-decl "bool" circuits nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (< const-decl "bool" reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (insert? const-decl "finseq" seq_extras "structures/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (walk?_caret formula-decl nil walks nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (O const-decl "finseq" finite_sequences nil)
    (^ const-decl "finseq" finite_sequences nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (cycle? const-decl "bool" cycles nil)
    (circuit? const-decl "bool" circuits nil)
    (pre_circuit? const-decl "bool" circuits nil)
    (w2 skolem-const-decl "prewalk[T]" cycles nil)
    (w1 skolem-const-decl "prewalk[T]" cycles nil)
    (last const-decl "T" seq_extras "structures/")
    (not_empty_seq type-eq-decl nil seq_extras "structures/")
    (/= const-decl "boolean" notequal nil)
    (add_first const-decl "finseq" seq_extras "structures/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (cycle_prefix formula-decl nil cycles nil))
   shostak))
 (Pigeon_hole 0
  (Pigeon_hole-1 nil 3507100929
   ("" (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" (assertnil nil))
                  nil))
                nil))
              nil))
            nil))
          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))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Digraph type-eq-decl nil digraphs nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil cycles 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 "Digraph[T]" cycles nil)
    (Walk type-eq-decl nil walks nil)
    (w!1 skolem-const-decl "Walk[T](GF!1)" cycles nil))
   nil)))


¤ Dauer der Verarbeitung: 0.65 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff