|
(sos
(step_TCC1 0
(step_TCC1-1 nil 3398574509 ("" (grind) nil nil)
((V formal-nonempty-type-decl nil sos nil)
(<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
nil))
(tr_TCC1 0
(tr_TCC1-1 nil 3398576863 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(>= const-decl "bool" 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(tr_TCC2 0
(tr_TCC2-1 nil 3398576863 ("" (termination-tcc) nil nil) nil nil))
(tr_TCC3 0
(tr_TCC3-1 nil 3398576863 ("" (cases-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(>= const-decl "bool" 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(tr_add 0
(tr_add-1 nil 3398681577
(""
(case "FORALL (c0, c2: Config, k1, k2: nat):
tr(k1 + k2)(c0, c2) =>
(EXISTS c1: tr(k1)(c0, c1) AND tr(k2)(c1, c2))")
(("1"
(case "FORALL (c0, c1,c2: Config, k1, k2: nat):tr(k1)(c0, c1) AND tr(k2)(c1, c2) => tr(k1 + k2)(c0, c2)")
(("1" (skosimp)
(("1" (split)
(("1" (flatten)
(("1" (inst -3 "c0!1" "c2!1" "k1!1" "k2!1")
(("1" (assert) nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (inst - "c0!1" "c1!1" "c2!1" "k1!1" "k2!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2" (induct "k1")
(("1" (skosimp)
(("1" (expand "tr" -1) (("1" (assert) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (expand "tr" (-2 1))
(("2" (flatten)
(("2" (assert)
(("2"
(inst - "step(S(c0!1), s(c0!1))" "c1!1" "c2!1"
"k2!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "k1")
(("1" (skosimp)
(("1" (inst + "c0!1")
(("1" (expand "tr" 1 1) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "tr" -2)
(("2" (flatten)
(("2" (assert)
(("2" (expand "tr" 1 1)
(("2" (inst - "step(S(c0!1), s(c0!1))" "c2!1" "k2!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(V formal-nonempty-type-decl nil sos nil)
(Stm type-decl nil Stm nil)
(State nonempty-type-eq-decl nil State nil)
(step def-decl "[Config]" sos nil)
(I? adt-recognizer-decl "[Config -> boolean]" sos nil)
(S adt-accessor-decl "[(I?) -> Stm[V]]" sos nil)
(s adt-accessor-decl "[(I?) -> State[V]]" sos nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(Config type-decl nil sos nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(tr def-decl "bool" sos nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
shostak))
(tr_eq 0
(tr_eq-1 nil 3398682719
("" (induct "k")
(("1" (skosimp) (("1" (expand "tr") (("1" (assert) nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (expand "tr" (-2 -3))
(("2" (flatten)
(("2" (assert)
(("2" (inst - "step(S(c0!1), s(c0!1))" "c1!1" "c2!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((s adt-accessor-decl "[(I?) -> State[V]]" sos nil)
(S adt-accessor-decl "[(I?) -> Stm[V]]" sos nil)
(I? adt-recognizer-decl "[Config -> boolean]" sos nil)
(step def-decl "[Config]" sos nil)
(State nonempty-type-eq-decl nil State nil)
(Stm type-decl nil Stm nil)
(V formal-nonempty-type-decl nil sos nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(tr def-decl "bool" sos nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Config type-decl nil sos nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
shostak))
(tr_split 0
(tr_split-1 nil 3398576875
("" (induct "k")
(("1" (skosimp)
(("1" (inst + "s0!1" "0" "0")
(("1" (assert)
(("1" (expand "tr") (("1" (propax) nil nil)) nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "tr" -2)
(("2" (expand "step" -2)
(("2" (case "T?(step(S1!1, s0!1))")
(("1" (case "exists s: step(S1!1, s0!1) = T(s)")
(("1" (skosimp)
(("1" (replace -1)
(("1" (assert)
(("1" (hide -2)
(("1" (inst + "s!1" "1" "j!1")
(("1" (replace -3)
(("1" (hide -2 -3)
(("1" (expand "tr")
(("1"
(expand "tr")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (inst + "s1(step(S1!1, s0!1))")
(("2" (assert)
(("2" (expand "step")
(("2" (case "Assign?(S1!1)")
(("1" (assert) nil nil)
("2" (case "Skip?(S1!1)")
(("1" (assert) nil nil)
("2" (case "Sequence?(S1!1)")
(("1" (assert)
(("1"
(lift-if)
(("1" (assert) nil nil))
nil))
nil)
("2" (case "Conditional?(S1!1)")
(("1"
(assert)
(("1"
(lift-if)
(("1" (assert) nil nil))
nil))
nil)
("2"
(case "While?(S1!1)")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "I?(step(S1!1, s0!1))")
(("1" (case "exists (S1,s): step(S1!1,s0!1)=I(S1,s)")
(("1" (skosimp)
(("1" (hide -2 1)
(("1" (replace -1)
(("1" (assert)
(("1" (inst - "S1!2" "S2!1" "s!1" "s2!1")
(("1" (assert)
(("1" (skosimp)
(("1"
(inst + "s1!1" "1+k1!1" "k2!1")
(("1"
(assert)
(("1"
(hide -3 -4 -5)
(("1"
(expand "tr" 1)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2"
(inst + "S(step(S1!1, s0!1))"
"s(step(S1!1, s0!1))")
(("2" (decompose-equality) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((step def-decl "[Config]" sos nil)
(Config_I_extensionality formula-decl nil sos nil)
(S adt-accessor-decl "[(I?) -> Stm[V]]" sos nil)
(s adt-accessor-decl "[(I?) -> State[V]]" sos nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(S1!1 skolem-const-decl "Stm[V]" sos nil)
(s0!1 skolem-const-decl "State[V]" sos nil)
(s1 adt-accessor-decl "[(T?) -> State[V]]" sos nil)
(Skip? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
(Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
(While? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
(Assign? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
(nat_induction formula-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T adt-constructor-decl "[State[V] -> (T?)]" sos nil)
(T? adt-recognizer-decl "[Config -> boolean]" sos nil)
(Sequence adt-constructor-decl "[[Stm, Stm] -> (Sequence?)]" Stm
nil)
(Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(State nonempty-type-eq-decl nil State nil)
(Stm type-decl nil Stm nil)
(V formal-nonempty-type-decl nil sos nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
shostak))
(tr_partial 0
(tr_partial-1 nil 3398579757
("" (induct "k")
(("1" (skosimp) (("1" (expand "tr") (("1" (propax) nil nil)) nil))
nil)
("2" (skosimp)
(("2" (expand "tr" 1)
(("2" (skosimp)
(("2" (case "T?(step(S1!1, s0!1))")
(("1" (case "exists s1: step(S1!1,s0!1)=T(s1)")
(("1" (skosimp)
(("1" (replace -1)
(("1" (expand "step" 1)
(("1" (assert)
(("1" (replace -1)
(("1" (assert)
(("1" (hide -3)
(("1" (expand "tr")
(("1"
(case-replace "j!1=0")
(("1"
(assert)
(("1"
(hide -2)
(("1"
(decompose-equality)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (inst + "s1(step(S1!1, s0!1))")
(("2" (decompose-equality) nil nil)) nil))
nil))
nil)
("2" (case "I?(step(S1!1, s0!1))")
(("1" (case "exists S1,s1: step(S1!1,s0!1)=I(S1,s1)")
(("1" (skosimp)
(("1" (hide -2 1)
(("1" (replace -1)
(("1" (expand "step" 1)
(("1" (replace -1)
(("1" (assert)
(("1" (inst - "S1!2" "S2!1" "s1!2" "s1!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2"
(inst + "S(step(S1!1, s0!1))"
"s(step(S1!1, s0!1))")
(("2" (decompose-equality) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Config_I_extensionality formula-decl nil sos nil)
(S adt-accessor-decl "[(I?) -> Stm[V]]" sos nil)
(s adt-accessor-decl "[(I?) -> State[V]]" sos nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(s1 adt-accessor-decl "[(T?) -> State[V]]" sos nil)
(S1!1 skolem-const-decl "Stm[V]" sos nil)
(s0!1 skolem-const-decl "State[V]" sos nil)
(Config_T_extensionality formula-decl nil sos nil)
(step def-decl "[Config]" sos nil)
(nat_induction formula-decl nil naturalnumbers nil)
(Sequence adt-constructor-decl "[[Stm, Stm] -> (Sequence?)]" Stm
nil)
(Sequence? adt-recognizer-decl "[Stm -> boolean]" 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)
(tr def-decl "bool" sos nil) (Config type-decl nil sos nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(State nonempty-type-eq-decl nil State nil)
(Stm type-decl nil Stm nil)
(V formal-nonempty-type-decl nil sos nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
shostak))
(tr_deterministic 0
(tr_deterministic-1 nil 3398678984
("" (skosimp)
(("" (lemma "trich_lt" ("x" "k1!1" "y" "k2!1"))
(("" (split -1)
(("1"
(lemma "tr_add"
("k1" "k1!1" "k2" "k2!1-k1!1" "c0" "c!1" "c2" "T(s2!1)"))
(("1" (assert)
(("1" (skosimp)
(("1"
(lemma "tr_eq"
("k" "k1!1" "c0" "c!1" "c1" "c1!1" "c2" "T(s1!1)"))
(("1" (assert)
(("1" (replace -1)
(("1" (expand "tr" -3) (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (replace -1 * rl)
(("2"
(lemma "tr_eq"
("k" "k1!1" "c0" "c!1" "c1" "T(s1!1)" "c2" "T(s2!1)"))
(("2" (assert)
(("2" (hide-all-but (-1 1))
(("2" (decompose-equality) nil nil)) nil))
nil))
nil))
nil)
("3"
(lemma "tr_add"
("k1" "k2!1" "k2" "k1!1-k2!1" "c0" "c!1" "c2" "T(s1!1)"))
(("1" (assert)
(("1" (skosimp)
(("1"
(lemma "tr_eq"
("k" "k2!1" "c0" "c!1" "c1" "c1!1" "c2" "T(s2!1)"))
(("1" (assert)
(("1" (replace -1)
(("1" (expand "tr" -3) (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(trich_lt formula-decl nil real_props nil)
(s1 adt-accessor-decl "[(T?) -> State[V]]" sos nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(State nonempty-type-eq-decl nil State nil)
(T adt-constructor-decl "[State[V] -> (T?)]" sos nil)
(T? adt-recognizer-decl "[Config -> boolean]" sos nil)
(V formal-nonempty-type-decl nil sos nil)
(Config type-decl nil sos nil) (tr_add formula-decl nil sos nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(tr def-decl "bool" sos nil) (tr_eq formula-decl nil sos nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil))
shostak))
(SS_TCC1 0
(SS_TCC1-1 nil 3398678981 ("" (subtype-tcc) nil nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(V formal-nonempty-type-decl nil sos nil)
(State nonempty-type-eq-decl nil State nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(>= const-decl "bool" reals 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)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(SS_deterministic 0
(SS_deterministic-1 nil 3398683355
("" (skosimp)
(("" (split)
(("1" (skosimp*)
(("1" (expand "SS")
(("1" (lift-if)
(("1" (assert)
(("1"
(case-replace
"EXISTS n, s1: tr(n)(I(S!1, s!1), T(s1))")
(("1" (hide -1)
(("1"
(case "nonempty?({s1_1: State |
EXISTS (n_1: nat): tr(n_1)(I(S!1, s!1), T(s1_1))})")
(("1"
(lemma "choose_member"
("a" "{s1_1: State |
EXISTS (n_1: nat): tr(n_1)(I(S!1, s!1), T(s1_1))}"))
(("1" (split -1)
(("1"
(name-replace "CC" "choose({s1_1: State |
EXISTS (n_1: nat): tr(n_1)(I(S!1, s!1), T(s1_1))})")
(("1" (expand "member")
(("1" (skosimp)
(("1"
(lemma
"tr_deterministic"
("k1"
"n!1"
"c"
"sos.I(S!1, s!1)"
"s1"
"s1!1"
"k2"
"n!2"
"s2"
"CC"))
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (propax) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "s1!1")
(("2" (inst + "n!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (inst + "n!1" "s1!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "SS")
(("2" (lift-if)
(("2" (assert)
(("2" (prop)
(("2"
(case "nonempty?[State]({s1 | EXISTS n: tr(n)(I(S!1, s!1), T(s1))})")
(("1"
(lemma "choose_member"
("a"
"{s1 | EXISTS n: tr(n)(I(S!1, s!1), T(s1))}"))
(("1"
(name-replace "CC"
"choose({s1 | EXISTS n: tr(n)(I(S!1, s!1), T(s1))})")
(("1" (split -1)
(("1" (expand "member")
(("1" (skolem!)
(("1" (inst + "n!1")
(("1"
(case-replace "CC=s1!1")
(("1"
(hide-all-but (-4 1))
(("1"
(assert)
(("1"
(rewrite "up_equal")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (hide -2 2)
(("2" (skosimp)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "s1!2")
(("2" (inst + "n!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((SS const-decl "Cont" sos nil) (empty? const-decl "bool" sets nil)
(choose_member formula-decl nil sets_lemmas nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(choose const-decl "(p)" sets nil)
(tr_deterministic formula-decl nil sos nil)
(member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets 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)
(Stm type-decl nil Stm nil) (tr def-decl "bool" sos nil)
(Config type-decl nil sos nil)
(State nonempty-type-eq-decl nil State nil)
(V formal-nonempty-type-decl nil sos nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(up_equal formula-decl nil lift_props "orders/"))
shostak)))
¤ Dauer der Verarbeitung: 0.59 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
