Quelle axiomatic.prf
Sprache: Lisp
(axiomaticnil 3399608346 ("" (termination-tcc) nil nil )"Stm" axiomatic nil )) nil ))nil 3399608346 ("" (subtype-tcc) nil nil )"Stm" axiomatic nil )) nil ))nil 3399608346 ("" (termination-tcc) nil nil )"(strict_well_founded?[tree])" axiomatic nil )"Stm" axiomatic nil ))nil ))nil 3399608883 ("" (termination-tcc) nil nil )"(strict_well_founded?[tree])" axiomatic nil )"Stm" axiomatic nil ))nil ))nil 3399608883 ("" (subtype-tcc) nil nil )"Stm" axiomatic nil )) nil ))nil 3399608883 ("" (subtype-tcc) nil nil )"Stm" axiomatic nil )) nil ))nil 3399608883 ("" (termination-tcc) nil nil )"(strict_well_founded?[tree])" axiomatic nil )"Stm" axiomatic nil ))nil ))nil 3399608883 ("" (termination-tcc) nil nil )"(strict_well_founded?[tree])" axiomatic nil )"Stm" axiomatic nil ))nil ))nil 3399608883 ("" (subtype-tcc) nil nil )"Stm" axiomatic nil )) nil ))nil 3399608883"" (termination-tcc) nil nil )"(strict_well_founded?[tree])" axiomatic nil )"Stm" axiomatic nil ))nil ))nil 3399608883 ("" (subtype-tcc) nil nil )"Stm" axiomatic nil )) nil ))nil 3399608883"" (termination-tcc) nil nil )"(strict_well_founded?[tree])" axiomatic nil ))nil ))nil 3399608346"" (expand "inference_tree?" )"" (expand "S" )"" (expand "P" ) (("" (expand "Q" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil )"Stm" axiomatic nil )"Predicate" axiomatic nil )"Predicate" axiomatic nil )"bool" axiomatic nil ))nil ))nil 3399619747"" (skosimp)"" (expand "wlp" )"" (expand "|=" )"" (skosimp*)"" (inst - "s1!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" axiomatic 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 axiomatic nil )"bool" axiomatic nil ))nil 3399619791"" (skosimp*)"" (expand "|>" )"" (skosimp)"" (expand "|=" )"" (expand "wlp" )"" (skosimp)"" (inst - "s!1" "s1!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" axiomatic nil )"bool" axiomatic 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 axiomatic nil )"bool" axiomatic nil ))nil 3399608945"" (expand "|-" )"" (case "forall (t:inference_tree): |=(H(t))" )"1" (skosimp)"1" (skosimp)"1" (inst - "t!1" )"1" (replace -2) (("1" (propax) nil nil )) nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "t" )"1" (typepred "t!1" ) (("1" (propax) nil nil )) nil )"2" (skolem + ("HH" ))"2" (flatten)"2" (expand "|=" )"2" (skosimp)"2" (expand "H" )"2" (expand "inference_tree?" )"2" (flatten)"2" (expand "assign" )"2" (expand "Q" )"2" (expand "P" )"2" expand "S" )"2" replace -2 -3 rl)"2" assert )"2" "2" rewrite "SS_deterministic" "2" "2" expand "tr" )"2" expand "step" )"2" expand "tr" )"2" "2" "2" replace -1)"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 )"3" (skolem + ("HH" ))"3" (flatten)"3" (expand "|=" )"3" (skosimp)"3" (expand "inference_tree?" )"3" (flatten)"3" (expand "H" )"3" (expand "Q" )"3" (expand "P" )"3" rewrite "SS_deterministic" -4 :dir rl)"3" "3" expand "tr" )"3" expand "step" )"3" assert )"3" expand "S" )"3" assert )"3" expand "tr" )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skolem + ("HH" "T1" "T2" ))"4" (flatten)"4" (expand "inference_tree?" -3)"4" (flatten)"4" (expand "H" 1)"4" (expand "|=" )"4" (skosimp)"4" (replace -6)"4" (replace -7)"4" (hide -6 -7)"4" expand "S" (-4 -5))"4" expand "P" )"4" expand "Q" )"4" replace -6)"4" rewrite "SS_deterministic" "4" "4" expand "S" )"4" "tr_split" "k" "n!1" "S1" "S1(HH`2)" "S2" "S2(HH`2)" "s0" "s!1" "s2" "s1!1" ))"4" "Sequence(S1(HH`2), S2(HH`2))=HH`2" )"1" assert )"1" "1" replace -8)"1" replace -9)"1" replace -11)"1" replace "1" "1" "s!1" "s1!2" )"1" replace "1" "1" "s1!2" "s1!1" )"1" replace "1" "1" nil nil )"2" rewrite "SS_deterministic" "2" "k2!1" )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "SS_deterministic" "2" "k1!1" )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 )"5" (skolem + ("HH" "T1" "T2" ))"5" (flatten)"5" (expand "inference_tree?" -3)"5" (flatten)"5" (assert )"5" (expand "S" )"5" (expand "P" )"5" (expand "Q" )"5" (expand "|=" )"5" (expand "H" 1)"5" "5" rewrite "SS_deterministic" "5" "5" replace -8)"5" replace -9)"5" replace -10)"5" replace -11)"5" "5" "s!1" "s1!1" )"5" "s!1" "s1!1" )"5" expand "&" )"5" replace -6)"5" expand "~" )"5" "B(b(HH`2))(s!1)" )"1" "1" nil nil )"2" rewrite "SS_deterministic" "2" "n!1-1" )"1" expand "tr" "1" expand "step" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" expand "tr" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "1" nil nil )"2" rewrite "SS_deterministic" "2" "n!1-1" )"1" expand "tr" "1" expand "step" )"1" assert )nil nil ))nil ))nil )"2" expand "tr" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" 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 )"6" (assert )"6" (skolem + ("HH" "T1" ))"6" (flatten)"6" (copy -2)"6" (expand "inference_tree?" -1)"6" (flatten)"6" (assert )"6" (expand "H" 1)"6" (expand "|=" )"6" (skosimp)"6" expand "S" )"6" expand "P" )"6" expand "Q" )"6" rewrite "SS_deterministic" "6" "6" replace -3)"6" replace -4)"6" replace -5)"6" "6" expand "&" )"6" expand "~" )"6" "NAT_induction" "p" "lambda (k: nat): FORALL (x, y: State): AND tr(k)(I(HH`2, x), T(y)) => NOT B(b(HH`2))(y) AND HH`1(y)")) "1" "1" "n!1" )"1" "s!1" "s1!1" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" expand "tr" "2" expand "step" "2" assert )"2" "j!1=0" )"2" assert )"2" expand "tr" "2" expand "step" "2" "j!1 - 1 = 0" )"2" assert )"2" "B(b(HH`2))(x!1)" )"1" "tr_split" "k" "j!1-2" "S1" "S1(HH`2)" "S2" "HH`2" "s0" "x!1" "s2" "y!1" ))"1" assert )"1" "1" "k2!1" )"1" assert )"1" "s1!2" "y!1" )"1" replace "1" "x!1" "s1!2" )"1" replace "1" replace "1" "1" replace "1" nil nil ))nil )"2" rewrite "SS_deterministic" "2" "k1!1" )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "tr" "2" expand "step" "2" expand "tr" "2" "1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (skolem + ("HH" "T1" ))"7" (flatten)"7" (expand "|=" )"7" (skosimp)"7" (expand "H" -3)"7" (expand "H" -4)"7" (expand "H" 1)"7" (expand "inference_tree?" -2)"7" (flatten)"7" (replace -2)"7" "s!1" "s1!1" )"7" expand "S" )"7" replace -3 * rl)"7" expand "P" )"7" expand "Q" )"7" assert )"7" expand "|>" )"7" "s!1" )"7" assert )"7" assert )"7" "s1!1" )"7" 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 )"Hoare" axiomatic nil )nil axiomatic nil )"bool" axiomatic nil ) (Stm type-decl nil Stm nil )nil axiomatic 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 numbers nil )nil axiomatic nil )nil axiomatic nil )"bool" axiomatic nil )nil booleans nil )nil booleans nil )nil axiomatic nil )"[bool, bool -> bool]" booleans nil )nil axiomatic nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" axiomatic nil )"Predicate" axiomatic nil )"[Config]" sos nil )"[T, T -> boolean]" equalities nil )nil sos nil )"[Config -> boolean]" sos nil )"[(T?) -> State[V]]" sos nil )"[State[V] -> (T?)]" sos nil )"State" State nil )"[Stm -> boolean]" Stm nil )"[(Assign?) -> V]" Stm nil )nil AExp nil )"[State -> int]" AExp nil )"[(Assign?) -> AExp[V]]" Stm nil )"bool" sos nil )nil sos nil )"Stm" axiomatic nil )"Predicate" axiomatic nil )nil sos nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[Stm -> boolean]" Stm nil )"[Stm -> boolean]" Stm nil )"[Stm -> boolean]" Stm nil )"[{x: Stm | Sequence?(x) OR Conditional?(x) OR While?(x)} -> Stm]" nil )"[{x: Stm | Sequence?(x) OR Conditional?(x)} -> Stm]" Stm nil )"bool" reals nil )nil naturalnumbers nil )nil Stm nil )"Hoare" axiomatic nil )"[[Stm, Stm] -> (Sequence?)]" Stmnil )"[{x: Stm | Conditional?(x) OR While?(x)} -> BExp[V]]" Stm nil )"[State -> bool]" BExp nil )nil BExp nil )"nat" axiomatic nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )"bool" axiomatic nil )"bool" axiomatic nil )"[[Stm[V], State[V]] -> (I?)]" sos nil )"[Config -> boolean]" sos nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"bool" axiomatic nil )"bool" axiomatic nil ))nil 3399619607"" (case "FORALL (Q: Predicate, S: Stm): |-(wlp(S,Q), S, Q)" )"1" (skosimp)"1" (inst - "Q!1" "S!1" )"1" (lemma "wlp_is_weakest" ("P" "P!1" "S" "S!1" "Q" "Q!1" ))"1" (assert )"1" (hide -3)"1" (expand "|-" )"1" (skosimp)"1" (inst + "cons((P!1, S!1, Q!1),t!1)" )"1" (expand "H" 1) (("1" (propax) nil nil )) nil )"2" (typepred "t!1" )"2" (expand "inference_tree?" 1)"2" (replace -3)"2" (expand "S" )"2" (expand "P" )"2" expand "Q" )"2" expand "|>" )"2" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "S" )"1" (skolem + ("x!1" "a!1" ))"1" (skosimp)"1" (expand "|-" )"1" "ass((wlp(Assign(x!1, a!1), Q!1), Assign(x!1, a!1), Q!1))" )"1" (expand "H" ) (("1" (propax) nil nil )) nil )"2" (expand "inference_tree?" )"2" (assert )"2" (expand "S" )"2" (expand "Q" )"2" (expand "P" )"2" (expand "wlp" )"2" (apply-extensionality :hide? t)"2" "assign(x!1, a!1)(Q!1)(x!2)" )"1" "1" rewrite "SS_deterministic" "1" "1" expand "tr" )"1" expand "step" )"1" expand "tr" )"1" "1" "1" expand "assign" -3)"1" replace -1)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" assert )"2" expand "assign" 1)"2" "assign(x!1, A(a!1))(x!2)" )"2" assert )"2" rewrite "SS_deterministic" "2" "1" )"2" expand "tr" )"2" expand "step" )"2" expand "tr" )"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 )"2" (skosimp)"2" (expand "|-" )"2" (inst + "skip((wlp(Skip, Q!1), Skip, Q!1))" )"1" (expand "H" ) (("1" (propax) nil nil )) nil )"2" (expand "inference_tree?" )"2" (expand "S" )"2" (expand "P" )"2" (expand "Q" )"2" (expand "wlp" )"2" (apply-extensionality :hide? t)"2" (case-replace "Q!1(x!1)" )"1" (skosimp)"1" rewrite "SS_deterministic" * :dir rl)"1" "1" expand "tr" )"1" expand "step" )"1" expand "tr" )"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "x!1" )"2" "1" (propax) nil nil )"2" rewrite "SS_deterministic" "2" "1" )"2" expand "tr" )"2" expand "step" )"2" expand "tr" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem + ("S!1" "S!2" ))"3" (skosimp*)"3" (expand "|-" )"3" (inst - "wlp(S!2,Q!1)" )"3" (inst - "Q!1" )"3" (skosimp*)"3" "cons((wlp(Sequence(S!1, S!2), Q!1), Sequence(S!1, S!2), Q!1),comp((wlp(S!1, wlp(S!2, Q!1)), Sequence(S!1, S!2), Q!1),t!1,t!2))" )"1" (expand "H" ) (("1" (propax) nil nil )) nil )"2" (expand "inference_tree?" )"2" (expand "inference_tree?" )"2" (expand "S" )"2" (replace -1)"2" replace -2)"2" "2" assert )"2" expand "P" )"2" expand "Q" )"2" expand "H" )"2" "1" expand "|>" )"1" "1" expand "wlp" 1 1)"1" "1" expand "wlp" )"1" "1" "s1!2" )"1" assert )"1" "1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" "1" "tr_partial" "k" "n!1" "S1" "S!1" "S2" "S!2" "s0" "s!1" "s1" "s1!1" ))"1" assert )"1" "n!1+n!2" )"1" "tr_add" "k1" "n!1" "k2" "n!2" "c0" "sos.I(Sequence(S!1, S!2), s!1)" "c2" "T(s1!2)" ))"1" replace "1" "1" "sos.I(S!2, s1!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "|>" )"2" (skosimp) 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" (expand "|-" )"4" (inst - "Q!1" )"4" (inst - "Q!1" )"4" (skosimp*)"4" "PP" "lambda s: (B(b!1)(s) AND wlp(S!1, Q!1)(s)) OR ((NOT B(b!1)(s)) AND wlp(S!2, Q!1)(s))" )"4" "cons((wlp(Conditional(b!1, S!1, S!2), Q!1), Conditional(b!1, S!1, S!2), s((~B(b!1) & PP,S!2, Q!1),t!2)))") "1" (expand "H" ) (("1" (propax) nil nil ))nil )"2" (expand "inference_tree?" )"2" (expand "inference_tree?" )"2" (expand "inference_tree?" )"2" expand "S" )"2" replace -2)"2" replace -3)"2" "2" "2" expand "PP" )"2" expand "H" )"2" expand "Q" )"2" expand "&" )"2" expand "P" )"2" expand "|>" )"2" "1" "1" assert )nil nil ))nil )"2" nil nil )"3" "3" assert )"3" expand "~" )"3" assert )nil nil ))nil ))nil ))nil )"4" nil nil )"5" "5" expand "wlp" )"5" "B(b!1)(s!1)" )"1" "1" "s1!1" )"1" assert )"1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" "1" "n!1+1" )"1" expand "tr" "1" expand "step" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "2" "s1!1" )"2" assert )"2" rewrite "SS_deterministic" "2" rewrite "SS_deterministic" "2" "2" "n!1+1" )"2" expand "tr" "2" expand "step" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" 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" "S!1" ))"5" (skosimp*)"5" (name-replace "PP" "wlp(While(b!1, S!1),Q!1)" )"5" (case "(~B(b!1)&PP) |> Q!1" )"1" (case "(B(b!1)&PP) |> wlp(S!1, PP)" )"1" (inst - "PP" )"1" (expand "|-" )"1" (skosimp)"1" "cons((PP, While(b!1, S!1), Q!1),while((PP,While(b!1, S!1),~B(b!1) & PP),cons((B(b!1) & PP, S!1, PP),t!1)))" )"1" (expand "H" 1) (("1" (propax) nil nil ))nil )"2" (expand "inference_tree?" )"2" (expand "inference_tree?" )"2" expand "inference_tree?" )"2" expand "S" )"2" expand "P" )"2" expand "Q" )"2" replace -3)"2" assert )"2" expand "H" 1 1)"2" expand "H" 1 1)"2" expand "H" 1 1)"2" expand "H" 1 1)"2" expand "H" 1 1)"2" expand "H" 1 1)"2" assert )"2" expand "|>" "2" "1" 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 )"2" (hide 2)"2" (expand "PP" )"2" (expand "&" )"2" (expand "~" )"2" (expand "|>" )"2" (skosimp*)"2" expand "wlp" 1 1)"2" "2" expand "wlp" 1)"2" "2" rewrite "SS_deterministic" "2" rewrite "SS_deterministic" "2" "2" expand "wlp" )"2" "s1!2" )"2" "1" nil nil )"2" rewrite "SS_deterministic" "2" expand "tr" 1)"2" expand "step" )"2" "2" expand "tr" "2" expand "step" )"2" assert )"2" "n!1+n!2+2" )"2" assert )"2" "tr_partial" "k" "n!1" "S1" "S!1" "S2" "While(b!1, S!1)" "s0" "s!1" "s1" "s1!1" ))"2" assert )"2" "tr_add" "k1" "n!1" "k2" "n!2" "c0" "sos.I(Sequence(S!1, While(b!1, S!1)), s!1)" "c2" "T(s1!2)" ))"2" replace "2" "2" "sos.I(While(b!1, S!1), s1!1)" )"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 )"2" (hide 2)"2" (expand "|>" )"2" (expand "&" )"2" (expand "~" )"2" (skosimp)"2" (expand "PP" )"2" (expand "wlp" )"2" "s!1" )"2" assert )"2" rewrite "SS_deterministic" "2" "3" )"2" expand "tr" )"2" expand "step" )"2" expand "tr" )"2" expand "step" )"2" expand "tr" )"2" expand "step" )"2" expand "tr" )"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 )"[Stm -> boolean]" Stm nil )"[[BExp[V], Stm] -> (While?)]" Stm nil )"inference_tree" axiomatic nil )"[[Hoare, tree] -> (while?)]" axiomaticnil )"[tree -> boolean]" axiomatic nil )"Predicate" axiomatic nil )"Stm[V]" axiomatic nil )"BExp[V]" axiomatic nil )"[State[V] -> bool]" axiomatic nil )"posint" nil )"[State -> bool]" BExp nil )nil BExp nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"posint" nil )"[Stm -> boolean]" Stm nil )"[[BExp[V], Stm, Stm] -> (Conditional?)]" Stm nil )"BExp[V]" axiomatic nil )"Stm[V]" axiomatic nil )"Stm[V]" axiomatic nil )"Predicate" axiomatic nil )"[tree -> boolean]" axiomatic nil )"[[Hoare, tree, tree] -> (iif?)]" nil )"[State[V] -> boolean]" axiomatic nil )"bool" axiomatic nil )"inference_tree" axiomatic nil )"bool" axiomatic nil )"inference_tree" axiomatic nil )"inference_tree" axiomatic nil )"inference_tree" axiomatic nil )"[[Hoare, tree, tree] -> (comp?)]" nil )"[tree -> boolean]" axiomatic nil )"Predicate" axiomatic nil )"Stm[V]" axiomatic nil )"Stm[V]" axiomatic nil )"[[Stm, Stm] -> (Sequence?)]" Stmnil )"[Stm -> boolean]" Stm nil )nil sos nil )"[Config -> boolean]" sos nil )"[[Stm[V], State[V]] -> (I?)]" sos nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )nil sos nil )"Predicate" axiomatic nil )"(Skip?)" Stm nil )"[Stm -> boolean]" Stm nil )"[Hoare -> (skip?)]" axiomatic nil )"[tree -> boolean]" axiomatic nil )"int" integers nil )"bool" axiomatic nil )"[bool, bool -> bool]" booleans nil )nil lift_adt nil )"[T, T -> boolean]" equalities nil )nil Cont nil )"Cont" sos nil )"[lift -> boolean]" lift_adt nil )"[T -> (up?)]" lift_adt nil )nil naturalnumbers nil )"bool" reals nil ) (step def-decl "[Config]" sos nil )nil sos nil )"[Config -> boolean]" sos nil )"[(T?) -> State[V]]" sos nil )"[State[V] -> (T?)]" sos nil )"State" State nil )"[State -> int]" AExp nil ) (tr def-decl "bool" sos nil )nil sos nil )"[tree -> boolean]" axiomatic nil )"[Hoare -> (ass?)]" axiomatic nil )nil AExp nil )"[Stm -> boolean]" Stm nil )"[[V, AExp[V]] -> (Assign?)]" Stm nil )"V" axiomatic nil )"AExp[V]" axiomatic nil )"Predicate" axiomatic nil )nil Stm nil )nil axiomatic nil )NOT const-decl "[bool -> bool]" booleans nil )"Predicate" axiomatic nil )"bool" axiomatic nil )"Predicate" axiomatic nil )"Stm" axiomatic nil )"Hoare" axiomatic nil )nil axiomatic nil )"bool" axiomatic nil )"[tree -> boolean]" axiomatic nil )"[[Hoare, tree] -> (cons?)]" axiomaticnil )"Predicate" axiomatic nil )"Stm[V]" axiomatic nil )"Predicate" axiomatic nil )nil axiomatic nil )"inference_tree" axiomatic nil )nil axiomatic 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 State nil )nil booleans nil )nil axiomatic nil )nil Stm nil ) (\|- const-decl "bool" axiomatic nil )"bool" axiomatic nil ))nil 3399627948"" (skosimp)"" (split)"1" (flatten)"1" (lemma "completeness" ("P" "P!1" "Q" "Q!1" "S" "S!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (flatten)"2" (lemma "soundness" ("P" "P!1" "Q" "Q!1" "S" "S!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil Stm nil )nil axiomatic 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 axiomatic nil )nil axiomatic nil )nil axiomatic nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.60 Sekunden
(vorverarbeitet am 2026-05-01)
¤ *© Formatika GbR, Deutschland
2026-05-26
