57 lines
2.4 KiB
Plaintext
57 lines
2.4 KiB
Plaintext
(sumn
|
|
(sum_TCC1 0
|
|
(sum_TCC1-1 nil 3864858118 ("" (subtype-tcc) nil nil) nil nil
|
|
(sum subtype "(number_fields.-)(sumn.n, 1)" "nat")))
|
|
(sum_TCC2 0
|
|
(sum_TCC2-1 nil 3864858118 ("" (termination-tcc) nil nil) nil nil
|
|
(sum termination "sumn.sum((number_fields.-)(sumn.n, 1))" "nil")))
|
|
(nnatsum 0
|
|
(nnatsum-1 nil 3864865657
|
|
("" (induct "n")
|
|
(("1" (expand "sum") (("1" (propax) nil nil)) nil)
|
|
("2" (skolem!)
|
|
(("2" (flatten)
|
|
(("2" (expand "sum" +) (("2" (assert) nil nil)) nil)) nil))
|
|
nil))
|
|
nil)
|
|
((nnint_times_nnint_is_nnint application-judgement "nonneg_int"
|
|
integers nil)
|
|
(even_times_int_is_even application-judgement "even_int" integers
|
|
nil)
|
|
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
|
|
rationals nil)
|
|
(nnint_plus_posint_is_posint application-judgement "posint"
|
|
integers nil)
|
|
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
|
|
integers nil)
|
|
(posint_plus_nnint_is_posint application-judgement "posint"
|
|
integers nil)
|
|
(posrat_div_posrat_is_posrat application-judgement "posrat"
|
|
rationals nil)
|
|
(nat_induction formula-decl nil naturalnumbers nil)
|
|
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
|
|
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
|
|
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
|
|
(nznum nonempty-type-eq-decl nil number_fields nil)
|
|
(/= const-decl "boolean" notequal nil)
|
|
(numfield nonempty-type-eq-decl nil number_fields nil)
|
|
(sum def-decl "nat" sumn nil)
|
|
(= const-decl "[T, T -> boolean]" equalities 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)))
|
|
|