|
(csequence_limit
(prefix_chain_TCC1 0
(prefix_chain_TCC1-1 nil 3513785036
("" (expand "ascending_chain?")
(("" (skosimp*)
(("" (use "prefix?_order") (("" (assert) nil nil)) nil)) nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(prefix?_is_partial_order name-judgement
"(partial_order?[csequence])" csequence_limit nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(csequence type-decl nil csequence_codt 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T formal-type-decl nil csequence_limit nil)
(prefix?_order formula-decl nil csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil))
nil))
(suffix_chain_TCC1 0
(suffix_chain_TCC1-1 nil 3513785036
("" (induct "n")
(("1" (skolem-typepred)
(("1" (expand* "suffix" "ascending_chain?") nil nil)) nil)
("2" (skosimp* t)
(("2" (expand "ascending_chain?")
(("2" (skolem!)
(("2" (expand "suffix" +)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "prefix?" +) (("1" (propax) nil nil))
nil)
("2" (expand "prefix?" +) (("2" (propax) nil nil))
nil)
("3" (inst - "n!1")
(("3" (expand "prefix?" -2)
(("3" (propax) nil nil)) nil))
nil)
("4"
(inst -3
"LAMBDA n: IF empty?(chain!1(n)) THEN empty_cseq ELSE rest(chain!1(n)) ENDIF")
(("1" (inst -3 "n!1") (("1" (assert) nil nil))
nil)
("2" (hide -2 2 3 4)
(("2" (expand "ascending_chain?")
(("2" (skolem!)
(("2" (lift-if)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(ground)
(("1"
(expand "prefix?" +)
(("1" (propax) nil nil))
nil)
("2"
(expand "prefix?" +)
(("2" (propax) nil nil))
nil)
("3"
(inst - "n!2")
(("3"
(expand "prefix?" -)
(("3" (propax) nil nil))
nil))
nil)
("4"
(inst - "n!2")
(("4"
(expand "prefix?" -)
(("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp) (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(chain!1 skolem-const-decl
"ascending_chain[csequence[T], prefix?[T]]" csequence_limit nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
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)
(nat_induction formula-decl nil naturalnumbers nil)
(suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))"
csequence_suffix nil)
(suffix? inductive-decl "bool" csequence_suffix nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_limit 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)
(prefix?_is_partial_order name-judgement
"(partial_order?[csequence])" csequence_limit nil))
nil))
(rest_chain_TCC1 0
(rest_chain_TCC1-1 nil 3513785036 ("" (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)
(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)
(T formal-type-decl nil csequence_limit nil)
(csequence type-decl nil csequence_codt nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(rest_chain_TCC2 0
(rest_chain_TCC2-1 nil 3513785036
("" (skolem!)
(("" (typepred "suffix_chain(chain!1, 1)")
((""
(expand* "suffix_chain" "suffix" "suffix" "ascending_chain?")
(("" (skolem!) (("" (reduce) nil nil)) nil)) nil))
nil))
nil)
((suffix_chain const-decl "ascending_chain" csequence_limit nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_limit nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(prefix?_is_partial_order name-judgement
"(partial_order?[csequence])" csequence_limit nil)
(suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))"
csequence_suffix nil))
nil))
(ascending_chain?_nth 0
(ascending_chain?_nth-1 nil 3513785384
("" (skosimp)
(("" (lemma "ascending_chain?_def")
(("" (inst - "chain!1" "n!1" "m!1")
(("" (assert)
(("" (forward-chain "prefix?_index")
(("" (use "prefix?_nth") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((prefix? coinductive-decl "bool" csequence_prefix nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_limit nil)
(ascending_chain?_def formula-decl nil ascending_chains nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(prefix?_nth formula-decl nil csequence_prefix nil)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(prefix?_is_partial_order name-judgement
"(partial_order?[csequence])" csequence_limit nil)
(prefix?_index formula-decl nil csequence_prefix nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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))
shostak))
(limit_struct_TCC1 0
(limit_struct_TCC1-1 nil 3513785036 ("" (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)
(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)
(T formal-type-decl nil csequence_limit nil)
(csequence type-decl nil csequence_codt nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(prefix?_is_partial_order name-judgement
"(partial_order?[csequence])" csequence_limit nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(limit_struct_TCC2 0
(limit_struct_TCC2-1 nil 3513785036 ("" (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)
(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)
(T formal-type-decl nil csequence_limit nil)
(csequence type-decl nil csequence_codt nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(limit_empty 0
(limit_empty-1 nil 3513785427
("" (expand* "limit" "limit_struct" "coreduce")
(("" (reduce) nil 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)
(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)
(T formal-type-decl nil csequence_limit nil)
(csequence type-decl nil csequence_codt nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(limit const-decl "csequence" csequence_limit nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(limit_struct const-decl "csequence_struct[T, ascending_chain]"
csequence_limit nil))
shostak))
(limit_nonempty 0
(limit_nonempty-1 nil 3513785452
("" (skolem!) (("" (use "limit_empty") (("" (reduce) nil nil)) nil))
nil)
((limit_empty formula-decl nil csequence_limit nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_limit 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(limit_first_TCC1 0
(limit_first_TCC1-1 nil 3513785036
("" (skosimp)
(("" (rewrite "limit_nonempty") (("" (inst + "n!1") nil nil)) nil))
nil)
((limit_nonempty formula-decl nil csequence_limit 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)
(T formal-type-decl nil csequence_limit nil)
(csequence type-decl nil csequence_codt nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(ascending_chain type-eq-decl nil ascending_chains nil))
nil))
(limit_first 0
(limit_first-1 nil 3513785517
("" (skosimp)
(("" (expand* "limit" "limit_struct" "coreduce")
(("" (reduce)
(("" (typepred "min({n | nonempty?(chain!1(n))})")
(("1" (inst - "n!1")
(("1" (assert)
(("1" (lemma "ascending_chain?_nth")
(("1"
(inst - "chain!1" "min({n | nonempty?(chain!1(n))})"
"n!1" 0)
(("1" (assert)
(("1" (expand* "index?" "nth")
(("1" (assert) nil nil)) nil))
nil)
("2" (expand* "nonempty?" "empty?" "member")
(("2" (inst - "n!1") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand* "nonempty?" "empty?" "member")
(("2" (inst - "n!1") nil nil)) nil))
nil))
nil))
nil))
nil)
((limit_struct const-decl "csequence_struct[T, ascending_chain]"
csequence_limit nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(limit const-decl "csequence" csequence_limit nil)
(min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_nat nil)
(<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_limit nil)
(chain!1 skolem-const-decl "ascending_chain[csequence, prefix?]"
csequence_limit nil)
(nth def-decl "T" csequence_nth nil)
(index? def-decl "bool" csequence_nth nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(ascending_chain?_nth formula-decl nil csequence_limit nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans 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))
shostak))
(limit_rest_chain 0
(limit_rest_chain-1 nil 3513785594
("" (skosimp)
(("" (expand* "limit" "limit_struct")
(("" (expand "coreduce" -)
(("" (expand "coreduce" 1 1) (("" (reduce) nil nil)) nil))
nil))
nil))
nil)
((limit_struct const-decl "csequence_struct[T, ascending_chain]"
csequence_limit nil)
(limit const-decl "csequence" csequence_limit nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil))
shostak))
(limit_suffix_chain 0
(limit_suffix_chain-1 nil 3513785625
("" (induct "n")
(("1" (skolem!)
(("1" (expand* "suffix_chain" "suffix")
(("1" (replace-eta "chain!1") nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (expand "suffix_chain")
(("2" (expand "suffix" +)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "limit" +)
(("1" (expand* "limit_struct" "coreduce")
(("1" (smash)
(("1" (skolem!)
(("1" (inst - "n!1") (("1" (assert) nil nil))
nil))
nil)
("2" (skolem!)
(("2" (inst - "n!1") (("2" (assert) nil nil))
nil))
nil)
("3" (skolem!)
(("3" (inst - "n!1")
(("3" (assert)
(("3" (hide -3 2)
(("3"
(expand* "limit" "limit_struct"
"coreduce")
(("3"
(lift-if)
(("3" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (hide -2 -3 2 3)
(("4" (expand* "limit" "limit_struct" "coreduce")
(("4" (lift-if) (("4" (ground) nil nil)) nil))
nil))
nil)
("5" (hide -2 2 3 4)
(("5" (expand* "limit" "limit_struct" "coreduce")
(("5" (lift-if) (("5" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst - "rest_chain(chain!1)")
(("2" (use "limit_rest_chain")
(("2" (assert)
(("2" (replace -1 :dir rl)
(("2"
(case-replace
"(LAMBDA m: suffix(rest_chain(chain!1)(m), j!1)) = (LAMBDA m: IF empty?(chain!1(m)) THEN chain!1(m) ELSE suffix(rest(chain!1(m)), j!1) ENDIF)")
(("1" (hide -1 -2 3)
(("1" (decompose-equality)
(("1" (lift-if)
(("1"
(ground)
(("1"
(expand* "rest_chain" "suffix")
(("1" (assert) nil nil))
nil)
("2"
(expand "rest_chain")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2" (skosimp)
(("2"
(expand "rest_chain")
(("2" (assert) nil nil))
nil))
nil)
("3" (skosimp) (("3" (assert) nil nil))
nil)
("4" (skosimp)
(("4"
(expand* "rest_chain" "suffix?")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(limit_struct const-decl "csequence_struct[T, ascending_chain]"
csequence_limit nil)
(limit_rest_chain formula-decl nil csequence_limit nil)
(suffix?_is_preorder name-judgement "(preorder?[csequence])"
csequence_limit nil)
(j!1 skolem-const-decl "nat" csequence_limit nil)
(chain!1 skolem-const-decl "ascending_chain[csequence, prefix?]"
csequence_limit nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(rest_chain const-decl "ascending_chain" csequence_limit nil)
(nat_induction formula-decl nil naturalnumbers nil)
(suffix_chain const-decl "ascending_chain" csequence_limit nil)
(limit const-decl "csequence" csequence_limit nil)
(suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))"
csequence_suffix nil)
(suffix? inductive-decl "bool" csequence_suffix nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_limit 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))
(limit_lub 0
(limit_lub-1 nil 3513785904
("" (skolem!)
(("" (expand "least_upperbound?")
(("" (split)
(("1" (expand "upperbound?")
(("1" (skolem!)
(("1" (rewrite "prefix?_prefix")
(("1" (flatten)
(("1" (lemma "coinduction")
(("1"
(inst -
"LAMBDA (cseq1, cseq2: csequence): EXISTS chain, n: cseq1 = chain(n) AND cseq2 = limit(chain) AND NOT (EXISTS m: chain(n) = prefix(limit(chain), m))"
"chain!1(n!1)" "limit(chain!1)")
(("1" (assert)
(("1" (inst + "chain!1" "n!1") nil nil)) nil)
("2" (delete 2 3)
(("2" (expand "bisimulation?")
(("2" (skosimp*)
(("2" (replace*)
(("2" (hide -1 -2)
(("2"
(smash)
(("1"
(inst + 0)
(("1"
(expand "prefix")
(("1" (assert) nil nil))
nil))
nil)
("2"
(rewrite "limit_empty")
(("2"
(inst - "n!2")
(("2" (assert) nil nil))
nil))
nil)
("3"
(inst + "rest_chain(chain!2)" "n!2")
(("3"
(rewrite "limit_rest_chain")
(("1"
(expand "rest_chain" 2 1)
(("1"
(skolem!)
(("1"
(use "limit_rest_chain")
(("1"
(split)
(("1"
(replace -1 :dir rl)
(("1"
(hide -1)
(("1"
(inst + "1 + m!1")
(("1"
(expand "prefix" +)
(("1"
(lift-if)
(("1"
(prop)
(("1"
(rewrite
"limit_empty")
(("1"
(inst
-
"n!2")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"rest_chain"
-)
(("2"
(decompose-equality)
(("2"
(forward-chain
"limit_first")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"limit_nonempty")
(("2"
(inst + "n!2")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "limit_nonempty")
(("2" (inst + "n!2") nil nil))
nil))
nil))
nil)
("4"
(forward-chain "limit_first")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "prefix?_coinduction")
(("2"
(inst -
"LAMBDA (cseq1, cseq2: csequence): EXISTS chain: cseq1 = limit(chain) AND upperbound?(chain)(cseq2)")
(("2" (split)
(("1" (skosimp)
(("1" (inst - "limit(chain!1)" "u!1")
(("1" (assert) (("1" (inst + "chain!1") nil nil))
nil))
nil))
nil)
("2" (delete 2)
(("2" (skosimp*)
(("2" (replace -1)
(("2" (hide -1)
(("2" (rewrite "limit_empty")
(("2" (skolem!)
(("2" (ground)
(("1" (expand* "upperbound?" "prefix?")
(("1" (inst - "n!1") nil nil)) nil)
("2"
(expand* "limit" "limit_struct"
"coreduce")
(("2"
(reduce)
(("2"
(expand* "upperbound?" "prefix?")
(("2"
(inst
-
"min({n | nonempty?(chain!2(n))})")
(("1" (assert) nil nil)
("2"
(expand*
"nonempty?"
"empty?"
"member")
(("2"
(inst - "n!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (inst + "rest_chain(chain!2)")
(("3"
(rewrite "limit_rest_chain")
(("1"
(expand "upperbound?")
(("1"
(skolem!)
(("1"
(inst - "n!2")
(("1"
(expand "prefix?" -)
(("1"
(expand "rest_chain" 2)
(("1"
(lift-if)
(("1"
(expand "prefix?" 2 1)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "limit_nonempty")
(("2"
(inst + "n!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((least_upperbound? const-decl "bool" ascending_chains nil)
(prefix?_coinduction formula-decl nil csequence_prefix nil)
(limit_struct const-decl "csequence_struct[T, ascending_chain]"
csequence_limit nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_nat nil)
(chain!2 skolem-const-decl "ascending_chain[csequence, prefix?]"
csequence_limit nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(prefix?_is_partial_order name-judgement
"(partial_order?[csequence])" csequence_limit nil)
(upperbound? const-decl "bool" ascending_chains nil)
(prefix?_prefix formula-decl nil csequence_prefix nil)
(csequence type-decl nil csequence_codt 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)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(limit const-decl "csequence" csequence_limit nil)
(T formal-type-decl nil csequence_limit nil)
(coinduction formula-decl nil csequence_codt nil)
(rest_chain const-decl "ascending_chain" csequence_limit nil)
(limit_nonempty formula-decl nil csequence_limit nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(limit_first formula-decl nil csequence_limit nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(csequence_add_extensionality formula-decl nil csequence_codt nil)
(add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
csequence_codt nil)
(first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(limit_rest_chain formula-decl nil csequence_limit nil)
(limit_empty formula-decl nil csequence_limit nil)
(PRED type-eq-decl nil defined_types nil)
(bisimulation? adt-def-decl "boolean" csequence_codt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(is_finite inductive-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(prefix def-decl "{fseq | prefix?(fseq, cseq)}" csequence_prefix
nil))
shostak))
(limit_nth 0
(limit_nth-1 nil 3513786305
("" (skosimp)
(("" (use "limit_lub")
(("" (expand "least_upperbound?")
(("" (flatten)
(("" (expand "upperbound?" -1)
(("" (inst - "n!1")
(("" (forward-chain "prefix?_index")
(("" (use "prefix?_nth") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((limit_lub formula-decl nil csequence_limit nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_limit 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)
(prefix?_nth formula-decl nil csequence_prefix nil)
(indexes type-eq-decl nil csequence_nth nil)
(m!1 skolem-const-decl "nat" csequence_limit nil)
(n!1 skolem-const-decl "nat" csequence_limit nil)
(chain!1 skolem-const-decl "ascending_chain[csequence, prefix?]"
csequence_limit nil)
(index? def-decl "bool" csequence_nth nil)
(prefix?_is_partial_order name-judgement
"(partial_order?[csequence])" csequence_limit nil)
(prefix?_index formula-decl nil csequence_prefix nil)
(limit const-decl "csequence" csequence_limit nil)
(upperbound? const-decl "bool" ascending_chains nil)
(least_upperbound? const-decl "bool" ascending_chains nil))
shostak))
(limit_def 0
(limit_def-1 nil 3513786368
("" (skolem!)
(("" (prop)
(("1" (skolem!)
(("1" (use "limit_lub")
(("1" (replace -2)
(("1" (expand "least_upperbound?")
(("1" (prop)
(("1" (use "limit_suffix_chain")
(("1"
(lemma "limit_empty"
("chain" "suffix_chain(chain!1, n!1)"))
(("1" (prop)
(("1" (inst - "n!1")
(("1" (expand "suffix_chain" -2)
(("1" (replace -3 -1 :dir rl)
(("1" (rewrite "suffix_empty" -1)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (skolem!)
(("2" (inst + "n!2")
(("2" (expand "suffix_chain" 1)
(("2" (rewrite "suffix_empty")
(("2"
(assert)
(("2"
(forward-chain "limit_nth")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (forward-chain "limit_nth")
(("2" (assert) nil nil)) nil))
nil)
("3" (skosimp)
(("3" (forward-chain "limit_nth")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "coinduction")
(("2"
(inst -
"LAMBDA (cseq1, cseq2: csequence): EXISTS chain: cseq1 = limit(chain) AND (FORALL t, n: index?(cseq2)(n) AND nth(cseq2, n) = t IFF (EXISTS m: index?(chain(m))(n) AND nth(chain(m), n) = t))"
"limit(chain!1)" "cseq!1")
(("1" (assert) (("1" (inst + "chain!1") nil nil)) nil)
("2" (delete -1 2)
(("2" (expand "bisimulation?")
(("2" (skosimp*)
(("2" (replace -1)
(("2" (hide -1)
(("2" (case "empty?(y!1)")
(("1" (reduce)
(("1" (rewrite "limit_empty")
(("1" (skolem!)
(("1" (inst - "first(chain!2(n!1))" 0)
(("1"
(expand* "index?" "nth")
(("1"
(inst + "n!1")
(("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (smash)
(("1" (rewrite "limit_empty")
(("1" (inst - "first(y!1)" 0)
(("1" (expand* "index?" "nth")
(("1"
(skosimp)
(("1"
(inst - "m!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "rest_chain(chain!2)")
(("2" (rewrite "limit_rest_chain")
(("1" (skolem!)
(("1"
(prop)
(("1"
(inst
-
"nth(y!1, n!1 + 1)"
"n!1 + 1")
(("1"
(expand "index?" -4)
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst + "m!1")
(("1"
(expand "rest_chain")
(("1"
(expand "nth" -6)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "index?" 1)
(("2" (propax) nil nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand "rest_chain")
(("2"
(lift-if)
(("2"
(ground)
(("1"
(expand "index?" -4)
(("1" (propax) nil nil))
nil)
("2"
(inst - "t!1" "n!1 + 1")
(("2"
(expand "index?" -4)
(("2"
(expand "nth" +)
(("2"
(inst + "m!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(expand "rest_chain")
(("3"
(lift-if)
(("3"
(ground)
(("1"
(expand "index?" -4)
(("1" (propax) nil nil))
nil)
("2"
(inst - "t!1" "n!1 + 1")
(("2"
(expand "index?" -4)
(("2"
(expand "nth" -4)
(("2"
(inst + "m!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "limit_nonempty")
(("2"
(inst - "first(y!1)" 0)
(("2"
(expand "index?" -)
(("2"
(expand "nth" -)
(("2"
(skosimp)
(("2" (inst + "m!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (inst - "first(y!1)" 0)
(("3" (expand "index?" -)
(("3" (expand "nth" -)
(("3"
(skosimp)
(("3"
(forward-chain "limit_first")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((limit_lub formula-decl nil csequence_limit nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_limit 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)
(least_upperbound? const-decl "bool" ascending_chains nil)
(limit_suffix_chain formula-decl nil csequence_limit nil)
(limit const-decl "csequence" csequence_limit nil)
(suffix_empty formula-decl nil csequence_suffix nil)
(limit_nth formula-decl nil csequence_limit nil)
(suffix_chain const-decl "ascending_chain" csequence_limit nil)
(limit_empty formula-decl nil csequence_limit nil)
(nth def-decl "T" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(index? def-decl "bool" csequence_nth nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bisimulation? adt-def-decl "boolean" csequence_codt nil)
(PRED type-eq-decl nil defined_types nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(chain!2 skolem-const-decl "ascending_chain[csequence, prefix?]"
csequence_limit nil)
(n!1 skolem-const-decl "nat" csequence_limit nil)
(first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
(limit_first formula-decl nil csequence_limit nil)
(rest_chain const-decl "ascending_chain" csequence_limit nil)
(limit_nonempty formula-decl nil csequence_limit nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(y!1 skolem-const-decl "csequence[T]" csequence_limit nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(n!1 skolem-const-decl "nat" csequence_limit nil)
(limit_rest_chain formula-decl nil csequence_limit nil)
(coinduction formula-decl nil csequence_codt nil))
shostak))
(limit_prefix_chain 0
(limit_prefix_chain-1 nil 3513786783
("" (skolem!)
(("" (rewrite "limit_def")
(("" (expand "prefix_chain")
(("" (skolem!)
(("" (prop)
(("1" (inst + "n!1 + 1")
(("1" (rewrite "prefix_index")
(("1" (assert)
(("1" (lemma "prefix?_nth")
(("1"
(inst - "prefix(cseq!1, 1 + n!1)" "cseq!1" "n!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (rewrite "prefix_index") (("2" (flatten) nil nil))
nil))
nil)
("3" (skosimp)
(("3" (rewrite "prefix_index")
(("3" (flatten)
(("3" (lemma "prefix?_nth")
(("3" (inst - "prefix(cseq!1, m!1)" "cseq!1" "n!1")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((limit_def formula-decl nil csequence_limit 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)
(T formal-type-decl nil csequence_limit nil)
(csequence type-decl nil csequence_codt nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(ascending_chain type-eq-decl nil ascending_chains nil)
(prefix_chain const-decl "ascending_chain" csequence_limit nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(indexes type-eq-decl nil csequence_nth nil)
(index? def-decl "bool" csequence_nth nil)
(prefix def-decl "{fseq | prefix?(fseq, cseq)}" csequence_prefix
nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(prefix?_is_partial_order name-judgement
"(partial_order?[csequence])" csequence_limit nil)
(prefix?_nth formula-decl nil csequence_prefix nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(prefix_index formula-decl nil csequence_prefix nil))
shostak))
(limit_prefix_compact_TCC1 0
(limit_prefix_compact_TCC1-1 nil 3513785036
("" (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)
(T formal-type-decl nil csequence_limit nil)
(csequence type-decl nil csequence_codt nil)
(prefix? coinductive-decl "bool" csequence_prefix nil)
(ascending_chain? const-decl "bool" ascending_chains nil)
(ascending_chain type-eq-decl nil ascending_chains 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))
(limit_prefix_compact 0
(limit_prefix_compact-1 nil 3513786874
("" (induct "n")
(("1" (skosimp)
(("1" (inst + 0) (("1" (expand* "prefix" "prefix?") nil nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2" (expand "prefix" +)
(("2" (expand "prefix?" +)
(("2" (assert)
(("2" (inst - "rest(cseq!1)" "rest_chain(chain!1)")
(("1" (expand "rest_chain")
(("1" (expand "index?" -2)
(("1" (case "j!1 = 0")
(("1" (smash)
(("1" (skolem!)
(("1" (lift-if)
(("1" (ground)
(("1"
(expand*
"prefix"
"prefix"
"prefix?"
"prefix?")
(("1"
(flatten)
(("1"
(hide -2)
(("1"
(rewrite "limit_nonempty")
(("1"
(skolem!)
(("1"
(inst + "n!1")
(("1"
(assert)
(("1"
(forward-chain
"limit_first")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.361 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.
|
