|
(csequence_nth
(index?_TCC1 0
(index?_TCC1-1 nil 3513452743 ("" (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))
(index?_TCC2 0
(index?_TCC2-1 nil 3513452743 ("" (termination-tcc) nil nil) nil
nil))
(index?_0 0
(index?_0-1 nil 3513452758
("" (expand "index?") (("" (propax) nil nil)) nil)
((index? def-decl "bool" csequence_nth nil)) shostak))
(index?_ub 0
(index?_ub-1 nil 3513452798
("" (induct "n")
(("1" (expand* "index?" "is_finite") (("1" (reduce) nil nil)) nil)
("2" (skosimp*)
(("2" (expand "index?" +)
(("2" (expand "is_finite" +)
(("2" (inst - "rest(cseq!1)") (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
((nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(is_finite inductive-decl "bool" csequence_props nil)
(index? def-decl "bool" csequence_nth nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth 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))
(index?_lt 0
(index?_lt-1 nil 3513452862
("" (measure-induct+ "i" ("cseq" "i"))
(("" (typepred "x!2")
(("" (skosimp)
(("" (expand "index?" (-1 +))
(("" (ground)
(("" (inst - "rest(x!1)" "x!2 - 1")
(("" (inst - "n!1 - 1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(indexes type-eq-decl nil csequence_nth nil)
(index? def-decl "bool" csequence_nth 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)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(index?_finite 0
(index?_finite-1 nil 3513452922
("" (induct "fseq" :name "is_finite_induction")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (skosimp*)
(("3" (expand "index?" +)
(("3" (expand "length" +)
(("3" (lift-if)
(("3" (ground)
(("1" (inst - "n!1 - 1") (("1" (assert) nil nil)) nil)
("2" (inst - "n!1 - 1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(is_finite_induction formula-decl nil csequence_props nil)
(T formal-type-decl nil csequence_nth nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(has_length def-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(< const-decl "bool" reals nil)
(index? def-decl "bool" csequence_nth nil)
(IFF const-decl "[bool, bool -> bool]" booleans 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)
(is_finite inductive-decl "bool" csequence_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil))
shostak))
(index?_finite_bound 0
(index?_finite_bound-1 nil 3513452978
("" (skolem!)
(("" (use "index?_finite")
(("" (assert) (("" (inst + "length(fseq!1)") nil nil)) nil))
nil))
nil)
((index?_finite formula-decl nil csequence_nth nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props 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_nth nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(has_length def-decl "bool" csequence_props 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(index?_infinite 0
(index?_infinite-1 nil 3513453017
("" (induct "n")
(("1" (skolem-typepred)
(("1" (expand* "index?" "is_finite") (("1" (assert) nil nil))
nil))
nil)
("2" (skosimp* t)
(("2" (expand "is_finite" +)
(("2" (expand "index?" +)
(("2" (ground) (("2" (inst - "rest(iseq!1)") nil nil)) nil))
nil))
nil))
nil))
nil)
((rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(index? def-decl "bool" csequence_nth nil)
(infinite_csequence type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth 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))
(index?_infinite_full 0
(index?_infinite_full-1 nil 3513453068
("" (skolem!)
(("" (expand* "full?" "member")
(("" (prop)
(("1" (use "index?_infinite") nil nil)
("2" (use "index?_finite")
(("2" (inst - "length(cseq!1)") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(full? const-decl "bool" sets nil)
(index?_finite formula-decl nil csequence_nth nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(has_length def-decl "bool" csequence_props 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(cseq!1 skolem-const-decl "csequence[T]" csequence_nth nil)
(infinite_csequence type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(NOT const-decl "[bool -> bool]" booleans 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_nth nil)
(index?_infinite formula-decl nil csequence_nth nil))
shostak))
(index?_prop 0
(index?_prop-1 nil 3513453116
("" (skolem!)
(("" (use "index?_ub")
(("" (rewrite "index?_finite") (("" (ground) nil nil)) nil))
nil))
nil)
((index?_ub formula-decl nil csequence_nth 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)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(index?_finite formula-decl nil csequence_nth nil))
shostak))
(index?_nonempty 0
(index?_nonempty-1 nil 3513453138
("" (skolem-typepred)
(("" (expand "index?") (("" (flatten) nil nil)) nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(indexes type-eq-decl nil csequence_nth nil)
(index? def-decl "bool" csequence_nth 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)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(nth_TCC1 0
(nth_TCC1-1 nil 3513452743
("" (skosimp) (("" (use "index?_nonempty") nil nil)) nil)
((T formal-type-decl nil csequence_nth 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)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(index?_nonempty formula-decl nil csequence_nth nil))
nil))
(nth_TCC2 0
(nth_TCC2-1 nil 3513452743
("" (skosimp) (("" (use "index?_nonempty") nil nil)) nil)
((T formal-type-decl nil csequence_nth 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)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(index?_nonempty formula-decl nil csequence_nth nil))
nil))
(nth_TCC3 0
(nth_TCC3-1 nil 3513452743
("" (skosimp :preds? t)
(("" (assert)
(("" (expand "index?" -) (("" (propax) nil nil)) nil)) nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil csequence_nth nil)
(csequence type-decl nil csequence_codt 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)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil))
nil))
(nth_TCC4 0
(nth_TCC4-1 nil 3513452743 ("" (termination-tcc) nil nil) nil nil))
(nth_extensionality_TCC1 0
(nth_extensionality_TCC1-1 nil 3513452743 ("" (subtype-tcc) nil nil)
((indexes type-eq-decl nil csequence_nth nil)
(index? def-decl "bool" csequence_nth 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)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(nth_extensionality 0
(nth_extensionality-1 nil 3513453402
("" (skosimp)
(("" (lemma "coinduction")
((""
(inst -
"LAMBDA cseq1, cseq2: index?(cseq1) = index?(cseq2) AND (FORALL (n: indexes(cseq1)): nth(cseq1, n) = nth(cseq2, n))"
"cseq1!1" "cseq2!1")
(("1" (assert) nil nil)
("2" (delete -1 -2 2)
(("2" (expand "bisimulation?")
(("2" (skosimp)
(("2" (lemma "index?_0")
(("2" (inst-cp - "y!1")
(("2" (inst - "x!1")
(("2" (smash)
(("1" (skolem!)
(("1" (inst - "1 + n!1")
(("1" (expand "nth" -)
(("1" (propax) nil nil)) nil)
("2" (expand "index?" +)
(("2" (propax) nil nil)) nil))
nil))
nil)
("2" (decompose-equality)
(("2" (decompose-equality)
(("2" (inst - "1 + x!2")
(("2" (expand "index?" -)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil)
("3" (inst - 0)
(("3" (expand "nth") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*) (("3" (assert) nil nil)) nil))
nil))
nil))
nil)
((T formal-type-decl nil csequence_nth nil)
(coinduction formula-decl nil csequence_codt nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(x!1 skolem-const-decl "csequence[T]" csequence_nth nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(n!1 skolem-const-decl "indexes(rest(x!1))" csequence_nth nil)
(index?_0 formula-decl nil csequence_nth 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)
(nth def-decl "T" csequence_nth nil)
(csequence type-decl nil csequence_codt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil))
shostak))
(nth_every 0
(nth_every-1 nil 3513453611
("" (skolem!)
(("" (prop)
(("1" (skolem-typepred)
(("1" (generalize-skolem-constants)
(("1" (skolem + ("_" "_" "p"))
(("1"
(measure-induct+ "i_1" ("cseq_1" "i_1")
:skolem-typepreds? t)
(("1" (expand "index?")
(("1" (expand "every" -3)
(("1" (expand "nth" +)
(("1" (lift-if)
(("1" (ground)
(("1" (inst - "rest(x!1)" "x!2 - 1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (iff) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (lemma "every_weak_coinduction")
(("2"
(inst - "p!1"
"LAMBDA cseq: FORALL (i: indexes(cseq)): p!1(nth(cseq, i))")
(("2" (split)
(("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil)
("2" (delete -1 2)
(("2" (skosimp)
(("2" (lift-if)
(("2" (ground)
(("1" (inst - 0)
(("1" (expand "nth") (("1" (propax) nil nil))
nil)
("2" (expand "index?") (("2" (propax) nil nil))
nil))
nil)
("2" (skolem!)
(("2" (inst - "1 + i!1")
(("1" (expand "nth" -) (("1" (propax) nil nil))
nil)
("2" (expand "index?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nth def-decl "T" csequence_nth nil)
(pred type-eq-decl nil defined_types nil)
(every coinductive-decl "boolean" csequence_codt nil)
(PRED type-eq-decl nil defined_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(well_founded? const-decl "bool" orders nil)
(< const-decl "bool" reals nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(measure_induction formula-decl nil measure_induction nil)
(wf_nat formula-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(TRUE const-decl "bool" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(indexes type-eq-decl nil csequence_nth nil)
(index? def-decl "bool" csequence_nth 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)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(i!1 skolem-const-decl "indexes(rest(a!1))" csequence_nth nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(a!1 skolem-const-decl "csequence[T]" csequence_nth nil)
(every_weak_coinduction formula-decl nil csequence_codt nil))
shostak))
(nth_some 0
(nth_some-1 nil 3513453839
("" (skolem!)
(("" (prop)
(("1" (lemma "some_weak_induction")
(("1"
(inst - "p!1"
"LAMBDA cseq: EXISTS (i: indexes(cseq)): p!1(nth(cseq, i))")
(("1" (split)
(("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil)
("2" (delete -1 2)
(("2" (skosimp)
(("2" (lift-if)
(("2" (ground)
(("1" (inst + 0)
(("1" (expand "nth") (("1" (propax) nil nil))
nil)
("2" (expand "index?") (("2" (propax) nil nil))
nil))
nil)
("2" (skolem!)
(("2" (inst + "1 + i!1")
(("1" (expand "nth" +) (("1" (propax) nil nil))
nil)
("2" (expand "index?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skolem-typepred)
(("2" (generalize-skolem-constants)
(("2" (skolem + ("_" "_" "p"))
(("2"
(measure-induct+ "i_1" ("cseq_1" "i_1")
:skolem-typepreds? t)
(("1" (expand "index?")
(("1" (expand "some" +)
(("1" (expand "nth" -3)
(("1" (lift-if)
(("1" (ground)
(("1" (inst - "rest(x!1)" "x!2 - 1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (iff) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(pred type-eq-decl nil defined_types nil)
(csequence type-decl nil csequence_codt 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)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(nth def-decl "T" csequence_nth nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(i!1 skolem-const-decl "indexes(rest(a!1))" csequence_nth nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(a!1 skolem-const-decl "csequence[T]" csequence_nth nil)
(some_weak_induction formula-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth nil)
(some inductive-decl "boolean" csequence_codt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(well_founded? const-decl "bool" orders nil)
(< const-decl "bool" reals nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(measure_induction formula-decl nil measure_induction nil)
(wf_nat formula-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(TRUE const-decl "bool" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(last_TCC1 0
(last_TCC1-1 nil 3513452743
("" (skolem-typepred)
(("" (rewrite "length_nonempty?_rew")
(("" (assert) (("" (rewrite "index?_finite") nil nil)) nil))
nil))
nil)
((length_nonempty?_rew formula-decl nil csequence_length nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(index?_finite formula-decl nil csequence_nth 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(has_length def-decl "bool" csequence_props nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nonempty_finite_csequence type-eq-decl nil csequence_props nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_nth nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(last_rest_TCC1 0
(last_rest_TCC1-1 nil 3513452743
("" (skosimp :preds? t)
(("" (expand "is_finite" -) (("" (assert) nil 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)
(T formal-type-decl nil csequence_nth nil)
(csequence type-decl nil csequence_codt nil)
(is_finite inductive-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(nonempty_finite_csequence type-eq-decl nil csequence_props nil))
nil))
(last_rest 0
(last_rest-1 nil 3513454103
("" (induct "nfseq" :name "is_finite_induction")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (assert) nil nil)
("4" (skosimp)
(("4" (expand "last")
(("4" (expand "length" 2 2)
(("4" (expand "nth" 2 2)
(("4" (lemma "length_empty?_rew" ("cseq" "rest(cseq!1)"))
(("4" (reduce) nil nil)) nil))
nil))
nil))
nil))
nil)
("5" (skosimp) (("5" (forward-chain "last_rest_TCC1") nil nil))
nil))
nil)
((last_rest_TCC1 subtype-tcc nil csequence_nth nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(length_empty?_rew formula-decl nil csequence_length nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nth def-decl "T" csequence_nth nil)
(is_finite_induction formula-decl nil csequence_props nil)
(T formal-type-decl nil csequence_nth nil)
(last const-decl "T" csequence_nth nil)
(nonempty_finite_csequence type-eq-decl nil csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(is_finite inductive-decl "bool" csequence_props nil))
shostak)))
¤ Dauer der Verarbeitung: 0.48 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.
|
