| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/while/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 151 kB |
|
Quelle natural.prfSprache: Lisp |
|||||||||||||||
|
(natural (depth_TCC1 0 (depth_TCC1-1 nil 3400243711 ("" (termination-tcc) nil nil) ((<< adt-def-decl "(strict_well_founded?[tree])" natural nil)) nil)) (depth_TCC2 0 (depth_TCC2-1 nil 3400243711 ("" (termination-tcc) nil nil) ((<< adt-def-decl "(strict_well_founded?[tree])" natural nil)) nil)) (depth_TCC3 0 (depth_TCC3-1 nil 3400243711 ("" (termination-tcc) nil nil) ((<< adt-def-decl "(strict_well_founded?[tree])" natural nil)) nil)) (derivation_tree?_TCC1 0 (derivation_tree?_TCC1-1 nil 3400238483 ("" (subtype-tcc) nil nil) ((S const-decl "Stm" natural nil) (s1 const-decl "State" natural nil) (s0 const-decl "State" natural nil) (V formal-nonempty-type-decl nil natural nil) (assign const-decl "State" State nil)) nil)) (derivation_tree?_TCC2 0 (derivation_tree?_TCC2-1 nil 3400238483 ("" (termination-tcc) nil nil) ((S const-decl "Stm" natural nil)) nil)) (derivation_tree?_TCC3 0 (derivation_tree?_TCC3-1 nil 3400238483 ("" (termination-tcc) nil nil) ((S const-decl "Stm" natural nil) (S const-decl "Stm" natural nil)) nil)) (derivation_tree?_TCC4 0 (derivation_tree?_TCC4-1 nil 3400238483 ("" (subtype-tcc) nil nil) ((S const-decl "Stm" natural nil) (S const-decl "Stm" natural nil) (s0 const-decl "State" natural nil) (s0 const-decl "State" natural nil) (s1 const-decl "State" natural nil) (s1 const-decl "State" natural nil)) nil)) (derivation_tree?_TCC5 0 (derivation_tree?_TCC5-1 nil 3400238483 ("" (subtype-tcc) nil nil) ((s1 const-decl "State" natural nil) (s1 const-decl "State" natural nil) (s0 const-decl "State" natural nil) (s0 const-decl "State" natural nil) (S const-decl "Stm" natural nil)) nil)) (derivation_tree?_TCC6 0 (derivation_tree?_TCC6-1 nil 3400238483 ("" (subtype-tcc) nil nil) ((S const-decl "Stm" natural nil) (s0 const-decl "State" natural nil) (S const-decl "Stm" natural nil) (s1 const-decl "State" natural nil) (s1 const-decl "State" natural nil) (s0 const-decl "State" natural nil)) nil)) (derivation_tree_TCC1 0 (derivation_tree_TCC1-1 nil 3400238483 ("" (expand "derivation_tree?") (("" (expand "S") (("" (expand "s1") (("" (expand "s0") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((S const-decl "Stm" natural nil) (s0 const-decl "State" natural nil) (s1 const-decl "State" natural nil) (derivation_tree? def-decl "bool" natural nil)) nil)) (dt_eq 0 (dt_eq-1 nil 3400238504 ("" (case "FORALL (d1, d2: derivation_tree,n:nat): depth(d1)<=n&depth(d2)<=n& S(d1) = S(d2) 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" (hide -1 -2) (("1" (case-replace "Assign?(d(d2!1)`1)") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "Skip?(d(d2!1)`1)") (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (decompose-equality) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (decompose-equality) (("2" (decompose-equality) 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" (lift-if) (("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" (lift-if) (("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" (lift-if) (("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" (case-replace "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" (flatten) (("1" (expand "s0") (("1" (expand "s0") (("1" (expand "s1") (("1" (expand "s1") (("1" (expand "S") (("1" (expand "S") (("1" (case-replace "B(b(d(d1!1)`1))(d(d1!1)`2)") (("1" (assert) (("1" (inst - "t1(d1!1)" "t1(d2!1)") (("1" (expand "depth" (-15 -16)) (("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 1) (("1" (case "d2!1=branch1((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3),t1(d2!1))") (("1" (replace -1 1) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-13 1)) (("2" (decompose-equality) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-12 1)) (("2" (decompose-equality) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "t1(d1!1)" "t1(d2!1)") (("2" (expand "depth" (-14 -15)) (("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 2) (("1" (case "d2!1=branch1((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3),t1(d2!1))") (("1" (replace -1 2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-13 1)) (("2" (decompose-equality) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-11 1)) (("2" (decompose-equality) (("2" (decompose-equality) 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" (flatten) (("2" (assert) (("2" (expand "S") (("2" (expand "s1") (("2" (expand "s0") (("2" (expand "s1") (("2" (expand "s0") (("2" (expand "S") (("2" (assert) (("2" (lift-if) (("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" (case-replace "leaf?(d2!1)") (("1" (assert) nil nil) ("2" (case-replace "branch1?(d2!1)") (("1" (assert) (("1" (typepred "d1!1") (("1" (typepred "d2!1") (("1" (expand "derivation_tree?") (("1" (assert) (("1" (flatten) (("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" (typepred "d1!1") (("2" (typepred "d2!1") (("2" (expand "derivation_tree?") (("2" (assert) (("2" (expand "S") (("2" (expand "s1") (("2" (expand "s1") (("2" (expand "s0") (("2" (expand "s0") (("2" (split -2) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("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" (hide -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" (hide -1) (("1" (typepred "d1!1") (("1" (typepred "d2!1") (("1" (expand "derivation_tree?") (("1" (lift-if) (("1" (assert) (("1" (expand "S") (("1" (expand "S") (("1" (expand "s0") (("1" (expand "s0") (("1" (expand "s1") (("1" (expand "s1") (("1" (case-replace " Sequence?(d(d1!1)`1)") (("1" (assert) (("1" (flatten) (("1" (inst-cp - "t1(d1!1)" "t1(d2!1)") (("1" (inst - "t2(d1!1)" "t2(d2!1)") (("1" (expand "depth" (-20 -21)) (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (inst-cp - "t1(d1!1)" "t1(d2!1)") (("2" (inst - "t2(d1!1)" "t2(d2!1)") (("2" (expand "depth" (-23 -24)) (("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" (hide-all-but (-1 1)) (("2" (decompose-equality) (("2" (decompose-equality) nil nil)) nil)) nil) ("3" (propax) nil nil) ("4" (flatten) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (decompose-equality) (("2" (decompose-equality) nil nil)) nil)) nil) ("3" (propax) nil nil) ("4" (assert) nil nil)) nil) ("2" (typepred "d1!1") (("2" (typepred "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" (flatten) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (case-replace "Sequence?(d(d1!1)`1)") (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("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) ((branch1 adt-constructor-decl "[[[Stm[V], State[V], State[V]], tree] -> (branch1?)]" natural nil) (tree_branch1_extensionality formula-decl nil natural nil) (BExp type-decl nil BExp nil) (B def-decl "[State -> bool]" BExp nil) (Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (While? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (b shared-adt-accessor-decl "[{x: Stm | Conditional?(x) OR While?(x)} -> BExp[V]]" Stm nil) (s1 const-decl "State" natural nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (d2!1 skolem-const-decl "derivation_tree" natural nil) (d1!1 skolem-const-decl "derivation_tree" natural nil) (tree_branch2_extensionality formula-decl nil natural nil) (branch2 adt-constructor-decl "[[[Stm[V], State[V], State[V]], tree, tree] -> (branch2?)]" natural nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (branch1? adt-recognizer-decl "[tree -> boolean]" natural nil) (branch2? adt-recognizer-decl "[tree -> boolean]" natural nil) (t1 shared-adt-accessor-decl "[{x: tree | branch1?(x) OR branch2?(x)} -> tree]" natural nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (t2 adt-accessor-decl "[(branch2?) -> tree]" natural nil) (NOT const-decl "[bool -> bool]" booleans nil) (S const-decl "Stm" natural nil) (s0 const-decl "State" natural nil) (s1 const-decl "State" natural nil) (tree_leaf_extensionality formula-decl nil natural nil) (Assign? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (Skip? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (d shared-adt-accessor-decl "[tree -> [Stm[V], State[V], State[V]]]" natural nil) (leaf adt-constructor-decl "[[Stm[V], State[V], State[V]] -> (leaf?)]" natural nil) (leaf? adt-recognizer-decl "[tree -> boolean]" natural nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (tree type-decl nil natural nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (derivation_tree? def-decl "bool" natural nil) (derivation_tree nonempty-type-eq-decl nil natural nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (depth def-decl "nat" natural nil) (V formal-nonempty-type-decl nil natural nil) (Stm type-decl nil Stm nil) (= const-decl "[T, T -> boolean]" equalities nil) (S const-decl "Stm" natural nil) (State nonempty-type-eq-decl nil State nil) (s0 const-decl "State" natural nil)) shostak)) (SS_TCC1 0 (SS_TCC1-1 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) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (derivation_tree nonempty-type-eq-decl nil natural nil) (derivation_tree? def-decl "bool" natural nil) (bool nonempty-type-eq-decl nil booleans nil) (s1 const-decl "State" natural nil) (tree type-decl nil natural nil) (State nonempty-type-eq-decl nil State nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (V formal-nonempty-type-decl nil natural nil) (empty? const-decl "bool" sets nil)) nil)) (SS_deterministic 0 (SS_deterministic-1 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 | EXISTS (d_1: derivation_tree): S(d_1) = S!1 AND s0(d_1) = s0!1 AND s1(d_1) = s1})") (("1" (lemma "choose_member" ("a" "{s1 | EXISTS (d_1: derivation_tree): S(d_1) = S!1 AND s0(d_1) = s0!1 AND s1(d_1) = s1}")) (("1" (split -1) (("1" (name-replace "CC" "choose({s1 | EXISTS (d_1: derivation_tree): S(d_1) = S!1 AND s0(d_1) = s0!1 AND s1(d_1) = s1})") (("1" (expand "member") (("1" (hide -2 -3) (("1" (skosimp) (("1" (split) (("1" (skosimp*) (("1" (lemma "dt_eq" ("d1" "d!1" "d2" "d!2")) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (inst + "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) ((SS const-decl "Cont" natural nil) (s1 const-decl "State" natural nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil) (up_equal formula-decl nil lift_props "orders/") (dt_eq formula-decl nil natural nil) (choose const-decl "(p)" sets nil) (choose_member formula-decl nil sets_lemmas nil) (empty? const-decl "bool" sets nil) (s0 const-decl "State" natural nil) (State nonempty-type-eq-decl nil State nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S const-decl "Stm" natural nil) (= const-decl "[T, T -> boolean]" equalities nil) (Stm type-decl nil Stm nil) (V formal-nonempty-type-decl nil natural nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (derivation_tree nonempty-type-eq-decl nil natural nil) (derivation_tree? def-decl "bool" natural nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (tree type-decl nil natural nil)) shostak)) (natural_le_sos 0 (natural_le_sos-1 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 (("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" (flatten) (("1" (rewrite "sos.SS_deterministic" 1 :dir rl) (("1" (inst + "1") (("1" (expand "tr") (("1" (expand "step") (("1" (assert) (("1" (expand "tr") (("1" (replace -2 1) (("1" (propax) 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" (flatten) (("2" (rewrite "sos.SS_deterministic" 1 :dir rl) (("2" (inst + "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" (flatten) (("3" (rewrite "sos.SS_deterministic" + :dir rl) (("3" (expand "tr") (("3" (expand "step") (("3" (assert) (("3" (expand "tr") (("3" (expand "step") (("3" (expand "tr") (("3" (expand "step") (("3" (expand "tr") (("3" (inst + "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" (case-replace "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" (hide 1) (("1" (rewrite "sos.SS_deterministic" + :dir rl) (("1" (expand "tr") (("1" (expand "step") (("1" (assert) (("1" (expand "depth" -8) (("1" (case-replace "B(b(S!1))(s1!1)") (("1" (inst - "S1(S!1)" "s1!1" "s2!1") (("1" (split -8) (("1" (rewrite "sos.SS_deterministic" - :dir rl) (("1" (skosimp) (("1" (inst + "n!2+1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst + "t1(d!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "S2(S!1)" "s1!1" "s2!1") (("2" (split -7) (("1" (rewrite "sos.SS_deterministic" - :dir rl) (("1" (skosimp) (("1" (inst + "n!2+1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "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" (case-replace "Sequence?(S!1)") (("1" (assert) (("1" (flatten) (("1" (inst-cp - "S1(S!1)" "s1!1" "d(t2(d!1))`2") (("1" (inst - "S2(S!1)" "d(t2(d!1))`2" "s2!1") (("1" (split -10) (("1" (split -11) (("1" (rewrite "sos.SS_deterministic" * :dir rl) (("1" (rewrite "sos.SS_deterministic" * :dir rl) (("1" (rewrite "sos.SS_deterministic" * :dir rl) (("1" (skosimp*) (("1" (inst + "n!2+n!3") (("1" (lemma "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" (case-replace "Sequence(S1(S!1), S2(S!1))=S!1") (("1" (hide -1) (("1" (lemma "tr_add" ("k1" "n!2" "k2" "n!3" "c0" "sos.I(S!1, s1!1)" "c2" "T(s2!1)")) (("1" (replace -1 1) (("1" (hide -1) (("1" (inst + "sos.I(S2(S!1), d(t2(d!1))`2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "t1(d!1)") (("2" (assert) nil nil)) nil)) nil) ("2" (inst + "t2(d!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (hide 1) (("2" (inst-cp - "S1(S!1)" "s1!1" "d(t2(d!1))`2") (("2" (split -12) (("1" (inst - "S!1" "d(t2(d!1))`2" "s2!1") (("1" (split -12) (("1" (hide-all-but (-1 -2 -5 -6 1)) (("1" (name-replace "s3!1" "d(t2(d!1))`2") (("1" (rewrite "sos.SS_deterministic" * :dir rl) (("1" (rewrite "sos.SS_deterministic" * :dir rl) (("1" (rewrite "sos.SS_deterministic" * :dir rl) (("1" (skosimp*) (("1" (expand "tr" 1) (("1" (expand "step") (("1" (assert) (("1" (expand "tr" 1) (("1" (expand "step") (("1" (inst + "n!2+n!3+2") (("1" (assert) (("1" (lemma "tr_partial" ("k" "n!3" "S1" "S1(S!1)" "s0" "s1!1" "s1" "s3!1" "S2" "S!1")) (("1" (assert) (("1" (lemma "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" (hide -1) (("1" (inst + "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" (inst + "t2(d!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "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) ((up adt-constructor-decl "[T -> (up?)]" lift_adt nil) (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (SS const-decl "Cont" sos nil) (Cont nonempty-type-eq-decl nil Cont nil) (lift type-decl nil lift_adt nil) (s1 const-decl "State" natural nil) (s0 const-decl "State" natural nil) (S const-decl "Stm" natural nil) (= const-decl "[T, T -> boolean]" equalities nil) (depth def-decl "nat" natural nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (derivation_tree nonempty-type-eq-decl nil natural nil) (derivation_tree? def-decl "bool" natural nil) (tree type-decl nil natural nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (State nonempty-type-eq-decl nil State nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Stm type-decl nil Stm nil) (V formal-nonempty-type-decl nil natural nil) (SS_deterministic formula-decl nil natural nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (t2 adt-accessor-decl "[(branch2?) -> tree]" natural nil) (< const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (branch1? adt-recognizer-decl "[tree -> boolean]" natural nil) (branch2? adt-recognizer-decl "[tree -> boolean]" natural nil) (t1 shared-adt-accessor-decl "[{x: tree | branch1?(x) OR branch2?(x)} -> tree]" natural nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (S const-decl "Stm" natural nil) (s0 const-decl "State" natural nil) (SS_deterministic formula-decl nil sos nil) (tr def-decl "bool" sos nil) (step def-decl "[Config]" sos nil) (s1 const-decl "State" natural nil) (b shared-adt-accessor-decl "[{x: Stm | Conditional?(x) OR While?(x)} -> BExp[V]]" Stm nil) (While? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (B def-decl "[State -> bool]" BExp nil) (BExp type-decl nil BExp nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (S1 shared-adt-accessor-decl "[{x: Stm | Sequence?(x) OR Conditional?(x) OR While?(x)} -> Stm]" Stm nil) (S2 shared-adt-accessor-decl "[{x: Stm | Sequence?(x) OR Conditional?(x)} -> Stm]" Stm nil) (d shared-adt-accessor-decl "[tree -> [Stm[V], State[V], State[V]]]" natural nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (Stm_Sequence_extensionality formula-decl nil Stm nil) (T adt-constructor-decl "[State[V] -> (T?)]" sos nil) (T? adt-recognizer-decl "[Config -> boolean]" sos nil) (I adt-constructor-decl "[[Stm[V], State[V]] -> (I?)]" sos nil) (I? adt-recognizer-decl "[Config -> boolean]" sos nil) (Config type-decl nil sos nil) (tr_add formula-decl nil sos nil) (Sequence adt-constructor-decl "[[Stm, Stm] -> (Sequence?)]" Stm nil) (tr_partial formula-decl nil sos nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (leaf? adt-recognizer-decl "[tree -> boolean]" natural nil) (sq_le const-decl "bool" Cont nil)) shostak)) (sos_le_natural 0 (sos_le_natural-1 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 (("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" (inst + "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" (hide -3) (("2" (prop) (("2" (hide -1 -3 1) (("2" (decompose-equality) (("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" (prop) (("2" (hide -1 -3 1) (("2" (decompose-equality) (("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" (lemma "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" (inst - "s1!2" "s2!1") (("1" (split -5) (("1" (hide-all-but (-1 -2 1)) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (skosimp*) (("1" (inst + "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" (propax) 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" (inst + "k2!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "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" (inst - "s1!1" "s2!1") (("1" (split -3) (("1" (hide -3 -4 1) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (skosimp) (("1" (inst + "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" (propax) 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" (inst + "n!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -2 -5) (("2" (inst - "s1!1" "s2!1") (("2" (split -2) (("1" (hide -2 -3 2) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (skosimp) (("1" (inst + "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" (propax) 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" (inst + "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" (prop) (("5" (case-replace "B(b!1)(s1!1)") (("1" (lemma "tr_split" ("k" "n!1-2" "S1" "S!1" "S2" "While(b!1, S!1)" "s0" "s1!1" "s2" "s2!1")) (("1" (assert) (("1" (skosimp) (("1" (inst - "s1!1" "s1!2") (("1" (split -6) (("1" (inst - "While(b!1, S!1)" "s1!2" "s2!1") (("1" (split -8) (("1" (hide-all-but (-1 -2 -6 3)) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (skosimp*) (("1" (inst + "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" (propax) 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" (inst + "k2!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "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" (prop) (("2" (expand "tr" -1) (("2" (prop) (("2" (hide-all-but (-2 2 5)) (("2" (decompose-equality) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (rewrite "SS_deterministic" * :dir rl) (("2" (inst + "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" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "derivation_tree?") (("2" (expand "S") (("2" (expand "s1") (("2" (expand "s0") (("2" (propax) 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) ((up adt-constructor-decl "[T -> (up?)]" lift_adt nil) (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (SS const-decl "Cont" natural nil) (Cont nonempty-type-eq-decl nil Cont nil) (= const-decl "[T, T -> boolean]" equalities nil) (lift type-decl nil lift_adt nil) (T adt-constructor-decl "[State[V] -> (T?)]" sos nil) (T? adt-recognizer-decl "[Config -> boolean]" sos nil) (I adt-constructor-decl "[[Stm[V], State[V]] -> (I?)]" sos nil) (I? adt-recognizer-decl "[Config -> boolean]" sos nil) (tr def-decl "bool" sos nil) (Config type-decl nil sos nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (State nonempty-type-eq-decl nil State nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Stm type-decl nil Stm nil) (V formal-nonempty-type-decl nil natural nil) (SS_deterministic formula-decl nil sos nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (d!1 skolem-const-decl "derivation_tree" natural nil) (d!2 skolem-const-decl "derivation_tree" natural nil) (s2!1 skolem-const-decl "State[V]" natural nil) (s1!1 skolem-const-decl "State[V]" natural nil) (S!1 skolem-const-decl "Stm[V]" natural nil) (b!1 skolem-const-decl "BExp[V]" natural nil) (While adt-constructor-decl "[[BExp[V], Stm] -> (While?)]" Stm nil) (While? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (d!1 skolem-const-decl "derivation_tree" natural nil) (d!1 skolem-const-decl "derivation_tree" natural nil) (s2!1 skolem-const-decl "State[V]" natural nil) (s1!1 skolem-const-decl "State[V]" natural nil) (S!2 skolem-const-decl "Stm[V]" natural nil) (S!1 skolem-const-decl "Stm[V]" natural nil) (b!1 skolem-const-decl "BExp[V]" natural nil) (branch1 adt-constructor-decl "[[[Stm[V], State[V], State[V]], tree] -> (branch1?)]" natural nil) (branch1? adt-recognizer-decl "[tree -> boolean]" natural nil) (Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (Conditional adt-constructor-decl "[[BExp[V], Stm, Stm] -> (Conditional?)]" Stm nil) (n!1 skolem-const-decl "nat" natural nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (BExp type-decl nil BExp nil) (B def-decl "[State -> bool]" BExp nil) (tr_split formula-decl nil sos nil) (Sequence adt-constructor-decl "[[Stm, Stm] -> (Sequence?)]" Stm nil) (Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (branch2? adt-recognizer-decl "[tree -> boolean]" natural nil) (branch2 adt-constructor-decl "[[[Stm[V], State[V], State[V]], tree, tree] -> (branch2?)]" natural nil) (S!1 skolem-const-decl "Stm[V]" natural nil) (S!2 skolem-const-decl "Stm[V]" natural nil) (s1!1 skolem-const-decl "State[V]" natural nil) (s2!1 skolem-const-decl "State[V]" natural nil) (d!2 skolem-const-decl "derivation_tree" natural nil) (d!1 skolem-const-decl "derivation_tree" natural nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (s1!1 skolem-const-decl "State[V]" natural nil) (s2!1 skolem-const-decl "State[V]" natural nil) (Skip? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (Skip adt-constructor-decl "(Skip?)" Stm nil) (tree type-decl nil natural nil) (derivation_tree? def-decl "bool" natural nil) (leaf? adt-recognizer-decl "[tree -> boolean]" natural nil) (leaf adt-constructor-decl "[[Stm[V], State[V], State[V]] -> (leaf?)]" natural nil) (x!1 skolem-const-decl "V" natural nil) (a!1 skolem-const-decl "AExp[V]" natural nil) (s1!1 skolem-const-decl "State[V]" natural nil) (s2!1 skolem-const-decl "State[V]" natural nil) (derivation_tree nonempty-type-eq-decl nil natural nil) (S const-decl "Stm" natural nil) (s0 const-decl "State" natural nil) (s1 const-decl "State" natural nil) (s1 const-decl "State" natural nil) (s0 const-decl "State" natural nil) (S const-decl "Stm" natural nil) (A def-decl "[State -> int]" AExp nil) (assign const-decl "State" State nil) (s1 adt-accessor-decl "[(T?) -> State[V]]" sos nil) (step def-decl "[Config]" sos nil) (SS_deterministic formula-decl nil natural nil) (AExp type-decl nil AExp nil) (Assign? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (Assign adt-constructor-decl "[[V, AExp[V]] -> (Assign?)]" Stm nil) (Stm_induction formula-decl nil Stm nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sq_le const-decl "bool" Cont nil)) shostak)) (natural_eq_sos 0 (natural_eq_sos-1 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) ((Stm type-decl nil Stm nil) (V formal-nonempty-type-decl nil natural nil) (sos_le_natural formula-decl nil natural nil) (sq_le const-decl "bool" Cont nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pred type-eq-decl nil defined_types nil) (Cont nonempty-type-eq-decl nil Cont nil) (lift type-decl nil lift_adt nil) (State nonempty-type-eq-decl nil State nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sq_le_pdcpo name-judgement "(pointed_directed_complete_partial_order?[Cont])" natural nil) (sq_le_pdcpo name-judgement "(pointed_directed_complete_partial_order?[Cont])" continuation nil) (sq_le_pdcpo name-judgement "(pointed_directed_complete_partial_order?[Cont])" sos nil) (partial_order_antisymmetric formula-decl nil partial_order_props "orders/") (natural_le_sos formula-decl nil natural nil)) shostak)))
¤ Dauer der Verarbeitung: 0.110 Sekunden (vorverarbeitet am 2026-04-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26