|
(integral_cont_scaf
(IMP_integral_prep_TCC1 0
(IMP_integral_prep_TCC1-1 nil 3253546854
("" (skosimp*)
(("" (lemma "connected_domain")
(("" (inst?) (("" (inst -1 "y!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((connected_domain formula-decl nil integral_cont_scaf nil)) nil))
(IMP_integral_prep_TCC2 0
(IMP_integral_prep_TCC2-1 nil 3253546854
("" (skosimp*)
(("" (lemma "not_one_element") (("" (inst?) nil nil)) nil)) nil)
((not_one_element formula-decl nil integral_cont_scaf nil)) nil))
(adh_lem 0
(adh_lem-2 nil 3477662882
("" (skosimp*)
(("" (expand "adh")
(("" (skosimp*)
(("" (expand "fullset")
(("" (case "x!1+e!1/2 <= b!1")
(("1" (inst + "x!1+e!1/2")
(("1" (expand "abs") (("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (lemma "connected_domain")
(("2" (expand "connected?")
(("2" (inst -1 "a!1" "b!1" "e!1/2 + x!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (inst + "b!1")
(("1" (expand "abs") (("1" (ground) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(adh const-decl "setof[real]" convergence_functions nil)
(fullset const-decl "set" sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(e!1 skolem-const-decl "posreal" integral_cont_scaf nil)
(x!1 skolem-const-decl "T" integral_cont_scaf nil)
(a!1 skolem-const-decl "T" integral_cont_scaf nil)
(b!1 skolem-const-decl "T" integral_cont_scaf nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(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)
(connected_domain formula-decl nil integral_cont_scaf nil)
(connected? const-decl "bool" deriv_domain_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_pred const-decl "[real -> boolean]" integral_cont_scaf nil)
(T formal-subtype-decl nil integral_cont_scaf 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 "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))
nil)
(adh_lem-1 nil 3253546854
("" (skosimp*)
(("" (expand "adh")
(("" (skosimp*)
(("" (expand "fullset")
(("" (case "x!1+e!1/2 <= b!1")
(("1" (inst + "x!1+e!1/2")
(("1" (expand "abs") (("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (lemma "connected_domain")
(("2" (inst -1 "a!1" "b!1" "e!1/2 + x!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (inst + "b!1")
(("1" (expand "abs") (("1" (ground) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((adh const-decl "setof[real]" convergence_functions nil)
(closed_interval type-eq-decl nil intervals_real "reals/"))
nil))
(cont_restrict 0
(cont_restrict-1 nil 3253546854
("" (skosimp*)
(("" (typepred "x!1")
(("" (expand "continuous?")
(("" (skosimp*)
(("" (inst - "epsilon!1")
(("" (skosimp*)
(("" (inst + "delta!1")
(("" (skosimp*)
(("" (expand "restrict")
(("" (inst - "x!2") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((closed_interval type-eq-decl nil intervals_real "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-subtype-decl nil integral_cont_scaf nil)
(T_pred const-decl "[real -> boolean]" integral_cont_scaf nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_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)
(restrict const-decl "R" restrict 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)
(continuous? const-decl "bool" continuous_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(cont_interv_TCC1 0
(cont_interv_TCC1-1 nil 3374402964
("" (skosimp*) (("" (typepred "ii!1") (("" (assert) nil nil)) nil))
nil)
((partition type-eq-decl nil integral_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-subtype-decl nil integral_cont_scaf nil)
(T_pred const-decl "[real -> boolean]" integral_cont_scaf nil)
(below type-eq-decl nil nat_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(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)
(< const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(cont_interv_TCC2 0
(cont_interv_TCC2-1 nil 3374402964
("" (skosimp*) (("" (typepred "ii!1") (("" (assert) nil nil)) nil))
nil)
((partition type-eq-decl nil integral_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-subtype-decl nil integral_cont_scaf nil)
(T_pred const-decl "[real -> boolean]" integral_cont_scaf nil)
(below type-eq-decl nil nat_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(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)
(< const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(cont_interv 0
(cont_interv-3 nil 3477662850
("" (skosimp*)
(("" (expand "continuous?")
(("" (skosimp*)
(("" (expand "restrict")
(("" (inst?)
(("1" (assert)
(("1" (rewrite "continuity_def")
(("1" (rewrite "continuity_def")
(("1" (expand "convergence")
(("1" (expand "convergence")
(("1" (prop)
(("1" (hide -2)
(("1" (assert)
(("1" (expand "adh")
(("1"
(skosimp*)
(("1"
(inst -1 "e!1")
(("1"
(skosimp*)
(("1"
(typepred "x0!1")
(("1"
(typepred "x!1")
(("1"
(case
"x0!1 = seq(P!1)(ii!1)")
(("1"
(case
"e!1 <= seq(P!1)(1 + ii!1) - x0!1")
(("1"
(inst + "x0!1+e!1/2")
(("1"
(assert)
(("1"
(expand "fullset")
(("1"
(expand "abs" 1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"connected_domain")
(("2"
(expand
"connected?")
(("2"
(inst
-1
"x0!1"
"seq(P!1)(1 + ii!1)"
"(e!1 / 2 + x0!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
+
"(seq(P!1)(1 + ii!1) + x0!1)/2")
(("1"
(expand "fullset")
(("1"
(expand "abs" 2)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(lemma
"connected_domain")
(("2"
(expand "connected?")
(("2"
(inst
-1
"x0!1"
"seq(P!1)(1 + ii!1)"
"(seq(P!1)(1 + ii!1) + x0!1) / 2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"e!1 <= x0!1 - seq(P!1)(ii!1)")
(("1"
(inst + "x0!1 - e!1/2")
(("1"
(expand "fullset")
(("1"
(expand "abs" 2)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"connected_domain")
(("2"
(expand
"connected?")
(("2"
(inst
-1
"seq(P!1)(ii!1)"
"x0!1"
"(x0!1 - e!1 / 2)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
+
"(x0!1 + seq(P!1)(ii!1))/2")
(("1"
(expand "fullset")
(("1"
(expand "abs")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil))
nil)
("2"
(lemma
"connected_domain")
(("2"
(expand "connected?")
(("2"
(inst
-1
"seq(P!1)(ii!1)"
"x0!1"
"(seq(P!1)(ii!1) + x0!1) / 2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (skosimp*)
(("2" (inst -1 "epsilon!1")
(("2"
(skosimp*)
(("2"
(inst + "delta!1")
(("2"
(skosimp*)
(("2"
(inst?)
(("1" (assert) nil nil)
("2"
(typepred "x!1")
(("2"
(hide -1 -4 -5 -6 2)
(("2"
(typepred "P!1")
(("2"
(lemma "parts_order")
(("2"
(inst-cp
-1
"a!1"
"b!1"
"P!1"
"0"
"ii!1")
(("2"
(inst
-1
"a!1"
"b!1"
"P!1"
"ii!1+1"
"length(P!1)-1")
(("2"
(assert)
(("2"
(split -1)
(("1"
(assert)
(("1"
(split -2)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(typepred
"ii!1")
(("2"
(case
"ii!1 = length(P!1) - 2")
(("1"
(assert)
nil
nil)
("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)
("2" (assert)
(("2" (hide 2)
(("2" (typepred "x0!1")
(("2" (lemma "parts_order")
(("2" (inst-cp -1 "a!1" "b!1" "P!1" "0" "ii!1")
(("2"
(inst -1 "a!1" "b!1" "P!1" "ii!1+1"
"length(P!1)-1")
(("2" (assert)
(("2" (split -1)
(("1" (split -2)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil)
("2" (assert)
(("2"
(split -1)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous? const-decl "bool" continuous_functions nil)
(restrict const-decl "R" restrict nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_functions nil)
(x!1 skolem-const-decl
"closed_interval[T](xx!1(ii!1), xx!1(1 + ii!1))"
integral_cont_scaf nil)
(parts_order formula-decl nil integral_def nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(adh const-decl "setof[real]" convergence_functions nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(e!1 skolem-const-decl "posreal" integral_cont_scaf nil)
(fullset const-decl "set" sets 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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(connected_domain formula-decl nil integral_cont_scaf nil)
(connected? const-decl "bool" deriv_domain_def nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(convergence const-decl "bool" lim_of_functions nil)
(continuity_def formula-decl nil continuous_functions 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)
(<= const-decl "bool" reals nil)
(T_pred const-decl "[real -> boolean]" integral_cont_scaf nil)
(T formal-subtype-decl nil integral_cont_scaf nil)
(a!1 skolem-const-decl "T" integral_cont_scaf 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)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(b!1 skolem-const-decl "T" integral_cont_scaf nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals 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)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(partition type-eq-decl nil integral_def nil)
(P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_cont_scaf
nil)
(xx!1 skolem-const-decl "[below(length(P!1)) -> T]"
integral_cont_scaf nil)
(ii!1 skolem-const-decl "below(length(P!1) - 1)" integral_cont_scaf
nil)
(x0!1 skolem-const-decl
"closed_interval[T](xx!1(ii!1), xx!1(1 + ii!1))"
integral_cont_scaf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil)
(cont_interv-2 nil 3477662725
(";;; Proof cont_interv-1 for formula integral_cont_scaf.cont_interv"
(skosimp*)
((";;; Proof cont_interv-1 for formula integral_cont_scaf.cont_interv"
(expand "continuous?")
((";;; Proof cont_interv-1 for formula integral_cont_scaf.cont_interv"
(skosimp*)
((";;; Proof cont_interv-1 for formula integral_cont_scaf.cont_interv"
(expand "restrict")
((";;; Proof cont_interv-1 for formula integral_cont_scaf.cont_interv"
(inst?)
(("1" (assert)
(("1" (rewrite "continuity_def")
(("1" (rewrite "continuity_def")
(("1" (expand "convergence")
(("1" (expand "convergence")
(("1" (prop)
(("1" (hide -2)
(("1" (assert)
(("1" (expand "adh")
(("1"
(skosimp*)
(("1"
(inst -1 "e!1")
(("1"
(skosimp*)
(("1"
(typepred "x0!1")
(("1"
(typepred "x!1")
(("1"
(case
"x0!1 = seq(P!1)(ii!1)")
(("1"
(case
"e!1 <= seq(P!1)(1 + ii!1) - x0!1")
(("1"
(inst + "x0!1+e!1/2")
(("1"
(assert)
(("1"
(expand "fullset")
(("1"
(expand "abs" 1)
(("1"
(assert)
nil)))))))
("2"
(assert)
(("2"
(lemma
"connected_domain")
(("2"
("expand "
connected?
")
(inst -1 "
x0!1
" "
seq
(P!1)
(1 + ii!1)
" "
(e!1 / 2 + x0!1)
")
(assert))))
("
2
"
(inst + "
(seq
(P!1)
(1 + ii!1)
+
x0!1)
/2
")
(("
1
" (expand "
fullset
") (expand "
abs
" 2) (assert))
("
2
"
(lemma "
connected_domain
") ("
expand
"connected?")
(("2"
(inst
-1
"x0!1"
"seq(P!1)(1 + ii!1)"
"(seq(P!1)(1 + ii!1) + x0!1) / 2")
(("2"
(assert)
nil)))))))))))))
("2"
(case
"e!1 <= x0!1 - seq(P!1)(ii!1)")
(("1"
(inst + "x0!1 - e!1/2")
(("1"
(expand "fullset")
(("1"
(expand "abs" 2)
(("1"
(assert)
nil)))))
("2"
(assert)
(("2"
(lemma
"connected_domain")
(("2"
("expand "
connected?
")
(inst -1 "
seq
(P!1)
(ii!1)
" "
x0!1
" "
(x0!1 - e!1 / 2)
")
(assert))))
("
2
"
(inst + "
(x0!1
+
seq
(P!1)
(ii!1))
/2
")
(("
1
" (expand "
fullset
") (expand "
abs
") (lift-if) (ground))
("
2
"
(lemma "
connected_domain
") ("
expand
"connected?")
(("2"
(inst
-1
"seq(P!1)(ii!1)"
"x0!1"
"(seq(P!1)(ii!1) + x0!1) / 2")
(("2"
(assert)
nil)))))))))))))))))))))))))))))))
("2" (hide -1)
(("2" (skosimp*)
(("2" (inst -1 "epsilon!1")
(("2"
(skosimp*)
(("2"
(inst + "delta!1")
(("2"
(skosimp*)
(("2"
(inst?)
(("1" (assert) nil)
("2"
(typepred "x!1")
(("2"
(hide -1 -4 -5 -6 2)
(("2"
(typepred "P!1")
(("2"
(lemma "parts_order")
(("2"
(inst-cp
-1
"a!1"
"b!1"
"P!1"
"0"
"ii!1")
(("2"
(inst
-1
"a!1"
"b!1"
"P!1"
"ii!1+1"
"length(P!1)-1")
(("2"
(assert)
(("2"
(split -1)
(("1"
(assert)
(("1"
(split -2)
(("1"
(assert)
nil)
("2"
(assert)
nil)))))
("2"
(assert)
(("2"
(typepred
"ii!1")
(("2"
(case
"ii!1 = length(P!1) - 2")
(("1"
(assert)
nil)
("2"
(assert)
nil)))))))))))))))))))))))))))))))))))))))))))))))))
("2" (assert)
(("2" (hide 2)
(("2" (typepred "x0!1")
(("2" (lemma "parts_order")
(("2" (inst-cp -1 "a!1" "b!1" "P!1" "0" "ii!1")
(("2"
(inst -1 "a!1" "b!1" "P!1" "ii!1+1"
"length(P!1)-1")
(("2" (assert)
(("2" (split -1)
(("1" (split -2)
(("1" (assert) nil) ("2" (assert) nil)))
("2" (assert)
(("2"
(split -1)
(("1" (assert) nil)
("2"
(assert)
nil))))))))))))))))))))))))))))))
";;; developed with shostak decision procedures")
nil nil)
(cont_interv-1 nil 3253546854
("" (skosimp*)
(("" (expand "continuous?")
(("" (skosimp*)
(("" (expand "restrict")
(("" (inst?)
(("1" (assert)
(("1" (rewrite "continuity_def")
(("1" (rewrite "continuity_def")
(("1" (expand "convergence")
(("1" (expand "convergence")
(("1" (prop)
(("1" (hide -2)
(("1" (assert)
(("1" (expand "adh")
(("1"
(skosimp*)
(("1"
(inst -1 "e!1")
(("1"
(skosimp*)
(("1"
(typepred "x0!1")
(("1"
(typepred "x!1")
(("1"
(case
"x0!1 = seq(P!1)(ii!1)")
(("1"
(case
"e!1 <= seq(P!1)(1 + ii!1) - x0!1")
(("1"
(inst + "x0!1+e!1/2")
(("1"
(assert)
(("1"
(expand "fullset")
(("1"
(expand "abs" 1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"connected_domain")
(("2"
(inst
-1
"x0!1"
"seq(P!1)(1 + ii!1)"
"(e!1 / 2 + x0!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
+
"(seq(P!1)(1 + ii!1) + x0!1)/2")
(("1"
(expand "fullset")
(("1"
(expand "abs" 2)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(lemma
"connected_domain")
(("2"
(inst
-1
"x0!1"
"seq(P!1)(1 + ii!1)"
"(seq(P!1)(1 + ii!1) + x0!1) / 2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(case
"e!1 <= x0!1 - seq(P!1)(ii!1)")
(("1"
(inst + "x0!1 - e!1/2")
(("1"
(expand "fullset")
(("1"
(expand "abs" 2)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"connected_domain")
(("2"
(inst
-1
"seq(P!1)(ii!1)"
"x0!1"
"(x0!1 - e!1 / 2)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
+
"(x0!1 + seq(P!1)(ii!1))/2")
(("1"
(expand "fullset")
(("1"
(expand "abs")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil))
nil)
("2"
(lemma
"connected_domain")
(("2"
(inst
-1
"seq(P!1)(ii!1)"
"x0!1"
"(seq(P!1)(ii!1) + x0!1) / 2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (skosimp*)
(("2" (inst -1 "epsilon!1")
(("2"
(skosimp*)
(("2"
(inst + "delta!1")
(("2"
(skosimp*)
(("2"
(inst?)
(("1" (assert) nil nil)
("2"
(typepred "x!1")
(("2"
(hide -1 -4 -5 -6 2)
(("2"
(typepred "P!1")
(("2"
(lemma "parts_order")
(("2"
(inst-cp
-1
"a!1"
"b!1"
"P!1"
"0"
"ii!1")
(("2"
(inst
-1
"a!1"
"b!1"
"P!1"
"ii!1+1"
"length(P!1)-1")
(("2"
(assert)
(("2"
(split -1)
(("1"
(assert)
(("1"
(split -2)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(typepred
"ii!1")
(("2"
(case
"ii!1 = length(P!1) - 2")
(("1"
(assert)
nil
nil)
("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)
("2" (assert)
(("2" (hide 2)
(("2" (typepred "x0!1")
(("2" (lemma "parts_order")
(("2" (inst-cp -1 "a!1" "b!1" "P!1" "0" "ii!1")
(("2"
(inst -1 "a!1" "b!1" "P!1" "ii!1+1"
"length(P!1)-1")
(("2" (assert)
(("2" (split -1)
(("1" (split -2)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil)
("2" (assert)
(("2"
(split -1)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((convergence const-decl "bool" convergence_functions nil)
(parts_order formula-decl nil integral_def nil)
(adh const-decl "setof[real]" convergence_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(continuity_def formula-decl nil continuous_functions nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(partition type-eq-decl nil integral_def nil))
nil))
(fmin_nonempty_TCC1 0
(fmin_nonempty_TCC1-1 nil 3253546854 ("" (subtype-tcc) nil nil)
((real_minus_real_is_real application-judgement "real" reals nil))
nil))
(fmin_nonempty_TCC2 0
(fmin_nonempty_TCC2-1 nil 3253546854 ("" (subtype-tcc) nil nil)
((real_minus_real_is_real application-judgement "real" reals nil))
nil))
(fmin_nonempty_TCC3 0
(fmin_nonempty_TCC3-1 nil 3253546854 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" integral_cont_scaf nil)
(T formal-subtype-decl nil integral_cont_scaf nil)
(> const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(finite_sequence type-eq-decl nil finite_sequences 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)
(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) (< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(partition type-eq-decl nil integral_def nil)
(continuous? const-decl "bool" continuous_functions nil)
(restrict const-decl "R" restrict nil)
(fun_cont_on type-eq-decl nil integral_cont_scaf nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(fmin_nonempty_TCC4 0
(fmin_nonempty_TCC4-1 nil 3253546854
("" (skosimp*)
(("" (lemma "cont_interv")
(("" (inst -1 "a!1" "b!1" "f!1" "P!1" "seq(P!1)")
(("" (assert)
(("" (split -1)
(("1" (inst?)
(("1" (expand "continuous?" -1) (("1" (inst?) nil nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "continuous?")
(("2" (typepred "f!1") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cont_interv formula-decl nil integral_cont_scaf nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(continuous? const-decl "bool" continuous_functions nil)
(partition type-eq-decl nil integral_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.86 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
