| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/while/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 109 kB |
|
Quelle am.prfSprache: Lisp |
|||||||||||||||
|
(am (check2_TCC1 0 (check2_TCC1-1 nil 3398743350 ("" (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) (number nonempty-type-decl nil numbers nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (Stack nonempty-type-eq-decl nil am nil)) nil)) (step_TCC1 0 (step_TCC1-1 nil 3398491018 ("" (skosimp) (("" (assert) nil nil)) nil) nil nil)) (step_TCC2 0 (step_TCC2-1 nil 3398491018 ("" (skosimp*) (("" (assert) (("" (expand "check1") (("" (propax) nil nil)) nil)) nil)) nil) ((check1 const-decl "bool" am nil)) nil)) (step_TCC3 0 (step_TCC3-1 nil 3398491018 ("" (skosimp*) (("" (expand "check2") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil) ((check2 const-decl "bool" am nil)) nil)) (step_TCC4 0 (step_TCC4-1 nil 3398491018 ("" (skosimp*) (("" (expand "check2") (("" (flatten) (("" (assert) (("" (expand "pop") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((check2 const-decl "bool" am nil) (pop const-decl "Stack" am nil)) nil)) (step_TCC5 0 (step_TCC5-1 nil 3398491018 ("" (skosimp*) (("" (expand "check1") (("" (assert) nil nil)) nil)) nil) ((check1 const-decl "bool" am nil)) nil)) (step_TCC6 0 (step_TCC6-1 nil 3398491018 ("" (skosimp*) (("" (expand "check1") (("" (assert) nil nil)) nil)) nil) ((check1 const-decl "bool" am nil)) nil)) (tr_TCC1 0 (tr_TCC1-1 nil 3398743350 ("" (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) (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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (tr_TCC2 0 (tr_TCC2-1 nil 3398743350 ("" (termination-tcc) nil nil) ((step const-decl "Config" am nil)) nil)) (step_append 0 (step_append-1 nil 3399091849 ("" (skosimp*) (("" (expand "step") (("" (assert) (("" (lemma "append_is_null" ("l1" "c1!1" "l2" "c2!1")) (("" (assert) (("" (case-replace "car(append(c1!1, c2!1))=car(c1!1)") (("1" (case-replace "cdr(append(c1!1, c2!1))=append(cdr(c1!1),c2!1)") (("1" (case "PUSH?(car(c1!1))") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (case "FETCH?(car(c1!1))") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (case "UNARY?(car(c1!1))") (("1" (assert) (("1" (expand "check1") (("1" (lift-if) (("1" (assert) (("1" (case-replace "null?(e!1)") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "BINARY?(car(c1!1))") (("1" (assert) (("1" (expand "check2") (("1" (case-replace "null?(e!1)") (("1" (case-replace "null?(cdr(e!1))") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "STORE?(car(c1!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e!1)") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOOP?(car(c1!1))") (("1" (assert) nil nil) ("2" (case "BRANCH?(car(c1!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e!1)") (("1" (assert) (("1" (case-replace "top(e!1) = 1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (rewrite "append_assoc" * :dir rl) (("1" (replace -5 * rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (rewrite "append_assoc" * :dir rl) (("2" (replace -4 * rl) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "LOOP?(car(c1!1))") (("1" (assert) (("1" (name-replace "CB" "c3(car(c1!1))") (("1" (name-replace "IB" "BRANCH(append(c4(car(c1!1)), cons(LOOP(CB, c4(car(c1!1))), null[Instruction])), null[Instruction])") (("1" (name-replace "IBR" "BRANCH(append(c4(car(c1!1)), cons(LOOP(CB, c4(car(c1!1))), null[Instruction])), cons(NOOP, null[Instruction]))") (("1" (lemma "append_eq2" ("l2" "c1!1" "l3" "append(CB, cons(IBR, cdr(c1!1)))" "l1" "c2!1")) (("1" (replace -1 -5 rl) (("1" (replace -5 10) (("1" (rewrite "append_assoc") (("1" (expand "append" 10 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "append" 1 1) (("2" (propax) nil nil)) nil)) nil) ("2" (expand "append" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((step const-decl "Config" am nil) (Instruction type-decl nil Instruction nil) (V formal-nonempty-type-decl nil am nil) (Code nonempty-type-eq-decl nil Instruction nil) (list type-decl nil list_adt nil) (append_is_null formula-decl nil list_props_aux nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (append def-decl "list[T]" list_props nil) (PUSH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (UNARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (check1 const-decl "bool" am nil) (Stack nonempty-type-eq-decl nil am nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (STORE? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (BRANCH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (c2 adt-accessor-decl "[(BRANCH?) -> list[Instruction]]" Instruction nil) (append_assoc formula-decl nil list_props nil) (c1 adt-accessor-decl "[(BRANCH?) -> list[Instruction]]" Instruction nil) (top const-decl "int" am nil) (null adt-constructor-decl "(null?)" list_adt nil) (LOOP adt-constructor-decl "[[list[Instruction], list[Instruction]] -> (LOOP?)]" Instruction nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (c4 adt-accessor-decl "[(LOOP?) -> list[Instruction]]" Instruction nil) (BRANCH adt-constructor-decl "[[list[Instruction], list[Instruction]] -> (BRANCH?)]" Instruction nil) (append_eq2 formula-decl nil list_props_aux nil) (NOOP adt-constructor-decl "(NOOP?)" Instruction nil) (c3 adt-accessor-decl "[(LOOP?) -> list[Instruction]]" Instruction nil) (LOOP? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (NOOP? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (check2 const-decl "bool" am nil) (BINARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (FETCH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)) shostak)) (tr_add 0 (tr_add-1 nil 3398743779 ("" (induct "k1") (("1" (skosimp) (("1" (split) (("1" (flatten) (("1" (inst + "cf0!1") (("1" (expand "tr" 1 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "tr" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (split) (("1" (flatten) (("1" (expand "tr" 1 1) (("1" (expand "tr" -1) (("1" (flatten) (("1" (assert) (("1" (inst - "step(cf0!1)" "cf2!1" "k2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "tr" (-1 1)) (("2" (flatten) (("2" (assert) (("2" (inst - "step(cf0!1)" "cf2!1" "k2!1") (("2" (replace -3) (("2" (hide -3) (("2" (inst + "cf1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (step const-decl "Config" am nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (tr def-decl "bool" am nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (Config nonempty-type-eq-decl nil am nil) (State nonempty-type-eq-decl nil State nil) (Stack nonempty-type-eq-decl nil am nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (Code nonempty-type-eq-decl nil Instruction nil) (list type-decl nil list_adt nil) (Instruction type-decl nil Instruction nil) (V formal-nonempty-type-decl nil am nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (tr_eq 0 (tr_eq-1 nil 3398743611 ("" (induct "k") (("1" (skosimp) (("1" (expand "tr") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "tr" (-2 -3)) (("2" (flatten) (("2" (inst - "step(cf0!1)" "cf1!1" "cf2!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((step const-decl "Config" am nil) (nat_induction formula-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (tr def-decl "bool" am nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Config nonempty-type-eq-decl nil am nil) (State nonempty-type-eq-decl nil State nil) (Stack nonempty-type-eq-decl nil am nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (Code nonempty-type-eq-decl nil Instruction nil) (list type-decl nil list_adt nil) (Instruction type-decl nil Instruction nil) (V formal-nonempty-type-decl nil am nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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)) shostak)) (code_partial 0 (code_partial-1 nil 3398746849 ("" (induct "k") (("1" (expand "tr") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "tr" -2) (("2" (flatten) (("2" (expand "tr" 3) (("2" (lemma "append_is_null" ("l1" "c0!1" "l2" "c2!1")) (("2" (assert) (("2" (inst - "step(c0!1, e0!1, s0!1)`1" "c1!1" "c2!1" "step(c0!1, e0!1, s0!1)`2" "e1!1" "e2!1" "step(c0!1, e0!1, s0!1)`3" "s1!1") (("2" (case-replace "(step(c0!1, e0!1, s0!1)`1, step(c0!1, e0!1, s0!1)`2, step(c0!1, e0!1, s0!1)`3)=step(c0!1, e0!1, s0!1)") (("1" (hide -1) (("1" (replace -2 -1) (("1" (case-replace "(append(step(c0!1, e0!1, s0!1)`1, c2!1), append(step(c0!1, e0!1, s0!1)`2, e2!1), step(c0!1, e0!1, s0!1)`3)=step(append(c0!1, c2!1), append(e0!1, e2!1), s0!1)") (("1" (replace -2) (("1" (expand "/=" 4) (("1" (hide -2 -3) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (decompose-equality) (("1" (flatten) (("1" (expand "step") (("1" (case "PUSH?(car(c0!1))") (("1" (assert) (("1" (expand "push") (("1" (expand "append" -3 2) (("1" (lemma "length_append" ("l1" "c0!1" "l2" "c2!1")) (("1" (lemma "length_append" ("l1" "cdr(c0!1)" "l2" "c2!1")) (("1" (replace -4 -1 rl) (("1" (expand "length" -2 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FETCH?(car(c0!1))") (("1" (assert) (("1" (lemma "length_append" ("l1" "c0!1" "l2" "c2!1")) (("1" (expand "length" -1 2) (("1" (lemma "length_append" ("l1" "cdr(c0!1)" "l2" "c2!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "UNARY?(car(c0!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e0!1)") (("1" (assert) (("1" (lemma "length_append" ("l1" "cdr(c0!1)" "l2" "c2!1")) (("1" (lemma "length_append" ("l1" "c0!1" "l2" "c2!1")) (("1" (expand " length" -1 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "BINARY?(car(c0!1))") (("1" (assert) (("1" (expand "check2") (("1" (case-replace "null?(e0!1)") (("1" (assert) (("1" (case-replace "null?(cdr(e0!1))") (("1" (assert) (("1" (lemma "length_append" ("l1" "cdr(c0!1)" "l2" "c2!1")) (("1" (lemma "length_append" ("l1" "c0!1" "l2" "c2!1")) (("1" (expand "length" -1 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "STORE?(car(c0!1))") (("1" (assert) (("1" (expand "check1") (("1" (assert) (("1" (case-replace "null?(e0!1)") (("1" (assert) (("1" (lemma "length_append" ("l1" "cdr(c0!1)" "l2" "c2!1")) (("1" (lemma "length_append" ("l1" "c0!1" "l2" "c2!1")) (("1" (expand "length" -1 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOOP?(car(c0!1))") (("1" (assert) (("1" (lemma "length_append" ("l1" "cdr(c0!1)" "l2" "c2!1")) (("1" (lemma "length_append" ("l1" "c0!1" "l2" "c2!1")) (("1" (expand "length" -1 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "BRANCH?(car(c0!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e0!1)") (("1" (assert) (("1" (expand "top") (("1" (expand "pop") (("1" (lemma "length_append" ("l1" "cdr(e0!1)" "l2" "e2!1")) (("1" (lemma "length_append" ("l1" "e0!1" "l2" "e2!1")) (("1" (expand "length" -1 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "LOOP?(car(c0!1))") (("1" (assert) (("1" (name-replace "IB" "BRANCH(append(c4(car(c0!1)), cons (LOOP (c3(car(c0!1)), c4(car(c0!1))), null[Instruction])), null[Instruction])") (("1" (rewrite "append_assoc") (("1" (name-replace "IBR" "BRANCH(append(c4(car(c0!1)), cons(LOOP(c3(car(c0!1)), c4(car(c0!1))), null)), cons(NOOP, null))") (("1" (lemma "append_eq2" ("l2" "c0!1" "l3" "append(c3(car(c0!1)), cons(IBR, cdr(c0!1)))" "l1" "c2!1")) (("1" (replace -1 8 rl) (("1" (rewrite "append_assoc") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "append_eq2" ("l2" "e0!1" "l3" "step(c0!1, e0!1, s0!1)`2" "l1" "e2!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 5) (("2" (expand "step") (("2" (case-replace "car(append(c0!1, c2!1))= car(c0!1)") (("1" (case-replace "cdr(append(c0!1, c2!1))= append(cdr(c0!1),c2!1)") (("1" (case "PUSH?(car(c0!1))") (("1" (assert) (("1" (expand "push") (("1" (expand "append" 1 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "FETCH?(car(c0!1))") (("1" (assert) (("1" (expand "push") (("1" (expand "append" 2 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "UNARY?(car(c0!1))") (("1" (assert) (("1" (expand "check1") (("1" (expand "push") (("1" (expand "top") (("1" (lemma "append_is_null" ("l1" "e0!1" "l2" "e2!1")) (("1" (case-replace "null?(e0!1)") (("1" (assert) (("1" (expand "pop") (("1" (expand "append" 5 1) (("1" (expand "append" 5 2) (("1" (expand "append" 5 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "BINARY?(car(c0!1))") (("1" (assert) (("1" (expand "check2") (("1" (expand "pop") (("1" (expand "push") (("1" (expand "top") (("1" (case-replace "null?(e0!1)") (("1" (assert) (("1" (case-replace "null?(cdr(e0!1))") (("1" (assert) (("1" (lemma "append_is_null" ("l1" "e0!1" "l2" "e2!1")) (("1" (assert) (("1" (lemma "append_is_null" ("l1" "cdr(e0!1)" "l2" "e2!1")) (("1" (assert) (("1" (expand "append" 8 3) (("1" (expand "append" 8 1) (("1" (expand "append" 8 2) (("1" (case-replace "cdr(append(e0!1, e2!1)) = append(cdr(e0!1),e2!1)") (("1" (expand "append" 8 2) (("1" (name-replace "TOP" "f2(car(c0!1))(car(e0!1), car(cdr(e0!1)))") (("1" (expand "append" 8 2) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "append" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "STORE?(car(c0!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e0!1)") (("1" (assert) (("1" (expand "pop") (("1" (expand "top") (("1" (lemma "append_is_null" ("l1" "e0!1" "l2" "e2!1")) (("1" (assert) (("1" (expand "append" 7 2) (("1" (expand "append" 7) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOOP?(car(c0!1))") (("1" (assert) nil nil) ("2" (case "BRANCH?(car(c0!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e0!1)") (("1" (assert) (("1" (expand "pop") (("1" (expand "top") (("1" (lemma "append_is_null" ("l1" "e0!1" "l2" "e2!1")) (("1" (assert) (("1" (expand "append" 9 5) (("1" (expand "append" 9 7) (("1" (expand "append" 9 10) (("1" (case-replace "car(e0!1) = 1") (("1" (rewrite "append_assoc") nil nil) ("2" (assert) (("2" (rewrite "append_assoc") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "LOOP?(car(c0!1))") (("1" (assert) (("1" (name-replace "IB" "BRANCH(append(c4(car(c0!1)), cons (LOOP(c3(car(c0!1)), c4(car(c0!1))), null[Instruction])), null[Instruction])") (("1" (rewrite "append_assoc") (("1" (expand "append" 8 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "append" 1 1) (("2" (propax) nil nil)) nil)) nil) ("2" (expand "append" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((append_is_null formula-decl nil list_props_aux nil) (step const-decl "Config" am nil) (/= const-decl "boolean" notequal nil) (FETCH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (BINARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (check2 const-decl "bool" am nil) (NOOP? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (LOOP? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (null adt-constructor-decl "(null?)" list_adt nil) (c3 adt-accessor-decl "[(LOOP?) -> list[Instruction]]" Instruction nil) (LOOP adt-constructor-decl "[[list[Instruction], list[Instruction]] -> (LOOP?)]" Instruction nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (c4 adt-accessor-decl "[(LOOP?) -> list[Instruction]]" Instruction nil) (BRANCH adt-constructor-decl "[[list[Instruction], list[Instruction]] -> (BRANCH?)]" Instruction nil) (append_eq2 formula-decl nil list_props_aux nil) (append_assoc formula-decl nil list_props nil) (NOOP adt-constructor-decl "(NOOP?)" Instruction nil) (top const-decl "int" am nil) (pop const-decl "Stack" am nil) (BRANCH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (STORE? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (check1 const-decl "bool" am nil) (UNARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (length def-decl "nat" list_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length_append formula-decl nil list_props nil) (push const-decl "Stack" am nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (PUSH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (f2 adt-accessor-decl "[(BINARY?) -> [[int, int] -> int]]" Instruction nil) (c2 adt-accessor-decl "[(BRANCH?) -> list[Instruction]]" Instruction nil) (c1 adt-accessor-decl "[(BRANCH?) -> list[Instruction]]" Instruction nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat_induction formula-decl nil naturalnumbers nil) (append def-decl "list[T]" list_props nil) (tr def-decl "bool" am nil) (Config nonempty-type-eq-decl nil am nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (State nonempty-type-eq-decl nil State nil) (Stack nonempty-type-eq-decl nil am nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (Code nonempty-type-eq-decl nil Instruction nil) (list type-decl nil list_adt nil) (Instruction type-decl nil Instruction nil) (V formal-nonempty-type-decl nil am nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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)) shostak)) (code_split 0 (code_split-1 nil 3399030329 ("" (induct "k") (("1" (skosimp*) (("1" (expand "tr") (("1" (flatten) (("1" (inst + "e!1" "s!1" "0" "0") (("1" (assert) (("1" (lemma "append_is_null" ("l1" "c1!1" "l2" "c2!1")) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case-replace "c1!1=null[Instruction]") (("1" (expand "append" -3) (("1" (inst + "e!1" "s!1" "0" "1+j!1") (("1" (assert) (("1" (expand "tr") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "cons?(c1!1)") (("1" (hide 1) (("1" (expand "tr" -3) (("1" (flatten) (("1" (hide 1) (("1" (lemma "step_append" ("c1" "c1!1" "c2" "c2!1" "e" "e!1" "s" "s!1")) (("1" (assert) (("1" (expand "/=" -1 1) (("1" (replace 1 -1) (("1" (case "step(append(c1!1, c2!1), e!1, s!1) = (append(step(c1!1, e!1, s!1)`1,c2!1),step(c1 (("1" (inst - "step(c1!1, e!1, s!1)`1" "c2!1" "step(c1!1, e!1, s!1)`2" "e2!1" "step(c1!1, e!1, s!1)`3" "s2!1") (("1" (replace -1 -4 rl) (("1" (replace -5) (("1" (skosimp) (("1" (case-replace "(step(c1!1, e!1, s!1)`1, step(c1!1, e!1, s!1)`2, step(c1!1, e!1, s!1)`3)=step(c1!1, e!1, s!1)") (("1" (hide -1) (("1" (inst + "e1!1" "s1!1" "k1!1+1" "k2!1") (("1" (assert) (("1" (hide -1 -2 -5 -6 -4 2) (("1" (expand "tr" 2) (("1" (assert) (("1" (expand "/=") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 -4 3) (("2" (expand "step") (("2" (lemma "append_is_null" ("l1" "c1!1" "l2" "c2!1")) (("2" (assert) (("2" (case-replace "car(append(c1!1, c2!1))=car(c1!1)") (("1" (case-replace "cdr(append(c1!1, c2!1))=append(cdr(c1!1),c2!1)") (("1" (case "PUSH?(car(c1!1))") (("1" (assert) nil nil) ("2" (case "FETCH?(car(c1!1))") (("1" (assert) nil nil) ("2" (case "UNARY?(car(c1!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "BINARY?(car(c1!1))") (("1" (assert) (("1" (expand "check2") (("1" (case-replace "null?(e!1)") (("1" (case-replace "null?(cdr(e!1))") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "STORE?(car(c1!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "NOOP?(car(c1!1))") (("1" (assert) nil nil) ("2" (case "BRANCH?(car(c1!1))") (("1" (assert) (("1" (expand "check1") (("1" (case-replace "null?(e!1)") (("1" (assert) (("1" (case-replace "top(e!1) = 1") (("1" (assert) (("1" (hide-all-but (-3 9 -5)) (("1" (rewrite "append_assoc") nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "append_assoc") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "LOOP?(car(c1!1))") (("1" (assert) (("1" (name-replace "IB" "BRANCH(append(c4(car(c1!1)), cons (LOOP (c3(car(c1!1)), c4(car(c1!1))), null)), null)") (("1" (rewrite "append_assoc") (("1" (name-replace "IBR" "BRANCH(append(c4(car(c1!1)), cons(LOOP(c3(car(c1!1)), c4(car(c1!1))), null)), cons(NOOP, null))") (("1" (expand "append" 9 4) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "append" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "append" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (PUSH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (UNARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (check1 const-decl "bool" am nil) (STORE? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (BRANCH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (c2 adt-accessor-decl "[(BRANCH?) -> list[Instruction]]" Instruction nil) (c1 adt-accessor-decl "[(BRANCH?) -> list[Instruction]]" Instruction nil) (append_assoc formula-decl nil list_props nil) (top const-decl "int" am nil) (NOOP adt-constructor-decl "(NOOP?)" Instruction nil) (BRANCH adt-constructor-decl "[[list[Instruction], list[Instruction]] -> (BRANCH?)]" Instruction nil) (c4 adt-accessor-decl "[(LOOP?) -> list[Instruction]]" Instruction nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (LOOP adt-constructor-decl "[[list[Instruction], list[Instruction]] -> (LOOP?)]" Instruction nil) (c3 adt-accessor-decl "[(LOOP?) -> list[Instruction]]" Instruction nil) (LOOP? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (NOOP? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (check2 const-decl "bool" am nil) (BINARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (FETCH? adt-recognizer-decl "[Instruction -> boolean]" Instruction nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (step const-decl "Config" am nil) (/= const-decl "boolean" notequal nil) (step_append formula-decl nil am nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (append_is_null formula-decl nil list_props_aux nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (append def-decl "list[T]" list_props nil) (tr def-decl "bool" am nil) (Config nonempty-type-eq-decl nil am nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (State nonempty-type-eq-decl nil State nil) (Stack nonempty-type-eq-decl nil am nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (Code nonempty-type-eq-decl nil Instruction nil) (list type-decl nil list_adt nil) (Instruction type-decl nil Instruction nil) (V formal-nonempty-type-decl nil am nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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)) shostak)) (M_TCC1 0 (M_TCC1-1 nil 3398492510 ("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (inst - "s1!1") (("" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (State nonempty-type-eq-decl nil State 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) (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) (V formal-nonempty-type-decl nil am nil) (empty? const-decl "bool" sets nil)) nil)) (M_deterministic 0 (M_deterministic-1 nil 3398744455 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (expand "M") (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (case "nonempty?({s1 | EXISTS n: tr(n)((c!1, null, s!1), (null, null, s1))})") (("1" (lemma "choose_member" ("a" "{s1 | EXISTS n: tr(n)((c!1, null, s!1), (null, null, s1))}")) (("1" (split) (("1" (name-replace "CC" "choose({s1 | EXISTS n: tr(n)((c!1, null, s!1), (null, null, s1))})") (("1" (expand "member") (("1" (skosimp) (("1" (inst + "n!1") (("1" (rewrite "up_equal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "s1!2") (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "M") (("2" (lift-if) (("2" (assert) (("2" (prop) (("1" (case "nonempty?({s1 | EXISTS n: tr(n)((c!1, null, s!1), (null, null, s1))})") (("1" (lemma "choose_member" ("a" "{s1 | EXISTS n: tr(n)((c!1, null, s!1), (null, null, s1))}")) (("1" (split) (("1" (name-replace "CC" "choose({s1 | EXISTS n: tr(n)((c!1, null, s!1), (null, null, s1))})") (("1" (expand "member") (("1" (skosimp) (("1" (decompose-equality) (("1" (hide -2 -3) (("1" (skosimp) (("1" (lemma "trich_lt" ("x" "n!1" "y" "n!2")) (("1" (split) (("1" (lemma "tr_add" ("k1" "n!1" "k2" "n!2-n!1" "cf0" "(c!1, null[int], s!1)" "cf2" "(null[Instruction], null[int], s1!1)")) (("1" (replace -4) (("1" (flatten) (("1" (skosimp) (("1" (lemma "tr_eq" ("k" "n!1" "cf0" "(c!1, null[int], s!1)" "cf1" "cf1!1" "cf2" "(null[Instruction], null[int], CC)")) (("1" (assert) (("1" (expand "tr" -3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (hide -1) (("2" (lemma "tr_eq" ("k" "n!1" "cf0" "(c!1, null[int], s!1)" "cf1" "(null[Instruction], null[int], CC)" "cf2" "(null[Instruction], null[int], s1!1)")) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "tr_add" ("k1" "n!2" "k2" "n!1-n!2" "cf0" "(c!1, null[int], s!1)" "cf2" "(null[Instruction], null[int],CC)")) (("1" (assert) (("1" (skosimp) (("1" (lemma "tr_eq" ("k" "n!2" "cf0" "(c!1, null[int], s!1)" "cf1" "cf1!1" "cf2" "(null[Instruction], null[int], s1!1)")) (("1" (assert) (("1" (expand "tr" -3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "every") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "s1!2") (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst + "n!1" "s1!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((M const-decl "Cont" am nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (tr def-decl "bool" am nil) (Config nonempty-type-eq-decl nil am nil) (Stack nonempty-type-eq-decl nil am nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (Code nonempty-type-eq-decl nil Instruction nil) (list type-decl nil list_adt nil) (Instruction type-decl nil Instruction nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (State nonempty-type-eq-decl nil State 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) (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) (V formal-nonempty-type-decl nil am nil) (member const-decl "bool" sets nil) (up_equal formula-decl nil lift_props "orders/") (choose const-decl "(p)" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (choose_member formula-decl nil sets_lemmas nil) (empty? const-decl "bool" sets nil) (c!1 skolem-const-decl "Code[V]" am nil) (s!1 skolem-const-decl "State[V]" am nil) (up adt-constructor-decl "[T -> (up?)]" lift_adt nil) (s1!1 skolem-const-decl "State[V]" am nil) (lift_up_extensionality formula-decl nil lift_adt nil) (lift type-decl nil lift_adt nil) (every adt-def-decl "boolean" lift_adt nil) (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (tr_eq formula-decl nil am 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) (tr_add formula-decl nil am nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (trich_lt formula-decl nil real_props nil)) shostak)))
¤ Dauer der Verarbeitung: 0.76 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26