|
(omega_2D
(IMP_metric_space_real_fun_TCC1 0
(IMP_metric_space_real_fun_TCC1-1 nil 3476187108
("" (lemma "product_is_metric") (("" (propax) nil nil)) nil)
((product_is_metric formula-decl nil cross_metric_spaces
"analysis/")
(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)
(nnreal type-eq-decl nil real_types nil)
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(dist const-decl "nnreal" distance_2D "vectors/"))
nil))
(IMP_ms_composition_cont_TCC1 0
(IMP_ms_composition_cont_TCC1-1 nil 3476187108
("" (lemma "vect2_metric_space") (("" (propax) nil nil)) nil)
((vect2_metric_space formula-decl nil vect2_metric_space
"vect_analysis/"))
nil))
(IMP_ms_composition_cont_TCC2 0
(IMP_ms_composition_cont_TCC2-1 nil 3476187108
("" (lemma "real_metric_space") (("" (inst?) nil nil)) nil)
((fullset const-decl "set" sets nil) (set type-eq-decl nil sets 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_metric_space formula-decl nil real_metric_space "analysis/"))
nil))
(horiz_dist_cont_scaf 0
(horiz_dist_cont_scaf-1 nil 3476187166
("" (skosimp*)
(("" (expand "horiz_dist_scaf")
((""
(case "NOT (LAMBDA (t: real, v): sqv(s!1 + t * v) - sq(D)) = ((LAMBDA (t: real, v): sqv(s!1))+((LAMBDA (t: real, v): 2)*((LAMBDA (t: real, v): t)*(LAMBDA (t: real, v): s!1*v)))+((LAMBDA (t: real, v): sq(t))*(LAMBDA (t: real, v): sqv(v))))-(LAMBDA (t: real, v): sq(D))")
(("1" (hide 2)
(("1" (expand "+")
(("1" (expand "-")
(("1" (expand "*")
(("1" (decompose-equality) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (hide -1)
(("2" (rewrite "diff_continuous[[real,Vect2],d]")
(("1" (hide 2)
(("1" (rewrite "sum_continuous[[real,Vect2],d]")
(("1" (hide 2)
(("1" (rewrite "sum_continuous[[real,Vect2],d]")
(("1" (hide 2)
(("1" (expand "continuous?")
(("1" (skeep)
(("1" (expand "continuous_at?")
(("1"
(skosimp*)
(("1"
(inst + "1")
(("1"
(skeep)
(("1"
(expand "member")
(("1"
(expand "ball")
(("1"
(expand "real_dist")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(rewrite "prod_continuous[[real,Vect2],d]")
(("1" (hide 2)
(("1" (expand "continuous?")
(("1"
(skosimp*)
(("1"
(expand "continuous_at?")
(("1"
(skosimp*)
(("1"
(inst + "1")
(("1"
(skeep)
(("1"
(expand "member")
(("1"
(expand "ball")
(("1"
(expand "real_dist")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(rewrite
"prod_continuous[[real,Vect2],d]")
(("1"
(hide 2)
(("1"
(expand "continuous?")
(("1"
(skosimp*)
(("1"
(expand "continuous_at?")
(("1"
(skosimp*)
(("1"
(inst + "epsilon!1")
(("1"
(skosimp*)
(("1"
(expand "member")
(("1"
(expand "ball")
(("1"
(expand "real_dist")
(("1"
(expand "d")
(("1"
(expand
"real_dist")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "continuous?")
(("2"
(skosimp*)
(("2"
(lemma "dot_cont_vr")
(("2"
(inst
-
"(LAMBDA (v): s!1)"
"(LAMBDA (v): v)")
(("1"
(expand "continuous_vr?")
(("1"
(expand "continuous_at?")
(("1"
(expand "continuous_vr?")
(("1"
(inst - "x!1`2")
(("1"
(skosimp*)
(("1"
(inst
-
"epsilon!1")
(("1"
(skosimp*)
(("1"
(inst
+
"delta!1")
(("1"
(skosimp*)
(("1"
(inst
-
"y!1`2")
(("1"
(expand
"member")
(("1"
(expand
"ball")
(("1"
(expand
"real_dist")
(("1"
(lemma
"abs_neg")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"d")
(("1"
(expand
"dist")
(("1"
(lemma
"sq_dist_norm")
(("1"
(inst?)
(("1"
(lemma
"sqrt_eq")
(("1"
(inst?)
(("1"
(assert)
(("1"
(case
"norm(x!1`2 - y!1`2) = norm(y!1`2 - x!1`2)")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
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))
nil)
("2"
(rewrite "id_cont_vv_fun")
nil
nil)
("3"
(lemma "const_cont_vv_fun")
(("3"
(inst - "s!1")
(("3"
(expand "const_fun")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "prod_continuous[[real,Vect2],d]")
(("1" (hide 2)
(("1"
(case "NOT (LAMBDA (t: real, v): sq(t)) = (LAMBDA (t: real, v): t)*(LAMBDA (t: real, v): t)")
(("1" (hide 2)
(("1" (expand "*")
(("1"
(expand "sq")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (hide -1)
(("2"
(rewrite
"prod_continuous[[real,Vect2],d]")
(("1"
(hide 2)
(("1" (grind) nil nil))
nil)
("2"
(hide 2)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "sqv_cont_vr")
(("2" (inst - "(LAMBDA (v): v)")
(("1" (expand "continuous?")
(("1"
(expand "continuous_vr?")
(("1"
(skosimp*)
(("1"
(inst - "x!1`2")
(("1"
(expand "continuous_vr?")
(("1"
(expand "continuous_at?")
(("1"
(skosimp*)
(("1"
(inst - "epsilon!1")
(("1"
(skosimp*)
(("1"
(inst + "delta!1")
(("1"
(skosimp*)
(("1"
(inst - "y!1`2")
(("1"
(assert)
(("1"
(expand "ball")
(("1"
(expand
"real_dist")
(("1"
(lemma
"abs_neg")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"d")
(("1"
(expand
"dist")
(("1"
(lemma
"sq_dist_norm")
(("1"
(inst?)
(("1"
(lemma
"sqrt_eq")
(("1"
(inst?)
(("1"
(assert)
(("1"
(case
"norm(x!1`2 - y!1`2) = norm(y!1`2 - x!1`2)")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
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))
nil))
nil))
nil)
("2" (rewrite "id_cont_vv") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
(diff_continuous formula-decl nil metric_space_real_fun
"analysis/")
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(B formal-const-decl "nnreal" omega_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil)
(Lookahead type-eq-decl nil Lookahead nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(fullset const-decl "set" sets nil)
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(dist const-decl "nnreal" distance_2D "vectors/")
(d const-decl "nnreal" cross_metric_spaces "analysis/")
(sum_continuous formula-decl nil metric_space_real_fun "analysis/")
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(continuous_at? const-decl "bool" continuity_ms_def "analysis/")
(member const-decl "bool" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(abs_0 formula-decl nil abs_lems "reals/")
(ball const-decl "set[T]" metric_spaces "analysis/")
(prod_continuous formula-decl nil metric_space_real_fun
"analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(dot_cont_vr formula-decl nil vect2_cont_dot "vect_analysis/")
(const_cont_vv_fun formula-decl nil cont_vect2_vect2
"vect_analysis/")
(const_fun const-decl "[Vect2 -> Vect2]" limit_vect2_vect2
"vect_analysis/")
(id_cont_vv_fun formula-decl nil cont_vect2_vect2 "vect_analysis/")
(continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/")
(continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/")
(minus_real_is_real application-judgement "real" reals nil)
(sq_dist_norm formula-decl nil distance_2D "vectors/")
(sqrt_eq formula-decl nil sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sq_dist const-decl "nnreal" distance_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(abs_neg formula-decl nil abs_lems "reals/")
(s!1 skolem-const-decl "Vect2" omega_2D nil)
(continuous_vv? const-decl "bool" cont_vect2_vect2
"vect_analysis/")
(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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sqv_cont_vr formula-decl nil vect_cont_2D "vect_analysis/")
(id_cont_vv formula-decl nil vect_cont_2D "vect_analysis/")
(continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2
"vect_analysis/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_plus_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" omega_2D nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "real" vectors_2D "vectors/"))
nil))
(conflict_2D_on_open_interval 0
(conflict_2D_on_open_interval-1 nil 3476702880
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (expand "conflict_2D?")
(("1" (skosimp*)
(("1" (lemma "horiz_dist_cont_scaf")
(("1" (inst - "s")
(("1" (expand "continuous?")
(("1" (inst - "(t!1,v)")
(("1" (expand "continuous_at?")
(("1" (inst - "sq(D) - sqv(s+t!1*v)")
(("1" (skosimp*)
(("1" (expand "member")
(("1" (expand "ball")
(("1"
(expand "real_dist")
(("1"
(expand "horiz_dist_scaf")
(("1"
(expand "d")
(("1"
(expand "real_dist")
(("1"
(case "t!1 = B")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(name
"newt"
"min(B+delta!1/2,(B+T)/2)")
(("1"
(case
"B < newt AND newt < T")
(("1"
(flatten)
(("1"
(inst
-4
"(newt,v)")
(("1"
(assert)
(("1"
(split -4)
(("1"
(inst
+
"newt")
(("1"
(assert)
nil
nil))
nil)
("2"
(replace
-3
:dir
rl)
(("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand "extend")
(("2"
(assert)
(("2"
(expand
"fullset")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1 :dir rl)
(("2"
(hide-all-but 1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "t!1 = T")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(name
"newt"
"max(T-delta!1/2,(B+T)/2)")
(("1"
(case
"B < newt AND newt < T")
(("1"
(flatten)
(("1"
(inst
-4
"(newt,v)")
(("1"
(assert)
(("1"
(split -4)
(("1"
(inst
+
"newt")
(("1"
(assert)
nil
nil))
nil)
("2"
(replace
-3
:dir
rl)
(("2"
(expand
"abs")
(("2"
(typepred
"max(T - delta!1 / 2, (B + T) / 2)")
(("2"
(name
"AA"
"max(T - delta!1 / 2, (B + T) / 2)")
(("2"
(replace
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"extend")
(("2"
(assert)
(("2"
(expand
"fullset")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-1
:dir
rl)
(("2"
(hide-all-but 1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "t!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (expand "extend")
(("2" (expand "fullset") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (skosimp*)
(("2" (expand "conflict_2D?")
(("2" (inst + "topen!1") nil nil)) nil))
nil))
nil))
nil))
nil)
((conflict_2D? const-decl "bool" cd2d nil)
(horiz_dist_cont_scaf formula-decl nil omega_2D nil)
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(continuous_at? const-decl "bool" continuity_ms_def "analysis/")
(ball const-decl "set[T]" metric_spaces "analysis/")
(horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
(newt skolem-const-decl
"{p: real | p >= T - delta!1 / 2 AND p >= (B + T) / 2}" omega_2D
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(+ const-decl "[numfield, numfield -> numfield]" 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)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(dist_eq_args formula-decl nil distance_2D "vectors/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(newt skolem-const-decl
"{z: posreal | z <= B + delta!1 / 2 AND z <= (B + T) / 2}"
omega_2D nil)
(delta!1 skolem-const-decl "posreal" omega_2D nil)
(< const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(d const-decl "nnreal" cross_metric_spaces "analysis/")
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(member const-decl "bool" sets nil)
(* const-decl "Vector" vectors_2D "vectors/")
(s skolem-const-decl "Vect2" omega_2D nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(D formal-const-decl "posreal" omega_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(B formal-const-decl "nnreal" omega_2D 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)
(T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil)
(Lookahead type-eq-decl nil Lookahead nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil) (set type-eq-decl nil sets nil)
(fullset const-decl "set" sets nil)
(t!1 skolem-const-decl "Lookahead[B, T]" omega_2D nil)
(v skolem-const-decl "Vect2" omega_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
shostak))
(circle_hit 0
(circle_hit-1 nil 3476190111
("" (skeep)
(("" (name "ep" "M - horiz_dist_scaf(s)(t,v)")
(("" (lemma "horiz_dist_cont_scaf")
(("" (inst - "s")
(("" (expand "continuous?")
(("" (inst - "(t,v)")
(("1" (expand "continuous_at?")
(("1" (inst - "ep")
(("1" (skeep -1)
(("1" (inst + "delta")
(("1" (skeep)
(("1" (inst - "(t1,v)")
(("1" (expand "member")
(("1" (expand "ball")
(("1"
(expand "d")
(("1"
(expand "real_dist")
(("1"
(assert)
(("1"
(prop)
(("1"
(name
"A1"
"horiz_dist_scaf(s)(t,v)")
(("1"
(replace -1)
(("1"
(name
"B2"
"horiz_dist_scaf(s)(t1,v)")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(hide -1)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-3 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "extend")
(("2" (expand "fullset")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (expand "extend")
(("2" (expand "fullset") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Lookahead type-eq-decl nil Lookahead nil)
(T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil)
(B formal-const-decl "nnreal" omega_2D nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
(D formal-const-decl "posreal" omega_2D 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-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)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil) (set type-eq-decl nil sets nil)
(fullset const-decl "set" sets nil)
(t skolem-const-decl "Lookahead[B, T]" omega_2D nil)
(v skolem-const-decl "Vect2" omega_2D 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)
(ep skolem-const-decl "real" omega_2D nil)
(t1 skolem-const-decl "Lookahead[B, T]" omega_2D nil)
(ball const-decl "set[T]" metric_spaces "analysis/")
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(dist_eq_args formula-decl nil distance_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(d const-decl "nnreal" cross_metric_spaces "analysis/")
(member const-decl "bool" sets nil)
(continuous_at? const-decl "bool" continuity_ms_def "analysis/")
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(horiz_dist_cont_scaf formula-decl nil omega_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(horiz_dist_scaf_bounded_below 0
(horiz_dist_scaf_bounded_below-1 nil 3476190147
("" (skosimp*)
(("" (expand "bounded_below?")
(("" (inst + "-sq(D)")
(("" (skeep)
(("" (expand "horiz_dist_scaf") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(D formal-const-decl "posreal" omega_2D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(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 -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil))
nil))
(omega_2D_TCC1 0
(omega_2D_TCC1-1 nil 3476187108
("" (skeep)
(("" (expand "bounded_below?")
(("" (inst + "-sq(D)")
(("" (skeep)
(("" (expand "horiz_dist_scaf") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(D formal-const-decl "posreal" omega_2D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(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 -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil))
nil))
(omega_2D_TCC2 0
(omega_2D_TCC2-1 nil 3476187108
("" (inst + "B") (("" (assert) nil nil)) nil)
((Lookahead type-eq-decl nil Lookahead nil)
(T formal-const-decl "{AB: posreal | AB > B}" omega_2D 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)
(B formal-const-decl "nnreal" omega_2D nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(tau_2D_nonempty 0
(tau_2D_nonempty-1 nil 3476190288
("" (skosimp*)
(("" (lemma "curried_min_exists_2D")
((""
(inst -
"(LAMBDA (t: real, v: Vect2): IF (B<= t AND t <= T) THEN horiz_dist_scaf(s!1)(t,v) ELSE 0 ENDIF)"
"B" "T")
(("1" (ground)
(("1" (inst - "v!1")
(("1" (ground)
(("1" (hide-all-but (-4 1))
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (skosimp*)
(("1" (inst -2 "tmin!1")
(("1" (typepred "tmin!1")
(("1" (assert)
(("1"
(expand "omega_2D")
(("1"
(expand "inf")
(("1"
(lemma "glb_lem")
(("1"
(inst
-1
"Im(LAMBDA (t: Lookahead): horiz_dist_scaf(s!1)(t, v!1))"
"horiz_dist_scaf(s!1)(tmin!1, v!1)")
(("1"
(assert)
(("1"
(expand
"greatest_lower_bound?")
(("1"
(hide 2)
(("1"
(split 1)
(("1"
(expand "lower_bound?")
(("1"
(skosimp*)
(("1"
(typepred "s!2")
(("1"
(expand "Im" -)
(("1"
(skosimp*)
(("1"
(inst
-
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"lower_bound?")
(("2"
(inst
-
"horiz_dist_scaf(s!1)(tmin!1, v!1)")
(("2"
(expand "Im")
(("2"
(inst
+
"tmin!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "tmin!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "horiz_dist_cont_scaf")
(("2" (inst - "s!1")
(("2" (expand "continuous?")
(("2" (skosimp*)
(("2" (inst - "x!1")
(("1" (expand "continuous_at?")
(("1" (skosimp*)
(("1" (inst - "epsilon!1")
(("1" (skosimp*)
(("1"
(inst + "delta!1")
(("1"
(skosimp*)
(("1"
(inst - "y!1")
(("1"
(assert)
(("1"
(typepred "y!1")
(("1"
(expand "extend")
(("1"
(split -1)
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand "ball")
(("1"
(expand
"real_dist")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.193 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.
|
