|
(continuity_interval
(J_TCC1 0
(J_TCC1-1 nil 3442580979
("" (inst 1 "a") (("" (assert) nil nil)) nil)
((b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(bolz_weier 0
(bolz_weier-1 nil 3442580979
("" (skolem!)
(("" (lemma "bolzano_weierstrass4")
(("" (inst -1 "a" "b" "u!1")
(("" (prop)
(("1" (skosimp) (("1" (inst?) (("1" (assert) nil nil)) nil))
nil)
("2" (delete 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((bolzano_weierstrass4 formula-decl nil convergence_sequences nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(c!1 skolem-const-decl "real" continuity_interval nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(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)
(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)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(a formal-const-decl "real" continuity_interval 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))
(unbounded_sequence 0
(unbounded_sequence-1 nil 3442580979
("" (skosimp)
(("" (expand "bounded_above?")
(("" (inst 2 "lambda (n : nat) : epsilon! (x : J) : f!1(x) > n")
(("" (skosimp)
(("" (assert)
(("" (use "epsilon_ax[J]")
(("" (ground)
(("" (inst? 2)
(("" (delete 3)
(("" (skolem!)
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")
(epsilon_ax formula-decl nil epsilons 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)
(> const-decl "bool" reals nil)
(epsilon const-decl "T" epsilons nil)
(pred type-eq-decl nil defined_types nil)
(sequence type-eq-decl nil sequences nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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))
(bounded_from_above 0
(bounded_from_above-1 nil 3442580979
("" (skosimp)
(("" (use "unbounded_sequence")
(("" (assert)
(("" (skolem!)
(("" (use "bolz_weier")
(("" (skolem!)
(("" (expand "continuous?")
(("" (inst? -3)
(("" (forward-chain "continuity_accumulation[J]")
(("" (delete -2 -4 1)
(("" (expand "accumulation")
(("" (expand "o")
((""
(case "EXISTS (m : nat) : f!1(c!1) + 1 < m")
(("1" (skolem!)
(("1"
(inst -2 "1" "m!1")
(("1"
(skosimp)
(("1"
(inst?)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (delete -)
(("2"
(use "axiom_of_archimedes")
(("2"
(skolem!)
(("2"
(inst
1
"IF i!1 < 0 THEN 0 ELSE i!1 ENDIF")
(("1"
(lift-if)
(("1" (assert) nil nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((unbounded_sequence formula-decl nil continuity_interval nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(O const-decl "T3" function_props nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(i!1 skolem-const-decl "int" continuity_interval nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(axiom_of_archimedes formula-decl nil 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(accumulation const-decl "bool" convergence_sequences nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(continuity_accumulation formula-decl nil continuity_props nil)
(continuous? const-decl "bool" continuous_functions 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)
(bolz_weier formula-decl nil continuity_interval nil))
nil))
(bounded_from_below 0
(bounded_from_below-2 nil 3442582177
("" (skosimp)
(("" (lemma "bounded_from_above" ("f" "-f!1"))
(("" (rewrite "bounded_above_neg[J]")
(("" (assert) (("" (rewrite "neg_fun_continuous [J]") nil nil))
nil))
nil))
nil))
nil)
((- const-decl "[T -> real]" real_fun_ops "reals/")
(J nonempty-type-eq-decl nil continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(bounded_from_above formula-decl nil continuity_interval nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(neg_fun_continuous judgement-tcc nil continuous_functions nil)
(bounded_above_neg formula-decl nil real_fun_props "reals/"))
nil)
(bounded_from_below-1 nil 3442580979
("" (skosimp)
(("" (lemma "bounded_from_above" ("f" "-f!1"))
(("" (rewrite "bounded_above_opposite[J]")
(("" (assert) (("" (rewrite "neg_fun_continuous [J]") nil nil))
nil))
nil))
nil))
nil)
nil nil))
(max_extraction_TCC1 0
(max_extraction_TCC1-1 nil 3442580979
("" (lemma "bounded_from_above") (("" (propax) nil nil)) nil)
((bounded_from_above formula-decl nil continuity_interval nil))
nil))
(max_extraction 0
(max_extraction-1 nil 3442580979
("" (skosimp)
(("" (forward-chain "bounded_from_above")
(("" (assert)
((""
(inst 1
"LAMBDA (n : nat) : epsilon! (x : J) : sup(f!1) - f!1(x) < 1 / (1 + n)")
(("" (skolem!)
((""
(lemma "epsilon_ax"
("p"
"LAMBDA (x: J): sup(f!1) - f!1(x) < 1 / (1 + n!1)"))
(("" (assert)
(("" (delete 2)
((""
(lemma "supfun_is_sup[J]"
("g" "f!1" "epsilon" "1/(1+n!1)"))
(("" (skolem!)
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_from_above formula-decl nil continuity_interval 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_minus_real_is_real application-judgement "real" 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)
(pred type-eq-decl nil defined_types nil)
(epsilon const-decl "T" epsilons nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(sup const-decl "real" real_fun_supinf nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(epsilon_ax formula-decl nil epsilons 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)
(supfun_is_sup formula-decl nil real_fun_supinf nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(sup_is_reached 0
(sup_is_reached-1 nil 3442580979
("" (skosimp)
(("" (forward-chain "bounded_from_above")
(("" (assert)
(("" (forward-chain "max_extraction")
(("" (skolem!)
(("" (use "bolz_weier")
(("" (skolem!)
(("" (expand "continuous?")
(("" (inst? -4)
(("" (forward-chain "continuity_accumulation[J]")
(("" (delete -2 -4 -5)
(("" (inst? 1)
(("" (expand "accumulation")
(("" (expand "o")
((""
(use "supfun_is_bound[J]")
((""
(name "eps" "sup(f!1) - f!1(c!1)")
((""
(assert)
((""
(use
"archimedean2"
("x" "eps/2"))
((""
(skolem!)
((""
(inst -4 "eps/2" "a!1")
((""
(skosimp)
((""
(inst -6 "i!1")
((""
(case
"1 / (1 + i!1) < 1 / a!1")
(("1"
(expand "abs")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil)
("2"
(rewrite
"both_sides_div_pos_lt2"
1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_from_above formula-decl nil continuity_interval 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(max_extraction formula-decl nil continuity_interval nil)
(bolz_weier formula-decl nil continuity_interval 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)
(continuous? const-decl "bool" continuous_functions nil)
(continuity_accumulation formula-decl nil continuity_props nil)
(O const-decl "T3" function_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sup const-decl "real" real_fun_supinf 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 "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal 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)
(archimedean2 formula-decl nil real_facts "reals/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(both_sides_div_pos_lt2 formula-decl nil real_props nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(supfun_is_bound formula-decl nil real_fun_supinf nil)
(accumulation const-decl "bool" convergence_sequences nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(maximum_exists 0
(maximum_exists-1 nil 3442580979
("" (skosimp)
(("" (forward-chain "sup_is_reached")
(("" (skolem!)
(("" (inst?)
(("" (rewrite "max_upper_bound[J]")
(("" (assert) (("" (rewrite "bounded_from_above") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sup_is_reached formula-decl nil continuity_interval 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(bounded_from_above formula-decl nil continuity_interval nil)
(max_upper_bound formula-decl nil real_fun_supinf nil))
nil))
(max_pt_TCC1 0
(max_pt_TCC1-1 nil 3442580979
(""
(inst +
"(LAMBDA (f: {f | continuous?[J](f)}): choose({xj: J | is_maximum[J](xj, f)}))")
(("" (skosimp*)
(("" (lemma "maximum_exists")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst?)
(("" (expand "member") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(maximum_exists formula-decl nil continuity_interval nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(is_maximum? const-decl "bool" real_fun_preds "reals/")
(continuous? const-decl "bool" continuous_functions nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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))
(inf_is_reached_TCC1 0
(inf_is_reached_TCC1-1 nil 3442580979
("" (lemma "bounded_from_below") (("" (propax) nil nil)) nil)
((bounded_from_below formula-decl nil continuity_interval nil))
nil))
(inf_is_reached 0
(inf_is_reached-1 nil 3442580979
("" (skosimp)
(("" (use "sup_is_reached" ("f" "-f!1"))
(("" (split)
(("1" (skolem!)
(("1" (rewrite "supfun_neg[J]")
(("1" (expand "-")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (rewrite "bounded_from_below") nil nil))
nil))
nil)
("2" (rewrite "neg_fun_continuous [J]") nil nil))
nil))
nil))
nil)
((sup_is_reached formula-decl nil continuity_interval 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(neg_fun_continuous judgement-tcc nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(bounded_from_below formula-decl nil continuity_interval nil)
(minus_real_is_real application-judgement "real" reals nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(supfun_neg formula-decl nil real_fun_supinf nil))
nil))
(minimum_exists 0
(minimum_exists-1 nil 3442580979
("" (skosimp)
(("" (use "maximum_exists" ("f" "-f!1"))
(("" (split)
(("1" (skolem!)
(("1" (rewrite "max_neg[J]") (("1" (inst?) nil nil)) nil))
nil)
("2" (rewrite "neg_fun_continuous [J]") nil nil))
nil))
nil))
nil)
((maximum_exists formula-decl nil continuity_interval 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(neg_fun_continuous judgement-tcc nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(max_neg formula-decl nil real_fun_props "reals/"))
nil))
(min_pt_TCC1 0
(min_pt_TCC1-2 nil 3445335662
(""
(inst +
"(LAMBDA (f: {f | continuous?[J](f)}): choose({xj: J | is_minimum[J](xj, f)}))")
(("" (skosimp*)
(("" (lemma "minimum_exists")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst?)
(("" (expand "member") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(minimum_exists formula-decl nil continuity_interval nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(is_minimum? const-decl "bool" real_fun_preds "reals/")
(continuous? const-decl "bool" continuous_functions nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(min_pt_TCC1-1 nil 3442580979
(""
(inst +
"(LAMBDA (f: {f | continuous[J](f)}): choose({xj: J | is_minimum[J](xj, f)}))")
(("" (skosimp*)
(("" (lemma "minimum_exists")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst?)
(("" (expand "member") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((is_minimum? const-decl "bool" real_fun_preds "reals/")) nil))
(intermediate_value1_TCC1 0
(intermediate_value1_TCC1-1 nil 3442580979
("" (skosimp) (("" (assert) (("" (assert) nil nil)) nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(intermediate_value1_TCC2 0
(intermediate_value1_TCC2-1 nil 3442580979
("" (skosimp) (("" (assert) 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))
nil))
(intermediate_value1 0
(intermediate_value1-1 nil 3442580979
("" (skosimp)
(("" (name "E" "{y:real| a <= y AND y <= b AND f!1(y) < x!1}")
(("1" (case "nonempty?(E) AND bounded_above?(E)")
(("1" (assert)
(("1" (ground)
(("1" (case "a <= lub(E) AND lub(E) <= b")
(("1" (assert)
(("1" (ground)
(("1" (hide -1 -2 -3 -4)
(("1" (expand "continuous?")
(("1" (inst - "lub(E)")
(("1" (inst + "lub(E)")
(("1"
(auto-rewrite "abs" "subset_fullset[real]")
(("1" (case "x!1 < f!1(lub(E))")
(("1"
(assert)
(("1"
(expand "continuous?")
(("1"
(inst - "f!1(lub(E)) - x!1")
(("1"
(skolem!)
(("1"
(use
"adherence_sup"
("epsilon" "delta!1"))
(("1"
(skolem-typepred)
(("1"
(replace -4 -1 rl)
(("1"
(assert)
(("1"
(use
"lub_is_bound"
("U" "E" "x" "x!2"))
(("1"
(ground)
(("1"
(inst - "x!2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name
"F"
"{y:real | lub(E) < y AND y <= b}")
(("2"
(rewrite "continuity_def[J]")
(("2"
(lemma
"subset_convergence2[J]"
("E1" "F"))
(("2"
(inst
-
"fullset[real]"
"f!1"
"lub(E)"
"f!1(lub(E))")
(("1"
(ground)
(("1"
(delete -4)
(("1"
(lemma
"convergence_lower_bound[J]"
("b" "x!1"))
(("1"
(inst
-
"F"
"f!1"
"lub(E)"
"f!1(lub(E))")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(replace -3 -1 rl)
(("1"
(assert)
(("1"
(use
"lub_is_bound"
("U"
"E"
"x"
"x!2"))
(("1"
(assert)
nil
nil)
("2"
(replace
-4
+
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 -2 -4 -5 2 3)
(("2"
(expand "convergence")
(("2"
(expand "convergence")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(replace -1 + rl)
(("2"
(expand "adh")
(("2"
(skosimp)
(("2"
(case "b < lub(E) + e!1")
(("1"
(assert)
(("1"
(inst + "b")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(inst
+
"lub(E) + e!1/2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (delete -1 -2 -4 -5 -6 2)
(("2" (ground)
(("1" (rewrite "lub_is_bound")
(("1" (replace -1 + rl) (("1" (assert) nil nil))
nil))
nil)
("2" (rewrite "lub_is_lub")
(("2" (skolem-typepred)
(("2" (replace -2 - rl)
(("2" (assert) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1 + rl)
(("2" (delete -1 -2 2)
(("2" (grind :if-match nil)
(("1" (inst + "b")
(("1" (skolem!) (("1" (assert) nil nil)) nil)) nil)
("2" (inst - "a") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp) (("2" (assert) nil nil)) nil))
nil))
nil)
((J nonempty-type-eq-decl nil continuity_interval nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(upper_bound? const-decl "bool" bounded_real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(least_upper_bound? const-decl "bool" bounded_real_defs nil)
(lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(continuous? const-decl "bool" continuous_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(continuous? const-decl "bool" continuous_functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(lub_is_bound formula-decl nil real_facts "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(adherence_sup formula-decl nil real_facts "reals/")
(>= 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(continuity_def formula-decl nil continuous_functions nil)
(adh const-decl "setof[real]" convergence_functions nil)
(F skolem-const-decl "[real -> boolean]" continuity_interval nil)
(E skolem-const-decl "[real -> boolean]" continuity_interval nil)
(fullset const-decl "set" sets nil)
(convergence const-decl "bool" convergence_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergence_lower_bound formula-decl nil convergence_functions
nil)
(subset_fullset formula-decl nil sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(setof type-eq-decl nil defined_types nil)
(subset_convergence2 formula-decl nil convergence_functions nil)
(lub_is_lub formula-decl nil real_facts "reals/")
(bounded_above? const-decl "bool" bounded_real_defs nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil))
nil))
(intermediate_value2_TCC1 0
(intermediate_value2_TCC1-1 nil 3442580979
("" (skosimp) (("" (assert) nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(intermediate_value2 0
(intermediate_value2-1 nil 3442580979
("" (skosimp)
(("" (use "intermediate_value1")
(("" (assert)
(("" (split)
(("1" (propax) nil nil)
("2" (inst 2 "a") (("2" (assert) nil nil)) nil)
("3" (inst 2 "b") (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((intermediate_value1 formula-decl nil continuity_interval nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(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))
nil))
(intermediate_value3_TCC1 0
(intermediate_value3_TCC1-1 nil 3442580979
("" (skosimp) (("" (assert) nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(intermediate_value3 0
(intermediate_value3-1 nil 3442580979
("" (skosimp)
(("" (lemma "intermediate_value1" ("f" "-f!1" "x" "-x!1"))
(("" (auto-rewrite "neg_fun_continuous [J]" "-")
(("" (assert)
(("" (skolem!) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(J nonempty-type-eq-decl nil continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(intermediate_value1 formula-decl nil continuity_interval 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)
(neg_fun_continuous judgement-tcc nil continuous_functions nil))
nil))
(intermediate_value4 0
(intermediate_value4-1 nil 3442580979
("" (skosimp)
(("" (use "intermediate_value3")
(("" (assert)
(("" (split)
(("1" (propax) nil nil)
("2" (inst 2 "b") (("2" (assert) nil nil)) nil)
("3" (inst 2 "a") (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((intermediate_value3 formula-decl nil continuity_interval nil)
(J nonempty-type-eq-decl nil continuity_interval nil)
(b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
(a formal-const-decl "real" continuity_interval nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(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))
nil)))
¤ Dauer der Verarbeitung: 0.77 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.
|
