|
(convergence_sequences
(unique_limit 0
(unique_limit-1 nil 3253549181
("" (skosimp)
(("" (expand "convergence")
(("" (rewrite "abs_diff_0")
(("" (name "eps" "abs(l1!1 - l2!1)/3")
(("" (assert)
(("" (inst -2 "eps")
(("" (inst -3 "eps")
(("" (skolem!)
(("" (skolem!)
(("" (inst -2 "n!1+n!2")
(("" (inst -3 "n!1+n!2")
(("" (assert)
(("" (lemma "triangle2")
((""
(inst -1 "eps" "eps" "l1!1"
"u!1(n!1+n!2)" "l2!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_sequences nil)
(nnreal type-eq-decl nil real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_gt_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)
(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)
(sequence type-eq-decl nil sequences nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(triangle2 formula-decl nil abs_lems "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(abs_diff_0 formula-decl nil abs_lems "reals/"))
nil))
(limit_lemma 0
(limit_lemma-1 nil 3253549181
("" (skolem-typepred)
(("" (name-replace "ll" "limit(v!1)" :hide? nil)
(("" (expand "limit")
(("" (expand "convergent?")
((""
(lemma "epsilon_ax"
("p" "LAMBDA (l: real): convergence(v!1, l)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(limit const-decl "real" convergence_sequences nil)
(epsilon_ax formula-decl nil epsilons nil)
(pred type-eq-decl nil defined_types nil)
(convergence const-decl "bool" convergence_sequences nil)
(convergent? const-decl "bool" convergence_sequences 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))
nil))
(limit_def 0
(limit_def-1 nil 3253549181
("" (skolem!)
(("" (use "limit_lemma")
(("" (ground)
(("" (use "unique_limit") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((limit_lemma formula-decl nil convergence_sequences nil)
(convergent? const-decl "bool" convergence_sequences 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)
(unique_limit formula-decl nil convergence_sequences nil)
(limit const-decl "real" convergence_sequences nil))
nil))
(convergence_subsequence 0
(convergence_subsequence-1 nil 3253549181
(""
(grind :defs nil :rewrites ("subseq" "convergence") :if-match nil)
(("" (delete -1 -2 -3 -4)
(("" (inst -1 "epsilon!1")
(("" (skolem!)
(("" (inst 1 "n!1")
(("" (skosimp)
(("" (inst? -2)
(("" (replace -2)
(("" (inst?)
(("" (assert)
(("" (use "extract_incr3")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_odd_is_odd application-judgement "odd_int" 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)
(extract_incr3 formula-decl nil sequence_props 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)
(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)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(extraction type-eq-decl nil sequence_props 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(subseq const-decl "bool" sequence_props nil)
(convergence const-decl "bool" convergence_sequences nil))
nil))
(limit_accumulation 0
(limit_accumulation-1 nil 3253549181
(""
(grind :defs nil :rewrites ("convergence" "accumulation") :if-match
nil)
(("" (inst?)
(("" (skolem!)
(("" (inst -5 "n!1+n!2")
(("" (inst 1 "n!1+n!2") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
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)
(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)
(>= 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)
(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)
(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)
(real_minus_real_is_real application-judgement "real" reals nil)
(accumulation const-decl "bool" convergence_sequences nil)
(convergence const-decl "bool" convergence_sequences nil))
nil))
(g_TCC1 0
(g_TCC1-1 nil 3253549181 ("" (skosimp) (("" (assert) nil 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))
(g_TCC2 0
(g_TCC2-1 nil 3253549181 ("" (skosimp) (("" (assert) nil nil)) 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))
nil))
(g_TCC3 0 (g_TCC3-1 nil 3253549181 ("" (skosimp*) nil nil) nil nil))
(g_prop 0
(g_prop-1 nil 3253549181
("" (skosimp*)
(("" (expand "accumulation")
(("" (name-replace "y" "g(u!1, a!1)(n!1 + 1)" :hide? nil)
(("" (expand "g" -1)
(("" (assert)
((""
(lemma "epsilon_ax"
("p"
"LAMBDA (i: nat): g(u!1, a!1)(n!1) < i AND abs(u!1(i) - a!1) < 1 / (1 + n!1)"))
(("" (replace -2)
(("" (split -1)
(("1" (assert) nil nil)
("2" (inst -2 "1/(1+n!1)" "g(u!1, a!1)(n!1) + 1")
(("2" (skosimp)
(("2" (inst 1 "i!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((accumulation const-decl "bool" convergence_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(epsilon_ax formula-decl nil epsilons nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(g def-decl "nat" convergence_sequences 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(g_increasing 0
(g_increasing-1 nil 3253549181
("" (skosimp)
(("" (rewrite "strict_incr_condition")
(("" (skolem!)
(("" (forward-chain "g_prop")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((strict_incr_condition formula-decl nil sequence_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)
(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)
(g def-decl "nat" convergence_sequences nil)
(g_prop formula-decl nil convergence_sequences nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(g_convergence 0
(g_convergence-1 nil 3253549181
("" (skosimp*)
(("" (forward-chain "g_prop")
(("" (inst -1 "n!1") (("" (flatten) nil nil)) nil)) nil))
nil)
((g_prop 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)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(accumulation_subsequence 0
(accumulation_subsequence-1 nil 3253549181
("" (skolem!)
(("" (prop)
(("1" (inst 1 "LAMBDA (i : nat) : u!1(g(u!1, a!1)(i))")
(("1" (split)
(("1" (forward-chain "g_increasing")
(("1" (expand "subseq")
(("1" (inst 1 "g(u!1, a!1)") (("1" (skolem!) nil nil))
nil))
nil))
nil)
("2" (forward-chain "g_convergence")
(("2" (expand "convergence")
(("2" (skolem!)
(("2" (lemma "archimedean2" ("x" "epsilon!1"))
(("2" (skolem!)
(("2" (inst 1 "a!2")
(("2" (skosimp)
(("2" (assert)
(("2" (inst -2 "i!1 - 1")
(("2" (assert)
(("2"
(case "1/i!1 <= 1/a!2")
(("1" (assert) nil nil)
("2"
(rewrite "both_sides_div_pos_le2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(grind :defs nil :rewrites
("subseq" "convergence" "accumulation") :if-match nil)
(("2" (inst? -6)
(("2" (skolem!)
(("2" (inst -5 "n!1 + n!2")
(("2" (inst -6 "n!1+n!2")
(("2" (inst?)
(("2" (assert)
(("2" (assert)
(("2" (use "extract_incr3")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subseq const-decl "bool" sequence_props nil)
(extraction type-eq-decl nil sequence_props nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(u!1 skolem-const-decl "sequence[real]" convergence_sequences nil)
(a!1 skolem-const-decl "real" convergence_sequences nil)
(g_increasing formula-decl nil convergence_sequences nil)
(convergence const-decl "bool" convergence_sequences nil)
(archimedean2 formula-decl nil real_facts "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
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)
(both_sides_div_pos_le2 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal 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_minus_real_is_real application-judgement "real" reals nil)
(g_convergence formula-decl nil convergence_sequences nil)
(g def-decl "nat" convergence_sequences 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(extract_incr3 formula-decl nil sequence_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(accumulation const-decl "bool" convergence_sequences nil))
nil))
(cauchy_accumulation 0
(cauchy_accumulation-1 nil 3253549181
(""
(grind :defs nil :rewrites ("cauchy" "accumulation" "convergence")
:if-match nil)
(("" (inst -4 "epsilon!1/2")
(("" (skolem!)
(("" (inst -5 "epsilon!1/2" "n!1")
(("" (skosimp)
(("" (inst 1 "i!1")
(("" (skosimp)
(("" (inst -4 "i!1" "i!2")
(("" (assert)
(("" (lemma "triangle2")
(("" (assert)
((""
(inst -1 "epsilon!1/2" "epsilon!1/2"
"u!1(i!2)" "u!1(i!1)" "a!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types 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)
(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)
(triangle2 formula-decl nil abs_lems "reals/")
(sequence type-eq-decl nil sequences nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(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)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_sequences nil)
(accumulation const-decl "bool" convergence_sequences nil)
(cauchy const-decl "bool" convergence_sequences nil))
nil))
(cauchy_subsequence 0
(cauchy_subsequence-1 nil 3253549181
("" (skosimp)
(("" (rewrite "cauchy_accumulation" 1)
(("" (rewrite "accumulation_subsequence")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((cauchy_accumulation 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)
(accumulation_subsequence formula-decl nil convergence_sequences
nil))
nil))
(increasing_bounded_convergence 0
(increasing_bounded_convergence-1 nil 3253549181
("" (skosimp)
(("" (assert)
((""
(grind :defs nil :if-match nil :rewrites
("increasing?" "convergence"))
(("" (use "supfun_is_sup[nat]")
(("" (skolem!)
(("" (inst 1 "x!1")
(("" (skosimp)
(("" (inst -4 "x!1" "i!1")
(("" (assert)
(("" (use "supfun_is_bound" ("x" "i!1"))
(("" (assert)
(("" (expand "abs")
(("" (lift-if) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(supfun_is_sup formula-decl nil real_fun_supinf nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(sequence type-eq-decl nil sequences nil)
(supfun_is_bound formula-decl nil real_fun_supinf nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(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)
(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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_sequences nil)
(increasing? const-decl "bool" real_fun_preds "reals/"))
nil))
(decreasing_bounded_convergence 0
(decreasing_bounded_convergence-1 nil 3253549181
("" (skosimp)
(("" (assert)
((""
(grind :defs nil :if-match nil :rewrites
("decreasing?" "convergence"))
(("" (use "inffun_is_inf[nat]")
(("" (skolem!)
(("" (inst 1 "x!1")
(("" (skosimp)
(("" (inst -4 "x!1" "i!1")
(("" (assert)
(("" (use "inffun_is_bound" ("x" "i!1"))
(("" (assert)
(("" (expand "abs") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(inffun_is_inf formula-decl nil real_fun_supinf nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(sequence type-eq-decl nil sequences nil)
(inffun_is_bound formula-decl nil real_fun_supinf nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_sequences nil)
(decreasing? const-decl "bool" real_fun_preds "reals/"))
nil))
(bolzano_weierstrass1 0
(bolzano_weierstrass1-1 nil 3253549181
("" (skolem!)
(("" (use "monotone_subsequence")
(("" (skosimp)
(("" (use* "bounded_above_subseq" "bounded_below_subseq")
(("" (assert)
(("" (expand "subseq")
(("" (skolem!)
((""
(auto-rewrite "supfun_is_sup2[nat]"
"inffun_is_inf2[nat]"
"supfun_is_bound[nat]"
"inffun_is_bound[nat]"
"accumulation_subsequence")
(("" (ground)
(("1"
(forward-chain "increasing_bounded_convergence")
(("1" (inst? +)
(("1" (ground)
(("1" (inst - "0")
(("1" (use "supfun_is_bound" ("g" "s!1"))
(("1"
(use "inffun_is_bound" ("h" "w!1"))
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (skolem!)
(("2" (inst?)
(("2"
(replace*)
(("2" (assert) nil nil))
nil))
nil))
nil)
("3" (inst?) (("3" (assert) nil nil)) nil))
nil))
nil))
nil)
("2"
(forward-chain "decreasing_bounded_convergence")
(("2" (inst? +)
(("2" (ground)
(("1" (skolem!)
(("1" (inst?)
(("1"
(replace -5)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (inst - "0")
(("2" (use "inffun_is_bound" ("h" "s!1"))
(("2"
(use "supfun_is_bound" ("g" "w!1"))
(("2" (assert) nil nil))
nil))
nil))
nil)
("3" (inst?) (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((monotone_subsequence formula-decl nil monotone_subsequence nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(AND const-decl "[bool, bool -> bool]" booleans 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)
(bounded_above_subseq formula-decl nil sequence_props nil)
(bounded_below_subseq formula-decl nil sequence_props nil)
(subseq const-decl "bool" sequence_props nil)
(decreasing_bounded_convergence formula-decl nil
convergence_sequences nil)
(inffun_is_inf2 formula-decl nil real_fun_supinf nil)
(inf const-decl "real" real_fun_supinf nil)
(increasing_bounded_convergence formula-decl nil
convergence_sequences nil)
(supfun_is_sup2 formula-decl nil real_fun_supinf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(supfun_is_bound formula-decl nil real_fun_supinf nil)
(extraction type-eq-decl nil sequence_props nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(inffun_is_bound formula-decl nil real_fun_supinf nil)
(sup const-decl "real" real_fun_supinf nil)
(accumulation_subsequence formula-decl nil convergence_sequences
nil))
nil))
(bolzano_weierstrass2 0
(bolzano_weierstrass2-1 nil 3253549181
("" (skolem!)
(("" (use "bolzano_weierstrass1")
(("" (skosimp) (("" (inst?) nil nil)) nil)) nil))
nil)
((bolzano_weierstrass1 formula-decl nil convergence_sequences nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(AND const-decl "[bool, bool -> bool]" booleans 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))
nil))
(bolzano_weierstrass3 0
(bolzano_weierstrass3-1 nil 3253549181
("" (skosimp)
(("" (use "bolzano_weierstrass1")
(("" (skosimp)
(("" (rewrite "accumulation_subsequence")
(("" (skosimp)
(("" (inst?)
(("" (assert)
(("" (expand "convergent?") (("" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bolzano_weierstrass1 formula-decl nil convergence_sequences nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(AND const-decl "[bool, bool -> bool]" booleans 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)
(accumulation_subsequence formula-decl nil convergence_sequences
nil)
(convergent? const-decl "bool" convergence_sequences nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(bolzano_weierstrass4 0
(bolzano_weierstrass4-1 nil 3253549181
("" (skosimp)
(("" (case "bounded_above?(u!1) AND bounded_below?(u!1)")
(("1" (ground)
(("1" (case "a!1 <= inf(u!1) AND sup(u!1) <= b!1")
(("1" (ground)
(("1" (use "bolzano_weierstrass1")
(("1" (skosimp)
(("1" (inst + "a!2") (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (ground)
(("1" (rewrite "inffun_is_inf2[nat]")
(("1" (skolem!)
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (rewrite "supfun_is_sup2[nat]")
(("2" (skolem!)
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (delete 2)
(("2" (grind :if-match nil)
(("1" (inst + "a!1")
(("1" (skolem!)
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (inst + "b!1")
(("2" (skolem!)
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")
(sequence type-eq-decl nil sequences nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sup const-decl "real" real_fun_supinf nil)
(inf const-decl "real" real_fun_supinf nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bolzano_weierstrass1 formula-decl nil convergence_sequences nil)
(supfun_is_sup2 formula-decl nil real_fun_supinf nil)
(inffun_is_inf2 formula-decl nil real_fun_supinf nil))
nil))
(prefix_bounded1 0
(prefix_bounded1-1 nil 3253549181
("" (skolem 1 (_ "u!1"))
(("" (induct "n")
(("1" (inst 1 "u!1(0)")
(("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (inst 1 "max(a!1, u!1(j!1+1))")
(("2" (skosimp) (("2" (inst?) (("2" (assert) 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)
(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)
(pred type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(sequence type-eq-decl nil sequences nil)
(nat_induction formula-decl nil naturalnumbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(prefix_bounded2 0
(prefix_bounded2-1 nil 3253549181
("" (skolem 1 (_ "u!1"))
(("" (induct "n")
(("1" (inst 1 "u!1(0)")
(("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (inst 1 "min(a!1, u!1(j!1+1))")
(("2" (skosimp)
(("2" (inst -1 "i!1") (("2" (assert) 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)
(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)
(pred type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(sequence type-eq-decl nil sequences nil)
(nat_induction formula-decl nil naturalnumbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(cauchy_bounded 0
(cauchy_bounded-1 nil 3253549181
("" (skosimp)
(("" (expand "cauchy")
(("" (inst - "1")
(("" (skolem!)
(("" (inst - "n!1" _)
(("" (auto-rewrite "bounded_above?" "bounded_below?" "abs")
(("" (ground)
(("1" (use "prefix_bounded1" ("n" "n!1"))
(("1" (skolem!)
(("1" (inst + "a!1 + 1")
(("1" (skolem!)
(("1" (inst-cp - "n!1")
(("1" (inst - "x!1")
(("1" (inst - "x!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (use "prefix_bounded2" ("n" "n!1"))
(("2" (skolem!)
(("2" (inst + "a!1 - 1")
(("2" (skolem!)
(("2" (inst-cp - "n!1")
(("2" (inst - "x!1")
(("2" (inst - "x!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(cauchy const-decl "bool" convergence_sequences nil)
(prefix_bounded2 formula-decl nil convergence_sequences nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(prefix_bounded1 formula-decl nil convergence_sequences nil)
(sequence type-eq-decl nil sequences 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)
(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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(bounded_below? const-decl "bool" real_fun_preds "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))
nil))
(convergence_cauchy1 0
(convergence_cauchy1-1 nil 3253549181
(""
(grind :defs nil :rewrites ("convergent?" "convergence" "cauchy")
:if-match nil)
(("" (delete -1 -2 -3)
(("" (inst -1 "epsilon!1/2")
(("" (skolem!)
(("" (inst? 1)
(("" (skosimp)
(("" (inst-cp -1 "i!1")
(("" (inst -1 "j!1")
(("" (assert)
(("" (rewrite "abs_diff_commute" -1)
(("" (rewrite "abs_diff_commute" -2)
(("" (lemma "triangle2")
((""
(inst -1 "epsilon!1/2" "epsilon!1/2"
"u!1(j!1)" "l!1" "u!1(i!1)")
(("" (assert)
((""
(rewrite "abs_diff_commute" +)
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sequence type-eq-decl nil sequences nil)
(abs_diff_commute formula-decl nil abs_lems "reals/")
(triangle2 formula-decl nil abs_lems "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types 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)
(>= 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)
(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)
(real_minus_real_is_real application-judgement "real" reals nil)
(cauchy const-decl "bool" convergence_sequences nil)
(convergent? const-decl "bool" convergence_sequences nil)
(convergence const-decl "bool" convergence_sequences nil))
nil))
(convergence_cauchy2 0
(convergence_cauchy2-1 nil 3253549181
("" (skosimp)
(("" (use "bolzano_weierstrass2")
(("1" (skolem!)
(("1" (expand "convergent?")
(("1" (inst?) (("1" (rewrite "cauchy_accumulation") nil nil))
nil))
nil))
nil)
("2" (rewrite "cauchy_bounded") nil nil))
nil))
nil)
((bolzano_weierstrass2 formula-decl nil convergence_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, 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)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(sequence type-eq-decl nil sequences nil)
(u!1 skolem-const-decl "sequence[real]" convergence_sequences nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(convergent? const-decl "bool" convergence_sequences nil)
(cauchy_accumulation formula-decl nil convergence_sequences nil)
(cauchy_bounded formula-decl nil convergence_sequences nil))
nil))
(convergence_cauchy 0
(convergence_cauchy-1 nil 3253549181
("" (skolem!)
(("" (prop)
(("1" (rewrite "convergence_cauchy1") nil nil)
("2" (rewrite "convergence_cauchy2") nil nil))
nil))
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)
(convergence_cauchy1 formula-decl nil convergence_sequences nil)
(convergence_cauchy2 formula-decl nil convergence_sequences nil))
nil)))
¤ Dauer der Verarbeitung: 0.51 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.
|
