Quelle natural.prf
Sprache: Lisp
(naturalnil 3400243711 ("" (termination-tcc) nil nil )"(strict_well_founded?[tree])" natural nil )) nil ))nil 3400243711 ("" (termination-tcc) nil nil )"(strict_well_founded?[tree])" natural nil )) nil ))nil 3400243711 ("" (termination-tcc) nil nil )"(strict_well_founded?[tree])" natural nil )) nil ))nil 3400238483 ("" (subtype-tcc) nil nil )"Stm" natural nil )"State" natural nil )"State" natural nil )nil natural nil )"State" State nil ))nil ))nil 3400238483"" (termination-tcc) nil nil ) ((S const-decl "Stm" natural nil ))nil ))nil 3400238483"" (termination-tcc) nil nil )"Stm" natural nil ) (S const-decl "Stm" natural nil ))nil ))nil 3400238483 ("" (subtype-tcc) nil nil )"Stm" natural nil ) (S const-decl "Stm" natural nil )"State" natural nil )"State" natural nil )"State" natural nil )"State" natural nil ))nil ))nil 3400238483 ("" (subtype-tcc) nil nil )"State" natural nil )"State" natural nil )"State" natural nil )"State" natural nil )"Stm" natural nil ))nil ))nil 3400238483 ("" (subtype-tcc) nil nil )"Stm" natural nil )"State" natural nil )"Stm" natural nil )"State" natural nil )"State" natural nil )"State" natural nil ))nil ))nil 3400238483"" (expand "derivation_tree?" )"" (expand "S" )"" (expand "s1" )"" (expand "s0" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )"Stm" natural nil )"State" natural nil )"State" natural nil )"bool" natural nil ))nil ))nil 3400238504"" case "FORALL (d1, d2: derivation_tree,n:nat): depth(d1)<=n&depth(d2)<=n& AND s0(d1) = s0(d2) => d1 = d2") "1" (skosimp)"1" (inst - "d1!1" "d2!1" "max(depth(d1!1),depth(d2!1))" )"1" (expand "max" )"1" (case-replace "depth(d1!1) < depth(d2!1)" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skosimp)"1" (case "leaf?(d1!1)" )"1" (case "leaf?(d2!1)" )"1" (hide -3 -4)"1" (typepred "d1!1" )"1" (typepred "d2!1" )"1" (expand "derivation_tree?" )"1" (assert )"1" (expand "S" )"1" (expand "S" )"1" (expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" case "d1!1=leaf((d(d1!1)`1,d(d1!1)`2,d(d1!1)`3))" )"1" replace -1 1)"1" case "d2!1=leaf((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3))" )"1" replace -1 1)"1" "1" "Assign?(d(d2!1)`1)" )"1" (assert ) nil nil )"2" assert )"2" "Skip?(d(d2!1)`1)" )"1" assert )nil nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 2)"2" (typepred "d1!1" )"2" (typepred "d2!1" )"2" (expand "derivation_tree?" )"2" (assert )"2" (split -2)"1" (flatten)"1" (assert )"1" expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "S" )"2" expand "S" )"2" expand "s0" )"2" expand "s0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (flatten)"3" (expand "S" )"3" expand "S" )"3" expand "s0" )"3" expand "s0" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (expand "depth" )"2" (lift-if)"2" (assert )"2" (typepred "depth(t1(d1!1))" )"1" (typepred "depth(t2(d1!1))" )"1" (assert )"1" (expand "max" )"1" "depth(t1(d1!1)) < depth(t2(d1!1))" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem + ("n!1" ))"2" (skosimp*)"2" (expand "S" )"2" (expand "S" )"2" (expand "s0" )"2" (expand "s0" )"2" (case "branch1?(d1!1)" )"1" (case "branch1?(d2!1)" )"1" (typepred "d1!1" )"1" (typepred "d2!1" )"1" (expand "derivation_tree?" )"1" assert )"1" "1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" expand "S" )"1" expand "S" )"1" "B(b(d(d1!1)`1))(d(d1!1)`2)" )"1" assert )"1" "t1(d1!1)" "t1(d2!1)" )"1" expand "depth" "1" assert )"1" case "d1!1=branch1((d(d1!1)`1,d(d1!1)`2,d(d1!1)`3),t1(d1!1))" )"1" replace "1" case "d2!1=branch1((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3),t1(d2!1))" )"1" replace "1" assert )nil nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "t1(d1!1)" "t1(d2!1)" )"2" expand "depth" "2" assert )"2" case "d1!1=branch1((d(d1!1)`1,d(d1!1)`2,d(d1!1)`3),t1(d1!1))" )"1" replace "1" case "d2!1=branch1((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3),t1(d2!1))" )"1" replace "1" assert )nil nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 -5 -6 1))"2" (typepred "d1!1" )"2" (typepred "d2!1" )"2" expand "derivation_tree?" )"2" assert )"2" "2" assert )"2" expand "S" )"2" expand "s1" )"2" expand "s0" )"2" expand "s1" )"2" expand "s0" )"2" expand "S" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "leaf?(d1!1)" )"1" (inst - "d1!1" "d2!1" )"1" (assert )"1" (expand "depth" )"1" assert )"1" "leaf?(d2!1)" )"1" (assert ) nil nil )"2" "branch1?(d2!1)" )"1" assert )"1" "d1!1" )"1" "d2!1" )"1" expand "derivation_tree?" )"1" assert )"1" "1" assert )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" expand "S" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "d1!1" )"2" "d2!1" )"2" expand "derivation_tree?" )"2" assert )"2" expand "S" )"2" expand "s1" )"2" expand "s1" )"2" expand "s0" )"2" expand "s0" )"2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "branch2?(d1!1)" )"1" (hide 1 2)"1" (case "branch2?(d2!1)" )"1" case "d1!1=branch2((d(d1!1)`1,d(d1!1)`2,d(d1!1)`3),t1(d1!1),t2(d1!1))" )"1" replace -1 1)"1" "1" case "d2!1=branch2((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3),t1(d2!1),t2(d2!1))" )"1" replace -1 1)"1" "1" "d1!1" )"1" "d2!1" )"1" expand "derivation_tree?" )"1" "1" assert )"1" expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" " Sequence?(d(d1!1)`1)" )"1" assert )"1" "1" "t1(d1!1)" "t1(d2!1)" )"1" "t2(d1!1)" "t2(d2!1)" )"1" expand "depth" "1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "t1(d1!1)" "t1(d2!1)" )"2" "t2(d1!1)" "t2(d2!1)" )"2" expand "depth" "2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil )"3" (propax) nil nil )"4" (flatten) nil nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil )"3" (propax) nil nil )"4" (assert ) nil nil ))nil )"2" "d1!1" )"2" "d2!1" )"2" expand "derivation_tree?" )"2" assert )"2" expand "S" )"2" expand "S" )"2" expand "s1" )"2" expand "s1" )"2" expand "s0" )"2" expand "s0" )"2" assert )"2" "2" assert )"2" "2" assert )"2" "Sequence?(d(d1!1)`1)" )"1" assert )nil nil )"2" assert )"2" "2" assert )nil 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 )"[[[Stm[V], State[V], State[V]], tree] -> (branch1?)]" naturalnil )nil natural nil )nil BExp nil )"[State -> bool]" BExp nil )"[Stm -> boolean]" Stm nil )"[Stm -> boolean]" Stm nil )"[{x: Stm | Conditional?(x) OR While?(x)} -> BExp[V]]" Stm nil )"State" natural nil )"posint" nil )"[Stm -> boolean]" Stm nil )"derivation_tree" natural nil )"derivation_tree" natural nil )nil natural nil )"[[[Stm[V], State[V], State[V]], tree, tree] -> (branch2?)]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[tree -> boolean]" natural nil )"[tree -> boolean]" natural nil )"[{x: tree | branch1?(x) OR branch2?(x)} -> tree]" natural nil )"posint" nil )"(total_order?[real])" nil )"[(branch2?) -> tree]" natural nil )NOT const-decl "[bool -> bool]" booleans nil )"Stm" natural nil )"State" natural nil )"State" natural nil )nil natural nil )"[Stm -> boolean]" Stm nil )"[Stm -> boolean]" Stm nil )"[tree -> [Stm[V], State[V], State[V]]]" natural nil )"[[Stm[V], State[V], State[V]] -> (leaf?)]" natural nil )"[tree -> boolean]" natural nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )nil natural nil )nil booleans nil )nil booleans nil )"bool" natural nil )nil natural 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 )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (depth def-decl "nat" natural nil )nil natural nil )nil Stm nil )"[T, T -> boolean]" equalities nil )"Stm" natural nil )nil State nil )"State" natural nil ))nil 3400238483"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (inst - "s1(d!1)" )"" (inst + "d!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )nil natural nil )"bool" natural nil )nil booleans nil )"State" natural nil )nil natural 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 natural nil )"bool" sets nil ))nil ))nil 3400293675"" (skolem + ("S!1" "s0!1" "s1!1" ))"" (expand "SS" )"" (lift-if)"" (assert )"" (case-replace "EXISTS d: S(d) = S!1 AND s0(d) = s0!1" )"1" case "nonempty?({s1 | AND s0(d_1) = s0!1 AND s1(d_1) = s1})") "1" "choose_member" "a" "{s1 | AND s0(d_1) = s0!1 AND s1(d_1) = s1}")) "1" (split -1)"1" "CC" "choose({s1 | AND AND s1(d_1) = s1})") "1" (expand "member" )"1" (hide -2 -3)"1" (skosimp)"1" (split)"1" (skosimp*)"1" "dt_eq" ("d1" "d!1" "d2" "d!2" ))"1" (assert ) nil nil ))nil ))nil )"2" (flatten)"2" "d!1" )"2" rewrite "up_equal" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" ) (("2" (propax) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "s1(d!1)" )"2" (inst + "d!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" (skosimp)"2" (inst + "d!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Cont" natural nil )"State" natural nil )"bool" sets nil )set type-eq-decl nil sets nil ) (member const-decl "bool" sets nil )nil lift_props "orders/" )nil natural nil )"(p)" sets nil )nil sets_lemmas nil )"bool" sets nil )"State" natural 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 )"Stm" natural nil )"[T, T -> boolean]" equalities nil )nil Stm nil )nil natural nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil natural nil )"bool" natural nil )nil booleans nil )nil booleans nil )nil natural nil ))nil 3400294622"" (expand "sq_le" )"" case "forall (S:Stm,s1,s2:State,n:nat): (EXISTS d: depth(d) <= n &S(d) = S AND s0(d) = s1 AND s1(d) = s2)=>sos.SS(S)(s1) = up(s2)" )"1" (skosimp*)"1" (rewrite "SS_deterministic" * :dir rl)"1" (skosimp)"1" (inst - "S!1" "s1!1" "s2!1" "depth(d!1)" )"1" (split -1)"1" (propax) nil nil )"2" (inst + "d!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skosimp*)"1" (expand "depth" )"1" (lift-if)"1" (assert )"1" (prop)"1" (typepred "d!1" )"1" (expand "derivation_tree?" )"1" (assert )"1" (split)"1" (expand "S" )"1" expand "s1" )"1" expand "s0" )"1" expand "S" )"1" expand "s0" )"1" expand "s1" )"1" replace -3)"1" replace -4)"1" replace -5)"1" "1" rewrite "sos.SS_deterministic" "1" "1" )"1" expand "tr" )"1" expand "step" )"1" assert )"1" expand "tr" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "s0" )"2" expand "S" )"2" expand "S" )"2" expand "s0" )"2" expand "s1" )"2" expand "s1" )"2" replace -3)"2" replace -4)"2" replace -5)"2" "2" rewrite "sos.SS_deterministic" "2" "1" )"2" expand "tr" )"2" expand "step" )"2" expand "tr" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "S" )"3" expand "S" )"3" expand "s0" )"3" expand "s0" )"3" expand "s1" )"3" expand "s1" )"3" replace -3)"3" replace -4)"3" replace -5)"3" "3" rewrite "sos.SS_deterministic" "3" expand "tr" )"3" expand "step" )"3" assert )"3" expand "tr" )"3" expand "step" )"3" expand "tr" )"3" expand "step" )"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 ))nil ))nil ))nil ))nil ))nil )"2" (typepred "depth(t1(d!1))" )"2" (assert ) nil nil )) nil )"3" (typepred "depth(t1(d!1))" )"3" (expand "max" )"3" "depth(t1(d!1)) < depth(t2(d!1))" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem + ("n!1" ))"2" (skosimp*)"2" (case "leaf?(d!1)" )"1" (inst - "S!1" "s1!1" "s2!1" )"1" (split)"1" (propax) nil nil )"2" (inst + "d!1" )"2" (assert )"2" (expand "depth" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case "branch1?(d!1)" )"1" (typepred "d!1" )"1" (expand "derivation_tree?" )"1" (assert )"1" (flatten)"1" (expand "S" )"1" (expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" replace -9)"1" replace -10)"1" replace -11)"1" "1" rewrite "sos.SS_deterministic" "1" expand "tr" )"1" expand "step" )"1" assert )"1" expand "depth" "1" "B(b(S!1))(s1!1)" )"1" "S1(S!1)" "s1!1" "s2!1" )"1" "1" rewrite "sos.SS_deterministic" "1" "1" "n!2+1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "t1(d!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "S2(S!1)" "s1!1" "s2!1" )"2" "1" rewrite "sos.SS_deterministic" "1" "1" "n!2+1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "t1(d!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 )"2" (case "branch2?(d!1)" )"1" (typepred "d!1" )"1" (expand "derivation_tree?" )"1" (assert )"1" (flatten)"1" (hide 1 2)"1" expand "depth" -6)"1" expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" replace -7)"1" replace -8)"1" replace -9)"1" "Sequence?(S!1)" )"1" assert )"1" "1" "S1(S!1)" "s1!1" "d(t2(d!1))`2" )"1" "S2(S!1)" "d(t2(d!1))`2" "s2!1" )"1" "1" "1" rewrite "sos.SS_deterministic" "1" rewrite "sos.SS_deterministic" "1" rewrite "sos.SS_deterministic" "1" "1" "n!2+n!3" )"1" "tr_partial" "k" "n!2" "S1" "S1(S!1)" "s0" "s1!1" "s1" "d(t2(d!1))`2" "S2" "S2(S!1)" ))"1" assert )"1" "Sequence(S1(S!1), S2(S!1))=S!1" )"1" "1" "tr_add" "k1" "n!2" "k2" "n!3" "c0" "sos.I(S!1, s1!1)" "c2" "T(s2!1)" ))"1" replace "1" "1" "sos.I(S2(S!1), d(t2(d!1))`2)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "t1(d!1)" )"2" assert )nil nil ))nil ))nil )"2" "t2(d!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "2" "S1(S!1)" "s1!1" "d(t2(d!1))`2" )"2" "1" "S!1" "d(t2(d!1))`2" "s2!1" )"1" "1" "1" "s3!1" "d(t2(d!1))`2" )"1" rewrite "sos.SS_deterministic" "1" rewrite "sos.SS_deterministic" "1" rewrite "sos.SS_deterministic" "1" "1" expand "tr" "1" expand "step" )"1" assert )"1" expand "tr" "1" expand "step" )"1" "n!2+n!3+2" )"1" assert )"1" "tr_partial" "k" "n!3" "S1" "S1(S!1)" "s0" "s1!1" "s1" "s3!1" "S2" "S!1" ))"1" assert )"1" "tr_add" "k1" "n!3" "k2" "n!2" "c0" "sos.I(Sequence(S1(S!1), S!1), s1!1)" "c2" "T(s2!1)" ))"1" replace "1" "1" "sos.I(S!1, s3!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "t2(d!1)" )"2" assert )nil nil ))nil ))nil ))nil )"2" "t1(d!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 )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> (up?)]" lift_adt nil )"[lift -> boolean]" lift_adt nil )"Cont" sos nil )nil Cont nil )nil lift_adt nil )"State" natural nil )"State" natural nil )"Stm" natural nil )"[T, T -> boolean]" equalities nil )"nat" natural nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil natural nil )"bool" natural nil )nil natural nil )"[bool, bool -> bool]" booleans 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 Stm nil )nil natural nil )nil natural nil )"(total_order?[real])" nil )nil defined_types nil )nil naturalnumbers nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"[(branch2?) -> tree]" natural nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[tree -> boolean]" natural nil )"[tree -> boolean]" natural nil )"[{x: tree | branch1?(x) OR branch2?(x)} -> tree]" natural nil )"(total_order?[real])" nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integersnil )"even_int" integersnil )"Stm" natural nil )"State" natural nil )nil sos nil )"bool" sos nil ) (step def-decl "[Config]" sos nil )"State" natural nil )"[{x: Stm | Conditional?(x) OR While?(x)} -> BExp[V]]" Stm nil )"[Stm -> boolean]" Stm nil )"[Stm -> boolean]" Stm nil )"[State -> bool]" BExp nil )nil BExp nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields 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 )"[tree -> [Stm[V], State[V], State[V]]]" natural nil )"nonneg_int" nil )nil Stm nil )"[State[V] -> (T?)]" sos nil )"[Config -> boolean]" sos nil )"[[Stm[V], State[V]] -> (I?)]" sos nil )"[Config -> boolean]" sos nil )nil sos nil ) (tr_add formula-decl nil sos nil )"[[Stm, Stm] -> (Sequence?)]" Stmnil )nil sos nil )"posint" nil )"[tree -> boolean]" natural nil )"bool" Cont nil ))nil 3400296860"" (expand "sq_le" )"" case "forall (S:Stm,s1, s2:State,m:nat): (EXISTS (n:nat): n <= m & tr(n)(sos.I(S,s1),T(s2))) => SS(S)(s1) = up(s2)" )"1" (skosimp*)"1" (rewrite "sos.SS_deterministic" - :dir rl)"1" (skosimp)"1" (inst - "S!1" "s1!1" "s2!1" "n!1" )"1" (split)"1" (propax) nil nil )"2" (inst + "n!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "m" )"1" (skosimp*)"1" (expand "tr" ) (("1" (assert ) nil nil )) nil )) nil )"2" (skolem!)"2" (flatten)"2" (induct "S" )"1" (skolem + ("x!1" "a!1" ))"1" (skosimp)"1" (skosimp)"1" (rewrite "SS_deterministic" + :dir rl)"1" "leaf((Assign(x!1, a!1),s1!1,s2!1))" )"1" (assert )"1" (expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "derivation_tree?" )"2" (assert )"2" expand "S" )"2" expand "s1" )"2" expand "s0" )"2" expand "tr" )"2" expand "step" )"2" expand "tr" )"2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (hide -2)"2" (skosimp)"2" (rewrite "SS_deterministic" + :dir rl)"2" (inst + "leaf((Skip,s1!1,s2!1))" )"1" (expand "S" )"1" (expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "derivation_tree?" )"2" (expand "S" )"2" expand "s1" )"2" expand "s0" )"2" expand "tr" )"2" expand "step" )"2" expand "tr" )"2" "2" "2" "2" (assert ) 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" "tr_split" "k" "n!1" "S1" "S!1" "S2" "S!2" "s0" "s1!1" "s2" "s2!1" ))"3" (assert )"3" (skosimp)"3" (inst - "s1!1" "s1!2" )"3" (split -4)"1" "s1!2" "s2!1" )"1" "1" "1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" "1" "branch2((Sequence(S!1, S!2),s1!1,s2!1),d!2,d!1)" )"1" expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "derivation_tree?" )"2" assert )"2" expand "S" )"2" expand "S" )"2" expand "s0" )"2" expand "s0" )"2" expand "s1" )"2" expand "s1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "k2!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "k1!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skolem + ("b!1" "S!1" "S!2" ))"4" (skosimp*)"4" (expand "tr" -4)"4" (prop)"4" (expand "step" )"4" (case-replace "B(b!1)(s1!1)" )"1" (hide -4 -6)"1" "s1!1" "s2!1" )"1" "1" "1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" "1" "branch1((Conditional(b!1, S!1, S!2),s1!1,s2!1),d!1)" )"1" expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "derivation_tree?" )"2" expand "S" )"2" expand "s0" )"2" expand "s0" )"2" expand "s1" )"2" expand "s1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1-1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "2" "s1!1" "s2!1" )"2" "1" "1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" "1" "branch1((Conditional(b!1, S!1, S!2),s1!1,s2!1),d!1)" )"1" expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "derivation_tree?" )"2" expand "S" )"2" expand "s0" )"2" expand "s0" )"2" expand "s1" )"2" expand "s1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1-1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (skolem + ("b!1" "S!1" ))"5" (skosimp*)"5" (expand "tr" -3)"5" (expand "step" )"5" (prop)"5" (expand "tr" -1)"5" (expand "step" )"5" "5" "B(b!1)(s1!1)" )"1" "tr_split" "k" "n!1-2" "S1" "S!1" "S2" "While(b!1, S!1)" "s0" "s1!1" "s2" "s2!1" ))"1" assert )"1" "1" "s1!1" "s1!2" )"1" "1" "While(b!1, S!1)" "s1!2" "s2!1" )"1" "1" "1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" rewrite "SS_deterministic" "1" "1" "branch2((While(b!1, S!1),s1!1,s2!1),d!2,d!1)" )"1" expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "derivation_tree?" )"2" expand "S" )"2" expand "S" )"2" expand "s0" )"2" expand "s0" )"2" expand "s1" )"2" expand "s1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "k2!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "k1!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" assert )"2" expand "tr" -1)"2" expand "step" )"2" "2" expand "tr" -1)"2" "2" "2" "2" replace -1 * rl)"2" "2" rewrite "SS_deterministic" "2" "leaf((While(b!1, S!1),s1!1,s1!1))" )"1" expand "S" )"1" expand "S" )"1" expand "s0" )"1" expand "s0" )"1" expand "s1" )"1" expand "s1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "derivation_tree?" )"2" expand "S" )"2" expand "s1" )"2" expand "s0" )"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 ))nil ))nil )"[T -> (up?)]" lift_adt nil )"[lift -> boolean]" lift_adt nil )"Cont" natural nil )nil Cont nil )"[T, T -> boolean]" equalities nil )nil lift_adt 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" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans 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 Stm nil )nil natural nil )nil sos nil )"(total_order?[real])" nil )nil defined_types nil )nil naturalnumbers nil )"derivation_tree" natural nil )"derivation_tree" natural nil )"State[V]" natural nil )"State[V]" natural nil )"Stm[V]" natural nil )"BExp[V]" natural nil )"[[BExp[V], Stm] -> (While?)]" Stm nil )"[Stm -> boolean]" Stm nil )"derivation_tree" natural nil )"derivation_tree" natural nil )"State[V]" natural nil )"State[V]" natural nil )"Stm[V]" natural nil )"Stm[V]" natural nil )"BExp[V]" natural nil )"[[[Stm[V], State[V], State[V]], tree] -> (branch1?)]" naturalnil )"[tree -> boolean]" natural nil )"[Stm -> boolean]" Stm nil )"[[BExp[V], Stm, Stm] -> (Conditional?)]" Stm nil )"nat" natural nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )nil BExp nil )"[State -> bool]" BExp nil )nil sos nil )"[[Stm, Stm] -> (Sequence?)]" Stmnil )"[Stm -> boolean]" Stm nil )"[tree -> boolean]" natural nil )"[[[Stm[V], State[V], State[V]], tree, tree] -> (branch2?)]" nil )"Stm[V]" natural nil )"Stm[V]" natural nil )"State[V]" natural nil )"State[V]" natural nil )"derivation_tree" natural nil )"derivation_tree" natural nil )"posint" nil )"nonneg_int" nil )"State[V]" natural nil )"State[V]" natural nil )"[Stm -> boolean]" Stm nil )"(Skip?)" Stm nil )nil natural nil )"bool" natural nil )"[tree -> boolean]" natural nil )"[[Stm[V], State[V], State[V]] -> (leaf?)]" natural nil )"V" natural nil )"AExp[V]" natural nil )"State[V]" natural nil )"State[V]" natural nil )nil natural nil )"Stm" natural nil )"State" natural nil )"State" natural nil )"State" natural nil )"State" natural nil )"Stm" natural nil )"[State -> int]" AExp nil )"State" State nil )"[(T?) -> State[V]]" sos nil )"[Config]" sos nil )nil natural nil )nil AExp nil )"[Stm -> boolean]" Stm nil )"[[V, AExp[V]] -> (Assign?)]" Stm nil )nil Stm nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"bool" Cont nil ))nil 3400294525"" (skosimp)"" (lemma "sos_le_natural" ("S" "S!1" ))"" (lemma "natural_le_sos" ("S" "S!1" ))"" (typepred "sq_le" )"" (expand "partial_order?" )"" (flatten)"" (expand "antisymmetric?" )"" (inst - "SS(S!1)" "sos.SS(S!1)" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil Stm nil )nil natural nil )nil natural nil )"bool" Cont nil )"bool" "orders/" )nil defined_types nil )nil Cont nil )nil lift_adt 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 )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(pointed_directed_complete_partial_order?[Cont])" natural nil )"(pointed_directed_complete_partial_order?[Cont])" continuationnil )"(pointed_directed_complete_partial_order?[Cont])" sos nil )nil partial_order_props"orders/" )nil natural nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.104 Sekunden
(vorverarbeitet am 2026-04-29)
¤ *© Formatika GbR, Deutschland
2026-05-26
