(bisimulationnil 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" "C3" "cons(BINARY(LAMBDA (i, j: int): i + j), null[Instruction])" )"1" case "am.tr ") "1" "1" "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" "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" "(append(C1, C3), cons(N2, e!1), s!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "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" "2" "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" "2" "(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" "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" "C3" "cons(BINARY(LAMBDA (i, j: int): i - j), null[Instruction])" )"1" "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" "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" "1" "1" "1" "1" "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" "1" "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" "(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" "(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" "C3" "cons(BINARY(LAMBDA (i, j: int): i * j), null[Instruction])" )"1" "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" "(append(C1, C3),cons(N2, e!1), s!1)" )"1" "1" "1" "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" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "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" "2" assert )"2" "2" "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 "2" "(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" "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" 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 )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, numfield -> numfield]" number_fields nil )"odd_int" integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"odd_int" integersnil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"Stack" am nil ) (top const-decl "int" am nil )"bool" am nil ) (tr_add formula-decl nil am nil )"posint" nil )nil list_props nil )nil am nil )"list[T]" list_props nil )"[[[int, int] -> int] -> (BINARY?)]" nil )"[Instruction -> boolean]" Instructionnil )"int" integers nil )"nonneg_int" nil )"[T, T -> boolean]" equalities nil )"Config" am nil )"even_int" integersnil )"Stack" am nil )nil AExp nil )nil bisimulation nil )"[State -> int]" AExp nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"Code" compiler nil ) (tr def-decl "bool" am nil )nil am nil )nil am nil )nil Instruction nil )nil Instruction nil )nil naturalnumbers nil )"bool" reals nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil list_adt nil )nil numbers nil )nil booleans nil )nil AExp nil ))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" "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" "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" "C2" "append(CA(a!1), LAMBDA (i, j: int): b2n(i = j)), null))") "3" "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" "1" "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" "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" "(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" "2" "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), ")) "2" replace -1)"2" "(cons(BINARY(LAMBDA (i_1, j_1: int): b2n(i_1 = j_1)), null[Instruction]), ") "2" assert )"2" "2" expand "tr" )"2" expand "tr" )"2" expand "step" )"2" expand "check2" )"2" expand "top" )"2" expand "pop" )"2" expand "push" )"2" 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" "correct_AExp" ("a" "a!2" "e" "e!1" "s" "s!1" ))"4" "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 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" "C2" "append(CA(a!1), LAMBDA (i, j: int): b2n(i <= j)), null))") "1" "CF2" "(null[Instruction], cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1)" )"1" "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" "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" "1" "(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" "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" "am.tr_add" "k1" "n!1" "k2" "1" "cf0" "(append(CA(a!1), LAMBDA (i, j: int): b2n(i <= j)), null))," "cf2" "(null[Instruction], cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1)" ))"2" replace -1)"2" "(cons(BINARY(LAMBDA (i_1, j_1: int): b2n(i_1 <= j_1)), ") "2" assert )"2" "2" expand "tr" )"2" expand "tr" )"2" expand "step" )"2" expand "check2" )"2" expand "top" )"2" expand "pop" )"2" expand "push" )"2" 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" "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" "CF0" "(append(CB(b!1), cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])), e!1, s!1)" )"5" replace -1)"5" "5" "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" "5" "(cons(UNARY(LAMBDA (i_1: int): 1 - i_1), null[Instruction]), ") "5" assert )"5" "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" "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 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" "C2" "append(CB(b!1), LAMBDA (i, j: int): i * j),") "1" "CF2" "(null[Instruction], cons(IF B1 AND B2 THEN 1 ELSE 0 ENDIF, e!1), ") "1" "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" "n!2+n!1+1" )"1" "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" "(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" "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), " "e2" "null[int]" ))"2" assert )"2" rewrite "append_null" )"2" rewrite "append_null" )"2" expand "append" -1 2)"2" "CF0" "(append(CB(b!1), LAMBDA (i, j: int): i * j),") "2" "am.tr_add" "k1" "n!1" "k2" "1" "cf0" "CF0" "cf2" "(null[Instruction], cons(IF B1 AND B2 THEN 1 ELSE 0 ENDIF, e!1), ")) "2" replace -1)"2" "(cons(BINARY(LAMBDA (i_1, j_1: int): i_1 * j_1), ") "2" assert )"2" "2" expand "tr" )"2" expand "tr" )"2" expand "step" )"2" expand "check2" )"2" expand "top" )"2" expand "pop" )"2" expand "push" )"2" expand "b2n" )"2" "B1" )"1" "B2" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )"2" "B2" )"1" assert )nil nil )"2" 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 ))nil ))nil )"nonneg_int" nil )"odd_int" integers nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" am nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[[int -> int] -> (UNARY?)]" nil )"[Instruction -> boolean]" Instructionnil )"bool" reals nil )"odd_int" integersnil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_int" nil )nil am nil )"posint" nil )"bool" am nil ) (pop const-decl "Stack" am nil )"int" am nil )"int" integers nil )"list[T]" list_props nil )nil list_props nil )"[T, T -> boolean]" equalities nil )"[[[int, int] -> int] -> (BINARY?)]" nil )"[Instruction -> boolean]" Instructionnil )"Code" compiler nil )nil am nil )"[State -> int]" AExp nil )nil AExp nil )nil bisimulation nil )"Stack" am nil ) (step const-decl "Config" am nil )nil BExp nil )nil bisimulation nil )"[State -> bool]" BExp nil )"nbit" bit nil ) (nbit type-eq-decl nil bit nil )"bool" reals nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"Code" compiler nil ) (tr def-decl "bool" am nil )nil am nil )nil am nil )nil Instruction nil )nil Instruction nil )nil naturalnumbers nil )"bool" reals nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil list_adt nil )nil numbers nil )nil booleans nil )nil BExp nil ))nil 3399296901"" (skosimp*)"" (lemma "trich_lt" ("x" "m!1" "y" "n!1" ))"" (split)"1" "am.tr_add" "k1" "m!1" "cf0" "(CA(a!1), e!1, s!1)" "cf2" "(null[Instruction], cons(A(a!1)(s!1), e!1), s!1)" "k2" "n!1-m!1" ))"1" (assert )"1" (skosimp)"1" "am.tr_eq" "k" "m!1" "cf0" "(CA(a!1), e!1, s!1)" "cf1" "ac!1" "cf2" "cf1!1" ))"1" (assert )"1" (replace -1)"1" (expand "tr" -3) (("1" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (replace -1)"2" "am.tr_eq" "k" "n!1" "cf0" "(CA(a!1), e!1, s!1)" "cf1" "ac!1" "cf2" "(null[Instruction], cons(A(a!1)(s!1), e!1), s!1)" ))"2" (assert ) nil nil )) nil ))nil )"3" "am.tr_add" "k1" "n!1" "k2" "m!1-n!1" "cf0" "(CA(a!1), e!1, s!1)" "cf2" "ac!1" ))"1" (assert )"1" (skosimp)"1" "am.tr_eq" "k" "n!1" "cf0" "(CA(a!1), e!1, s!1)" "cf1" "cf1!1" "cf2" "(null[Instruction], cons(A(a!1)(s!1), e!1), s!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 naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )nil bisimulation nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[State -> int]" AExp nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"Code" compiler nil ) (AExp type-decl nil AExp nil )nil am nil )nil State nil )nil am nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil Instruction nil )nil list_adt nil )nil Instruction nil )nil am nil )"int" integers nil )"(total_order?[real])" nil )"bool" am nil ) (tr_eq formula-decl nil am nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil 3399347957"" (induct "a" )"1" (skosimp)"1" (skosimp)"1" (expand "CA" )"1" (expand "tr" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (skosimp*)"2" (expand "CA" )"2" (expand "tr" ) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (skolem + ("a!1" "a!2" ))"3" (skosimp*)"3" (expand "CA" -3)"3" "code_split" "k" "n!1" "c1" "CA(a!2)" "c2" "append(CA(a!1), LAMBDA (i, j:int): i + j), null[Instruction]))" "e" "e!1" "s" "s!1" "e2" "cons(A(Add(a!1, a!2))(s!1), e!1)" "s2" "s!1" ))"3" (replace -4 -1)"3" (skosimp)"3" (inst -5 "e!1" "k1!1" "s!1" )"3" (assert )"3" (hide-all-but (-1 1))"3" "correct_AExp" "a" "a!2" "e" "e!1" "s" "s!1" ))"3" (skosimp)"3" "eq_AExp" "a" "a!2" "e" "e!1" "s" "s!1" "ac" "(null[Instruction], e1!1, s1!1)" "n" "n!2" "m" "k1!1" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skolem + ("a!1" "a!2" ))"4" (skosimp*)"4" (expand "CA" -3)"4" "code_split" "k" "n!1" "c1" "CA(a!2)" "c2" "append(CA(a!1), LAMBDA (i, j:int): i - j), null[Instruction]))" "e" "e!1" "s" "s!1" "e2" "cons(A(Sub(a!1, a!2))(s!1), e!1)" "s2" "s!1" ))"4" (assert )"4" (skosimp)"4" (hide -2 -6 -4)"4" "correct_AExp" "a" "a!2" "e" "e!1" "s" "s!1" ))"4" (skosimp)"4" "eq_AExp" "n" "n!2" "a" "a!2" "e" "e!1" "s" "s!1" "ac" "(null[Instruction], e1!1, s1!1)" "m" "k1!1" ))"4" (assert )"4" (flatten)"4" (inst - "e!1" "n!2" "s!1" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (skolem + ("a!1" "a!2" ))"5" (skosimp*)"5" (expand "CA" -3)"5" "code_split" "k" "n!1" "c1" "CA(a!2)" "c2" "append(CA(a!1), LAMBDA (i, j:int): i * j), null[Instruction]))" "e" "e!1" "s" "s!1" "e2" "cons(A(Mul(a!1, a!2))(s!1), e!1)" "s2" "s!1" ))"5" (assert )"5" (skosimp)"5" (hide -2 -4 -6)"5" "correct_AExp" "a" "a!2" "e" "e!1" "s" "s!1" ))"5" (skosimp)"5" (inst - "e!1" "n!2" "s!1" )"5" (assert )"5" "eq_AExp" "n" "n!2" "a" "a!2" "e" "e!1" "s" "s!1" "ac" "(null[Instruction], e1!1, s1!1)" "m" "k1!1" ))"5" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, numfield -> numfield]" number_fields nil )"[AExp -> boolean]" AExp nil )"[[AExp, AExp] -> (Mul?)]" AExp nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[AExp -> boolean]" AExp nil )"[[AExp, AExp] -> (Sub?)]" AExp nil )nil bisimulation nil )nil bisimulation nil )"nonneg_int" nil )"int" integers nil )nil am nil )"list[T]" list_props nil )"[Instruction -> boolean]" Instructionnil )"[[[int, int] -> int] -> (BINARY?)]" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[AExp -> boolean]" AExp nil )"[[AExp, AExp] -> (Add?)]" AExp nil )"(total_order?[real])" nil )nil AExp nil )nil bisimulation nil )"[State -> int]" AExp nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"Code" compiler nil ) (tr def-decl "bool" am nil )nil am nil )nil am nil )nil Instruction nil )nil Instruction nil )"[bool, bool -> bool]" booleans nil )nil State nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil list_adt nil )nil numbers nil )nil booleans nil )nil AExp nil ))nil 3399349553"" case "FORALL (a1,a2: AExp,f:[[int,int]->int]): AND pn <= n AND am.tr(pn)((CA(a1), e, s), ac)AND AND pn <= n AND am.tr(pn)((CA(a2), e, s), ac)AND AND ") "1" (induct "a" )"1" (hide -1)"1" (skolem + ("z!1" ))"1" (skosimp*)"1" (expand "CA" )"1" (case-replace "n!1=0" )"1" (assert ) nil nil )"2" (case-replace "n!1=1" )"1" (expand "tr" )"1" (expand "tr" )"1" (flatten)"1" (assert )"1" (expand "step" )"1" (assert )"1" expand "push" )"1" expand "A" )"1" assert )"1" replace -4 * rl)"1" assert )"1" expand "length" 4 1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 3)"2" (expand "tr" )"2" (assert )"2" (flatten)"2" (expand "tr" )"2" (flatten)"2" expand "step" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (skolem + ("x!1" ))"2" (skosimp)"2" (expand "CA" )"2" (expand "A" )"2" (case-replace "n!1=0" )"1" (assert ) nil nil )"2" (case-replace "n!1=1" )"1" (expand "tr" )"1" (flatten)"1" (expand "step" )"1" (expand "tr" )"1" (assert )"1" expand "push" )"1" replace -4 * rl)"1" assert )"1" expand "length" 4 1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 3)"2" (expand "tr" )"2" (expand "tr" )"2" (expand "step" )"2" (expand "push" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem + ("a!1" "a!2" ))"3" (inst - "a!1" "a!2" "lambda (i,j:int):i+j" )"3" (skosimp*)"3" (expand "CA" -3)"3" (expand "A" -3)"3" (replace -2 -6)"3" (split -6)"1" (inst - "ac!1" "e!1" "n!1" "pn!1" "s!1" )"1" (replace -4)"1" (replace -5)"1" (expand "CA" -6)"1" (replace -6) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skolem + ("a!1" "a!2" ))"4" (skosimp*)"4" (expand "CA" -3)"4" (expand "A" -3)"4" (inst -6 "a!1" "a!2" "lambda (i,j:int): i-j" )"4" (replace -2)"4" (split -6)"1" (expand "CA" -6)"1" (inst - "ac!1" "e!1" "n!1" "pn!1" "s!1" )"1" (replace -4)"1" (replace -5)"1" (replace -6) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (skolem + ("a!1" "a!2" ))"5" (skosimp*)"5" (inst -6 "a!1" "a!2" "lambda (i,j:int): i*j" )"5" (replace -2)"5" (split -6)"1" (inst - "ac!1" "e!1" "n!1" "pn!1" "s!1" )"1" (expand "CA" (-4 -6))"1" (expand "A" -4) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" "code_split" "k" "n!1" "c1" "CA(a2!1)" "c2" "append(CA(a1!1), cons(BINARY(f!1), null[Instruction]))" "e" "e!1" "s" "s!1" "e2" "cons(f!1(A(a1!1)(s!1), A(a2!1)(s!1)), e!1)" "s2" "s!1" ))"2" (assert )"2" (skosimp)"2" "correct_AExp" ("a" "a2!1" "e" "e!1" "s" "s!1" ))"2" (skosimp)"2" "eq_AExp" "n" "n!2" "a" "a2!1" "e" "e!1" "s" "s!1" "m" "k1!1" "ac" "(null[Instruction], e1!1, s1!1)" ))"2" (assert )"2" (flatten)"2" (replace -1)"2" (replace -2)"2" (replace -3)"2" "2" "_" "e!1" "k1!1" "pn!1" "s!1" )"2" replace -1)"2" "pn!1<=k1!1" )"1" "1" expand "<=" -1)"1" "1" "am.tr_add" "k1" "pn!1" "k2" "k1!1-pn!1" "cf0" "(CA(a2!1), e!1, s!1)" "cf2" "(null[Instruction], cons(A(a2!1)(s!1), e!1), s!1)" ))"1" assert )"1" "1" "cf1!1" )"1" assert )"1" "code_partial" "k" "pn!1" "c0" "CA(a2!1)" "c1" "cf1!1`1" "e0" "e!1" "e1" "cf1!1`2" "s0" "s!1" "s1" "cf1!1`3" "c2" "append(CA(a1!1), cons(BINARY(f!1), null[Instruction]))" "e2" "null[int]" ))"1" rewrite "append_null" )"1" rewrite "append_null" )"1" rewrite "append_assoc" "1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" replace "1" "CF0" "(append(append(CA(a2!1), CA(a1!1)), ") "1" "tr_eq" "k" "pn!1" "cf0" "CF0" "cf1" "(append(cf1!1`1, " "cf2" "ac!1" ))"1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" replace -1)"2" "2" "code_partial" "k" "k1!1" "c0" "CA(a2!1)" "e0" "e!1" "s0" "s!1" "c1" "null[Instruction]" "e1" "cons(A(a2!1)(s!1), e!1)" "s1" "s!1" "c2" "append(CA(a1!1), cons(BINARY(f!1), null[Instruction]))" "e2" "null[int]" ))"2" rewrite "append_null" )"2" rewrite "append_null" )"2" replace -2)"2" rewrite "append_assoc" "2" "CF0" "(append(append(CA(a2!1), CA(a1!1)), ") "2" expand "append" "2" "am.tr_eq" "cf0" "CF0" "cf1" "(append(CA(a1!1), cons(BINARY(f!1), null[Instruction])), " "cf2" "ac!1" "k" "k1!1" ))"2" assert )"2" replace "2" assert )"2" expand "length" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "pn!1>k1!1" )"1" "1" "1" "code_split" "k" "k2!1" "c1" "CA(a1!1)" "c2" "cons(BINARY(f!1), null[Instruction])" "e" "cons(A(a2!1)(s!1), e!1)" "s" "s!1" "e2" "cons(f!1(A(a1!1)(s!1), A(a2!1)(s!1)), e!1)" "s2" "s!1" ))"1" assert )"1" "1" "k2!2=1" )"1" "1" case "am.tr ") "1" "1" "1" "correct_AExp" "a" "a1!1" "e" "cons(A(a2!1)(s!1), e!1)" "s" "s!1" ))"1" "1" "eq_AExp" "n" "n!3" "e" "cons(A(a2!1)(s!1), e!1)" "s" "s!1" "ac" "(null[Instruction], e1!2, s1!2)" "m" "k1!2" "a" "a1!1" ))"1" replace "1" replace "1" "1" "1" replace "1" replace "1" replace "1" "1" "_" "cons(A(a2!1)(s!1), e!1)" "k1!2" "_" "s!1" )"1" replace "1" expand "<=" "1" "1" "_" "pn!1-k1!1" )"1" assert )"1" expand "length" "1" "CF0" "(CA(a1!1), cons(A(a2!1)(s!1), e!1), s!1)" )"1" "1" "tr_add" "k1" "pn!1 - k1!1" "k2" "k1!2-(pn!1 - k1!1)" "cf0" "CF0" "cf2" "(null[Instruction], cons(A(a1!1)(s!1), cons(A(a2!1)(s!1), e!1)), s!1)" ))"1" assert )"1" "1" "cf1!1" )"1" assert )"1" expand "CF0" "1" "code_partial" "k" "pn!1-k1!1" "c0" "CA(a1!1)" "e0" "cons(A(a2!1)(s!1), e!1)" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "cons(BINARY(f!1), null[Instruction])" "e2" "null[int]" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" replace "1" rewrite "append_null" )"1" rewrite "append_null" )"1" "CF1" "(append(CA(a1!1), cons(BINARY(f!1), null[Instruction])), ") "1" "1" "tr_eq" "k" "pn!1-k1!1" "cf0" "CF1" "cf1" "ac!1" "cf2" "(append(cf1!1`1, cons(BINARY(f!1), null[Instruction])), cf1!1`2, ")) "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "pn!1 - k1!1=k2!1" )"1" "CF0" "(append(CA(a1!1), cons(BINARY(f!1), null[Instruction])), ") "1" "1" "tr_eq" "k" "k2!1" "cf0" "CF0" "cf1" "ac!1" "cf2" "(null[Instruction], cons(f!1(A(a1!1)(s!1), A(a2!1)(s!1)), e!1), s!1)" ))"1" assert )"1" replace "1" assert )"1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "tr_add" "k1" "k1!1" "k2" "pn!1-k1!1" "cf0" "(append(CA(a2!1), append(CA(a1!1), cons(BINARY(f!1), null[Instruction]))), " "cf2" "ac!1" ))"2" assert )"2" "2" "code_partial" "k" "k1!1" "c0" "CA(a2!1)" "e0" "e!1" "s0" "s!1" "c1" "null[Instruction]" "e1" "cons(A(a2!1)(s!1), e!1)" "s1" "s!1" "c2" "append(CA(a1!1), cons(BINARY(f!1), null[Instruction]))" "e2" "null[int]" ))"2" rewrite "append_null" )"2" rewrite "append_null" )"2" replace "2" rewrite "append_assoc" "2" "CF0" "(append(append(CA(a2!1), CA(a1!1)), ") "2" expand "append" "2" "tr_eq" "k" "k1!1" "cf0" "CF0" "cf1" "(append(CA(a1!1), cons(BINARY(f!1), null[Instruction])), " "cf2" "cf1!1" ))"2" assert )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "k2!2=0" )"1" expand "tr" )"1" nil nil ))nil )"2" expand "tr" )"2" expand "step" )"2" expand "check2" )"2" assert )"2" "2" "null?(e1!2)" )"2" "null?(cdr(e1!2))" )"1" assert )"1" expand "pop" )"1" expand "top" )"1" expand "push" )"1" expand "tr" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil am nil )"nonneg_int" nil )nil am nil )nil list_props nil )nil list_props nil )nil am nil )nil am nil )"(strict_total_order?[real])" real_props nil )"bool" am nil )"[(cons?) -> list]" list_adt nil )"Stack" am nil ) (top const-decl "int" am nil )"posint" nil )"[Code[V], (cons?), State[V]]" bisimulationnil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil bisimulation nil )nil bisimulation nil )nil AExp nil )"int" integers nil )"(total_order?[real])" nil )"Stack" am nil ) (step const-decl "Config" am nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" nil )nil bisimulation nil )nil AExp nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil Instruction nil )nil list_adt nil )nil Instruction nil )nil defined_types nil )"boolean" list_adt nil )nil am nil )nil State nil )nil am nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" am nil ) (CA def-decl "Code" compiler nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[State -> int]" AExp nil )"bool" reals nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"list[T]" list_props nil )"[Instruction -> boolean]" Instructionnil )"[[[int, int] -> int] -> (BINARY?)]" nil ))nil 3399387180"" (skosimp*)"" (lemma "trich_lt" ("x" "m!1" "y" "n!1" ))"" (split -1)"1" "tr_add" "k1" "m!1" "k2" "n!1-m!1" "cf0" "(CB(b!1), e!1, s!1)" "cf2" "(null[Instruction], cons(b2n(B(b!1)(s!1)), e!1), s!1)" ))"1" (assert )"1" (skosimp)"1" "tr_eq" "k" "m!1" "cf0" "(CB(b!1), e!1, s!1)" "cf1" "cf1!1" "cf2" "ac!1" ))"1" (assert )"1" (replace -1)"1" (expand "tr" -3) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (replace -1)"2" "tr_eq" "k" "n!1" "cf0" "(CB(b!1), e!1, s!1)" "cf1" "ac!1" "cf2" "(null[Instruction], cons(b2n(B(b!1)(s!1)), e!1), s!1)" ))"2" (assert ) nil nil )) nil ))nil )"3" "tr_add" "k1" "n!1" "k2" "m!1-n!1" "cf0" "(CB(b!1), e!1, s!1)" "cf2" "ac!1" ))"1" (assert )"1" (skosimp)"1" "tr_eq" "k" "n!1" "cf0" "(CB(b!1), e!1, s!1)" "cf1" "cf1!1" "cf2" "(null[Instruction], cons(b2n(B(b!1)(s!1)), e!1), s!1)" ))"1" (assert )"1" (replace -1)"1" (expand "tr" -3) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )nil bisimulation nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[State -> bool]" BExp nil )"nbit" bit nil ) (nbit type-eq-decl nil bit nil )"bool" reals nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"Code" compiler nil ) (BExp type-decl nil BExp nil )nil am nil )nil State nil )nil am nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil Instruction nil )nil list_adt nil )nil Instruction nil )nil am nil )"int" integers nil )"(total_order?[real])" nil )"bool" am nil ) (tr_eq formula-decl nil am nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil 3399387606"" (skosimp*)"" (case-replace "n!1=0" )"1" (lemma "nonnull_CB" ("b" "b!1" ))"1" (expand "tr" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" am nil )nil bisimulation nil )nil BExp nil )nil compiler nil )"(total_order?[real])" nil ))nil 3399401505"" (induct "b" )"1" (skosimp*)"1" (expand "CB" )"1" (expand "tr" )"1" (case-replace "n!1=0" )"1" (case-replace "n!1=1" )"1" (assert )"1" (flatten)"1" (expand "step" )"1" (expand "B" )"1" (expand "push" )"1" (expand "tr" )"1" (assert )"1" (replace -3 * rl)"1" assert )"1" expand "length" 4 1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "step" )"2" (expand "push" )"2" (expand "B" )"2" (expand "tr" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "CB" )"2" (expand "B" )"2" (expand "tr" )"2" (expand "step" )"2" (expand "tr" )"2" (expand "push" )"2" (prop)"2" (replace -2 * rl)"2" (assert )"2" (expand "length" 2 1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem + ("a!1" "a!2" ))"3" (skosimp)"3" (expand "CB" )"3" (expand "B" )"3" "correct_AExp" ("a" "a!2" "e" "e!1" "s" "s!1" ))"3" (skosimp)"3" "correct_AExp" "a" "a!1" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1" ))"3" (skosimp)"3" "code_split" "c1" "CA(a!2)" "c2" "append(CA(a!1), LAMBDA (i, j:int): b2n(i = j)), null[Instruction]))" "e" "e!1" "s" "s!1" "e2" "cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1)" "s2" "s!1" "k" "n!1" ))"3" (assert )"3" (skosimp)"3" "eq_AExp" "a" "a!2" "e" "e!1" "s" "s!1" "ac" "(null[Instruction], e1!1, s1!1)" "n" "n!2" "m" "k1!1" ))"3" (assert )"3" "3" replace -1)"3" replace -2)"3" replace -3)"3" "3" "code_split" "c1" "CA(a!1)" "c2" "cons(BINARY(LAMBDA (i, j: int): b2n(i = j)), " "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1" "e2" "cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1)" "s2" "s!1" "k" "k2!1" ))"3" assert )"3" "3" "k2!2=1" )"1" "1" "eq_AExp" "n" "n!3" "a" "a!1" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1" "m" "k1!2" "ac" "(null[Instruction], e1!2, s1!2)" ))"1" assert )"1" "1" replace -1)"1" replace "1" replace "1" "1" case "pn!1<=k1!1" )"1" "1" "tr_add" "k1" "pn!1" "k2" "k1!1-pn!1" "cf0" "(CA(a!2), e!1, s!1)" "cf2" "(null[Instruction], cons(A(a!2)(s!1), e!1), s!1)" ))"1" assert )"1" "1" "code_partial" "c0" "CA(a!2)" "e0" "e!1" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "append(CA(a!1), LAMBDA (i, j:int): b2n(i = j)), null[Instruction]))" "e2" "null[int]" "k" "pn!1" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" "CF0" "(append(CA(a!2), LAMBDA (i, j: int): b2n(i = j)),") "1" "tr_eq" "k" "pn!1" "cf0" "CF0" "cf1" "(append(cf1!1`1, LAMBDA " "cf2" "ac!1" ))"1" assert )"1" replace "1" assert )"1" "1" "AExp_e" "n" "k1!1" "a" "a!2" "e" "e!1" "s" "s!1" "pn" "pn!1" "ac" "cf1!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "k1!1+1 <= pn!1" )"1" "1" replace "1" replace "1" assert )"1" "1" expand "<=" "1" "1" "AExp_e" "n" "k1!2" "a" "a!1" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1" "pn" "pn!1-k1!1" ))"1" replace "1" expand "length" "1" assert )"1" "tr_add" "k1" "pn!1-k1!1" "k2" "k1!1+k1!2-pn!1" "cf0" "(CA(a!1), cons(A(a!2)(s!1), e!1), s!1)" "cf2" "(null[Instruction], cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1)), s!1)" ))"1" assert )"1" "1" "cf1!1" )"1" assert )"1" "1" "code_partial" "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" "append(CA(a!1), LAMBDA (i, j: int): b2n(i = j))," "e2" "null[int]" "k" "k1!1" ))"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" expand "append" "1" "1" "code_partial" "c0" "CA(a!1)" "e0" "cons(A(a!2)(s!1), e!1)" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "cons(BINARY(LAMBDA (i, j: int): b2n(i = j)), " "e2" "null[int]" "k" "pn!1-k1!1" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" replace "1" rewrite "append_null" )"1" rewrite "append_null" )"1" "1" "CODE1" "append(CA(a!1), LAMBDA (i, j: int): b2n(i = j)),") "1" "1" "tr_add" "k1" "k1!1" "k2" "pn!1-k1!1" "cf0" "(append(CA(a!2), CODE1), e!1, s!1)" "cf2" "(append(cf1!1`1, LAMBDA (i_1, j_1: int): b2n(i_1 = j_1)),")) "1" "1" "1" "1" assert )"1" "tr_eq" "k" "pn!1" "cf0" "(append(CA(a!2), CODE1), e!1, s!1)" "cf1" "(append(cf1!1`1, LAMBDA (i_1, j_1: int): b2n(i_1 = j_1))," "cf2" "ac!1" ))"1" assert )nil nil ))nil ))nil )"2" "(CODE1, cons(A(a!2)(s!1), e!1), s!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "NN" "1 + k1!1 + k1!2" )"2" "2" "CF0" "(append(CA(a!2), LAMBDA (i, j:int): b2n(i = j)), null[Instruction]))),") "2" "tr_eq" "k" "NN" "cf0" "CF0" "cf1" "(null[Instruction], cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1), s!1)" "cf2" "ac!1" ))"2" assert )"2" replace "2" assert )"2" expand "length" "2" assert )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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "k2!2=0" )"1" expand "tr" )"1" nil nil ))nil )"2" expand "tr" )"2" expand "step" )"2" expand "check2" )"2" assert )"2" "2" expand "push" )"2" expand "pop" )"2" expand "top" )"2" "null?(e1!2)" )"2" "null?(cdr(e1!2))" )"1" assert )"1" expand "tr" )"1" nil nil ))nil ))nil )"2" 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 )"4" (skolem + ("a!1" "a!2" ))"4" (skosimp)"4" (expand "CB" )"4" (expand "B" )"4" "code_split" "k" "n!1" "c1" "CA(a!2)" "c2" "append(CA(a!1), LAMBDA (i, j:int): b2n(i <= j)), null[Instruction]))" "e" "e!1" "s" "s!1" "e2" "cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1)" "s2" "s!1" ))"4" (assert )"4" (skosimp)"4" "correct_AExp" "a" "a!2" "e" "e!1" "s" "s!1" ))"4" (skosimp)"4" "eq_AExp" "n" "n!2" "a" "a!2" "e" "e!1" "s" "s!1" "ac" "(null[Instruction], e1!1, s1!1)" "m" "k1!1" ))"4" (assert )"4" (flatten)"4" (replace -1)"4" replace -2)"4" replace -3)"4" "4" expand "<=" -5)"4" "1" "1" case "pn!1<=k1!1" )"1" "1" "tr_add" "k1" "pn!1" "k2" "k1!1-pn!1" "cf0" "(CA(a!2), e!1, s!1)" "cf2" "(null[Instruction], cons(A(a!2)(s!1), e!1), s!1)" ))"1" assert )"1" "1" "1" "AExp_e" "n" "k1!1" "a" "a!2" "e" "e!1" "s" "s!1" "pn" "pn!1" "ac" "cf1!1" ))"1" assert )"1" "code_partial" "k" "pn!1" "c0" "CA(a!2)" "e0" "e!1" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "append(CA(a!1), LAMBDA (i, j:int): b2n(i <= j)), null[Instruction]))" "e2" "null[int]" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" "CF0" "(append(CA(a!2), LAMBDA (i, j: int): b2n(i <= j)),") "1" "tr_eq" "k" "pn!1" "cf0" "CF0" "cf1" "(append(cf1!1`1, LAMBDA " "cf2" "ac!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "k1!1+1<=pn!1" )"1" "1" "code_split" "k" "k2!1" "c1" "CA(a!1)" "c2" "cons(BINARY(LAMBDA (i, j: int): b2n(i <= j)), null[Instruction])" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1" "e2" "cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1)" "s2" "s!1" ))"1" assert )"1" "1" "k2!2=1" )"1" "1" "correct_AExp" "a" "a!1" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1" ))"1" "1" "eq_AExp" "a" "a!1" "n" "n!3" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1" "ac" "(null[Instruction], e1!2, s1!2)" "m" "k1!2" ))"1" assert )"1" "1" replace "1" replace "1" "1" "tr_add" "k1" "pn!1-k1!1" "k2" "k1!1+k1!2-pn!1" "cf0" "(CA(a!1), cons(A(a!2)(s!1), e!1), s!1)" "cf2" "(null[Instruction], cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1)), s!1)" ))"1" assert )"1" "1" "AExp_e" "n" "k1!2" "a" "a!1" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1" "pn" "pn!1 - k1!1" "ac" "cf1!1" ))"1" assert )"1" expand "length" "1" "1" "code_partial" "k" "pn!1-k1!1" "c0" "CA(a!1)" "e0" "cons(A(a!2)(s!1), e!1)" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "cons(BINARY(LAMBDA (i, j:int): b2n(i <= j)), null[Instruction])" "e2" "null[int]" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" "CODE1" "append(CA(a!1), LAMBDA (i, j: int): b2n(i <= j)),") "1" "1" "tr_add" "k1" "k1!1" "k2" "pn!1-k1!1" "cf0" "(append(CA(a!2), CODE1), e!1, s!1)" "cf2" "(append(cf1!1`1, LAMBDA (i_1, j_1: int): b2n(i_1 <= j_1)),")) "1" "1" "1" "1" assert )"1" "tr_eq" "k" "pn!1" "cf0" "(append(CA(a!2), CODE1), e!1, s!1)" "cf1" "(append(cf1!1`1, LAMBDA (i_1, j_1: int): b2n(i_1 <= j_1))," "cf2" "ac!1" ))"1" assert )nil nil ))nil ))nil )"2" "(CODE1, cons(A(a!2)(s!1), e!1), s!1)" )"2" assert )"2" "2" "code_partial" "k" "k1!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" "CODE1" "e2" "null[int]" ))"2" rewrite "append_null" )"2" rewrite "append_null" )"2" replace "2" expand "append" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "tr" )"2" expand "step" )"2" expand "check2" )"2" expand "push" )"2" expand "top" )"2" expand "pop" )"2" "2" "null?(e1!2)" )"2" "null?(cdr(e1!2))" )"1" assert )"1" expand "tr" )"1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "CF0" "(append(CA(a!2), LAMBDA (i, j:int): b2n(i <= j)), null[Instruction]))),") "2" "tr_eq" "k" "n!1" "cf0" "CF0" "cf1" "(null[Instruction], cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1)" "cf2" "ac!1" ))"2" assert )"2" replace -1 1 rl)"2" assert )"2" expand "length" "2" 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 )"5" (skolem + ("b!1" ))"5" (skosimp*)"5" (expand "CB" (-2 -4))"5" (expand "B" -2)"5" "correct_BExp" ("b" "b!1" "e" "e!1" "s" "s!1" ))"5" (skosimp)"5" "code_split" "k" "n!1" "c1" "CB(b!1)" "c2" "cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])" "e" "e!1" "s" "s!1" "e2" "cons(b2n(NOT (B(b!1)(s!1))), e!1)" "s2" "s!1" ))"5" (assert )"5" (skosimp)"5" "eq_BExp" "n" "n!2" "b" "b!1" "e" "e!1" "s" "s!1" "ac" "(null[Instruction], e1!1, s1!1)" "m" "k1!1" ))"5" (assert )"5" (flatten)"5" (replace -1)"5" replace -2)"5" replace -3)"5" "5" "k2!1=1" )"1" "1" expand "<=" -6)"1" "1" "tr_add" "k1" "pn!1" "k2" "k1!1-pn!1" "cf0" "(CB(b!1), e!1, s!1)" "cf2" "(null[Instruction], cons(b2n(B(b!1)(s!1)), e!1), s!1)" ))"1" assert )"1" "1" "code_partial" "k" "pn!1" "c0" "CB(b!1)" "e0" "e!1" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "cons(UNARY(LAMBDA (i: int): 1 - i), null[Instruction])" "e2" "null[int]" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" "tr_eq" "k" "pn!1" "cf0" "(append(CB(b!1), LAMBDA (i: int): 1 - i), null[Instruction]))," "cf1" "(append(cf1!1`1, LAMBDA (i: int): 1 - i), null[Instruction]))," "cf2" "ac!1" ))"1" assert )"1" replace "1" assert )"1" "1" "cf1!1" "e!1" "k1!1" "pn!1" "s!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" replace -1)"2" "CF0" "(append(CB(b!1), cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])), e!1, s!1)" )"2" "2" "tr_eq" "k" "n!1" "cf0" "CF0" "cf1" "(null[Instruction], cons(b2n(NOT (B(b!1)(s!1))), e!1), s!1)" "cf2" "ac!1" ))"2" assert )"2" replace "2" assert )"2" expand "length" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "tr" )"2" expand "step" )"2" expand "check1" )"2" expand "push" )"2" expand "pop" )"2" expand "top" )"2" "2" expand "tr" )"2" "2" expand "b2n" )"2" "B(b!1)(s!1)" )"1" assert )nil nil )"2" 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 )"6" (skolem + ("b!1" "b!2" ))"6" (skosimp*)"6" (expand "CB" (-3 -5))"6" (expand "B" -3)"6" (inst - "_" "_" "_" "_" "s!1" )"6" (inst - "_" "_" "_" "_" "s!1" )"6" (expand "<=" -4)"6" (split -4)"1" "code_split" "k" "n!1" "c1" "CB(b!2)" "c2" "append(CB(b!1), LAMBDA (i, j:int): i * j), null[Instruction]))" "e" "e!1" "s" "s!1" "e2" "cons(b2n(B(b!1)(s!1) AND B(b!2)(s!1)), e!1)" "s2" "s!1" ))"1" (assert )"1" (replace -5 -1)"1" (skosimp)"1" "correct_BExp" "b" "b!2" "e" "e!1" "s" "s!1" ))"1" "1" "eq_BExp" "b" "b!2" "e" "e!1" "s" "s!1" "ac" "(null[Instruction], e1!1, s1!1)" "m" "k1!1" "n" "n!2" ))"1" assert )"1" "1" replace -1)"1" replace -2)"1" replace -3)"1" "1" case "pn!1<=k1!1" )"1" "1" "tr_add" "k1" "pn!1" "k2" "k1!1-pn!1" "cf0" "(CB(b!2), e!1, s!1)" "cf2" "(null[Instruction], cons(b2n(B(b!2)(s!1)), e!1), s!1)" ))"1" assert )"1" "1" "1" "code_partial" "k" "pn!1" "c0" "CB(b!2)" "e0" "e!1" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "append(CB(b!1), LAMBDA (i, j:int): i * j), null[Instruction]))" "e2" "null[int]" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" "CF0" "(append(CB(b!2), LAMBDA (i, j: int): i * j),") "1" "tr_eq" "k" "pn!1" "cf0" "CF0" "cf1" "(append(cf1!1`1, LAMBDA (i_1, j_1: int): i_1 * j_1)," "cf2" "ac!1" ))"1" assert )"1" replace "1" assert )"1" "cf1!1" "e!1" "k1!1" "pn!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "k1!1+1 <= pn!1" )"1" "1" "1" "code_split" "k" "k2!1" "c1" "CB(b!1)" "c2" "cons(BINARY(LAMBDA (i_1, j_1: int): i_1 * j_1), " "e" "cons(b2n(B(b!2)(s!1)),e!1)" "s" "s!1" "e2" "cons(b2n(B(b!1)(s!1) AND B(b!2)(s!1)), e!1)" "s2" "s!1" ))"1" replace -4)"1" "1" "k2!2=1" )"1" "1" "correct_BExp" "b" "b!1" "e" "cons(b2n(B(b!2)(s!1)), e!1)" "s" "s!1" ))"1" "1" "eq_BExp" "n" "n!3" "b" "b!1" "e" "cons(b2n(B(b!2)(s!1)), e!1)" "s" "s!1" "ac" "(null[Instruction], e1!2, s1!2)" "m" "k1!2" ))"1" assert )"1" "1" replace "1" replace "1" replace "1" "1" "tr_add" "k1" "pn!1-k1!1" "k2" "k1!2+k1!1-pn!1" "cf0" "(CB(b!1), cons(b2n(B(b!2)(s!1)), e!1), s!1)" "cf2" "(null[Instruction], cons(b2n(B(b!1)(s!1)), cons(b2n(B(b!2)(s!1)), e!1)), s!1)" ))"1" assert )"1" "1" "cf1!1" "cons(b2n(B(b!2)(s!1)), e!1)" "k1!2" "pn!1-k1!1" )"1" assert )"1" expand "length" "1" "1" "code_partial" "k" "pn!1-k1!1" "c0" "CB(b!1)" "e0" "cons(b2n(B(b!2)(s!1)), e!1)" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction])" "e2" "null[int]" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" "CODE1" "append(CB(b!1), LAMBDA (i, j: int): i * j),") "1" "1" "1" "code_partial" "k" "k1!1" "c0" "CB(b!2)" "e0" "e!1" "s0" "s!1" "c1" "null[Instruction]" "e1" "cons(b2n(B(b!2)(s!1)), e!1)" "s1" "s!1" "c2" "CODE1" "e2" "null[int]" ))"1" rewrite "append_null" )"1" rewrite "append_null" )"1" expand "append" "1" "CF1" "(CODE1, cons(b2n(B(b!2)(s!1)), e!1), s!1)" )"1" "CF0" "(append(CB(b!2), CODE1), e!1, s!1)" )"1" "tr_add" "k1" "k1!1" "k2" "pn!1-k1!1" "cf0" "CF0" "cf2" "(append(cf1!1`1, LAMBDA (i_1, j_1: int): i_1 * j_1),")) "1" "1" "1" "1" assert )"1" "tr_eq" "k" "pn!1" "cf0" "CF0" "cf1" "(append(cf1!1`1, LAMBDA (i_1, j_1: int): i_1 * j_1)," "cf2" "ac!1" ))"1" assert )nil nil ))nil ))nil )"2" "CF1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "tr" )"2" expand "step" )"2" expand "check2" )"2" expand "push" )"2" expand "pop" )"2" expand "top" )"2" "null?(e1!2)" )"1" nil nil )"2" "null?(cdr(e1!2))" )"1" nil nil )"2" assert )"2" expand "tr" )"2" nil nil ))nil ))nil )"3" assert )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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (hide -1 -2 -3)"2" "CF0" "(append(CB(b!2), LAMBDA (i, j:int): i * j), null[Instruction]))),") "2" "tr_eq" "k" "n!1" "cf0" "CF0" "cf1" "(null[Instruction], cons(b2n(B(b!1)(s!1) AND B(b!2)(s!1)), e!1), s!1)" "cf2" "ac!1" ))"2" (assert )"2" replace -2 -1)"2" replace -1 1 rl)"2" assert )"2" expand "length" 1 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, numfield -> numfield]" number_fields nil )nil bisimulation nil )"[Instruction -> boolean]" Instructionnil )"[[int -> int] -> (UNARY?)]" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" am nil )nil bisimulation nil )nil bisimulation nil )nil AExp nil )"[State -> int]" AExp nil )nil am nil )"Code" compiler nil )"list[T]" list_props nil )"[Instruction -> boolean]" Instructionnil )"[[[int, int] -> int] -> (BINARY?)]" nil )"nonneg_int" nil )"bool" am nil ) (pop const-decl "Stack" am nil )"[(cons?) -> list]" list_adt nil )"int" am nil )"posint" nil )nil am nil )"[numfield, numfield -> numfield]" number_fields nil )nil list_props nil )nil bisimulation nil )nil am nil )nil am nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"odd_int" integersnil )nil bisimulation nil )"Stack" am nil ) (step const-decl "Config" am nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"even_int" integersnil )"int" integers nil )"[T, T -> boolean]" equalities nil )nil BExp nil )nil bisimulation nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" list_props nil )"bool" reals nil )"[State -> bool]" BExp nil )"nbit" bit nil ) (nbit type-eq-decl nil bit nil )"bool" reals nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"Code" compiler nil ) (tr def-decl "bool" am nil )"[bool, bool -> bool]" booleans nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil am nil )nil State nil )nil integers nil )nil am nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil numbers nil )nil Instruction nil )nil list_adt nil )nil Instruction nil )nil booleans nil )nil BExp nil )"posint" nil ))nil 3399040375 ("" (subtype-tcc) nil nil )nil bisimulation nil )"bool" sos nil ))nil ))nil 3399040375 ("" (subtype-tcc) nil nil )nil bisimulation nil )"bool" sos nil ))nil ))nil 3399040388"" (induct "S" )"1" (skolem + ("x!1" "a!1" ))"1" (skosimp)"1" (expand "step" 1)"1" (expand "assign" )"1" (expand "assign" )"1" "correct_AExp" "a" "a!1" "s" "s!1" "e" "null[int]" ))"1" (skosimp)"1" "n!1+1" "(null[Instruction],null[int],LAMBDA (y:V): IF y = x!1 THEN A(a!1)(s!1) ELSE s!1(y) ENDIF)" )"1" (expand "~" )"1" (expand "terminal?" )"1" (flatten)"1" (expand "CS" )"1" "code_partial" "k" "n!1" "c0" "CA(a!1)" "e0" "null[int]" "s0" "s!1" "c1" "null[Instruction]" "e1" "cons(A(a!1)(s!1), null[int])" "s1" "s!1" "c2" "cons(STORE(x!1), null)" "e2" "null[int]" ))"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" expand "append" -1 2)"1" "1" "tr_add" "k1" "n!1" "k2" "1" "cf0" "ac0!1" "cf2" "(null[Instruction], null[int], LAMBDA (y:V):IF y = x!1 THEN A(a!1)(s!1) ELSE s!1(y) ENDIF)")) "1" replace -1)"1" "1" "(cons(STORE(x!1), null), cons(A(a!1)(s!1), null[int]), s!1)" )"1" assert )"1" "(append(CA(a!1), cons(STORE(x!1), null)), null[int], s!1)=ac0!1" )"1" replace -2)"1" "1" expand "tr" )"1" expand "tr" )"1" expand "step" )"1" expand "check1" )"1" expand "top" )"1" expand "pop" )"1" expand "assign" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" 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 )"2" (skosimp)"2" (inst + "1" "(null[Instruction],null[int],s!1)" )"2" (expand "~" )"2" (expand "terminal?" )"2" (assert )"2" (flatten)"2" (expand "step" )"2" (assert ) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem + ("S!1" "S!2" ))"3" (skosimp*)"3" (hide -2)"3" (expand "~" )"3" (expand "terminal?" )"3" (flatten)"3" (assert )"3" (inst - "(CS(S!1),null[int],s!1)" "s!1" )"3" (skosimp)"3" (expand "step" 1)"3" (assert )"3" (case-replace "T?(sos.step(S!1, s!1))" )"1" (assert )"1" "1" "code_partial" "k" "pn!1" "c0" "CS(S!1)" "e0" "null[int]" "e1" "null[int]" "e2" "null[int]" "c1" "null[Instruction]" "c2" "CS(S!2)" "s0" "s!1" "s1" "ac1!1`3" ))"1" "(null[Instruction], null[int], ac1!1`3)=ac1!1" )"1" assert )"1" expand "append" -2 2)"1" expand "append" -2 2)"1" expand "append" -2 2)"1" expand "CS" -8)"1" replace -8 * rl)"1" "pn!1" "(CS(S!2), null[int], ac1!1`3)" )"1" assert )"1" "(ac0!1`1, null[int], s!1)=ac0!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "2" assert )"2" expand "CS" -5)"2" expand "CS" 2)"2" "code_partial" "k" "pn!1" "c0" "CS(S!1)" "c1" "ac1!1`1" "c2" "CS(S!2)" "e0" "null[int]" "e1" "null[int]" "e2" "null[int]" "s0" "s!1" "s1" "ac1!1`3" ))"2" "(ac1!1`1, null[int], ac1!1`3)=ac1!1" )"1" assert )"1" expand "append" -2 2)"1" expand "append" -2 3)"1" replace -3 * rl)"1" "pn!1" "(append(ac1!1`1, CS(S!2)), null[int], ac1!1`3)" )"1" "(append(CS(S!1), CS(S!2)), null[int], s!1)=ac0!1" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skolem + ("b!1" "S!1" "S!2" ))"4" (skosimp)"4" (skosimp)"4" "correct_BExp" "b" "b!1" "e" "null[int]" "s" "s!1" ))"4" (skosimp)"4" (hide -2 -3)"4" (case "B(b!1)(s!1)" )"1" (inst + "n!1+1" "(CS(S!1),null[int],s!1)" )"1" (expand "step" 1)"1" (assert )"1" (expand "~" )"1" (expand "terminal?" )"1" (flatten)"1" expand "CS" -3)"1" "code_partial" "k" "n!1" "c0" "CB(b!1)" "e0" "null[int]" "s0" "s!1" "c1" "null[Instruction]" "e1" "cons(b2n(TRUE), null[int])" "s1" "s!1" "c2" "cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction])" "e2" "null[int]" ))"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" replace -4 * rl)"1" expand "append" -1 1)"1" "1" "am.tr_add" "k1" "n!1" "k2" "1" "cf0" "ac0!1" "cf2" "(CS(S!1), null[int], s!1)" ))"1" replace -1)"1" "1" "(ac0!1`1, null[int], s!1)=ac0!1" )"1" "(cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction]), ") "1" assert )"1" "1" expand "tr" )"1" expand "tr" )"1" expand "step" )"1" expand "check1" )"1" expand "b2n" )"1" expand "top" )"1" expand "pop" )"1" rewrite "append_null" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "n!1+1" "(CS(S!2),null[int],s!1)" )"2" (expand "step" 2)"2" (assert )"2" (expand "~" )"2" (expand "terminal?" )"2" (flatten)"2" expand "CS" -2)"2" "code_partial" "k" "n!1" "c0" "CB(b!1)" "e0" "null[int]" "s0" "s!1" "c1" "null[Instruction]" "e1" "cons(b2n(FALSE), null[int])" "s1" "s!1" "c2" "cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction])" "e2" "null[int]" ))"2" assert )"2" rewrite "append_null" )"2" rewrite "append_null" )"2" expand "append" -1 2)"2" replace -3 -1 rl)"2" "(ac0!1`1, null[int], s!1)=ac0!1" )"1" "1" "1" "am.tr_add" "k1" "n!1" "k2" "1" "cf0" "ac0!1" "cf2" "(CS(S!2), null[int], s!1)" ))"1" replace -1)"1" "1" "(cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction]), ") "1" assert )"1" "1" expand "tr" )"1" expand "tr" )"1" expand "step" )"1" expand "check1" )"1" expand "b2n" )"1" expand "top" )"1" expand "pop" )"1" rewrite "append_null" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" 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" "S!1" ))"5" (skosimp)"5" (skosimp)"5" (hide -1)"5" (expand "~" )"5" (expand "terminal?" )"5" (flatten)"5" (expand "step" )"5" "1" "(CS(Conditional(b!1, Sequence(S!1, While(b!1, S!1)), Skip)),null[int],s!1)" )"5" (expand "tr" )"5" (copy -1)"5" (expand "CS" -1)"5" (replace -1)"5" assert )"5" expand "step" )"5" replace -1)"5" assert )"5" expand "tr" )"5" "1" "1" case "forall b: length(CB(b))>=1" )"1" "b!1" )"1" "length_append" "l1" "CB(b!1)" "l2" "cons(BRANCH(append(CS(S!1), LOOP (CB(b!1), CS(S!1)), null[Instruction])),")) "1" replace -3 * rl)"1" replace -4 -1)"1" expand "length" "1" expand "length" "1" expand "length" "1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "b" )"1" nil nil )"2" nil nil )"3" "3" expand "CB" )"3" rewrite "append_assoc" "3" "length_append" "l1" "append(CA(Eq2_var!1), CA(Eq1_var!1))" "l2" "cons(BINARY(LAMBDA (i, j:int): b2n(i = j)), null[Instruction])" ))"3" expand "length" "3" expand "length" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "CB" )"4" "length_append" "l1" "append(CA(Le2_var!1), CA(Le1_var!1))" "l2" "cons(BINARY(LAMBDA (i, j:int): b2n(i <= j)), null[Instruction])" ))"4" expand "length" "4" expand "length" "4" rewrite "append_assoc" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" expand "CB" 1)"5" "length_append" "l1" "CB(Neg1_var!1)" "l2" "cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])" ))"5" expand "length" "5" assert )nil nil ))nil ))nil ))nil ))nil )"6" "6" expand "CB" 1)"6" rewrite "length_append" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "CS" 1 3)"2" expand "CS" 1 3)"2" expand "CS" 1 4)"2" expand "CS" 1 5)"2" 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 )"[Stm -> boolean]" Stm nil )"[[BExp[V], Stm, Stm] -> (Conditional?)]" Stm nil )"[Stm -> boolean]" Stm nil )"[[Stm, Stm] -> (Sequence?)]" Stmnil )"[Stm -> boolean]" Stm nil )"[[BExp[V], Stm] -> (While?)]" Stm nil )"[Stm -> boolean]" Stm nil )"(Skip?)" Stm nil )"nat" list_props nil )nil list_props nil )"(total_order?[real])" nil )nil BExp nil )nil list_props nil )"[Instruction -> boolean]" Instructionnil )"[[[int, int] -> int] -> (BINARY?)]" nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[[int -> int] -> (UNARY?)]" nil )"[Instruction -> boolean]" Instructionnil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, numfield -> numfield]" number_fields nil )LOOP ? adt-recognizer-decl "[Instruction -> boolean]" Instructionnil )LOOP adt-constructor-decl"[[list[Instruction], list[Instruction]] -> (LOOP?)]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"(NOOP?)" Instruction nil )"[State -> bool]" BExp nil )"Code" compiler nil )"[Instruction -> boolean]" Instructionnil )"[[list[Instruction], list[Instruction]] -> (BRANCH?)]" nil )"bool" reals nil ) (nbit type-eq-decl nil bit nil )"nbit" bit nil )"bool" booleans nil )"bool" booleans nil )nil BExp nil )nil bisimulation nil )"am[V].Config" bisimulation nil )"[Config -> boolean]" sos nil )"State" State nil )nil am nil )"Code" compiler nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[Instruction -> boolean]" Instructionnil )"[V -> (STORE?)]" Instruction nil )nil list_props nil )"list[T]" list_props nil )nil am nil ) (step const-decl "Config" am nil )"int" am nil ) (pop const-decl "Stack" am nil )"bool" am nil )"int" integers nil )"posint" nil )"Code" compiler nil )"bool" sos nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"[State -> int]" AExp nil )"posint" nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )nil AExp nil )nil bisimulation nil )"State" State nil )nil Stm nil )nil bisimulation nil )"bool" am nil )nil naturalnumbers nil )"[Config]" sos nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"[[Stm[V], State[V]] -> (I?)]" sos nil )"[Config -> boolean]" sos nil )"bool" bisimulation nil )nil sos nil )"[bool, bool -> bool]" booleans nil )nil am nil )nil State nil )nil integers nil )nil am nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil numbers nil )nil Instruction nil )nil list_adt nil )nil Instruction nil )nil booleans nil )nil Stm nil ))nil 3399106364"" (induct "n" )"1" (skosimp*) (("1" (expand "tr" ) (("1" (propax) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "tr" -2)"2" (case-replace "j!1=0" )"1" (expand "tr" -3)"1" (hide -2)"1" "sos_step" "S" "S!1" "s" "s0!1" "ac0" "(CS(S!1),null[int],s0!1)" ))"1" (expand "~" -1 1)"1" (expand "terminal?" )"1" (skosimp)"1" (replace -4)"1" (hide -3 -4)"1" (expand "~" )"1" (expand "terminal?" )"1" "1" "pn!1" )"1" "(null[Instruction], null[int], s1!1)=ac1!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "j!1>=1" )"1" (hide 1)"1" "sos_step" "S" "S!1" "s" "s0!1" "ac0" "(CS(S!1),null[int],s0!1)" ))"1" (expand "~" -1 1)"1" (expand "terminal?" )"1" (skosimp)"1" (expand "~" )"1" (expand "terminal?" )"1" (assert )"1" "T?(sos.step(S!1, s0!1))" )"1" "1" expand "tr" -8)"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" assert )"2" "2" case "I?(sos.step(S!1, s0!1))" )"1" "1" "S(sos.step(S!1, s0!1))" "s(sos.step(S!1, s0!1))" "s1!1" )"1" "sos.I(S(sos.step(S!1, s0!1)), s(sos.step(S!1, s0!1)))=step(S!1, s0!1)" )"1" assert )"1" "(CS(S(sos.step(S!1, s0!1))), null[int], ") "1" "1" "1" "pn!1+m!1" )"1" rewrite "tr_add" "1" "ac1!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"bool" bisimulation nil )nil integers nil )"bool" reals nil )nil integers nil )"am[V].Config" bisimulation nil )"bool" sos nil )nil bisimulation nil )"[Config]" sos nil ) (tr_add formula-decl nil am nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil sos nil )"[(I?) -> Stm[V]]" sos nil )"[(I?) -> State[V]]" sos nil )"(total_order?[real])" nil )nil naturalnumbers nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"Code" compiler nil ) (tr def-decl "bool" am nil )nil am nil )nil am nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil Instruction nil )nil list_adt nil )nil Instruction nil )"[State[V] -> (T?)]" sos nil )"[Config -> boolean]" sos nil )"[[Stm[V], State[V]] -> (I?)]" sos nil )"[Config -> boolean]" sos nil )"bool" sos nil ) (Config type-decl nil sos nil )"[bool, bool -> bool]" booleans nil )nil State nil )nil Stm nil )nil bisimulation nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3399359572"" (induct "S" )"1" (skolem + ("x!1" "a!1" ))"1" (skosimp)"1" (expand "step" )"1" (expand "~" )"1" (expand "terminal?" )"1" (flatten)"1" (expand "CS" -1)"1" "ac!1=(append(CA(a!1), cons(STORE(x!1), null[Instruction])),null[int],s!1)" )"1" (hide -1 -2 -3 -4)"1" "ac1!1=(null[Instruction],null[int],assign(x!1, A(a!1))(s!1))" )"1" (hide-all-but 1)"1" "correct_AExp" "a" "a!1" "e" "null[int]" "s" "s!1" ))"1" (skosimp)"1" "n!1+1" )"1" "am.tr ") "1" "1" expand "<=" -3)"1" "1" "AExp_e" "n" "n!1" "a" "a!1" "e" "null[int]" "s" "s!1" ))"1" replace -4)"1" expand "length" -1 2)"1" "n!2=0" )"1" expand "tr" -6)"1" replace -6 1 rl)"1" assert )nil nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "tr_add" "k1" "n!2" "k2" "n!1-n!2" "cf0" "(CA(a!1), null[int], s!1)" "cf2" "(null[Instruction], cons(A(a!1)(s!1), null[int]), s!1)" ))"2" assert )"2" "2" "cf1!1" "n!2" )"2" assert )"2" "code_partial" "c0" "CA(a!1)" "e0" "null[int]" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "cons(STORE(x!1), null[Instruction])" "e2" "null[int]" "k" "n!2" ))"2" assert )"2" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" replace "1" rewrite "append_null" )"1" rewrite "append_null" )"1" "CF0" "(append(CA(a!1), cons(STORE(x!1), null[Instruction])), null[int], ") "1" "1" "tr_eq" "k" "n!2" "cf0" "CF0" "cf1" "(append(cf1!1`1, cons(STORE(x!1), null[Instruction])), cf1!1`2, " "cf2" "ac2!1" ))"1" assert )"1" replace "1" assert )"1" "length_is_0" "l" "cf1!1`2" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "CF0" "(append(CA(a!1), cons(STORE(x!1), null[Instruction])), ") "2" expand "assign" )"2" expand "assign" )"2" "tr_eq" "k" "n!1+1" "cf0" "CF0" "cf1" "(null[Instruction], null[int], LAMBDA (y:V): IF y = x!1 THEN A(a!1)(s!1) ELSE s!1(y) ENDIF)" "cf2" "ac2!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "code_partial" "k" "n!1" "c0" "CA(a!1)" "e0" "null[int]" "s0" "s!1" "c1" "null[Instruction]" "e1" "cons(A(a!1)(s!1), null[int])" "s1" "s!1" "c2" "cons(STORE(x!1), null[Instruction])" "e2" "null[int]" ))"2" assert )"2" rewrite "append_null" )"2" rewrite "append_null" )"2" expand "append" -1 2)"2" expand "assign" )"2" expand "assign" )"2" "tr_add" "k1" "n!1" "k2" "1" "cf0" "(append(CA(a!1), cons(STORE(x!1), null[Instruction])), null[int], " "cf2" "(null[Instruction], null[int], LAMBDA (y:V): IF y = x!1 THEN A(a!1)(s!1) ELSE s!1(y) ENDIF)")) "2" replace -1 1)"2" "2" "(cons(STORE(x!1), null[Instruction]), ") "2" replace "2" "2" expand "tr" )"2" expand "tr" )"2" expand "step" )"2" expand "check1" )"2" expand "pop" )"2" expand "assign" )"2" expand "top" )"2" 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 )"2" (decompose-equality) nil nil ))nil ))nil )"2" (decompose-equality) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "step" )"2" (expand "~" )"2" (expand "terminal?" )"2" (flatten)"2" (expand "CS" )"2" "ac!1=(cons(NOOP, null[Instruction]),null[int],s!1)" )"1" (hide -1 -2 -3 -4)"1" "ac1!1=(null[Instruction],null[int],s!1)" )"1" (hide -1 -2 -3 -4)"1" (inst + "1" )"1" (expand "tr" )"1" (expand "step" )"1" expand "tr" 1 1)"1" "1" "n!1=0" )"1" (assert ) nil nil )"2" "n!1=1" )"1" assert )"1" expand "tr" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (decompose-equality) nil nil ))nil ))nil )"2" (decompose-equality) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem + ("S!1" "S!2" ))"3" (skosimp*)"3" (hide -2)"3" (inst - "_" "_" "s!1" )"3" (expand "~" )"3" (expand "terminal?" )"3" (flatten)"3" "ac!1=(CS(Sequence(S!1, S!2)),null[int],s!1)" )"1" (hide -3 -1 -4 -5)"1" "T?(sos.step(Sequence(S!1, S!2), s!1))" )"1" (flatten)"1" (hide-all-but -1)"1" (expand "step" )"1" "T?(step(S!1, s!1))" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (replace 1)"2" case "I?(sos.step(Sequence(S!1, S!2), s!1))" )"1" (hide 1)"1" "1" "ac1!1=(CS(S(sos.step(Sequence(S!1, S!2), s!1))),null[int],s(sos.step(Sequence(S!1, S!2), s!1)))" )"1" "1" "(CS(S!1),null[int],s!1)" "_" )"1" "T?(sos.step(S!1, s!1))" )"1" "(null[Instruction],null[int],s1(sos.step(S!1, s!1)))" )"1" "1" "pn!1" )"1" expand "CS" 1 3)"1" expand "step" 1)"1" assert )"1" expand "CS" 1 1)"1" "code_partial" "k" "pn!1" "c0" "CS(S!1)" "e0" "null[int]" "s0" "s!1" "c1" "null[Instruction]" "e1" "null[int]" "s1" "s1(sos.step(S!1, s!1))" "c2" "CS(S!2)" "e2" "null[int]" ))"1" replace -4)"1" rewrite "append_null" )"1" expand "append" "1" replace "1" "1" "tr_add" "k1" "n!1" "k2" "pn!1-n!1" "cf0" "(CS(S!1),null[int], s!1)" "cf2" "(null[Instruction], null[int], s1(sos.step(S!1, s!1)))" ))"1" replace "1" assert )"1" "1" "n!1" "cf1!1" )"1" assert )"1" "code_partial" "c0" "CS(S!1)" "e0" "null[int]" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "CS(S!2)" "e2" "null[int]" "k" "n!1" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" replace "1" rewrite "append_null" )"1" rewrite "append_null" )"1" "tr_eq" "k" "n!1" "cf0" "(append(CS(S!1), CS(S!2)), null[int], s!1)" "cf1" "(append(cf1!1`1, CS(S!2)), cf1!1`2, cf1!1`3)" "cf2" "ac2!1" ))"1" assert )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "I?(sos.step(S!1, s!1))" )"1" "1" "(CS(S(sos.step(S!1, s!1))),null[int],s(sos.step(S!1, s!1)))" )"1" "1" "pn!1" )"1" expand "step" 1)"1" expand "CS" 1)"1" "code_partial" "k" "pn!1" "c0" "CS(S!1)" "e0" "null[int]" "s0" "s!1" "c1" "CS(S(sos.step(S!1, s!1)))" "e1" "null[int]" "s1" "s(sos.step(S!1, s!1))" "c2" "CS(S!2)" "e2" "null[int]" ))"1" replace "1" rewrite "append_null" )"1" replace "1" "1" "n!1" "_" )"1" "tr_add" "k1" "n!1" "k2" "pn!1-n!1" "cf0" "(CS(S!1), null[int], s!1)" "cf2" "(CS(S(sos.step(S!1, s!1))), null[int], s(sos.step(S!1, s!1)))" ))"1" assert )"1" "1" "cf1!1" )"1" assert )"1" "code_partial" "k" "n!1" "c0" "CS(S!1)" "e0" "null[int]" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "CS(S!2)" "e2" "null[int]" ))"1" assert )"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" "tr_eq" "k" "n!1" "cf0" "(append(CS(S!1), CS(S!2)), null[int], s!1)" "cf1" "(append(cf1!1`1, CS(S!2)), cf1!1`2, cf1!1`3)" "cf2" "ac2!1" ))"1" assert )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (decompose-equality) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (decompose-equality) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skolem + ("b!1" "S!1" "S!2" ))"4" (skosimp*)"4" (hide -1 -2)"4" (expand "step" )"4" (expand "~" )"4" (expand "terminal?" )"4" (flatten)"4" (expand "CS" -1)"4" "correct_BExp" "b" "b!1" "s" "s!1" "e" "null[int]" ))"4" (skosimp)"4" (inst + "n!1+1" )"4" "ac!1=(append(CB(b!1), cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction])),null[int],s!1)" )"1" (hide -1 -3 -4 -5)"1" "ac1!1=(IF B(b!1)(s!1) THEN CS(S!1) ELSE CS(S!2) ENDIF,null[int],s!1)" )"1" "1" "code_partial" "c0" "CB(b!1)" "e0" "null[int]" "s0" "s!1" "c1" "null[Instruction]" "e1" "cons(b2n(B(b!1)(s!1)), null[int])" "s1" "s!1" "c2" "cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction])" "e2" "null[int]" "k" "n!1" ))"1" replace -2)"1" rewrite "append_null" )"1" rewrite "append_null" )"1" expand "append" -1 2)"1" "am.tr IF B(b!1)(s!1) THEN CS(S!1) ELSE CS(S!2) ENDIF, null[int],") "1" "1" "1" "n!2=0" )"1" expand "tr" -5)"1" replace "1" assert )nil nil ))nil ))nil )"2" "n!2=n!1+1" )"1" "CF0" "(append(CB(b!1), ") "1" "1" "1" "tr_eq" "k" "1+n!1" "cf0" "CF0" "cf1" "(IF B(b!1)(s!1) THEN CS(S!1) ELSE CS(S!2) ENDIF, null[int], s!1)" "cf2" "ac2!1" ))"1" assert )"1" replace "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "1<=n!2&n!2<=n!1" )"1" "1" "1" "BExp_e" "n" "n!1" "b" "b!1" "e" "null[int]" "s" "s!1" "pn" "n!2" ))"1" replace "1" expand "length" "1" "tr_add" "k1" "n!2" "k2" "n!1-n!2" "cf0" "(CB(b!1), null[int], s!1)" "cf2" "(null[Instruction], cons(b2n(B(b!1)(s!1)), null[int]), s!1)" ))"1" assert )"1" "1" "cf1!1" )"1" assert )"1" "code_partial" "c0" "CB(b!1)" "e0" "null[int]" "s0" "s!1" "c1" "cf1!1`1" "e1" "cf1!1`2" "s1" "cf1!1`3" "c2" "cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction])" "e2" "null[int]" "k" "n!2" ))"1" "(cf1!1`1, cf1!1`2, cf1!1`3)=cf1!1" )"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" "CF0" "(append(CB(b!1), ") "1" "tr_eq" "k" "n!2" "cf0" "CF0" "cf1" "(append(cf1!1`1, " "cf2" "ac2!1" ))"1" assert )"1" replace "1" assert )"1" "1" "length_is_0" "l" "cf1!1`2" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "tr_add" "k1" "n!1" "k2" "1" "cf0" "(append(CB(b!1), " "cf2" "(IF B(b!1)(s!1) THEN CS(S!1) ELSE CS(S!2) ENDIF, null[int], ")) "2" replace -1)"2" "2" "(cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction]), ") "2" replace -1)"2" "2" expand "tr" )"2" expand "step" )"2" expand "check1" )"2" expand "tr" )"2" expand "top" )"2" expand "pop" )"2" "B(b!1)(s!1)" )"1" expand "b2n" )"1" rewrite "append_null" )nil nil ))nil )"2" assert )"2" expand "b2n" )"2" rewrite "append_null" )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 )"2" (decompose-equality) nil nil ))nil ))nil )"2" (decompose-equality) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (skolem + ("b!1" "S!1" ))"5" (skosimp*)"5" (expand "step" -3)"5" (hide -1)"5" (expand "~" )"5" (expand "terminal?" )"5" (flatten)"5" (expand "CS" )"5" (expand "CS" -4)"5" (expand "CS" -4 2)"5" (inst + "1" )"5" (expand "tr" 1)"5" (assert )"5" expand "step" 1)"5" replace -1)"5" assert )"5" expand "tr" 1 1)"5" "CODE0" "cons(LOOP(CB(b!1), CS(S!1)), null[Instruction])" )"5" "CODE1" "append(CB(b!1), ]))") "5" "(CODE1, ac!1`2, ac!1`3) = ac1!1" )"1" "ac!1 = ac1!1" )"1" "1" replace -6)"1" "1" expand "CODE1" )"1" expand "CODE0" )"1" "nonnull_CB" "b" "b!1" ))"1" "length_append" "l1" "CB(b!1)" "l2" "cons(BRANCH(append(CS(S!1), LOOP (CB(b!1), CS(S!1)),")) "1" replace "1" expand "length" "1" expand "length" "1" expand "length" "1" expand "length" "1" "length_is_0" "l" "CB(b!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "n!1=0" )"1" replace "1" replace -4)"1" assert )nil nil ))nil ))nil )"2" "n!1=1" )"1" assert )"1" expand "tr" "1" replace "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"list[Instruction[V]]" bisimulation nil )nil compiler nil )nil list_props nil )"(cons?[Instruction[V]])" bisimulationnil )LOOP ? adt-recognizer-decl "[Instruction -> boolean]" Instructionnil )LOOP adt-constructor-decl"[[list[Instruction], list[Instruction]] -> (LOOP?)]" Instructionnil )nil bisimulation nil )nil BExp nil )nil bisimulation nil )"nbit" bit nil ) (nbit type-eq-decl nil bit nil )"bool" reals nil )"[State -> bool]" BExp nil )"Code" compiler nil )"[Instruction -> boolean]" Instructionnil )"[[list[Instruction], list[Instruction]] -> (BRANCH?)]" nil )"[(I?) -> State[V]]" sos nil )"[(I?) -> Stm[V]]" sos nil )"Stm[V]" bisimulation nil )"State[V]" bisimulation nil )"[(T?) -> State[V]]" sos nil )"odd_int" integers nil )"[Config -> boolean]" sos nil )"[Stm -> boolean]" Stm nil )"[[Stm, Stm] -> (Sequence?)]" Stmnil )"(NOOP?)" Instruction nil )"[Instruction -> boolean]" Instructionnil )"even_int" integersnil )"bool" sos nil )"Code" compiler nil )"int" integers nil )"State" State nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil bisimulation nil )"nat" list_props nil )nil am nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil list_props_aux nil )nil am nil )nil list_props nil )nil am nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"bool" am nil ) (top const-decl "int" am nil )"Stack" am nil ) (step const-decl "Config" am nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil bisimulation nil )"State" State nil )"[State -> int]" AExp nil )"list[T]" list_props nil )nil AExp nil ) (CA def-decl "Code" compiler nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[Instruction -> boolean]" Instructionnil )"[V -> (STORE?)]" Instruction nil )"(null?)" list_adt nil )nil Stm nil )nil bisimulation nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil ) (tr def-decl "bool" am nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil ) (step def-decl "[Config]" sos nil )"[[Stm[V], State[V]] -> (I?)]" sos nil )"[Config -> boolean]" sos nil )"bool" bisimulation nil )nil sos nil )"[bool, bool -> bool]" booleans nil )nil am nil )nil State nil )nil integers nil )nil am nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil numbers nil )nil Instruction nil )nil list_adt nil )nil Instruction nil )nil booleans nil )nil Stm nil ))nil 3399357571"" "NAT_induction" "p" "lambda (m:nat): FORALL (S: Stm, s0, s1: State): ")) "" (split)"1" (skosimp)"1" (inst - "m!1" )"1" (inst - "S!1" "s0!1" "s1!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (case-replace "j!1=0" )"1" (inst + "0" )"1" (hide -1 -2)"1" (expand "tr" )"1" (flatten)"1" (lemma "nonnull_CS" ("S" "S!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (case "j!1>=1" )"1" (hide 1)"1" (case "T?(step(S!1, s0!1))" )"1" (inst + "1" )"1" (expand "tr" 1)"1" (expand "tr" 1)"1" (hide-all-but (-1 1 -4 -2))"1" (expand "step" )"1" (assert )"1" "1" assert )"1" "Assign?(S!1)" )"1" expand "CS" )"1" assert )"1" "x!1" "x(S!1)" )"1" "a!1" "a(S!1)" )"1" "1" "1" "correct_AExp" "a" "a!1" "e" "null[int]" "s" "s0!1" ))"1" "1" "code_partial" "c0" "CA(a!1)" "e0" "null[int]" "s0" "s0!1" "c1" "null[Instruction]" "e1" "cons(A(a!1)(s0!1), null[int])" "s1" "s0!1" "c2" "cons(STORE(x!1), null[Instruction])" "e2" "null[int]" "k" "n!1" ))"1" assert )"1" rewrite "append_null" )"1" rewrite "append_null" )"1" expand "append" "1" "code_split" "k" "j!1" "c1" "CA(a!1)" "e" "null[int]" "s" "s0!1" "c2" "cons(STORE(x!1), null[Instruction])" "e2" "null[int]" "s2" "s1!1" ))"1" replace "1" "1" "eq_AExp" "a" "a!1" "e" "null[int]" "s" "s0!1" "ac" "(null[Instruction], e1!1, s1!2)" "n" "n!1" "m" "k1!1" ))"1" assert )"1" "1" replace "1" replace "1" replace "1" "1" "k2!1=1" )"1" "1" "1" expand "tr" )"1" expand "tr" )"1" expand "step" )"1" expand "check1" )"1" expand "pop" )"1" expand "top" )"1" expand "assign" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "k2!1=0" )"1" expand "tr" )"1" nil nil ))nil )"2" expand "tr" )"2" assert )"2" "2" expand "step" )"2" expand "check1" )"2" expand "pop" )"2" expand "top" )"2" expand "tr" )"2" nil
Messung V0.5 in Prozent C=100 H=98 G=98
¤ 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.0.864Bemerkung:
(vorverarbeitet am 2026-04-29)
¤ *Bot Zugriff
