|
(seq_extras
(first_TCC1 0
(first_TCC1-1 nil 3385301063 ("" (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)
(/= const-decl "boolean" notequal nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(not_empty_seq type-eq-decl nil seq_extras nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(last_TCC1 0
(last_TCC1-1 nil 3409227118 ("" (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)
(/= const-decl "boolean" notequal nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(not_empty_seq type-eq-decl nil seq_extras 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))
(rest_TCC1 0
(rest_TCC1-1 nil 3385301063 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(delete_TCC1 0
(delete_TCC1-1 nil 3388246700 ("" (subtype-tcc) nil nil) nil nil))
(delete_TCC2 0
(delete_TCC2-1 nil 3388246700 ("" (subtype-tcc) nil nil) nil nil))
(insert?_TCC1 0
(insert?_TCC1-1 nil 3388317884 ("" (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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(upto nonempty-type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_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))
nil))
(insert?_TCC2 0
(insert?_TCC2-1 nil 3388317884 ("" (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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(upto nonempty-type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_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))
nil))
(add_first_TCC1 0
(add_first_TCC1-1 nil 3390053856 ("" (subtype-tcc) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(add_last_TCC1 0
(add_last_TCC1-1 nil 3411672012 ("" (subtype-tcc) nil nil) nil nil))
(empty_0 0
(empty_0-1 nil 3384683401
("" (skeep)
(("" (grind)
(("" (decompose-equality)
(("1" (apply-extensionality) (("1" (grind) nil nil)) nil)
("2" (skeep) nil nil))
nil))
nil))
nil)
((empty_seq const-decl "finseq" finite_sequences nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(epsilon const-decl "T" epsilons 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)
(FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil))
shostak))
(empty_o_seq 0
(empty_o_seq-1 nil 3388766444
("" (skeep)
(("" (expand "o")
(("" (apply-extensionality)
(("1" (hide 2)
(("1" (expand "empty_seq") (("1" (propax) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (decompose-equality)
(("1" (lift-if)
(("1" (prop)
(("1" (expand "empty_seq") (("1" (assert) nil nil))
nil)
("2" (expand "empty_seq") (("2" (propax) nil nil))
nil))
nil))
nil)
("2" (skeep) (("2" (assert) nil nil)) nil))
nil))
nil)
("3" (hide 2)
(("3" (skeep)
(("3" (expand "empty_seq") (("3" (propax) nil nil)) nil))
nil))
nil)
("4" (hide 2) (("4" (skeep) (("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((O const-decl "finseq" finite_sequences 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(seq skolem-const-decl "finseq[T]" seq_extras nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers 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))
(seq_o_empty 0
(seq_o_empty-1 nil 3394279023
("" (skeep)
(("" (expand "o")
(("" (apply-extensionality)
(("1" (hide 2)
(("1" (expand "empty_seq") (("1" (propax) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (decompose-equality)
(("1" (lift-if)
(("1" (prop)
(("1" (typepred "x!1")
(("1" (expand "empty_seq") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (skeep) (("2" (assert) nil nil)) nil))
nil))
nil)
("3" (hide 2)
(("3" (skeep)
(("3" (expand "empty_seq") (("3" (propax) nil nil)) nil))
nil))
nil)
("4" (hide 2) (("4" (skeep) (("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((O const-decl "finseq" finite_sequences 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(seq skolem-const-decl "finseq[T]" seq_extras nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers 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))
(length_rest 0
(length_rest-1 nil 3388768632 ("" (skeep) (("" (grind) nil nil)) nil)
((posint_plus_nnint_is_posint application-judgement "posint"
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)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
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)
(empty_seq const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(rest const-decl "finseq" seq_extras nil))
shostak))
(length_delete_TCC1 0
(length_delete_TCC1-1 nil 3411689891 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(length_delete 0
(length_delete-1 nil 3411689938
("" (skosimp*) (("" (grind) nil nil)) 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)
(delete const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
shostak))
(seq_empty 0
(seq_empty-1 nil 3388767794
("" (skeep)
(("" (expand* "o" "empty_seq")
(("" (flatten)
(("" (decompose-equality) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((empty_seq const-decl "finseq" finite_sequences nil)
(O const-decl "finseq" finite_sequences nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(FALSE const-decl "bool" booleans nil)
(pred type-eq-decl nil defined_types nil)
(epsilon const-decl "T" epsilons nil)
(TRUE const-decl "bool" booleans nil))
shostak))
(seq_first_rest 0
(seq_first_rest-1 nil 3385301064
("" (skeep)
(("" (expand "add_first")
(("" (expand "insert?")
(("" (decompose-equality 2)
(("1" (expand "rest")
(("1" (expand "^")
(("1" (lift-if)
(("1" (prop)
(("1" (expand "empty_seq") (("1" (assert) nil nil))
nil)
("2" (expand "empty_seq") (("2" (assert) nil nil))
nil)
("3" (expand "min") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality)
(("1" (lift-if)
(("1" (prop)
(("1" (expand "first")
(("1" (replaces -1)
(("1" (expand "finseq_appl")
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (grind) nil nil))
nil))
nil)
("2" (skeep) (("2" (grind) nil nil)) nil)
("3" (skeep) (("3" (assert) nil nil)) nil))
nil)
("3" (skeep) (("3" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((add_first const-decl "finseq" seq_extras nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(seq skolem-const-decl "finseq[T]" seq_extras nil)
(rest const-decl "finseq" seq_extras nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(not_empty_seq type-eq-decl nil seq_extras nil)
(first const-decl "T" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(^ const-decl "finseq" finite_sequences nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(insert? const-decl "finseq" seq_extras nil))
shostak))
(seq_first_rest_1 0
(seq_first_rest_1-1 nil 3409227118
("" (skeep)
(("" (decompose-equality 2)
(("1" (expand "o") (("1" (grind) nil nil)) nil)
("2" (decompose-equality 1)
(("2" (expand "o")
(("2" (lift-if)
(("2" (prop) (("1" (grind) nil nil) ("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((O const-decl "finseq" finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(|#| const-decl "finite_sequence[T]" set2seq nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(not_empty_seq type-eq-decl nil seq_extras nil)
(first const-decl "T" seq_extras nil)
(rest const-decl "finseq" seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
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)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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) (< const-decl "bool" reals nil))
shostak))
(add_first_empty_seq 0
(add_first_empty_seq-1 nil 3412165021
("" (skeep)
(("" (decompose-equality)
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil)
((add_first const-decl "finseq" seq_extras nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(|#| const-decl "finite_sequence[T]" set2seq nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(insert? const-decl "finseq" seq_extras nil))
shostak))
(length_rest_0 0
(length_rest_0-1 nil 3409227389
("" (skeep)
(("" (prop)
(("1" (lemma "empty_0")
(("1" (inst -1 "rest(seq)")
(("1" (assert)
(("1" (lemma "seq_first_rest_1")
(("1" (inst?)
(("1" (assert)
(("1" (replace -1 2)
(("1" (hide -1)
(("1" (expand "o")
(("1" (hide -1) (("1" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind) nil nil) ("3" (grind) nil nil))
nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(rest const-decl "finseq" seq_extras nil)
(seq_first_rest_1 formula-decl nil seq_extras nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
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)
(int_plus_int_is_int application-judgement "int" integers nil)
(^ const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(O const-decl "finseq" finite_sequences nil)
(empty_0 formula-decl nil seq_extras nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(empty_seq const-decl "finseq" finite_sequences nil))
shostak))
(rest_add_first 0
(rest_add_first-1 nil 3411750449
("" (skeep)
(("" (decompose-equality)
(("1" (grind) nil nil)
("2" (case "length(seq) = 0")
(("1" (rewrite "empty_0") (("1" (grind) nil nil)) nil)
("2" (decompose-equality 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((rest const-decl "finseq" seq_extras nil)
(add_first const-decl "finseq" seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(^ const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(insert? const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(< const-decl "bool" reals 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)
(int_plus_int_is_int application-judgement "int" integers nil)
(empty_0 formula-decl nil seq_extras nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(first_add_TCC1 0
(first_add_TCC1-1 nil 3394562155 ("" (subtype-tcc) nil nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(insert? const-decl "finseq" seq_extras nil)
(add_first const-decl "finseq" seq_extras nil))
nil))
(first_add 0
(first_add-1 nil 3394562155
("" (skeep)
(("" (expand "first")
(("" (expand "finseq_appl")
(("" (expand "add_first")
(("" (expand "insert?") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((first const-decl "T" seq_extras nil)
(add_first const-decl "finseq" seq_extras nil)
(insert? const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
shostak))
(nth_add_first_TCC1 0
(nth_add_first_TCC1-1 nil 3411750374 ("" (subtype-tcc) nil nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(insert? const-decl "finseq" seq_extras nil)
(add_first const-decl "finseq" seq_extras nil))
nil))
(nth_add_first_TCC2 0
(nth_add_first_TCC2-1 nil 3411750374 ("" (subtype-tcc) nil nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(insert? const-decl "finseq" seq_extras nil)
(add_first const-decl "finseq" seq_extras nil))
nil))
(nth_add_first_TCC3 0
(nth_add_first_TCC3-1 nil 3411750374 ("" (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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(nth_add_first 0
(nth_add_first-1 nil 3411750375
("" (skosimp*)
(("" (prop)
(("1" (replaces -1)
(("1" (expand* "finseq_appl" "add_first" "insert?") nil nil))
nil)
("2" (expand* "add_first" "insert?" "finseq_appl")
(("2" (lift-if) (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(add_first const-decl "finseq" seq_extras nil)
(insert? const-decl "finseq" seq_extras nil))
shostak))
(first_add_last_TCC1 0
(first_add_last_TCC1-1 nil 3411672012 ("" (subtype-tcc) nil nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(/= const-decl "boolean" notequal nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(insert? const-decl "finseq" seq_extras nil)
(add_last const-decl "finseq" seq_extras nil))
nil))
(first_add_last 0
(first_add_last-1 nil 3411672012
("" (skeep) (("" (grind) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(first const-decl "T" seq_extras nil)
(add_last const-decl "finseq" seq_extras nil)
(insert? const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
shostak))
(rest_add_last 0
(rest_add_last-1 nil 3411672588
("" (skeep)
(("" (expand "rest" 2 1)
(("" (lift-if)
(("" (prop)
(("1" (grind) nil nil)
("2" (decompose-equality 2)
(("1" (grind) nil nil)
("2" (decompose-equality 1)
(("2" (expand "^")
(("2" (lift-if)
(("2" (prop)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (expand "add_last" 3)
(("3" (expand "insert?")
(("3" (lift-if)
(("3" (prop)
(("1" (grind) nil nil)
("2" (lift-if)
(("2"
(prop)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rest const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(insert? const-decl "finseq" seq_extras nil)
(add_last const-decl "finseq" seq_extras nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(< const-decl "bool" reals 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(^ const-decl "finseq" finite_sequences 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(seq skolem-const-decl "finseq[T]" seq_extras nil)
(x skolem-const-decl "T" seq_extras nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(add_first_last_commute 0
(add_first_last_commute-1 nil 3412162557
("" (skeep)
(("" (case "length(seq) = 0")
(("1" (decompose-equality 1)
(("1" (grind) nil nil)
("2" (decompose-equality 1) (("2" (grind) nil nil)) nil))
nil)
("2" (decompose-equality 2)
(("1" (grind) nil nil)
("2" (decompose-equality 1)
(("2"
(expand* "add_first" "add_last" "insert?" "finseq_appl")
(("2" (lift-if)
(("2" (lift-if)
(("2" (prop)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(< const-decl "bool" reals 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)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(insert? const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(add_first const-decl "finseq" seq_extras nil)
(add_last const-decl "finseq" seq_extras nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(add_first_last 0
(add_first_last-1 nil 3411673505
("" (skeep)
(("" (decompose-equality 2)
(("1" (grind) nil nil)
("2" (decompose-equality 1)
(("2"
(expand* "add_first" "first" "add_last" "rest" "insert?"
"finseq_appl")
(("2" (lift-if)
(("2" (lift-if)
(("2" (prop)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil) ("4" (grind) nil nil)
("5" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((add_first const-decl "finseq" seq_extras nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(not_empty_seq type-eq-decl nil seq_extras nil)
(first const-decl "T" seq_extras nil)
(add_last const-decl "finseq" seq_extras nil)
(rest const-decl "finseq" seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(insert? const-decl "finseq" seq_extras nil)
(^ const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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) (< const-decl "bool" reals nil))
shostak))
(add_last_delete 0
(add_last_delete-1 nil 3411684834
("" (skeep)
(("" (decompose-equality 2)
(("1" (grind) nil nil)
("2" (decompose-equality 1) (("2" (grind) nil nil)) nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(seq skolem-const-decl "finseq[T]" seq_extras nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(add_last const-decl "finseq" seq_extras 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)
(delete const-decl "finseq" seq_extras nil)
(/= const-decl "boolean" notequal nil)
(not_empty_seq type-eq-decl nil seq_extras nil)
(last const-decl "T" seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(insert? const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(add_last_delete_is_o 0
(add_last_delete_is_o-1 nil 3495983888
("" (skosimp*) (("" (grind) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(O const-decl "finseq" finite_sequences nil)
(|#| const-decl "finite_sequence[T]" set2seq nil)
(T formal-type-decl nil seq_extras nil)
(add_last const-decl "finseq" seq_extras nil)
(insert? const-decl "finseq" seq_extras nil)
(last const-decl "T" seq_extras nil)
(delete const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
shostak))
(nth_add_last_TCC1 0
(nth_add_last_TCC1-1 nil 3411679457 ("" (subtype-tcc) nil nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(insert? const-decl "finseq" seq_extras nil)
(add_last const-decl "finseq" seq_extras nil))
nil))
(nth_add_last_TCC2 0
(nth_add_last_TCC2-1 nil 3411679457 ("" (subtype-tcc) nil nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(insert? const-decl "finseq" seq_extras nil)
(add_last const-decl "finseq" seq_extras nil))
nil))
(nth_add_last_TCC3 0
(nth_add_last_TCC3-1 nil 3411679457 ("" (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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(nth_add_last 0
(nth_add_last-1 nil 3411679473
("" (skosimp*)
(("" (prop)
(("1" (replaces -1)
(("1" (expand* "finseq_appl" "add_last" "insert?") nil nil))
nil)
("2" (expand* "add_last" "insert?" "finseq_appl")
(("2" (lift-if) (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(add_last const-decl "finseq" seq_extras nil)
(insert? const-decl "finseq" seq_extras nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(add_first_compo 0
(add_first_compo-1 nil 3411750758
("" (skeep)
(("" (decompose-equality 1)
(("1" (grind) nil nil)
("2" (decompose-equality) (("2" (grind) nil nil)) nil))
nil))
nil)
((O const-decl "finseq" finite_sequences nil)
(add_first const-decl "finseq" seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(insert? const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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)
(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) (< const-decl "bool" reals nil))
shostak))
(first_compo_TCC1 0
(first_compo_TCC1-1 nil 3394276097 ("" (subtype-tcc) nil nil)
((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(/= const-decl "boolean" notequal nil)
(O const-decl "finseq" finite_sequences nil))
nil))
(first_compo 0
(first_compo-1 nil 3394276097
("" (skeep)
(("" (expand "first")
(("" (expand "o")
(("" (expand "finseq_appl")
(("" (lift-if)
(("" (prop)
(("" (hide 2)
(("" (typepred "seq1`length") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((first const-decl "T" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(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)
(O const-decl "finseq" finite_sequences nil))
shostak))
(rest_compo 0
(rest_compo-1 nil 3394277575
("" (skeep)
(("" (lemma "seq_first_rest")
(("" (inst -1 "seq1")
(("" (assert)
(("" (replaces -1 2)
(("" (rewrite "add_first_compo")
(("" (rewrite "rest_add_first")
(("" (rewrite "rest_add_first") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((seq_first_rest formula-decl nil seq_extras nil)
(add_first_compo formula-decl nil seq_extras nil)
(rest const-decl "finseq" seq_extras nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(not_empty_seq type-eq-decl nil seq_extras nil)
(first const-decl "T" seq_extras nil)
(O const-decl "finseq" finite_sequences nil)
(rest_add_first formula-decl nil seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
shostak))
(rest_pos_TCC1 0
(rest_pos_TCC1-1 nil 3409318490
("" (skosimp*) (("" (grind) nil nil)) nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(rest const-decl "finseq" seq_extras nil)
(^ const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(empty_seq const-decl "finseq" finite_sequences nil))
nil))
(rest_pos_TCC2 0
(rest_pos_TCC2-1 nil 3411689660 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(rest_pos_TCC3 0
(rest_pos_TCC3-1 nil 3412162502 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(rest const-decl "finseq" seq_extras nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(rest_pos 0
(rest_pos-1 nil 3409318604 ("" (skosimp*) (("" (grind) nil nil)) nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(rest const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
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)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(delete_is_empty_TCC1 0
(delete_is_empty_TCC1-1 nil 3412164710 ("" (subtype-tcc) nil nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(delete_is_empty 0
(delete_is_empty-1 nil 3412164710
("" (skeep)
(("" (decompose-equality 1)
(("1" (grind) nil nil)
("2" (decompose-equality 1)
(("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil))
nil))
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) (< const-decl "bool" reals nil)
(delete const-decl "finseq" seq_extras nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(delete_pos_TCC1 0
(delete_pos_TCC1-1 nil 3411688998 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(delete_pos_TCC2 0
(delete_pos_TCC2-1 nil 3411688998 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(delete const-decl "finseq" seq_extras nil))
nil))
(delete_pos 0
(delete_pos-1 nil 3411688999
("" (skosimp*)
(("" (expand "delete")
(("" (expand "finseq_appl") (("" (propax) nil nil)) nil)) nil))
nil)
((delete const-decl "finseq" seq_extras nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
shostak))
(insert_delete_TCC1 0
(insert_delete_TCC1-1 nil 3390053856 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(delete const-decl "finseq" seq_extras nil))
nil))
(insert_delete 0
(insert_delete-1 nil 3388246701
("" (skeep)
(("" (skolem 2 ("n"))
(("" (apply-extensionality 2)
(("1" (hide 2)
(("1" (expand "delete")
(("1" (expand "insert?") (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (hide 3)
(("2" (decompose-equality)
(("2" (expand "insert?")
(("2" (lift-if)
(("2" (split)
(("1" (flatten)
(("1" (expand "finseq_appl")
(("1" (expand "delete")
(("1" (assert)
(("1" (expand "finseq_appl")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (prop)
(("1" (expand "finseq_appl")
(("1" (replaces -1) nil nil)) nil)
("2" (expand "finseq_appl")
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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) (<= const-decl "bool" reals nil)
(upto nonempty-type-eq-decl nil nat_types nil)
(insert? const-decl "finseq" seq_extras nil)
(< const-decl "bool" reals nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(delete const-decl "finseq" seq_extras nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq_extras nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
shostak))
(add_first_delete_TCC1 0
(add_first_delete_TCC1-1 nil 3412187759 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(add_first_delete 0
(add_first_delete-1 nil 3412187760
("" (skosimp*)
(("" (expand "finseq_appl")
(("" (case "length(rest(delete(seq!1, n!1))) = 0")
(("1" (lemma "length_rest_0")
(("1" (inst?)
(("1" (prop)
(("1" (hide -1)
(("1" (hide 1)
(("1" (rewrite "empty_0")
(("1" (replaces -2)
(("1" (rewrite "add_first_empty_seq")
(("1" (typepred "n!1")
(("1" (decompose-equality 3)
(("1" (grind) nil nil)
("2" (decompose-equality 1)
(("2"
(typepred "x!1")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (1 4))
(("2" (typepred "n!1") (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality 4)
(("1" (grind) nil nil)
("2" (decompose-equality 1)
(("2" (case "x!1 = 0")
(("1" (replaces -1)
(("1" (expand "delete" 1 2)
(("1" (lemma "nth_add_first")
(("1" (inst?)
(("1" (inst -1 "0")
(("1" (expand "finseq_appl")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "x!1 < n!1")
(("1" (expand "delete" 2 2)
(("1" (assert)
(("1" (lemma "nth_add_first")
(("1" (inst?)
(("1" (inst -1 "x!1")
(("1" (assert)
(("1" (expand "finseq_appl")
(("1"
(replaces -1)
(("1" (grind) nil nil))
nil))
nil))
nil)
("2" (typepred "x!1")
(("2" (hide 3) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "delete" 3 2)
(("2" (assert)
(("2" (lemma "nth_add_first")
(("2" (inst?)
(("2" (inst -1 "x!1")
(("1" (assert)
(("1" (expand "finseq_appl")
(("1"
(replaces -1)
(("1"
(lemma "rest_pos")
(("1"
(inst?)
(("1"
(prop)
(("1"
(inst -1 "x!1 - 1")
(("1"
(expand "finseq_appl")
(("1"
(replace -1 3 rl)
(("1"
(hide -1)
(("1"
(expand*
"delete"
"finseq_appl")
nil
nil))
nil))
nil))
nil)
("2"
(typepred "x!1")
(("2"
(hide 4)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "x!1")
(("2" (hide 4) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(add_first const-decl "finseq" seq_extras nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(insert? const-decl "finseq" seq_extras nil)
(^ const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nth_add_first formula-decl nil seq_extras nil)
(rest_pos formula-decl nil seq_extras nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(seq!1 skolem-const-decl "finseq[T]" seq_extras nil)
(n!1 skolem-const-decl "below[seq!1`length]" seq_extras nil)
(x!1 skolem-const-decl
"below[add_first(seq!1`seq(0), rest(delete(seq!1, n!1)))`length]"
seq_extras nil)
(length_rest_0 formula-decl nil seq_extras nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(|#| const-decl "finite_sequence[T]" set2seq nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(add_first_empty_seq formula-decl nil seq_extras nil)
(empty_0 formula-decl nil seq_extras nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.94 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.
|
