Quelle compiler.prf
Sprache: Lisp
(compilernil 3398403700 ("" (grind) nil nil )nil compiler nil )"(strict_well_founded?[AExp])" AExp nil ))nil ))nil 3398403700 ("" (grind) nil nil )nil compiler nil )"(strict_well_founded?[AExp])" AExp nil ))nil ))nil 3398403700 ("" (grind) nil nil )nil compiler nil )"(strict_well_founded?[AExp])" AExp nil ))nil ))nil 3398403700 ("" (grind) nil nil )nil compiler nil )"(strict_well_founded?[AExp])" AExp nil ))nil ))nil 3398403700 ("" (grind) nil nil )nil compiler nil )"(strict_well_founded?[AExp])" AExp nil ))nil ))nil 3398403700 ("" (grind) nil nil )nil compiler nil )"(strict_well_founded?[AExp])" AExp nil ))nil ))nil 3399357896 ("" (termination-tcc) nil nil )nil compiler nil )"(strict_well_founded?[BExp])" BExp nil ))nil ))nil 3399357896 ("" (termination-tcc) nil nil )nil compiler nil )"(strict_well_founded?[BExp])" BExp nil ))nil ))nil 3399357896 ("" (termination-tcc) nil nil )nil compiler nil )"(strict_well_founded?[BExp])" BExp nil ))nil ))nil 3399357896 ("" (termination-tcc) nil nil )nil compiler nil )"(strict_well_founded?[Stm])" Stm nil ))nil ))nil 3399357896 ("" (termination-tcc) nil nil )nil compiler nil )"(strict_well_founded?[Stm])" Stm nil ))nil ))nil 3399357896 ("" (termination-tcc) nil nil )nil compiler nil )"(strict_well_founded?[Stm])" Stm nil ))nil ))nil 3399357896 ("" (termination-tcc) nil nil )nil compiler nil )"(strict_well_founded?[Stm])" Stm nil ))nil ))nil 3399357896 ("" (termination-tcc) nil nil )nil compiler nil )"(strict_well_founded?[Stm])" Stm nil ))nil ))nil 3399363243"" (induct "a" )"1" (expand "CA" ) (("1" (propax) nil nil )) nil )"2" (expand "CA" ) (("2" (propax) nil nil )) nil )"3" (skosimp*)"3" (expand "CA" -1)"3" "append_is_null" "l1" "CA(Add2_var!1)" "l2" "append(CA(Add1_var!1), LAMBDA (i, j:int): i + j), null[Instruction]))")) "3" (assert ) nil nil )) nil ))nil ))nil )"4" (skosimp)"4" "append_is_null" "l1" "CA(Sub2_var!1)" "l2" "append(CA(Sub1_var!1), LAMBDA (i, j:int): i - j), null[Instruction]))")) "4" (expand "CA" -2) (("4" (assert ) nil nil )) nil )) nil ))nil )"5" (skosimp*)"5" "append_is_null" "l1" "CA(Mul2_var!1)" "l2" "append(CA(Mul1_var!1), LAMBDA (i, j:int): i * j), null[Instruction]))")) "5" (expand "CA" -2) (("5" (assert ) nil nil )) nil )) nil ))nil ))nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"(null?)" list_adt nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[[[int, int] -> int] -> (BINARY?)]" nil )"[Instruction -> boolean]" Instructionnil )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 numbers nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"list[T]" list_props nil )nil list_props_aux nil )"int" integers nil )nil AExp nil )nil compiler nil )"Code" compiler nil )nil Instruction nil )"[list -> boolean]" list_adt nil )nil list_adt nil )nil Instruction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil AExp nil ))nil 3399363470"" (induct "b" )"1" (expand "CB" ) (("1" (propax) nil nil )) nil )"2" (expand "CB" ) (("2" (propax) nil nil )) nil )"3" (skosimp*)"3" (expand "CB" )"3" (lemma "nonnull_CA" ("a" "Eq2_var!1" ))"3" "append_is_null" "l1" "CA(Eq2_var!1)" "l2" "append(CA(Eq1_var!1), LAMBDA (i, j:int): b2n(i = j)), null[Instruction]))")) "3" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (skosimp*)"4" (expand "CB" )"4" "append_is_null" "l1" "CA(Le2_var!1)" "l2" "append(CA(Le1_var!1), LAMBDA (i, j:int): b2n(i <= j)), null[Instruction]))")) "4" (lemma "nonnull_CA" ("a" "Le2_var!1" ))"4" (assert ) nil nil )) nil ))nil ))nil ))nil )"5" (skolem + "b!1" )"5" (flatten)"5" (expand "CB" -1)"5" "append_is_null" "l1" "CB(b!1)" "l2" "cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])" ))"5" (assert ) nil nil )) nil ))nil ))nil ))nil )"6" (skolem + ("b!1" "b!2" ))"6" (flatten)"6" (expand "CB" -1)"6" "append_is_null" "l1" "CB(b!2)" "l2" "append(CB(b!1), cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction]))" ))"6" "append_is_null" "l1" "CB(b!1)" "l2" "cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction])" ))"6" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"[Instruction -> boolean]" Instructionnil )"[[int -> int] -> (UNARY?)]" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil compiler nil )nil AExp nil )nil list_props_aux nil )"Code" compiler nil )"list[T]" list_props nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )nil numbers 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 )"[Instruction -> boolean]" Instructionnil )"[[[int, int] -> int] -> (BINARY?)]" nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (nbit type-eq-decl nil bit nil )"nbit" bit nil )"[T, T -> boolean]" equalities nil )"(null?)" list_adt nil )nil BExp nil )nil compiler nil )"Code" compiler nil )nil Instruction nil )"[list -> boolean]" list_adt nil )nil list_adt nil )nil Instruction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil BExp nil ))nil 3399357897"" (induct "S" )"1" (expand "CS" )"1" (skolem + ("x!1" "a!1" ))"1" "append_is_null" "l1" "CA(a!1)" "l2" "cons(STORE(x!1), null[Instruction])" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand "CS" ) (("2" (propax) nil nil )) nil )"3" (skolem + ("S!1" "S!2" ))"3" (flatten)"3" (expand "CS" -1)"3" "append_is_null" ("l1" "CS(S!1)" "l2" "CS(S!2)" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (skolem + ("b!1" "S!1" "S!2" ))"4" (flatten)"4" (expand "CS" -1)"4" "append_is_null" "l1" "CB(b!1)" "l2" "cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction])" ))"4" (assert ) nil nil )) nil ))nil ))nil ))nil )"5" (skolem + ("b!1" "S!1" ))"5" (flatten)"5" (expand "CS" -1) (("5" (propax) nil nil )) nil )) nil ))nil ))nil )nil BExp nil ) (CB def-decl "Code" compiler nil )"[Instruction -> boolean]" Instructionnil )"[[list[Instruction], list[Instruction]] -> (BRANCH?)]" nil )"(null?)" list_adt nil )"[V -> (STORE?)]" Instruction nil )"[Instruction -> boolean]" Instructionnil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"Code" compiler nil ) (AExp type-decl nil AExp nil )nil list_props_aux nil )nil Stm nil )nil compiler nil )"Code" compiler nil )nil Instruction nil )"[list -> boolean]" list_adt nil )nil list_adt nil )nil Instruction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil Stm nil ))quality 98%
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
