|
(csequence_extract
(caret_TCC1 0
(caret_TCC1-1 nil 3513606610 ("" (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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(caret_TCC2 0
(caret_TCC2-1 nil 3513606610 ("" (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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(caret_TCC3 0
(caret_TCC3-1 nil 3513606610 ("" (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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(caret_TCC4 0
(caret_TCC4-1 nil 3513606610 ("" (termination-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)
(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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(caret_TCC5 0
(caret_TCC5-1 nil 3513606610 ("" (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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(caret_TCC6 0
(caret_TCC6-1 nil 3513606610 ("" (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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(caret_TCC7 0
(caret_TCC7-1 nil 3513606610 ("" (termination-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)
(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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(caret_TCC8 0
(caret_TCC8-1 nil 3513606610 ("" (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)
(add_finite application-judgement "nonempty_finite_csequence[T]"
csequence_extract nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(extract_empty 0
(extract_empty-1 nil 3513606633
("" (measure-induct+ "range`2" ("range"))
(("" (skolem!)
(("" (expand "^" +)
(("" (expand "is_finite" +)
(("" (expand "index?" +) (("" (reduce) nil nil)) nil)) nil))
nil))
nil))
nil)
((even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(add_finite application-judgement "nonempty_finite_csequence[T]"
csequence_extract nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(cseq!1 skolem-const-decl "csequence[T]" csequence_extract nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(x!1 skolem-const-decl "[nat, nat]" csequence_extract nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(index? def-decl "bool" csequence_nth nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_extract nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(naturalnumber type-eq-decl nil naturalnumbers 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)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(extract_nonempty 0
(extract_nonempty-1 nil 3513606721
("" (skolem!)
(("" (use "extract_empty") (("" (ground) nil nil)) nil)) nil)
((extract_empty formula-decl nil csequence_extract 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_extract nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(extract_length 0
(extract_length-1 nil 3513606732
("" (measure-induct+ "range`2" ("range"))
(("" (skolem!)
(("" (smash)
(("1" (use "length_empty?_rew")
(("1" (expand "^") (("1" (flatten) nil nil)) nil)) nil)
("2" (use "extract_empty")
(("2" (assert)
(("2" (rewrite "index?_prop")
(("2" (assert)
(("2" (rewrite "length_empty?_rew") nil nil)) nil))
nil))
nil))
nil)
("3" (expand "^" +)
(("3" (expand "length" 3 1)
(("3" (expand "length" 3 2)
(("3" (expand "length" 3 3)
(("3" (expand "length" (-3 2))
(("3" (expand "is_finite" -2)
(("3" (lift-if)
(("3" (ground)
(("1" (inst - "(x!1`1 - 1, x!1`2 - 1)")
(("1" (inst - "rest(cseq!1)")
(("1" (assert) nil nil)) nil))
nil)
("2" (inst - "(x!1`1, x!1`2 - 1)")
(("2" (inst - "rest(cseq!1)")
(("2" (assert)
(("2"
(lift-if)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "^" +)
(("4" (expand "length" 4 1)
(("4" (expand "length" 4 2)
(("4" (expand "length" 4 2)
(("4" (expand "length" (2 3))
(("4" (lift-if)
(("4" (ground)
(("1" (inst - "(x!1`1 - 1, x!1`2 - 1)")
(("1" (inst - "rest(cseq!1)")
(("1" (assert) nil nil)) nil))
nil)
("2" (inst - "(x!1`1, x!1`2 - 1)")
(("2" (inst - "rest(cseq!1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (expand "^" +)
(("5" (expand "length" 3 1)
(("5" (expand "length" 3 2)
(("5" (expand "length" 3 2)
(("5" (expand "is_finite" +)
(("5" (lift-if)
(("5" (ground)
(("1" (inst - "(x!1`1 - 1, x!1`2 - 1)")
(("1" (inst - "rest(cseq!1)")
(("1" (assert) nil nil)) nil))
nil)
("2" (inst - "(x!1`1, x!1`2 - 1)")
(("2" (inst - "rest(cseq!1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(extract_empty formula-decl nil csequence_extract nil)
(index?_prop formula-decl nil csequence_nth nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(length_empty?_rew formula-decl nil csequence_length nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(^ def-decl "finite_csequence" csequence_extract 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)
(is_finite inductive-decl "bool" csequence_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_extract nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(naturalnumber type-eq-decl nil naturalnumbers 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)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(extract_def 0
(extract_def-1 nil 3513607023
("" (induct "nfseq" :name "is_finite_induction")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (assert) nil nil)
("4" (skosimp*)
(("4" (expand "^" +)
(("4" (expand "length" -4)
(("4" (use "length_empty?_rew")
(("4" (lift-if)
(("4" (ground)
(("1" (decompose-equality)
(("1"
(lemma "length_empty?_rew" ("cseq" "rest(cseq!1)"))
(("1" (assert) nil nil)) nil))
nil)
("2" (decompose-equality 2)
(("2" (inst - "n!1 - 1") (("2" (assert) nil nil))
nil))
nil)
("3" (decompose-equality) nil nil)
("4" (decompose-equality 2)
(("4" (expand "^") (("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
(add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
csequence_codt nil)
(csequence_add_extensionality formula-decl nil csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(add_finite application-judgement "nonempty_finite_csequence[T]"
csequence_extract nil)
(length_empty?_rew formula-decl nil csequence_length nil)
(nonempty_finite_csequence type-eq-decl nil csequence_props nil)
(is_finite_induction formula-decl nil csequence_props nil)
(T formal-type-decl nil csequence_extract nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(= const-decl "[T, T -> boolean]" equalities 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(is_finite inductive-decl "bool" csequence_props nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(extract_rest_TCC1 0
(extract_rest_TCC1-1 nil 3513606610
("" (skolem-typepred)
(("" (rewrite "length_nonempty?_rew") (("" (assert) 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_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_extract nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(extract_rest 0
(extract_rest-1 nil 3513607165
("" (skolem!)
(("" (use "extract_rest_TCC1")
(("" (use "extract_def" ("n" "length(nfseq!1) - 1"))
(("" (assert)
(("" (expand "^")
(("" (lift-if)
(("" (ground)
(("1" (decompose-equality -) nil nil)
("2" (decompose-equality -) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extract_rest_TCC1 subtype-tcc nil csequence_extract 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)
(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_extract nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
csequence_codt nil)
(first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(add_finite application-judgement "nonempty_finite_csequence[T]"
csequence_extract nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(has_length def-decl "bool" csequence_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(extract_def formula-decl nil csequence_extract nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(extract_rest2 0
(extract_rest2-1 nil 3513607229
("" (induct "n")
(("1" (expand "^") (("1" (reduce) nil nil)) nil)
("2" (skosimp*)
(("2" (expand "^" (-2 +))
(("2" (smash)
(("1" (inst - "rest(cseq!1)" "m!1 - 1")
(("1" (assert)
(("1" (replace -1)
(("1" (expand "^" +) (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (inst - "rest(cseq!1)" "m!1 - 1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(add_finite application-judgement "nonempty_finite_csequence[T]"
csequence_extract nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_extract 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(extract_extract 0
(extract_extract-1 nil 3513607305
("" (measure-induct+ "range`2" ("range"))
(("" (skolem!)
(("" (expand "^" 1 1)
(("" (lift-if)
(("" (ground)
(("1" (expand "^") (("1" (propax) nil nil)) nil)
("2" (expand "^") (("2" (propax) nil nil)) nil)
("3" (inst - "(x!1`1 - 1, x!1`2 - 1)")
(("3" (inst - "rest(cseq!1)" "range2!1")
(("3" (assert)
(("3" (replace -2)
(("3" (hide -2)
(("3" (expand "^" 1 2)
(("3" (expand* "^" "min")
(("3" (reduce) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (hide -2)
(("4" (expand "^" 1 2)
(("4" (expand* "^" "^" "min") (("4" (reduce) nil nil))
nil))
nil))
nil)
("5" (expand "^" 2 2)
(("5" (lift-if)
(("5" (ground)
(("1" (expand* "^" "min") nil nil)
("2" (inst - "(x!1`1, x!1`2 - 1)")
(("2"
(inst - "rest(cseq!1)"
"(range2!1`1 - 1, range2!1`2 - 1)")
(("2" (assert)
(("2" (replace -2)
(("2" (hide -2)
(("2" (expand "^" 1 2)
(("2"
(expand* "^" "min")
(("2" (reduce) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand* "^" "min") nil nil)
("4" (inst - "(x!1`1, x!1`2 - 1)")
(("4"
(inst - "rest(cseq!1)"
"(range2!1`1, range2!1`2 - 1)")
(("4" (assert)
(("4" (replace -1)
(("4" (hide -1)
(("4" (expand "^" 2 2)
(("4"
(expand "min")
(("4" (reduce) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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_plus_int_is_int application-judgement "int" integers nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(add_finite application-judgement "nonempty_finite_csequence[T]"
csequence_extract nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_extract nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(naturalnumber type-eq-decl nil naturalnumbers 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)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(extract_index 0
(extract_index-1 nil 3513607514
("" (skolem!)
(("" (rewrite "index?_prop")
(("" (rewrite "index?_prop")
(("" (use "extract_length")
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((index?_prop formula-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)
(is_finite inductive-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(T formal-type-decl nil csequence_extract nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(extract_length formula-decl nil csequence_extract nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
shostak))
(extract_first_TCC1 0
(extract_first_TCC1-1 nil 3513606610
("" (skosimp)
(("" (use "extract_index")
(("" (assert)
(("" (expand "index?" 1) (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((extract_index formula-decl nil csequence_extract 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_extract nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(index? def-decl "bool" csequence_nth nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(extract_first 0
(extract_first-1 nil 3513607566
("" (induct "m")
(("1" (skosimp)
(("1" (expand* "^" "nth")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (skosimp*)
(("2" (expand "^" (-2 +))
(("2" (expand "nth" +)
(("2" (lift-if)
(("2" (ground)
(("2" (inst - "rest(cseq!1)" "n!1 - 1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (forward-chain "extract_first_TCC1") nil nil)) nil))
nil)
((extract_first_TCC1 subtype-tcc nil csequence_extract nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
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)
(nat_induction formula-decl nil naturalnumbers nil)
(nth def-decl "T" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types 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_extract nil)
(csequence type-decl nil csequence_codt nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(is_finite inductive-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(index? def-decl "bool" csequence_nth nil))
shostak))
(extract_nth_TCC1 0
(extract_nth_TCC1-1 nil 3513606610
("" (skolem-typepred)
(("" (rewrite "extract_index")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil)
((extract_index formula-decl nil csequence_extract nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props 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_extract nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(extract_nth 0
(extract_nth-1 nil 3513607662
("" (measure-induct+ "m + n" ("cseq" "m" "n"))
(("1" (skolem-typepred)
(("1" (rewrite "extract_index")
(("1" (flatten)
(("1" (expand "^" +)
(("1" (expand "nth" +)
(("1" (smash)
(("1" (expand "index?") (("1" (propax) nil nil)) nil)
("2" (inst - "rest(x!1)" "x!2 - 1" "x!3 - 1")
(("1" (inst - 0)
(("1" (expand "nth" -3 1) (("1" (propax) nil nil))
nil)
("2" (rewrite "extract_index")
(("2" (expand "index?" -)
(("2" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "index?" -) (("2" (assert) nil nil))
nil))
nil)
("3" (expand "index?") (("3" (propax) nil nil)) nil)
("4" (rewrite "extract_rest2")
(("1" (inst - "rest(x!1)" "x!2" "x!3 - 1")
(("1" (inst - "i!1 - 1") (("1" (assert) nil nil))
nil)
("2" (expand "index?" -)
(("2"
(use "index?_lt"
("cseq" "rest(x!1)" "i" "i!1 - 1 + x!2"))
(("2" (assert) nil nil)) nil))
nil))
nil)
("2" (rewrite "index?_0")
(("2" (rewrite "extract_index")
(("2" (expand "index?" -)
(("2"
(lemma "index?_lt"
("cseq" "rest(x!1)" "i" "i!1 - 1 + x!2" "n"
"x!2 - 1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("5" (inst - "rest(x!1)" "x!2" "x!3 - 1")
(("1" (inst - "i!1 - 1") (("1" (assert) nil nil))
nil)
("2" (expand "index?" -)
(("2"
(use "index?_lt"
("cseq" "rest(x!1)" "i" "i!1 - 1 + x!2"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (use "extract_nth_TCC1") (("2" (assert) nil nil)) nil)
("3" (skolem!)
(("3" (use "extract_nth_TCC1") (("3" (assert) nil nil)) nil))
nil)
("4" (skolem!)
(("4" (use "extract_nth_TCC1") (("4" (assert) nil nil)) nil))
nil)
("5" (use "extract_nth_TCC1") (("5" (assert) nil nil)) nil)
("6" (skolem!)
(("6" (use "extract_nth_TCC1") (("6" (assert) nil nil)) nil))
nil)
("7" (use "extract_nth_TCC1") (("7" (assert) nil nil)) nil))
nil)
((extract_nth_TCC1 subtype-tcc nil csequence_extract nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(extract_rest2 formula-decl nil csequence_extract nil)
(index?_lt formula-decl nil csequence_nth nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(index?_0 formula-decl nil csequence_nth nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(x!1 skolem-const-decl "csequence[T]" csequence_extract nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(x!2 skolem-const-decl "indexes[T](x!1)" csequence_extract nil)
(x!3 skolem-const-decl "nat" csequence_extract nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(extract_index formula-decl nil csequence_extract nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nth def-decl "T" csequence_nth nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(^ def-decl "finite_csequence" csequence_extract nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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_extract nil)
(measure_induction formula-decl nil measure_induction nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(extract_add_TCC1 0
(extract_add_TCC1-1 nil 3513606610 ("" (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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(extract_add_TCC2 0
(extract_add_TCC2-1 nil 3513606610 ("" (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)
(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)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(extract_add_TCC3 0
(extract_add_TCC3-1 nil 3513606610 ("" (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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(extract_add 0
(extract_add-1 nil 3513608880
("" (expand "^" 1 1)
(("" (expand "max") (("" (reduce) nil nil)) nil)) nil)
((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(^ def-decl "finite_csequence" csequence_extract nil))
shostak))
(extract_last_TCC1 0
(extract_last_TCC1-1 nil 3513606610
("" (skosimp)
(("" (rewrite "index?_prop")
(("" (expand "^") (("" (ground) nil nil)) nil)) nil))
nil)
((index?_prop formula-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)
(T formal-type-decl nil csequence_extract nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(^ def-decl "finite_csequence" csequence_extract nil))
nil))
(extract_last 0
(extract_last-1 nil 3513608941
("" (induct "n")
(("1" (skosimp)
(("1" (expand* "^" "last" "index?")
(("1" (expand "length" 1 1)
(("1" (expand "length" 1 1)
(("1" (expand "length" 1 1)
(("1" (expand "nth" 1 2)
(("1" (expand "nth" 1 2) (("1" (reduce) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "^" (-2 +))
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (ground)
(("1" (inst - "rest(cseq!1)" "m!1 - 1")
(("1" (expand "index?" -1)
(("1" (expand "nth" +) (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (inst - "rest(cseq!1)" "m!1 - 1")
(("2" (expand "index?" +)
(("2" (use "last_rest")
(("2" (assert)
(("2" (expand "^" -4)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (expand "index?" -1)
(("3" (use "add_last")
(("3" (lift-if)
(("3" (prop)
(("1" (rewrite "extract_empty")
(("1" (flatten)
(("1"
(lemma "index?_lt")
(("1"
(inst - "rest(cseq!1)" "j!1" "m!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (inst - "rest(cseq!1)" "m!1")
(("2" (expand "nth" +)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "index?" +)
(("4" (use "add_last")
(("4" (lift-if)
(("4" (prop)
(("1" (rewrite "extract_empty")
(("1" (flatten)
(("1"
(expand "index?" 1)
(("1"
(rewrite "length_nonempty?_rew")
(("1"
(flatten)
(("1"
(assert)
(("1"
(replace -3)
(("1"
(hide -3)
(("1"
(expand "last" +)
(("1"
(expand "length" 3)
(("1"
(expand "nth")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (hide -1)
(("2"
(inst - "rest(cseq!1)" "m!1")
(("2"
(assert)
(("2"
(use "last_rest")
(("2"
(expand "^" 1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp) (("3" (forward-chain "extract_last_TCC1") nil nil))
nil))
nil)
((extract_last_TCC1 subtype-tcc nil csequence_extract nil)
(add_finite application-judgement "nonempty_finite_csequence[T]"
csequence_extract nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
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)
(last_rest formula-decl nil csequence_nth nil)
(add_last formula-decl nil csequence_add nil)
(first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
(cseq!1 skolem-const-decl "csequence[T]" csequence_extract nil)
(j!1 skolem-const-decl "nat" csequence_extract nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(index?_lt formula-decl nil csequence_nth nil)
(extract_empty formula-decl nil csequence_extract nil)
(length_nonempty?_rew formula-decl nil csequence_length nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nth def-decl "T" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(last const-decl "T" csequence_nth nil)
(nonempty_finite_csequence type-eq-decl nil csequence_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types 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_extract nil)
(csequence type-decl nil csequence_codt nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(index? def-decl "bool" csequence_nth nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(is_finite inductive-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(^ def-decl "finite_csequence" csequence_extract nil))
shostak))
(extract_extensionality 0
(extract_extensionality-1 nil 3513609793
("" (skosimp)
(("" (use "nth_extensionality")
(("" (assert)
(("" (case "index?(cseq1!1) = index?(cseq2!1)")
(("1" (assert)
(("1" (skolem-typepred)
(("1" (assert)
(("1" (inst - "(0, n!1)")
(("1" (lemma "extract_index")
(("1" (inst - "cseq1!1" 0 "n!1" "n!1")
(("1" (assert)
(("1" (lemma "extract_nth")
(("1" (inst-cp - "cseq2!1" 0 "n!1" "n!1")
(("1" (inst - "cseq1!1" 0 "n!1" "n!1")
(("1" (assert) nil nil)
("2"
(use "index?_lt")
(("2" (assert) nil nil))
nil))
nil)
("2" (use "index?_lt")
(("2" (assert) nil nil)) nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.69 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.
|
