|
(convergence_ops
(cnv_seq_sum 0
(cnv_seq_sum-1 nil 3298633902
("" (expand "convergence")
(("" (skosimp*)
(("" (inst -1 "epsilon!1/2")
(("" (inst -2 "epsilon!1/2")
(("" (skolem!)
(("" (skolem!)
(("" (inst 1 "n!1 + n!2")
(("" (skosimp)
(("" (inst -1 "i!1")
(("" (inst -2 "i!1")
(("" (assert)
(("" (expand "+")
((""
(lemma "triangle"
("x" "s1!1(i!1) - l1!1" "y"
"s2!1(i!1) - l2!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sequence type-eq-decl nil sequences nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(triangle formula-decl nil real_props 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)
(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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(convergence const-decl "bool" convergence_sequences nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(cnv_seq_neg 0
(cnv_seq_neg-1 nil 3298633902
("" (expand "convergence")
(("" (skosimp*)
(("" (inst -1 "epsilon!1")
(("" (expand "-")
(("" (skolem!)
(("" (inst? 1)
(("" (skosimp)
(("" (inst?)
(("" (assert)
(("" (lemma "abs_neg" ("x" "s1!1(i!1) - l1!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((- const-decl "[T -> real]" real_fun_ops "reals/")
(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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs_neg formula-decl nil abs_lems "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sequence type-eq-decl nil 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(convergence const-decl "bool" convergence_sequences nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(cnv_seq_diff 0
(cnv_seq_diff-1 nil 3298633902
("" (skosimp)
(("" (rewrite "diff_function")
((""
(lemma "cnv_seq_sum"
("s1" "s1!1" "s2" "- s2!1" "l1" "l1!1" "l2" "-l2!1"))
(("" (assert) (("" (rewrite "cnv_seq_neg") nil nil)) nil))
nil))
nil))
nil)
((diff_function formula-decl nil real_fun_ops "reals/")
(sequence type-eq-decl nil sequences 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_minus_real_is_real application-judgement "real" reals nil)
(cnv_seq_neg formula-decl nil convergence_ops nil)
(minus_real_is_real application-judgement "real" reals nil)
(cnv_seq_sum formula-decl nil convergence_ops nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(- const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(cnv_seq_prod 0
(cnv_seq_prod-1 nil 3298633902
("" (expand "convergence")
(("" (skosimp*)
(("" (lemma "prod_epsilon")
(("" (inst -1 "epsilon!1" "l1!1" "l2!1")
(("" (skolem!)
(("" (inst -2 "e1!1")
(("" (inst -3 "e2!1")
(("" (skolem!)
(("" (skolem!)
(("" (inst 1 "n!1 + n!2")
(("" (skosimp)
(("" (inst -2 "i!1")
(("" (inst -3 "i!1")
(("" (assert)
((""
(expand "*" 1 1)
((""
(lemma "prod_bound")
((""
(inst
-1
"e1!1"
"e2!1"
"s1!1(i!1)"
"s2!1(i!1)"
"l1!1"
"l2!1")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(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)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(prod_bound formula-decl nil epsilon_lemmas nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sequence type-eq-decl nil sequences nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(prod_epsilon formula-decl nil epsilon_lemmas nil)
(convergence const-decl "bool" convergence_sequences nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(cnv_seq_const 0
(cnv_seq_const-1 nil 3298633902
("" (skolem!) (("" (grind :if-match nil) nil nil)) nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_sequences nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(cnv_seq_scal 0
(cnv_seq_scal-1 nil 3298633902
("" (skosimp)
(("" (rewrite "scal_function")
(("" (rewrite "cnv_seq_prod")
(("" (rewrite "cnv_seq_const") nil nil)) nil))
nil))
nil)
((scal_function formula-decl nil real_fun_ops "reals/")
(sequence type-eq-decl nil sequences 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)
(cnv_seq_const formula-decl nil convergence_ops nil)
(real_times_real_is_real application-judgement "real" reals nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(cnv_seq_prod formula-decl nil convergence_ops nil))
nil))
(cnv_seq_inv 0
(cnv_seq_inv-1 nil 3298633902
("" (expand "convergence")
(("" (skosimp*)
(("" (assert)
(("" (lemma "inv_epsilon" ("y1" "l2!1" "e" "epsilon!1"))
(("" (assert)
(("" (skosimp)
(("" (inst -3 "e1!1")
(("" (skolem!)
(("" (inst 2 "n!1")
(("" (skosimp)
(("" (inst -3 "i!1")
(("" (assert)
(("" (expand "/")
(("" (assert)
((""
(lemma "inv_bound")
((""
(inst -1 "e1!1" "s3!1(i!1)" "l2!1")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(inv_epsilon formula-decl nil epsilon_lemmas 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)
(sequence type-eq-decl nil sequences nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(inv_bound formula-decl nil epsilon_lemmas nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(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)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(convergence const-decl "bool" convergence_sequences nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(cnv_seq_div 0
(cnv_seq_div-1 nil 3298633902
("" (skosimp)
(("" (assert)
(("" (rewrite "div_function")
(("" (use "cnv_seq_prod" ("l2" "1/l2!1"))
(("" (assert) (("" (rewrite "cnv_seq_inv") nil nil)) nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cnv_seq_prod formula-decl nil convergence_ops nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(cnv_seq_inv formula-decl nil convergence_ops 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)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(sequence type-eq-decl nil sequences nil)
(div_function formula-decl nil real_fun_ops "reals/"))
nil))
(cnv_seq_abs 0
(cnv_seq_abs-1 nil 3298633902
("" (expand "convergence")
(("" (skosimp*)
(("" (inst -1 "epsilon!1")
(("" (skolem!)
(("" (inst 1 "n!1")
(("" (skosimp)
(("" (inst -1 "i!1")
(("" (assert)
(("" (expand "abs" 1 2)
(("" (expand "abs" 1 1)
(("" (lift-if)
((""
(lemma "abs_diff"
("x" "s1!1(i!1)" "y" "l1!1"))
((""
(lemma "abs_diff"
("x" "l1!1" "y" "s1!1(i!1)"))
(("" (rewrite "abs_diff_commute" -1)
(("" (assert) nil nil)) nil))
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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(abs_diff formula-decl nil abs_lems "reals/")
(sequence type-eq-decl nil sequences nil)
(abs_diff_commute formula-decl nil abs_lems "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(convergence const-decl "bool" convergence_sequences nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(cnv_seq_order 0
(cnv_seq_order-1 nil 3298633902
("" (skosimp)
(("" (expand "convergence")
(("" (case "l2!1 < l1!1")
(("1" (name "eps" "(l1!1 - l2!1) / 2")
(("1" (assert)
(("1" (inst -3 "eps")
(("1" (inst -4 "eps")
(("1" (skolem!)
(("1" (skolem!)
(("1" (inst -3 "n!1+n!2")
(("1" (inst -4 "n!1+n!2")
(("1" (inst -5 "n!1+n!2")
(("1" (assert)
(("1" (expand "abs")
(("1"
(lift-if)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_sequences 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_div_nzreal_is_real application-judgement "real" reals 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals 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)
(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))
nil))
(convergence_shift 0
(convergence_shift-1 nil 3298642564
("" (skosimp*)
(("" (prop)
(("1" (expand "convergence")
(("1" (skosimp*)
(("1" (inst - "epsilon!1")
(("1" (skosimp*)
(("1" (inst + "n!1")
(("1" (skosimp*)
(("1" (inst - "i!1 + m!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "convergence")
(("2" (skosimp*)
(("2" (inst - "epsilon!1")
(("2" (skosimp*)
(("2" (inst + "n!1+m!1")
(("2" (skosimp*)
(("2" (inst - "i!1-m!1")
(("1" (assert) nil nil) ("2" (assert) 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(convergence const-decl "bool" convergence_sequences nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(m!1 skolem-const-decl "nat" convergence_ops nil)
(i!1 skolem-const-decl "nat" convergence_ops nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(squeezing_variant 0
(squeezing_variant-1 nil 3298633902
("" (expand "convergence")
(("" (skosimp*)
(("" (inst -1 "epsilon!1")
(("" (inst -2 "epsilon!1")
(("" (skolem!)
(("" (skolem!)
(("" (inst 1 "N!1 + n!1 + n!2")
(("" (skosimp)
(("" (inst -1 "i!1")
(("" (inst -2 "i!1")
(("" (inst -3 "i!1")
(("" (assert)
(("" (flatten)
(("" (expand "abs")
((""
(lift-if)
((""
(split 1)
(("1"
(flatten)
(("1" (assert) nil nil))
nil)
("2"
(flatten)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_le_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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(convergence const-decl "bool" convergence_sequences nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(squeezing_const1 0
(squeezing_const1-1 nil 3298633902
("" (skosimp)
(("" (auto-rewrite "cnv_seq_const" "const_fun")
(("" (lemma "squeezing_variant")
(("" (inst -1 "N!1" "l!1" "s!1" "const_fun(l!1)" "s1!1")
(("" (assert) 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(cnv_seq_const formula-decl nil convergence_ops nil)
(squeezing_variant formula-decl nil convergence_ops nil))
nil))
(squeezing_const2 0
(squeezing_const2-1 nil 3298633902
("" (skosimp)
(("" (auto-rewrite "cnv_seq_const" "const_fun")
(("" (lemma "squeezing_variant")
(("" (inst -1 "N!1" "l!1" "s!1" "s1!1" "const_fun(l!1)")
(("" (assert) 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(cnv_seq_const formula-decl nil convergence_ops nil)
(squeezing_variant formula-decl nil convergence_ops nil))
nil))
(squeezing 0
(squeezing-1 nil 3298633902
("" (skosimp)
((""
(use "squeezing_variant"
("s1" "s1!1" "s2" "s2!1" "s" "s!1" "N" "0"))
(("" (assert) nil nil)) nil))
nil)
((squeezing_variant formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences nil))
nil))
(squeezing_gen 0
(squeezing_gen-1 nil 3302006364
("" (skosimp*)
((""
(use "squeezing_variant"
("s1" "s1!1" "s2" "s2!1" "s" "s!1" "N" "N!1"))
(("" (assert)
(("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((squeezing_variant formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(abs_convergence 0
(abs_convergence-1 nil 3298633902
("" (skolem!)
(("" (prop)
(("1" (forward-chain "cnv_seq_abs")
(("1" (expand "abs" -1 2) (("1" (propax) nil nil)) nil)) nil)
("2" (forward-chain "cnv_seq_neg")
(("2" (assert)
(("2"
(lemma "squeezing"
("s1" "- abs(s!1)" "s2" "abs(s!1)" "s" "s!1" "l" "0"))
(("2" (assert)
(("2" (skolem!)
(("2" (delete -1 -2 2)
(("2" (expand "-")
(("2" (expand "abs")
(("2" (expand "abs")
(("2" (lift-if) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sequence type-eq-decl nil sequences 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)
(cnv_seq_abs formula-decl nil convergence_ops nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(squeezing formula-decl nil convergence_ops nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(cnv_seq_neg formula-decl nil convergence_ops nil))
nil))
(convergent_sum 0
(convergent_sum-1 nil 3298633902
(""
(grind :exclude "convergence" :rewrites ("cnv_seq_sum") :if-match
nil)
(("" (inst + "l!1 + l!2") (("" (assert) nil nil)) nil)) nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cnv_seq_sum formula-decl nil convergence_ops 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)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(convergent_neg 0
(convergent_neg-1 nil 3298633902
("" (lemma "cnv_seq_neg")
(("" (auto-rewrite "convergent?")
(("" (reduce :if-match nil) (("" (reduce) nil nil)) nil)) nil))
nil)
((numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(minus_real_is_real application-judgement "real" reals nil)
(sequence type-eq-decl nil sequences 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)
(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)
(convergent? const-decl "bool" convergence_sequences nil)
(cnv_seq_neg formula-decl nil convergence_ops nil))
nil))
(convergent_diff 0
(convergent_diff-1 nil 3298633902
("" (lemma "cnv_seq_diff")
(("" (grind :exclude "convergence") nil nil)) nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sequence type-eq-decl nil sequences 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent? const-decl "bool" convergence_sequences nil)
(cnv_seq_diff formula-decl nil convergence_ops nil))
nil))
(convergent_prod 0
(convergent_prod-1 nil 3298633902
("" (lemma "cnv_seq_prod")
(("" (grind :exclude "convergence") nil nil)) nil)
((real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sequence type-eq-decl nil sequences 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent? const-decl "bool" convergence_sequences nil)
(cnv_seq_prod formula-decl nil convergence_ops nil))
nil))
(convergent_const 0
(convergent_const-1 nil 3298633902
("" (lemma "cnv_seq_const")
(("" (grind :exclude "convergence") 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)
(convergent? const-decl "bool" convergence_sequences nil)
(cnv_seq_const formula-decl nil convergence_ops nil))
nil))
(convergent_scal 0
(convergent_scal-1 nil 3298633902
("" (lemma "cnv_seq_scal")
(("" (grind :exclude "convergence") 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sequence type-eq-decl nil sequences 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)
(convergent? const-decl "bool" convergence_sequences nil)
(cnv_seq_scal formula-decl nil convergence_ops nil))
nil))
(convergent_inv 0
(convergent_inv-1 nil 3298633902
("" (skosimp)
(("" (assert)
(("" (expand "convergent?")
(("" (skolem!)
(("" (use "cnv_seq_inv")
(("" (assert)
(("" (rewrite "limit_def" -2 :dir rl)
(("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(limit_def formula-decl nil convergence_sequences 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 "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(sequence type-eq-decl nil sequences nil)
(cnv_seq_inv formula-decl nil convergence_ops nil)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(convergent_div 0
(convergent_div-1 nil 3298633902
("" (skosimp)
(("" (assert)
(("" (expand "convergent?")
(("" (skosimp*)
(("" (use "cnv_seq_div")
(("" (assert)
(("" (rewrite "limit_def" -3 :dir rl)
(("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(limit_def formula-decl nil convergence_sequences 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)
(sequence type-eq-decl nil sequences nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(cnv_seq_div formula-decl nil convergence_ops nil)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(convergent_abs 0
(convergent_abs-1 nil 3298633902
("" (lemma "cnv_seq_abs")
(("" (auto-rewrite "convergent?")
(("" (reduce :if-match nil) (("" (reduce) nil nil)) nil)) nil))
nil)
((nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sequence type-eq-decl nil sequences 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)
(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)
(convergent? const-decl "bool" convergence_sequences nil)
(cnv_seq_abs formula-decl nil convergence_ops nil))
nil))
(squeezing_abs_0 0
(squeezing_abs_0-1 nil 3298634764
("" (skosimp*)
(("" (rewrite "abs_convergence" +)
(("" (lemma "squeezing")
(("" (assert)
(("" (inst - "0" "abs(s!1)" "const_fun(0)" "abs(s1!1)")
(("" (assert)
(("" (split +)
(("1" (rewrite "cnv_seq_const") nil nil)
("2" (lemma "abs_convergence")
(("2" (inst - "s1!1") (("2" (assert) nil nil)) nil))
nil)
("3" (skosimp*)
(("3" (expand "const_fun")
(("3" (assert)
(("3" (inst - "n!1")
(("3" (assert)
(("3" (expand "abs" 1)
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_convergence formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences 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)
(cnv_seq_const formula-decl nil convergence_ops nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(squeezing formula-decl nil convergence_ops nil))
nil))
(squeezing_abs_0_gen 0
(squeezing_abs_0_gen-3 nil 3302006459
("" (skosimp*)
(("" (rewrite "abs_convergence" +)
(("" (lemma "squeezing_gen")
(("" (assert)
(("" (inst - "N!1" "0" "abs(s!1)" "const_fun(0)" "abs(s1!1)")
(("" (assert)
(("" (split +)
(("1" (rewrite "cnv_seq_const") nil nil)
("2" (lemma "abs_convergence")
(("2" (inst - "s1!1") (("2" (assert) nil nil)) nil))
nil)
("3" (skosimp*)
(("3" (expand "const_fun")
(("3" (assert)
(("3" (inst - "n!1")
(("3" (assert)
(("3" (expand "abs" 1)
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_convergence formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences 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)
(cnv_seq_const formula-decl nil convergence_ops nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(squeezing_gen formula-decl nil convergence_ops nil))
nil)
(squeezing_abs_0_gen-2 nil 3302006193
(""
("" (skosimp*) (rewrite "abs_convergence" +) (lemma "squeezing")
(assert) (inst - "0" "abs(s!1)" "const_fun(0)" "abs(s1!1)")
(assert) (split +)
(("1" (rewrite "cnv_seq_const"))
("2" (lemma "abs_convergence") (inst - "s1!1") (assert))
("3" (skosimp*) (expand "const_fun") (assert) (inst - "n!1")
(assert) (expand "abs" 1) (assert))))
nil nil)
nil nil)
(squeezing_abs_0_gen-1 nil 3302006112
("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak))
(constant_seq1 0
(constant_seq1-1 nil 3298633902
("" (lemma "convergent_const")
(("" (skosimp*)
(("" (expand "K_conversion")
(("" (expand "const_fun") (("" (inst?) nil nil)) nil)) nil))
nil))
nil)
((convergent_const formula-decl nil convergence_ops nil)) nil))
(constant_seq2 0
(constant_seq2-1 nil 3298633902
("" (skolem!)
(("" (use "cnv_seq_const")
((""
(case-replace
"K_conversion[nzreal, nat](b!1) = K_conversion[real, nat](b!1)")
(("1" (assert)
(("1" (auto-rewrite "limit_def" "convergent_nz?")
(("1" (assert)
(("1" (use "unique_limit" ("l2" "0"))
(("1" (assert)
(("1" (expand "const_fun") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "K_conversion") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
((cnv_seq_const formula-decl nil convergence_ops nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(constant_seq1 application-judgement "(convergent?)"
convergence_ops nil)
(limit_def formula-decl nil convergence_sequences nil)
(convergent_nz? const-decl "bool" convergence_ops nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(sequence type-eq-decl nil sequences nil)
(unique_limit formula-decl nil convergence_sequences nil)
(K_conversion const-decl "T1" K_conversion nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(K_preserves1 application-judgement "[T2 -> S]" K_props nil))
nil))
(conv_seq_plus 0
(conv_seq_plus-1 nil 3298633902
("" (skolem!) (("" (rewrite "convergent_sum") nil nil)) nil)
((convergent_sum formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(conv_seq_minus 0
(conv_seq_minus-1 nil 3298633902
("" (skolem!) (("" (rewrite "convergent_diff") nil nil)) nil)
((convergent_diff formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(conv_seq_times 0
(conv_seq_times-1 nil 3298633902
("" (skolem!) (("" (rewrite "convergent_prod") nil nil)) nil)
((convergent_prod formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(conv_seq_scal 0
(conv_seq_scal-1 nil 3298633902
("" (skolem!) (("" (rewrite "convergent_scal") nil nil)) nil)
((convergent_scal formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(conv_seq_neg 0
(conv_seq_neg-1 nil 3298633902
("" (skolem!) (("" (rewrite "convergent_neg") nil nil)) nil)
((convergent_neg formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(conv_seq_abs 0
(conv_seq_abs-1 nil 3298633902
("" (skolem!) (("" (rewrite "convergent_abs") nil nil)) nil)
((convergent_abs formula-decl nil convergence_ops 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)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences nil))
nil))
(conv_seq_div1 0
(conv_seq_div1-1 nil 3298633902
("" (auto-rewrite "convergent_div" "convergent_nz?")
(("" (skolem-typepred) (("" (assert) nil nil)) nil)) nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(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)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(convergent_nz? const-decl "bool" convergence_ops nil)
(convergent_div formula-decl nil convergence_ops nil))
nil))
(conv_seq_div2 0
(conv_seq_div2-1 nil 3298633902
("" (skolem!)
(("" (rewrite "scaldiv_function") (("" (assert) nil nil)) nil))
nil)
((scaldiv_function formula-decl nil real_fun_ops "reals/")
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences nil)
(convergent_nz? const-decl "bool" convergence_ops 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)
(constant_seq1 application-judgement "(convergent?)"
convergence_ops nil)
(conv_seq_div1 application-judgement "(convergent?)"
convergence_ops nil))
nil))
(limit_sum 0
(limit_sum-1 nil 3298633902
("" (auto-rewrite "limit_def" "cnv_seq_sum" "limit_lemma")
(("" (skolem!) (("" (assert) nil nil)) nil)) nil)
((limit_lemma formula-decl nil convergence_sequences nil)
(cnv_seq_sum formula-decl nil convergence_ops nil)
(limit_def formula-decl nil convergence_sequences nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(conv_seq_plus application-judgement "(convergent?)"
convergence_ops nil))
nil))
(limit_neg 0
(limit_neg-1 nil 3298633902
("" (auto-rewrite "limit_def" "cnv_seq_neg" "limit_lemma")
(("" (skolem!) (("" (assert) nil nil)) nil)) nil)
((limit_lemma formula-decl nil convergence_sequences nil)
(cnv_seq_neg formula-decl nil convergence_ops nil)
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.38Quellennavigators
Analyse erneut starten
]
|
