|
(csequence_remove
(remove_TCC1 0
(remove_TCC1-1 nil 3513478083 ("" (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))
nil))
(remove_TCC2 0
(remove_TCC2-1 nil 3513478083 ("" (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))
nil))
(remove_TCC3 0
(remove_TCC3-1 nil 3513478083 ("" (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))
(remove_TCC4 0
(remove_TCC4-1 nil 3513478083 ("" (termination-tcc) nil nil) nil
nil))
(remove_finite 0
(remove_finite-1 nil 3513478083
("" (induct "index")
(("1" (skolem-typepred)
(("1" (expand "remove")
(("1" (expand "is_finite" -) (("1" (ground) nil nil)) nil))
nil))
nil)
("2" (skosimp* t)
(("2" (expand "is_finite" (-1 +))
(("2" (expand "remove" +)
(("2" (lift-if)
(("2" (ground) (("2" (inst - "rest(fseq!1)") nil nil))
nil))
nil))
nil))
nil))
nil))
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)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat_induction formula-decl nil naturalnumbers nil)
(remove def-decl "csequence" csequence_remove 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_remove 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))
nil))
(remove_infinite 0
(remove_infinite-1 nil 3513478083
("" (induct "index")
(("1" (skolem-typepred)
(("1" (expand "remove")
(("1" (expand "is_finite" +) (("1" (ground) nil nil)) nil))
nil))
nil)
("2" (skosimp* t)
(("2" (expand "is_finite" (-3 +))
(("2" (expand "remove" -3)
(("2" (lift-if)
(("2" (ground) (("2" (inst - "rest(iseq!1)") nil nil))
nil))
nil))
nil))
nil))
nil))
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)
(nat_induction formula-decl nil naturalnumbers nil)
(remove def-decl "csequence" csequence_remove 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_remove 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))
nil))
(remove_0 0
(remove_0-1 nil 3513478205
("" (expand "remove") (("" (propax) nil nil)) nil)
((remove def-decl "csequence" csequence_remove nil)) shostak))
(remove_empty 0
(remove_empty-1 nil 3513478213
("" (expand "remove") (("" (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)
(>= 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)
(remove def-decl "csequence" csequence_remove nil))
shostak))
(remove_nonempty 0
(remove_nonempty-1 nil 3513478241
("" (expand "remove") (("" (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)
(>= 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)
(remove def-decl "csequence" csequence_remove nil))
shostak))
(remove_first_TCC1 0
(remove_first_TCC1-1 nil 3513478083
("" (skosimp)
(("" (rewrite "remove_nonempty") (("" (flatten) nil nil)) nil))
nil)
((remove_nonempty formula-decl nil csequence_remove nil)
(T formal-type-decl nil csequence_remove 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(remove_first_TCC2 0
(remove_first_TCC2-1 nil 3513478083
("" (skosimp)
(("" (rewrite "remove_nonempty") (("" (ground) nil nil)) nil)) nil)
((remove_nonempty formula-decl nil csequence_remove nil)
(T formal-type-decl nil csequence_remove 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(remove_first_TCC3 0
(remove_first_TCC3-1 nil 3513478083
("" (skosimp)
(("" (rewrite "remove_nonempty") (("" (flatten) nil nil)) nil))
nil)
((remove_nonempty formula-decl nil csequence_remove nil)
(T formal-type-decl nil csequence_remove 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(remove_first 0
(remove_first-1 nil 3513478308
("" (expand "remove") (("" (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)
(>= 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)
(remove def-decl "csequence" csequence_remove nil))
shostak))
(remove_rest_TCC1 0
(remove_rest_TCC1-1 nil 3513478083
("" (skosimp)
(("" (rewrite "remove_nonempty") (("" (assert) nil nil)) nil)) nil)
((remove_nonempty formula-decl nil csequence_remove nil)
(T formal-type-decl nil csequence_remove nil)
(csequence type-decl nil csequence_codt nil)
(boolean nonempty-type-decl nil booleans nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(nonempty_csequence type-eq-decl nil csequence_props 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(remove_rest_TCC2 0
(remove_rest_TCC2-1 nil 3513478083 ("" (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)
(T formal-type-decl nil csequence_remove nil)
(csequence type-decl nil csequence_codt nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(nonempty_csequence type-eq-decl nil csequence_props 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))
(remove_rest 0
(remove_rest-1 nil 3513478348
("" (induct "index")
(("1" (skosimp)
(("1" (expand "remove") (("1" (propax) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (expand "remove" +)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "remove") (("1" (propax) nil nil)) nil)
("2" (expand "remove") (("2" (propax) nil nil)) nil)
("3" (decompose-equality 2)
(("1" (expand "remove") (("1" (propax) nil nil)) nil)
("2" (inst - "rest(nseq!1)")
(("2" (assert)
(("2" (expand* "remove" "remove") nil nil)) nil))
nil)
("3" (expand "remove") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp) (("3" (assert) nil nil)) nil)
("4" (skosimp) (("4" (forward-chain "remove_rest_TCC1") nil nil))
nil))
nil)
((remove_rest_TCC1 subtype-tcc nil csequence_remove nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nseq!1 skolem-const-decl "nonempty_csequence[T]" csequence_remove
nil)
(j!1 skolem-const-decl "nat" csequence_remove 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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_remove nil)
(csequence type-decl nil csequence_codt nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(nonempty_csequence type-eq-decl nil csequence_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(remove def-decl "csequence" csequence_remove nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(remove_upfrom_length 0
(remove_upfrom_length-1 nil 3513478456
("" (induct "fseq" :name "is_finite_induction")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (skosimp* t)
(("3" (expand "remove" +)
(("3" (use "length_empty?_rew")
(("3" (lift-if)
(("3" (ground)
(("3" (decompose-equality 2)
(("3" (inst - "index!1 - 1")
(("3" (expand "length" -) (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(length_empty?_rew formula-decl nil csequence_length nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cseq!1 skolem-const-decl "csequence[T]" csequence_remove nil)
(index!1 skolem-const-decl "upfrom[length(cseq!1)]"
csequence_remove nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(is_finite_induction formula-decl nil csequence_props nil)
(T formal-type-decl nil csequence_remove nil)
(remove def-decl "csequence" csequence_remove nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(upfrom nonempty-type-eq-decl nil int_types 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)
(finite_csequence nonempty-type-eq-decl nil csequence_props 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))
(remove_length 0
(remove_length-1 nil 3513478533
("" (induct "fseq" :name "is_finite_induction")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (skosimp*)
(("3" (expand "remove" +)
(("3" (expand "length" 1 1)
(("3" (expand "length" 1 2)
(("3" (expand "length" 1 3)
(("3" (expand "index?" +) (("3" (reduce) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("4" (skosimp*)
(("4" (use "remove_finite" ("fseq" "fseq!2")) nil nil)) nil))
nil)
((remove_finite judgement-tcc nil csequence_remove nil)
(remove_finite application-judgement "finite_csequence"
csequence_remove nil)
(index!1 skolem-const-decl "nat" csequence_remove nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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_remove nil)
(index? def-decl "bool" csequence_nth nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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 "[T, T -> boolean]" equalities 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)
(is_finite inductive-decl "bool" csequence_props 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)
(remove def-decl "csequence" csequence_remove nil))
shostak))
(remove_index 0
(remove_index-1 nil 3513478587
("" (skolem!)
(("" (case "is_finite(cseq!1)")
(("1" (use "remove_finite")
(("1" (use "remove_length")
(("1" (lemma "index?_finite")
(("1" (reduce :if-match all) nil nil)) nil))
nil))
nil)
("2" (use "remove_infinite")
(("2" (lemma "index?_infinite")
(("2" (reduce :if-match all) nil nil)) nil))
nil))
nil))
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_remove nil)
(remove_length formula-decl nil csequence_remove nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(remove def-decl "csequence" csequence_remove nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(index?_finite formula-decl nil csequence_nth nil)
(cseq!1 skolem-const-decl "csequence[T]" csequence_remove nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props 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)
(remove_finite judgement-tcc nil csequence_remove nil)
(index?_infinite formula-decl nil csequence_nth nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(infinite_csequence type-eq-decl nil csequence_props nil)
(remove_infinite judgement-tcc nil csequence_remove nil))
shostak))
(remove_nth_TCC1 0
(remove_nth_TCC1-1 nil 3513478083
("" (grind :rewrites ("index?_prop" "remove_index")) nil nil)
((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(index?_prop formula-decl nil csequence_nth nil)
(T formal-type-decl nil csequence_remove 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)
(remove_index formula-decl nil csequence_remove nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(indexes type-eq-decl nil csequence_nth nil)
(remove def-decl "csequence" csequence_remove nil)
(index? def-decl "bool" csequence_nth nil)
(csequence type-decl nil csequence_codt 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))
nil))
(remove_nth 0
(remove_nth-1 nil 3513478688
("" (induct "n")
(("1" (skolem-typepred)
(("1" (expand "remove" +)
(("1" (expand "nth" 1 2)
(("1" (lift-if)
(("1" (ground) (("1" (expand* "remove" "index?") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp* t)
(("2" (expand "remove" +)
(("2" (expand "nth" +)
(("2" (smash)
(("1" (expand* "remove" "index?") nil nil)
("2" (inst - "rest(cseq!1)" "m!1 - 1")
(("2" (assert) nil nil)) nil)
("3" (inst - "rest(cseq!1)" "m!1 - 1")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (skolem!) (("3" (use "remove_nth_TCC1") nil nil)) nil))
nil)
((remove_nth_TCC1 subtype-tcc nil csequence_remove nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nth def-decl "T" csequence_nth 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_remove nil)
(csequence type-decl nil csequence_codt nil)
(index? def-decl "bool" csequence_nth nil)
(remove def-decl "csequence" csequence_remove nil)
(indexes type-eq-decl nil csequence_nth nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(< const-decl "bool" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil))
shostak))
(remove_add 0
(remove_add-1 nil 3513478786
("" (expand "remove" 1 2) (("" (propax) nil nil)) nil)
((remove def-decl "csequence" csequence_remove nil)) shostak))
(remove_last_TCC1 0
(remove_last_TCC1-1 nil 3513478083
("" (skosimp :preds? t)
(("" (rewrite "remove_nonempty")
(("" (ground)
(("1" (rewrite "index?_finite") nil nil)
("2" (expand* "length" "is_finite")
(("2" (use "length_nonempty?_rew") (("2" (assert) nil nil))
nil))
nil)
("3" (rewrite "index?_finite")
(("3" (expand* "length" "is_finite")
(("3" (use "length_nonempty?_rew") (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((remove_nonempty formula-decl nil csequence_remove nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(length_nonempty?_rew formula-decl nil csequence_length nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(index?_finite formula-decl nil csequence_nth nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers 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_remove 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)
(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))
nil))
(remove_last_TCC2 0
(remove_last_TCC2-1 nil 3513478083
("" (skosimp) (("" (expand "remove") (("" (assert) nil nil)) nil))
nil)
((remove def-decl "csequence" csequence_remove nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(remove_last 0
(remove_last-1 nil 3513478899
("" (induct "fseq" :name "is_finite_induction")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (skosimp*)
(("3" (case "empty?(cseq!1)")
(("1" (rewrite "remove_nonempty") (("1" (ground) nil nil)) nil)
("2" (ground)
(("2" (rewrite "remove_nonempty")
(("2" (expand "last")
(("2" (expand "remove" +)
(("2" (expand "length" +)
(("2" (expand "nth" +)
(("2" (smash)
(("1" (rewrite "remove_length")
(("1" (lift-if) (("1" (assert) nil nil)) nil))
nil)
("2" (rewrite "remove_length")
(("2" (lift-if)
(("2" (ground)
(("2" (rewrite "index?_finite") nil nil))
nil))
nil))
nil)
("3" (rewrite "remove_length")
(("3" (lift-if)
(("3" (ground)
(("3" (rewrite "index?_finite") nil nil))
nil))
nil))
nil)
("4" (inst - "index!1 - 1")
(("4" (assert)
(("4" (rewrite "remove_nonempty")
(("4" (expand "length" -)
(("4" (assert) nil nil)) nil))
nil))
nil))
nil)
("5" (inst - "index!1 - 1")
(("5" (assert)
(("5" (rewrite "remove_nonempty")
(("5" (ground)
(("5"
(expand "length" 4)
(("5" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("6"
(lemma "length_empty?_rew"
("cseq" "rest(cseq!1)"))
(("6" (assert)
(("6" (expand "remove" 2)
(("6" (propax) nil nil)) nil))
nil))
nil)
("7" (expand "length" -7)
(("7" (assert) nil nil)) nil)
("8" (expand "length" 3)
(("8" (expand "nth" +) (("8" (propax) nil nil))
nil))
nil)
("9" (rewrite "length_nonempty?_rew") nil nil)
("10" (expand "length" 4 2)
(("10" (expand "nth" 4 2)
(("10" (propax) nil nil)) nil))
nil)
("11" (rewrite "remove_length")
(("11" (lift-if) (("11" (assert) nil nil))
nil))
nil)
("12" (rewrite "remove_length")
(("12" (lift-if)
(("12" (ground)
(("12" (rewrite "index?_finite") nil nil))
nil))
nil))
nil)
("13" (expand "remove" 3)
(("13" (expand "length" -5)
(("13" (assert) nil nil)) nil))
nil)
("14" (inst - "index!1 - 1")
(("14" (assert)
(("14" (rewrite "remove_nonempty") nil nil))
nil))
nil)
("15" (inst - "index!1 - 1")
(("15" (assert)
(("15" (rewrite "remove_nonempty")
(("15" (flatten)
(("15"
(expand "remove" 5)
(("15"
(assert)
(("15"
(rewrite "length_nonempty?_rew")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("16" (rewrite "length_nonempty?_rew") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (skosimp*) (("4" (forward-chain "remove_last_TCC2") nil nil))
nil)
("5" (skosimp*) (("5" (forward-chain "remove_last_TCC1") nil nil))
nil)
("6" (skosimp*)
(("6" (use "remove_finite" ("fseq" "fseq!2")) nil nil)) nil))
nil)
((remove_finite judgement-tcc nil csequence_remove nil)
(remove_last_TCC1 subtype-tcc nil csequence_remove nil)
(remove_last_TCC2 subtype-tcc nil csequence_remove nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(remove_length formula-decl nil csequence_remove nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(index?_finite formula-decl nil csequence_nth nil)
(length_empty?_rew formula-decl nil csequence_length nil)
(length_nonempty?_rew formula-decl nil csequence_length nil)
(remove_nonempty formula-decl nil csequence_remove nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(is_finite_induction formula-decl nil csequence_props nil)
(T formal-type-decl nil csequence_remove 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(has_length def-decl "bool" csequence_props nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(index? def-decl "bool" 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)
(is_finite inductive-decl "bool" csequence_props 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)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(remove def-decl "csequence" csequence_remove nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(remove_remove_TCC1 0
(remove_remove_TCC1-1 nil 3513478083 ("" (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_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))
nil))
(remove_remove 0
(remove_remove-1 nil 3513479269
("" (induct "n")
(("1" (skolem!)
(("1" (lift-if)
(("1" (assert)
(("1" (expand "remove" 1 2)
(("1" (expand "remove" 1 2)
(("1" (lift-if)
(("1" (ground)
(("1" (expand "remove") (("1" (propax) nil nil)) nil)
("2" (lift-if)
(("2" (ground)
(("1" (expand "remove") (("1" (propax) nil nil))
nil)
("2" (rewrite "remove_rest") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "remove" 1 2)
(("2" (expand "remove" 1 4)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "remove") (("1" (propax) nil nil)) nil)
("2" (expand "remove" +) (("2" (propax) nil nil))
nil)
("3" (expand "remove" 1 1)
(("3" (expand "remove" 1 3)
(("3" (decompose-equality)
(("3" (inst - "rest(cseq!1)" "m!1 - 1")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil)
("4" (expand "remove" 2 1)
(("4" (lift-if)
(("4" (ground)
(("1" (expand "remove" 1 3)
(("1" (propax) nil nil)) nil)
("2" (expand "remove" 2 3)
(("2" (lift-if)
(("2" (ground)
(("1" (rewrite "remove_empty") nil nil)
("2"
(decompose-equality)
(("1" (rewrite "remove_first") nil nil)
("2"
(rewrite "remove_rest")
(("2"
(inst - "rest(cseq!1)" "m!1 - 1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp) (("3" (assert) nil nil)) nil))
nil)
((int_plus_int_is_int application-judgement "int" integers 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(remove_empty formula-decl nil csequence_remove nil)
(remove_first formula-decl nil csequence_remove nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(remove_rest formula-decl nil csequence_remove nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(nonempty_csequence type-eq-decl nil csequence_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(remove def-decl "csequence" csequence_remove nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_remove 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(remove_extensionality 0
(remove_extensionality-1 nil 3513479628
("" (induct "n")
(("1" (skosimp)
(("1" (expand* "remove" "index?" "nth")
(("1" (reduce) (("1" (decompose-equality +) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "remove" -2)
(("2" (expand "index?" -3)
(("2" (expand "nth" -3)
(("2" (smash)
(("1" (decompose-equality -2)
(("1" (inst - "rest(cseq1!1)" "rest(cseq2!1)")
(("1" (assert) (("1" (decompose-equality +) nil nil))
nil))
nil))
nil)
("2" (decompose-equality)
(("2" (inst - "rest(cseq1!1)" "rest(cseq2!1)")
(("2" (assert)
(("2"
(forward-chain "csequence_add_extensionality")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
(add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(csequence_add_extensionality formula-decl nil csequence_codt nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt 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)
(index? def-decl "bool" csequence_nth nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(remove def-decl "csequence" csequence_remove nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_remove 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))
(remove_some 0
(remove_some-1 nil 3513479748
("" (skolem!)
(("" (use "nth_some")
(("" (prop)
(("1" (skolem-typepred)
(("1" (rewrite "remove_index")
(("1" (flatten)
(("1" (rewrite "remove_nth")
(("1" (lift-if -4)
(("1" (split -)
(("1" (flatten)
(("1" (inst + "i!1") (("1" (assert) nil nil))
nil))
nil)
("2" (flatten)
(("2" (inst + "i!1 + 1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp :preds? t)
(("2" (case "n!1 < index!1")
(("1" (inst + "n!1")
(("1" (rewrite "remove_nth") (("1" (assert) nil nil))
nil)
("2" (rewrite "remove_index")
(("2" (flatten)
(("2" (rewrite "index?_finite")
(("2" (rewrite "index?_finite")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (inst + "n!1 - 1")
(("1" (rewrite "remove_nth") (("1" (assert) nil nil))
nil)
("2" (assert)
(("2" (rewrite "remove_index")
(("2" (prop)
(("1" (use "index?_lt" ("n" "n!1 - 1"))
(("1" (assert) nil nil)) nil)
("2" (rewrite "index?_finite")
(("2" (rewrite "index?_finite")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nth_some formula-decl nil csequence_nth nil)
(T formal-type-decl nil csequence_remove nil)
(pred type-eq-decl nil defined_types nil)
(remove def-decl "csequence" csequence_remove 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(index?_lt formula-decl nil csequence_nth nil)
(n!1 skolem-const-decl "indexes[T](cseq!1)" csequence_remove nil)
(index?_finite formula-decl nil csequence_nth nil)
(is_finite inductive-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(< const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(i!1 skolem-const-decl "indexes[T](remove(cseq!1, index!1))"
csequence_remove nil)
(index!1 skolem-const-decl "nat" csequence_remove nil)
(cseq!1 skolem-const-decl "csequence[T]" csequence_remove nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(remove_nth formula-decl nil csequence_remove nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(remove_index formula-decl nil csequence_remove nil))
shostak))
(remove_every 0
(remove_every-1 nil 3513479895
("" (skolem!)
(("" (use "every_some_rew")
(("" (use "remove_some")
(("" (expand "pred_NOT")
(("" (ground)
(("1" (skosimp)
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (skosimp)
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((every_some_rew formula-decl nil csequence_props nil)
(T formal-type-decl nil csequence_remove nil)
(remove def-decl "csequence" csequence_remove 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)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(pred_NOT const-decl "bool" csequence_props nil)
(remove_some formula-decl nil csequence_remove nil))
shostak)))
¤ Dauer der Verarbeitung: 0.72 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
