Quelle am.prf
Sprache: Lisp
(amnil 3398743350 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" 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 am nil ))nil ))nil 3398491018"" (skosimp) (("" (assert ) nil nil )) nil ) nil nil ))nil 3398491018"" (skosimp*)"" (assert ) (("" (expand "check1" ) (("" (propax) nil nil )) nil ))nil ))nil )"bool" am nil )) nil ))nil 3398491018"" (skosimp*)"" (expand "check2" ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil )"bool" am nil )) nil ))nil 3398491018"" (skosimp*)"" (expand "check2" )"" (flatten)"" (assert ) (("" (expand "pop" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" am nil ) (pop const-decl "Stack" am nil ))nil ))nil 3398491018"" (skosimp*) (("" (expand "check1" ) (("" (assert ) nil nil )) nil ))nil )"bool" am nil )) nil ))nil 3398491018"" (skosimp*) (("" (expand "check1" ) (("" (assert ) nil nil )) nil ))nil )"bool" am nil )) nil ))nil 3398743350 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3398743350 ("" (termination-tcc) nil nil )"Config" am nil )) nil ))nil 3399091849"" (skosimp*)"" (expand "step" )"" (assert )"" (lemma "append_is_null" ("l1" "c1!1" "l2" "c2!1" ))"" (assert )"" (case-replace "car(append(c1!1, c2!1))=car(c1!1)" )"1" "cdr(append(c1!1, c2!1))=append(cdr(c1!1),c2!1)" )"1" (case "PUSH?(car(c1!1))" )"1" (assert )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil )"2" (case "FETCH?(car(c1!1))" )"1" (assert )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil )"2" (case "UNARY?(car(c1!1))" )"1" (assert )"1" (expand "check1" )"1" (lift-if)"1" (assert )"1" "null?(e!1)" )"1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "BINARY?(car(c1!1))" )"1" (assert )"1" (expand "check2" )"1" (case-replace "null?(e!1)" )"1" "null?(cdr(e!1))" )"1" assert )"1" "1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (case "STORE?(car(c1!1))" )"1" (assert )"1" (expand "check1" )"1" "null?(e!1)" )"1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case "NOOP?(car(c1!1))" )"1" (assert ) nil nil )"2" (case "BRANCH?(car(c1!1))" )"1" assert )"1" expand "check1" )"1" "null?(e!1)" )"1" assert )"1" "top(e!1) = 1" )"1" assert )"1" "1" assert )"1" rewrite "append_assoc" "1" replace -5 * rl)"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" rewrite "append_assoc" "2" replace -4 * rl)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "LOOP?(car(c1!1))" )"1" assert )"1" "CB" "c3(car(c1!1))" )"1" "IB" "BRANCH(append(c4(car(c1!1)), LOOP (CB, c4(car(c1!1))), null[Instruction])),") "1" "IBR" "BRANCH(append(c4(car(c1!1)), LOOP (CB, c4(car(c1!1))), null[Instruction])),") "1" "append_eq2" "l2" "c1!1" "l3" "append(CB, cons(IBR, cdr(c1!1)))" "l1" "c2!1" ))"1" replace -1 -5 rl)"1" replace -5 10)"1" rewrite "append_assoc" )"1" expand "append" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "append" 1 1) (("2" (propax) nil nil ))nil ))nil )"2" (expand "append" 1 1) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Config" am nil )nil Instruction nil )nil am nil )nil Instruction nil )nil list_adt nil )nil list_props_aux nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[list -> boolean]" list_adt nil )"[(cons?) -> T]" list_adt nil )"list[T]" list_props nil )"[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"bool" am nil )nil am nil )"[list -> boolean]" list_adt 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 numbers nil )"[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"[(BRANCH?) -> list[Instruction]]" nil )nil list_props nil )"[(BRANCH?) -> list[Instruction]]" nil )"int" am nil )"(null?)" list_adt nil )LOOP adt-constructor-decl"[[list[Instruction], list[Instruction]] -> (LOOP?)]" Instructionnil )"[[T, list] -> (cons?)]" list_adt nil )"[(LOOP?) -> list[Instruction]]" Instructionnil )"[[list[Instruction], list[Instruction]] -> (BRANCH?)]" nil )nil list_props_aux nil )"(NOOP?)" Instruction nil )"[(LOOP?) -> list[Instruction]]" Instructionnil )LOOP ? adt-recognizer-decl "[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"bool" am nil )"[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"[(cons?) -> list]" list_adt nil ))nil 3398743779"" (induct "k1" )"1" (skosimp)"1" (split)"1" (flatten)"1" (inst + "cf0!1" )"1" (expand "tr" 1 1) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (expand "tr" -1) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (skosimp*)"2" (split)"1" (flatten)"1" (expand "tr" 1 1)"1" (expand "tr" -1)"1" (flatten)"1" (assert )"1" (inst - "step(cf0!1)" "cf2!1" "k2!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "tr" (-1 1))"2" (flatten)"2" (assert )"2" (inst - "step(cf0!1)" "cf2!1" "k2!1" )"2" (replace -3)"2" (hide -3)"2" (inst + "cf1!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"Config" am nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" am nil )"[bool, bool -> bool]" booleans 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 )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 )"nonneg_int" nil ))nil 3398743611"" (induct "k" )"1" (skosimp) (("1" (expand "tr" ) (("1" (assert ) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "tr" (-2 -3))"2" (flatten)"2" (inst - "step(cf0!1)" "cf1!1" "cf2!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"Config" am nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" am nil )"[bool, bool -> bool]" booleans 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 )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 3398746849"" (induct "k" )"1" (expand "tr" ) (("1" (skosimp*) (("1" (assert ) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "tr" -2)"2" (flatten)"2" (expand "tr" 3)"2" (lemma "append_is_null" ("l1" "c0!1" "l2" "c2!1" ))"2" (assert )"2" "step(c0!1, e0!1, s0!1)`1" "c1!1" "c2!1" "step(c0!1, e0!1, s0!1)`2" "e1!1" "e2!1" "step(c0!1, e0!1, s0!1)`3" "s1!1" )"2" "(step(c0!1, e0!1, s0!1)`1, step(c0!1, e0!1, s0!1)`2, ") "1" (hide -1)"1" (replace -2 -1)"1" "(append(step(c0!1, e0!1, s0!1)`1, c2!1), ") "1" (replace -2)"1" (expand "/=" 4)"1" "1" replace -1 -2 rl)"1" "1" "1" "1" expand "step" )"1" case "PUSH?(car(c0!1))" )"1" assert )"1" expand "push" )"1" expand "append" "1" "length_append" "l1" "c0!1" "l2" "c2!1" ))"1" "length_append" "l1" "cdr(c0!1)" "l2" "c2!1" ))"1" replace "1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FETCH?(car(c0!1))" )"1" assert )"1" "length_append" "l1" "c0!1" "l2" "c2!1" ))"1" expand "length" "1" "length_append" "l1" "cdr(c0!1)" "l2" "c2!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "UNARY?(car(c0!1))" )"1" assert )"1" expand "check1" )"1" "null?(e0!1)" )"1" assert )"1" "length_append" "l1" "cdr(c0!1)" "l2" "c2!1" ))"1" "length_append" "l1" "c0!1" "l2" "c2!1" ))"1" expand " length" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "BINARY?(car(c0!1))" )"1" assert )"1" expand "check2" )"1" "null?(e0!1)" )"1" assert )"1" "null?(cdr(e0!1))" )"1" assert )"1" "length_append" "l1" "cdr(c0!1)" "l2" "c2!1" ))"1" "length_append" "l1" "c0!1" "l2" "c2!1" ))"1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "STORE?(car(c0!1))" )"1" assert )"1" expand "check1" )"1" assert )"1" "null?(e0!1)" )"1" assert )"1" "length_append" "l1" "cdr(c0!1)" "l2" "c2!1" ))"1" "length_append" "l1" "c0!1" "l2" "c2!1" ))"1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOOP?(car(c0!1))" )"1" assert )"1" "length_append" "l1" "cdr(c0!1)" "l2" "c2!1" ))"1" "length_append" "l1" "c0!1" "l2" "c2!1" ))"1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "BRANCH?(car(c0!1))" )"1" assert )"1" expand "check1" )"1" "null?(e0!1)" )"1" assert )"1" expand "top" )"1" expand "pop" )"1" "length_append" "l1" "cdr(e0!1)" "l2" "e2!1" ))"1" "length_append" "l1" "e0!1" "l2" "e2!1" ))"1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "LOOP?(car(c0!1))" )"1" assert )"1" "IB" "BRANCH(append(c4(car(c0!1)), LOOP ") "1" rewrite "append_assoc" )"1" "IBR" "BRANCH(append(c4(car(c0!1)), LOOP (c3(car(c0!1)), c4(car(c0!1))),") "1" "append_eq2" "l2" "c0!1" "l3" "append(c3(car(c0!1)), cons(IBR, cdr(c0!1)))" "l1" "c2!1" ))"1" replace "1" rewrite "append_assoc" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "append_eq2" "l2" "e0!1" "l3" "step(c0!1, e0!1, s0!1)`2" "l1" "e2!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 5)"2" (expand "step" )"2" "car(append(c0!1, c2!1))= car(c0!1)" )"1" "cdr(append(c0!1, c2!1))= append(cdr(c0!1),c2!1)" )"1" case "PUSH?(car(c0!1))" )"1" assert )"1" expand "push" )"1" expand "append" 1 1)"1" (propax) nil nil ))nil ))nil ))nil )"2" case "FETCH?(car(c0!1))" )"1" assert )"1" expand "push" )"1" expand "append" 2 1)"1" (propax) nil nil ))nil ))nil ))nil )"2" case "UNARY?(car(c0!1))" )"1" assert )"1" expand "check1" )"1" expand "push" )"1" expand "top" )"1" "append_is_null" "l1" "e0!1" "l2" "e2!1" ))"1" "null?(e0!1)" )"1" assert )"1" expand "pop" )"1" expand "append" "1" expand "append" "1" expand "append" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "BINARY?(car(c0!1))" )"1" assert )"1" expand "check2" )"1" expand "pop" )"1" expand "push" )"1" expand "top" )"1" "null?(e0!1)" )"1" assert )"1" "null?(cdr(e0!1))" )"1" assert )"1" "append_is_null" "l1" "e0!1" "l2" "e2!1" ))"1" assert )"1" "append_is_null" "l1" "cdr(e0!1)" "l2" "e2!1" ))"1" assert )"1" expand "append" "1" expand "append" "1" expand "append" "1" "cdr(append(e0!1, e2!1)) = append(cdr(e0!1),e2!1)" )"1" expand "append" "1" "TOP" "f2(car(c0!1))(car(e0!1), car(cdr(e0!1)))" )"1" expand "append" "1" nil nil ))nil ))nil ))nil )"2" expand "append" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "STORE?(car(c0!1))" )"1" assert )"1" expand "check1" )"1" "null?(e0!1)" )"1" assert )"1" expand "pop" )"1" expand "top" )"1" "append_is_null" "l1" "e0!1" "l2" "e2!1" ))"1" assert )"1" expand "append" "1" expand "append" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOOP?(car(c0!1))" )"1" (assert ) nil nil )"2" case "BRANCH?(car(c0!1))" )"1" assert )"1" expand "check1" )"1" "null?(e0!1)" )"1" assert )"1" expand "pop" )"1" expand "top" )"1" "append_is_null" "l1" "e0!1" "l2" "e2!1" ))"1" assert )"1" expand "append" "1" expand "append" "1" expand "append" "1" "car(e0!1) = 1" )"1" rewrite "append_assoc" )nil nil )"2" assert )"2" rewrite "append_assoc" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "LOOP?(car(c0!1))" )"1" assert )"1" "IB" "BRANCH(append(c4(car(c0!1)), LOOP (c3(car(c0!1)), c4(car(c0!1))),") "1" rewrite "append_assoc" )"1" expand "append" "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "append" 1 1)"2" (propax) nil nil ))nil ))nil )"2" expand "append" 1 1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (decompose-equality) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil list_props_aux nil )"Config" am nil )"boolean" notequal nil )"[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"bool" am nil )"[Instruction -> boolean]" Instructionnil )LOOP ? adt-recognizer-decl "[Instruction -> boolean]" Instructionnil )"(null?)" list_adt nil )"[(LOOP?) -> list[Instruction]]" Instructionnil )LOOP adt-constructor-decl"[[list[Instruction], list[Instruction]] -> (LOOP?)]" Instructionnil )"[[T, list] -> (cons?)]" list_adt nil )"[(LOOP?) -> list[Instruction]]" Instructionnil )"[[list[Instruction], list[Instruction]] -> (BRANCH?)]" nil )nil list_props_aux nil )nil list_props nil )"(NOOP?)" Instruction nil )"int" am nil ) (pop const-decl "Stack" am nil )"[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"[list -> boolean]" list_adt nil )"bool" am nil )"[Instruction -> boolean]" Instructionnil )"[(cons?) -> list]" list_adt nil )"nat" list_props nil )"nonneg_int" nil )"posint" nil )nil list_props nil )"Stack" am nil )"[(cons?) -> T]" list_adt nil )"[list -> boolean]" list_adt nil )"[Instruction -> boolean]" Instructionnil )"[(BINARY?) -> [[int, int] -> int]]" nil )"[(BRANCH?) -> list[Instruction]]" nil )"[(BRANCH?) -> list[Instruction]]" nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"list[T]" list_props nil )"bool" am nil )nil am nil )"[bool, bool -> bool]" booleans 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 )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 3399030329"" (induct "k" )"1" (skosimp*)"1" (expand "tr" )"1" (flatten)"1" (inst + "e!1" "s!1" "0" "0" )"1" (assert )"1" (lemma "append_is_null" ("l1" "c1!1" "l2" "c2!1" ))"1" (assert )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (case-replace "c1!1=null[Instruction]" )"1" (expand "append" -3)"1" (inst + "e!1" "s!1" "0" "1+j!1" )"1" (assert )"1" (expand "tr" ) (("1" (propax) nil nil )) nil )) nil ))nil ))nil )"2" (case "cons?(c1!1)" )"1" (hide 1)"1" (expand "tr" -3)"1" (flatten)"1" (hide 1)"1" "step_append" "c1" "c1!1" "c2" "c2!1" "e" "e!1" "s" "s!1" ))"1" (assert )"1" (expand "/=" -1 1)"1" (replace 1 -1)"1" case "step(append(c1!1, c2!1), e!1, s!1) = (append(step(c1!1, e!1, s!1)`1,c2!1),step(c1!1, e!1, s!1)`2,step(c1!1, e!1, s!1)`3)" )"1" "step(c1!1, e!1, s!1)`1" "c2!1" "step(c1!1, e!1, s!1)`2" "e2!1" "step(c1!1, e!1, s!1)`3" "s2!1" )"1" replace -1 -4 rl)"1" replace -5)"1" "1" "(step(c1!1, e!1, s!1)`1, step(c1!1, e!1, s!1)`2, ") "1" "1" "e1!1" "s1!1" "k1!1+1" "k2!1" )"1" assert )"1" "1" expand "tr" 2)"1" assert )"1" expand "/=" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 -4 3)"2" expand "step" )"2" "append_is_null" "l1" "c1!1" "l2" "c2!1" ))"2" assert )"2" "car(append(c1!1, c2!1))=car(c1!1)" )"1" "cdr(append(c1!1, c2!1))=append(cdr(c1!1),c2!1)" )"1" case "PUSH?(car(c1!1))" )"1" (assert ) nil nil )"2" case "FETCH?(car(c1!1))" )"1" (assert ) nil nil )"2" case "UNARY?(car(c1!1))" )"1" assert )"1" expand "check1" )"1" "null?(e!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" case "BINARY?(car(c1!1))" )"1" assert )"1" expand "check2" )"1" "null?(e!1)" )"1" "null?(cdr(e!1))" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "STORE?(car(c1!1))" )"1" assert )"1" expand "check1" )"1" "null?(e!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" case "NOOP?(car(c1!1))" )"1" assert )nil nil )"2" case "BRANCH?(car(c1!1))" )"1" assert )"1" expand "check1" )"1" "null?(e!1)" )"1" assert )"1" "top(e!1) = 1" )"1" assert )"1" "1" rewrite "append_assoc" )nil nil ))nil ))nil )"2" assert )"2" rewrite "append_assoc" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "LOOP?(car(c1!1))" )"1" assert )"1" "IB" "BRANCH(append(c4(car(c1!1)), LOOP ") "1" rewrite "append_assoc" )"1" "IBR" "BRANCH(append(c4(car(c1!1)), LOOP (c3(car(c1!1)), c4(car(c1!1))),") "1" expand "append" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "append" 1 1)"2" (propax) nil nil ))nil ))nil ))nil )"2" "2" expand "append" 1 1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"[list -> boolean]" list_adt nil )"[(cons?) -> T]" list_adt nil )"[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"bool" am nil )"[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"[(BRANCH?) -> list[Instruction]]" nil )"[(BRANCH?) -> list[Instruction]]" nil )nil list_props nil )"int" am nil )"(NOOP?)" Instruction nil )"[[list[Instruction], list[Instruction]] -> (BRANCH?)]" nil )"[(LOOP?) -> list[Instruction]]" Instructionnil )"[[T, list] -> (cons?)]" list_adt nil )LOOP adt-constructor-decl"[[list[Instruction], list[Instruction]] -> (LOOP?)]" Instructionnil )"[(LOOP?) -> list[Instruction]]" Instructionnil )LOOP ? adt-recognizer-decl "[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"bool" am nil )"[Instruction -> boolean]" Instructionnil )"[Instruction -> boolean]" Instructionnil )"[(cons?) -> list]" list_adt nil )"posint" nil )"nonneg_int" nil )"Config" am nil )"boolean" notequal nil )nil am nil )"posint" nil )nil list_props_aux nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"list[T]" list_props nil )"bool" am nil )nil am nil )"[bool, bool -> bool]" booleans 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 )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 3398492510"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (inst - "s1!1" ) (("" (inst + "n!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans 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 )nil booleans nil )nil numbers nil )nil am nil )"bool" sets nil ))nil ))nil 3398744455"" (skosimp)"" (split)"1" (flatten)"1" (expand "M" )"1" (lift-if)"1" (assert )"1" (prop)"1" case "nonempty?({s1 | ") "1" "choose_member" "a" "{s1 | ")) "1" (split)"1" "CC" "choose({s1 | ") "1" (expand "member" )"1" (skosimp)"1" (inst + "n!1" )"1" rewrite "up_equal" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (hide -2 2)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (skosimp)"2" (inst - "s1!2" )"2" (inst + "n!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "M" )"2" (lift-if)"2" (assert )"2" (prop)"1" case "nonempty?({s1 | ") "1" "choose_member" "a" "{s1 | ")) "1" (split)"1" "CC" "choose({s1 | ") "1" (expand "member" )"1" (skosimp)"1" (decompose-equality)"1" "1" "1" "trich_lt" "x" "n!1" "y" "n!2" ))"1" "1" "tr_add" "k1" "n!1" "k2" "n!2-n!1" "cf0" "(c!1, null[int], s!1)" "cf2" "(null[Instruction], null[int], s1!1)" ))"1" replace -4)"1" "1" "1" "tr_eq" "k" "n!1" "cf0" "(c!1, null[int], s!1)" "cf1" "cf1!1" "cf2" "(null[Instruction], null[int], CC)" ))"1" assert )"1" expand "tr" -3)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" replace -1 * rl)"2" "2" "tr_eq" "k" "n!1" "cf0" "(c!1, null[int], s!1)" "cf1" "(null[Instruction], null[int], CC)" "cf2" "(null[Instruction], null[int], s1!1)" ))"2" (assert ) nil nil ))nil ))nil ))nil )"3" "tr_add" "k1" "n!2" "k2" "n!1-n!2" "cf0" "(c!1, null[int], s!1)" "cf2" "(null[Instruction], null[int],CC)" ))"1" assert )"1" "1" "tr_eq" "k" "n!2" "cf0" "(c!1, null[int], s!1)" "cf1" "cf1!1" "cf2" "(null[Instruction], null[int], s1!1)" ))"1" assert )"1" expand "tr" -3)"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "every" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (hide -2 2)"2" (skosimp)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "s1!2" )"2" (inst + "n!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) (("2" (inst + "n!1" "s1!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Cont" am nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"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 )nil naturalnumbers nil )"bool" reals nil )"bool" sets nil )set type-eq-decl nil sets nil )nil booleans 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 )nil booleans nil )nil numbers nil )nil am nil )"bool" sets nil )nil lift_props "orders/" )"(p)" sets nil )"[T, T -> boolean]" equalities nil )nil sets_lemmas nil )"bool" sets nil )"Code[V]" am nil )"State[V]" am nil )"[T -> (up?)]" lift_adt nil )"State[V]" am nil )nil lift_adt nil )nil lift_adt nil )"boolean" lift_adt nil )"[lift -> boolean]" lift_adt nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil am nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil am nil )"int" integers nil )"int" integers nil )nil real_props nil ))
Messung V0.5 in Prozent C=100 H=99 G=99
¤ Dauer der Verarbeitung: 0.58 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
