|
(bisimulation
(correct_AExp 0
(correct_AExp-1 nil 3398501093
("" (induct "a")
(("1" (skolem + "n!1")
(("1" (skosimp)
(("1" (expand "CA")
(("1" (expand "am.tr")
(("1" (expand "step")
(("1" (expand "push")
(("1" (expand "A")
(("1" (inst + "1")
(("1" (assert)
(("1" (expand "am.tr") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skolem + ("x!1"))
(("2" (skosimp)
(("2" (inst + "1")
(("2" (expand "CA")
(("2" (expand "A")
(("2" (expand "am.tr")
(("2" (expand "step")
(("2" (expand "am.tr")
(("2" (expand "push") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skolem + ("a!1" "a!2"))
(("3" (skosimp*)
(("3" (expand "A" 1)
(("3" (expand "CA" 1)
(("3" (inst -2 "e!1" "s!1")
(("3" (skosimp)
(("3" (inst - "cons(A(a!2)(s!1), e!1)" "s!1")
(("3" (skosimp)
(("3" (inst + "n!1+n!2+1")
(("3" (name-replace "C1" "CA(a!1)")
(("3" (name-replace "C2" "CA(a!2)")
(("3" (name-replace "N1" "A(a!1)(s!1)")
(("3" (name-replace "N2" "A(a!2)(s!1)")
(("3"
(case
"am.tr(1)((cons(BINARY(LAMBDA (i, j:int): i + j), null[Instruction]),cons(N1, cons(N2, e!1)), s!1),(null, cons(N1 + N2, e!1), s!1))")
(("1"
(name-replace
"C3"
"cons(BINARY(LAMBDA (i, j: int): i + j), null[Instruction])")
(("1"
(case
"am.tr
(n!2+1)((append(C1, C3),cons(N2, e!1), s!1), (null, cons(N1 + N2, e!1), s!1))")
(("1"
(hide -2 -3)
(("1"
(lemma
"code_partial"
("k"
"n!1"
"c0"
"C2"
"e0"
"e!1"
"s0"
"s!1"
"c1"
"null[Instruction]"
"e1"
"cons(N2, e!1)"
"s1"
"s!1"
"c2"
"append(C1, C3)"
"e2"
"null[int]"))
(("1"
(replace -3)
(("1"
(rewrite "append_null")
(("1"
(rewrite "append_null")
(("1"
(expand "append" -1 3)
(("1"
(lemma
"am.tr_add"
("k1"
"n!1"
"k2"
"n!2+1"
"cf0"
"(append(C2, append(C1, C3)), e!1, s!1)"
"cf2"
"(null[Instruction], cons(N1 + N2, e!1), s!1)"))
(("1"
(replace -1 1)
(("1"
(inst
+
"(append(C1, C3), cons(N2, e!1), s!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -3 2)
(("2"
(lemma
"code_partial"
("k"
"n!2"
"c0"
"C1"
"e0"
"cons(N2, e!1)"
"s0"
"s!1"
"c1"
"null[Instruction]"
"e1"
"cons(N1, cons(N2, e!1))"
"s1"
"s!1"
"c2"
"C3"
"e2"
"null[int]"))
(("2"
(replace -3)
(("2"
(rewrite "append_null")
(("2"
(rewrite "append_null")
(("2"
(expand "append" -1 2)
(("2"
(hide -3)
(("2"
(lemma
"am.tr_add"
("k1"
"n!2"
"k2"
"1"
"cf0"
"(append(C1, C3), cons(N2, e!1), s!1)"
"cf2"
"(null[Instruction], cons(N1 + N2, e!1), s!1)"))
(("2"
(replace -1 1)
(("2"
(hide -1)
(("2"
(inst
+
"(C3, cons(N1, cons(N2, e!1)), s!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (skolem + ("a!1" "a!2"))
(("4" (skosimp*)
(("4" (expand "A" 1)
(("4" (expand "CA" 1)
(("4" (inst - "cons(A(a!2)(s!1),e!1)" "s!1")
(("4" (inst - "e!1" "s!1")
(("4" (skosimp*)
(("4" (inst + "n!1+n!2+1")
(("4" (name-replace "N1" "A(a!1)(s!1)")
(("4" (name-replace "N2" "A(a!2)(s!1)")
(("4" (name-replace "C1" "CA(a!1)")
(("4" (name-replace "C2" "CA(a!2)")
(("4"
(case "am.tr(1)((cons(BINARY(LAMBDA (i, j:int): i - j), null[Instruction]),cons(N1, cons(N2, e!1)), s!1),(null, cons(N1 - N2, e!1), s!1))")
(("1"
(name-replace
"C3"
"cons(BINARY(LAMBDA (i, j: int): i - j), null[Instruction])")
(("1"
(lemma
"code_partial"
("k"
"n!1"
"c0"
"C1"
"c1"
"null[Instruction]"
"c2"
"C3"
"e0"
"cons(N2, e!1)"
"e1"
"cons(N1, cons(N2, e!1))"
"e2"
"null[int]"
"s0"
"s!1"
"s1"
"s!1"))
(("1"
(replace -3)
(("1"
(rewrite "append_null")
(("1"
(rewrite "append_null")
(("1"
(expand "append" -1 2)
(("1"
(lemma
"am.tr_add"
("k1"
"n!1"
"k2"
"1"
"cf0"
"(append(C1, C3), cons(N2, e!1), s!1)"
"cf2"
"(null[Instruction], cons(N1 - N2, e!1), s!1)"))
(("1"
(flatten)
(("1"
(hide -1)
(("1"
(split -1)
(("1"
(hide -2 -3 -4)
(("1"
(lemma
"code_partial"
("k"
"n!2"
"c0"
"C2"
"c1"
"null[Instruction]"
"c2"
"append(C1, C3)"
"e0"
"e!1"
"e1"
"cons(N2, e!1)"
"e2"
"null[int]"
"s0"
"s!1"
"s1"
"s!1"))
(("1"
(replace -3)
(("1"
(rewrite
"append_null")
(("1"
(rewrite
"append_null")
(("1"
(expand
"append"
-1
3)
(("1"
(hide
-3)
(("1"
(lemma
"am.tr_add"
("k1"
"n!2"
"k2"
"n!1+1"
"cf0"
"(append(C2, append(C1, C3)), e!1, s!1)"
"cf2"
"(null[Instruction], cons(N1 - N2, e!1), s!1)"))
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(inst
+
"(append(C1, C3), cons(N2, e!1), s!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
+
"(C3, cons(N1, cons(N2, e!1)), s!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (skolem + ("a!1" "a!2"))
(("5" (skosimp*)
(("5" (inst - "cons(A(a!2)(s!1),e!1)" "s!1")
(("5" (inst - "e!1" "s!1")
(("5" (skosimp*)
(("5" (inst + "n!1+n!2+1")
(("5" (expand "CA" 1)
(("5" (expand "A" 1)
(("5" (name-replace "C1" "CA(a!1)")
(("5" (name-replace "C2" "CA(a!2)")
(("5" (name-replace "N1" "A(a!1)(s!1)")
(("5" (name-replace "N2" "A(a!2)(s!1)")
(("5"
(case "am.tr(1)((cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction]),cons(N1, cons(N2, e!1)), s!1),(null, cons(N1 * N2, e!1), s!1))")
(("1"
(name-replace
"C3"
"cons(BINARY(LAMBDA (i, j: int): i * j), null[Instruction])")
(("1"
(lemma
"am.tr_add"
("k1"
"n!2"
"k2"
"n!1+1"
"cf0"
"(append(C2, append(C1, C3)), e!1, s!1)"
"cf2"
"(null[Instruction], cons(N1 * N2, e!1), s!1)"))
(("1"
(replace -1)
(("1"
(inst
+
"(append(C1, C3),cons(N2, e!1), s!1)")
(("1"
(hide -1)
(("1"
(split)
(("1"
(lemma
"code_partial"
("k"
"n!2"
"c0"
"C2"
"e0"
"e!1"
"s0"
"s!1"
"c1"
"null[Instruction]"
"e1"
"cons(N2, e!1)"
"s1"
"s!1"
"c2"
"append(C1, C3)"
"e2"
"null[int]"))
(("1"
(rewrite "append_null")
(("1"
(rewrite "append_null")
(("1"
(expand
"append"
-1
3)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide -3)
(("2"
(lemma
"code_partial"
("k"
"n!1"
"c0"
"C1"
"e0"
"cons(N2, e!1)"
"s0"
"s!1"
"c1"
"null[Instruction]"
"e1"
"cons(N1, cons(N2, e!1))"
"s1"
"s!1"
"c2"
"C3"
"e2"
"null[int]"))
(("2"
(rewrite "append_null")
(("2"
(rewrite
"append_null")
(("2"
(expand
"append"
-1
2)
(("2"
(assert)
(("2"
(hide -3)
(("2"
(lemma
"am.tr_add"
("k1"
"n!1"
"k2"
"1"
"cf0"
"(append(C1, C3), cons(N2, e!1), s!1)"
"cf2"
"(null[Instruction], cons(N1 * N2, e!1), s!1)"))
(("2"
(replace
-1)
(("2"
(inst
+
"(C3, cons(N1, cons(N2, e!1)), s!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(expand "am.tr")
(("2"
(expand "step")
(("2"
(expand "am.tr")
(("2"
(assert)
(("2"
(expand "check2")
(("2"
(expand "top")
(("2"
(expand "pop")
(("2"
(expand "push")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(pop const-decl "Stack" am nil) (top const-decl "int" am nil)
(check2 const-decl "bool" am nil) (tr_add formula-decl nil am nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(append_null formula-decl nil list_props nil)
(code_partial formula-decl nil am nil)
(append def-decl "list[T]" list_props nil)
(BINARY adt-constructor-decl "[[[int, int] -> int] -> (BINARY?)]"
Instruction nil)
(BINARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction
nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(step const-decl "Config" am nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(push const-decl "Stack" am nil)
(AExp_induction formula-decl nil AExp nil)
(V formal-nonempty-type-decl nil bisimulation nil)
(A def-decl "[State -> int]" AExp nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(null adt-constructor-decl "(null?)" list_adt nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(CA def-decl "Code" compiler nil) (tr def-decl "bool" am nil)
(Config nonempty-type-eq-decl nil am nil)
(Stack nonempty-type-eq-decl nil am nil)
(Code nonempty-type-eq-decl nil Instruction nil)
(Instruction type-decl nil Instruction nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(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)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(AExp type-decl nil AExp nil))
shostak))
(correct_BExp 0
(correct_BExp-1 nil 3399055662
("" (induct "b")
(("1" (skosimp)
(("1" (inst + "1")
(("1" (expand "tr")
(("1" (expand "CB")
(("1" (expand "tr")
(("1" (expand "step")
(("1" (expand "push")
(("1" (expand "B") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (inst + "1")
(("2" (expand "tr")
(("2" (expand "tr")
(("2" (expand "CB")
(("2" (expand "B")
(("2" (expand "step")
(("2" (expand "push") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skolem + ("a!1" "a!2"))
(("3" (skosimp)
(("3" (expand "CB")
(("3" (lemma "correct_AExp" ("a" "a!2" "e" "e!1" "s" "s!1"))
(("3" (skosimp)
(("3"
(lemma "correct_AExp"
("a" "a!1" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1"))
(("3" (skosimp)
(("3" (expand "B" 1)
(("3" (inst + "n!1+n!2+1")
(("3"
(lemma "code_partial"
("k" "n!2" "c0" "CA(a!1)" "e0"
"cons(A(a!2)(s!1), e!1)" "s0" "s!1" "c1"
"null[Instruction]" "e1"
"cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1))"
"s1" "s!1" "c2"
"cons(BINARY(LAMBDA (i, j:int): b2n(i = j)), null)"
"e2" "null[int]"))
(("3" (replace -2)
(("3" (rewrite "append_null")
(("3" (rewrite "append_null")
(("3"
(expand "append" -1 2)
(("3"
(name-replace
"C2"
"append(CA(a!1),
cons(BINARY(LAMBDA (i, j: int): b2n(i = j)), null))")
(("3"
(hide -2)
(("3"
(case
"tr(n!2+1)((C2, cons(A(a!2)(s!1), e!1), s!1),(null[Instruction],cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1), s!1))")
(("1"
(hide -2)
(("1"
(lemma
"code_partial"
("k"
"n!1"
"c0"
"CA(a!2)"
"e0"
"e!1"
"s0"
"s!1"
"c1"
"null[Instruction]"
"e1"
"cons(A(a!2)(s!1), e!1)"
"s1"
"s!1"
"c2"
"C2"
"e2"
"null[int]"))
(("1"
(assert)
(("1"
(rewrite "append_null")
(("1"
(rewrite "append_null")
(("1"
(expand
"append"
-1
2)
(("1"
(lemma
"am.tr_add"
("k1"
"n!1"
"k2"
"n!2+1"
"cf0"
"(append(CA(a!2), C2), e!1, s!1)"
"cf2"
"(null[Instruction], cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1), s!1)"))
(("1"
(replace -1 1)
(("1"
(inst
+
"(C2, cons(A(a!2)(s!1), e!1), s!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -2 2)
(("2"
(lemma
"tr_add"
("k1"
"n!2"
"k2"
"1"
"cf0"
"(C2, cons(A(a!2)(s!1), e!1), s!1)"
"cf2"
"(null[Instruction], cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1),
s!1)"))
(("2"
(replace -1)
(("2"
(inst
+
"(cons(BINARY(LAMBDA (i_1, j_1: int): b2n(i_1 = j_1)), null[Instruction]),
cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1)), s!1)")
(("2"
(assert)
(("2"
(hide-all-but 1)
(("2"
(expand "tr")
(("2"
(expand "tr")
(("2"
(expand "step")
(("2"
(expand
"check2")
(("2"
(expand
"top")
(("2"
(expand
"pop")
(("2"
(expand
"push")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (skolem + ("a!1" "a!2"))
(("4" (skosimp)
(("4" (expand "CB")
(("4" (expand "B")
(("4"
(lemma "correct_AExp" ("a" "a!2" "e" "e!1" "s" "s!1"))
(("4"
(lemma "correct_AExp"
("a" "a!1" "e" "cons(A(a!2)(s!1),e!1)" "s" "s!1"))
(("4" (skosimp*)
(("4" (inst + "n!1+n!2+1")
(("4"
(case "am.tr
(n!1+1)((append(CA(a!1),
cons(BINARY(LAMBDA (i, j:int): b2n(i <= j)), null)),cons(A(a!2)(s!1), e!1), s!1),(null, cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1))")
(("1" (hide -2)
(("1"
(name-replace "C2" "append(CA(a!1),
cons(BINARY(LAMBDA (i, j: int): b2n(i <= j)), null))")
(("1"
(name-replace "CF2"
"(null[Instruction], cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1)")
(("1"
(lemma "code_partial"
("k"
"n!2"
"c0"
"CA(a!2)"
"e0"
"e!1"
"s0"
"s!1"
"c1"
"null[Instruction]"
"e1"
"cons(A(a!2)(s!1), e!1)"
"s1"
"s!1"
"c2"
"C2"
"e2"
"null[int]"))
(("1"
(assert)
(("1"
(rewrite "append_null")
(("1"
(rewrite "append_null")
(("1"
(expand "append" -1 2)
(("1"
(assert)
(("1"
(lemma
"am.tr_add"
("k1"
"n!2"
"k2"
"n!1+1"
"cf0"
"(append(CA(a!2), C2), e!1, s!1)"
"cf2"
"CF2"))
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(inst
+
"(C2, cons(A(a!2)(s!1), e!1), s!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2)
(("2"
(lemma "code_partial"
("k" "n!1" "c0" "CA(a!1)" "e0"
"cons(A(a!2)(s!1),e!1)" "s0" "s!1" "c1"
"null[Instruction]" "e1"
"cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1))"
"s1" "s!1" "c2"
"cons(BINARY(LAMBDA (i, j: int): b2n(i <= j)), null[Instruction])"
"e2" "null[int]"))
(("2" (assert)
(("2" (rewrite "append_null")
(("2"
(rewrite "append_null")
(("2"
(expand "append" -1 2)
(("2"
(lemma
"am.tr_add"
("k1"
"n!1"
"k2"
"1"
"cf0"
"(append(CA(a!1),
cons(BINARY(LAMBDA (i, j: int): b2n(i <= j)), null)),
cons(A(a!2)(s!1), e!1), s!1)"
"cf2"
"(null[Instruction], cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1)"))
(("2"
(replace -1)
(("2"
(inst
+
"(cons(BINARY(LAMBDA (i_1, j_1: int): b2n(i_1 <= j_1)),
null[Instruction]),
cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1)), s!1)")
(("2"
(assert)
(("2"
(hide-all-but 2)
(("2"
(expand "tr")
(("2"
(expand "tr")
(("2"
(expand "step")
(("2"
(expand "check2")
(("2"
(expand "top")
(("2"
(expand "pop")
(("2"
(expand
"push")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (skolem + ("b!1"))
(("5" (skosimp*)
(("5" (inst - "e!1" "s!1")
(("5" (skosimp)
(("5" (inst + "n!1+1")
(("5" (expand "CB" 1)
(("5" (expand "B" 1)
(("5" (expand "b2n" 1)
(("5" (assert)
(("5"
(lemma "code_partial"
("k" "n!1" "c0" "CB(b!1)" "e0" "e!1" "s0"
"s!1" "c1" "null[Instruction]" "e1"
"cons(b2n(B(b!1)(s!1)), e!1)" "s1" "s!1" "c2"
"cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])"
"e2" "null[int]"))
(("5" (assert)
(("5" (rewrite "append_null")
(("5" (rewrite "append_null")
(("5"
(expand "append" -1 2)
(("5"
(name
"CF0"
"(append(CB(b!1), cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])), e!1, s!1)")
(("5"
(replace -1)
(("5"
(hide -1)
(("5"
(lemma
"am.tr_add"
("k1"
"n!1"
"k2"
"1"
"cf0"
"CF0"
"cf2"
"(null[Instruction], cons(IF NOT (B(b!1)(s!1)) THEN 1 ELSE 0 ENDIF, e!1), s!1)"))
(("5"
(replace -1 1)
(("5"
(hide -1)
(("5"
(inst
+
"(cons(UNARY(LAMBDA (i_1: int): 1 - i_1), null[Instruction]),
cons(b2n(B(b!1)(s!1)), e!1), s!1)")
(("5"
(assert)
(("5"
(hide -1 -2)
(("5"
(expand "tr")
(("5"
(expand "tr")
(("5"
(expand "step")
(("5"
(expand
"check1")
(("5"
(expand
"top")
(("5"
(expand
"push")
(("5"
(expand
"pop")
(("5"
(assert)
(("5"
(expand
"b2n")
(("5"
(assert)
(("5"
(lift-if)
(("5"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("6" (skolem + ("b!1" "b!2"))
(("6" (skosimp*)
(("6" (expand "CB" 1)
(("6" (expand "B" 1)
(("6" (inst - "cons(b2n(B(b!2)(s!1)),e!1)" "s!1")
(("6" (skosimp)
(("6" (inst - "e!1" "s!1")
(("6" (skosimp)
(("6" (expand "b2n" 1)
(("6" (name-replace "B1" "B(b!1)(s!1)")
(("6" (name-replace "B2" "B(b!2)(s!1)")
(("6"
(case "am.tr
(n!1+1)
((append(CB(b!1),
cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction])), cons(b2n(B2), e!1), s!1),(null[Instruction], cons(IF B1 AND B2 THEN 1 ELSE 0 ENDIF, e!1), s!1))")
(("1" (hide -2)
(("1"
(name-replace
"C2"
"append(CB(b!1),
cons(BINARY(LAMBDA (i, j: int): i * j),
null[Instruction]))")
(("1"
(name-replace
"CF2"
"(null[Instruction], cons(IF B1 AND B2 THEN 1 ELSE 0 ENDIF, e!1),
s!1)")
(("1"
(lemma
"code_partial"
("k"
"n!2"
"c0"
"CB(b!2)"
"e0"
"e!1"
"s0"
"s!1"
"c1"
"null[Instruction]"
"e1"
"cons(b2n(B2), e!1)"
"s1"
"s!1"
"c2"
"C2"
"e2"
"null[int]"))
(("1"
(assert)
(("1"
(rewrite "append_null")
(("1"
(rewrite "append_null")
(("1"
(expand "append" -1 2)
(("1"
(inst + "n!2+n!1+1")
(("1"
(lemma
"am.tr_add"
("k1"
"n!2"
"k2"
"1+n!1"
"cf0"
"(append(CB(b!2), C2), e!1, s!1)"
"cf2"
"CF2"))
(("1"
(replace -1)
(("1"
(inst
+
"(C2, cons(b2n(B2), e!1), s!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2)
(("2"
(lemma
"code_partial"
("k"
"n!1"
"c0"
"CB(b!1)"
"e0"
"cons(b2n(B2), e!1)"
"s0"
"s!1"
"c1"
"null[Instruction]"
"e1"
"cons(b2n(B1), cons(b2n(B2), e!1))"
"s1"
"s!1"
"c2"
"cons(BINARY(LAMBDA (i, j: int): i * j),
null[Instruction])"
"e2"
"null[int]"))
(("2"
(assert)
(("2"
(rewrite "append_null")
(("2"
(rewrite "append_null")
(("2"
(expand "append" -1 2)
(("2"
(name-replace
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.52 Sekunden
in einem neuen Tab ansehen
¤
|
Die farbliche Syntaxdarstellung ist noch experimentell.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
