|
(gs_bands_2D
(gs_band_pos 0
(gs_band_pos-2 nil 3444146224
("" (skeep :preds? t)
(("" (hide -1) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
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)
(ConnectedGt type-eq-decl nil connected_set "reals/")
(> const-decl "bool" reals nil)
(Connected type-eq-decl nil connected_set "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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))
nil)
(gs_band_pos-1 nil 3444146224 ("" (judgement-tcc) nil nil) nil nil))
(gs2v2_continuous 0
(gs2v2_continuous-2 nil 3459320448
("" (skeep)
(("" (expand "gs2v2")
(("" (rewrite "scal_cont_rv")
(("1" (hide 2) (("1" (rewrite "const_cont_rv") nil nil)) nil)
("2" (hide 2) (("2" (rewrite "id_cont") nil nil)) nil))
nil))
nil))
nil)
((gs2v2 const-decl "Vect2" bands_util nil)
(id_cont formula-decl nil continuous_lambda "analysis/")
(const_cont_rv formula-decl nil vect_cont_2D "vect_analysis/")
(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)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(^ const-decl "Normalized" vectors_2D "vectors/")
(Normalized type-eq-decl nil vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Nz_vector type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions
"analysis/")
(continuous? const-decl "bool" continuous_functions "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(scal_cont_rv formula-decl nil vect2_cont_dot "vect_analysis/"))
nil)
(gs2v2_continuous-1 nil 3459320431 ("" (judgement-tcc) nil nil) nil
nil))
(Vgs_continuous 0
(Vgs_continuous-2 nil 3444142683
("" (skeep)
(("" (expand "Vgs")
(("" (rewrite "sub_cont_rv")
(("1" (hide 2) (("1" (rewrite "const_cont_rv") nil nil)) nil)
("2" (hide 2)
(("2"
(case-replace
"(LAMBDA (gs:real):gs2v2(vo)(gs)) = gs2v2(vo)")
(("1" (assert) nil nil)
("2" (decompose-equality 1) nil nil))
nil))
nil))
nil))
nil))
nil)
((Vgs const-decl "Vect2" gs_bands_2D nil)
(gs2v2_continuous application-judgement "continuous_rv_fun"
gs_bands_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(const_cont_rv formula-decl nil vect_cont_2D "vect_analysis/")
(gs2v2 const-decl "Vect2" bands_util nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(continuous_rv_fun nonempty-type-eq-decl nil cont_real_vect2
"vect_analysis/")
(continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
(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)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sub_cont_rv formula-decl nil vect_cont_2D "vect_analysis/"))
nil)
(Vgs_continuous-1 nil 3444142661 ("" (judgement-tcc) nil nil) nil
nil))
(Omega_gs_TCC1 0
(Omega_gs_TCC1-2 nil 3444142120
("" (skeep)
(("" (rewrite "comp_vr_rv_cont")
(("" (hide 2)
(("" (lemma "omega_v2_continuous")
(("" (inst?)
(("" (expand "continuous?")
(("" (expand "continuous?")
(("" (expand "continuous_vr?")
(("" (expand "continuous_at?")
(("" (expand "continuous_vr?")
(("" (expand "member")
(("" (expand "ball")
(("" (expand "real_dist")
(("" (skeep)
((""
(inst - "x0")
(("1"
(skosimp*)
(("1"
(inst - "epsilon!1")
(("1"
(skosimp*)
(("1"
(inst + "delta!1")
(("1"
(skosimp*)
(("1"
(inst - "x!1")
(("1"
(lemma "dist_norm")
(("1"
(inst?)
(("1"
(case
"abs(omega_v2[D, B, T](s)(x0) - omega_v2[D, B, T](s)(x!1)) = abs(omega_v2[D,B, T](s)(x!1) - omega_v2[D, B, T](s)(x0)) and norm(x0-x!1) = norm(x!1-x0)")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(grind
:exclude
"omega_v2")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vgs_continuous application-judgement "continuous_rv_fun"
gs_bands_2D nil)
(comp_vr_rv_cont formula-decl nil vect2_cont_comp "vect_analysis/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(bool nonempty-type-eq-decl nil booleans nil)
(continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(Vgs const-decl "Vect2" gs_bands_2D nil)
(continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/")
(>= 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)
(D formal-const-decl "posreal" gs_bands_2D nil)
(nnreal type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" gs_bands_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" gs_bands_2D nil)
(omega_v2 const-decl "real" omega_v2 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)
(omega_v2_continuous formula-decl nil omega_v2 nil)
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(real_minus_real_is_real application-judgement "real" reals nil)
(continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/")
(ball const-decl "set[T]" metric_spaces "analysis/")
(dist_norm formula-decl nil distance_2D "vectors/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(x!1 skolem-const-decl "Vect2" gs_bands_2D nil)
(x0 skolem-const-decl "Vect2" gs_bands_2D nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(member const-decl "bool" sets nil)
(continuous_at? const-decl "bool" continuity_ms_def "analysis/")
(continuous? const-decl "bool" continuity_ms_def "analysis/"))
nil)
(Omega_gs_TCC1-1 nil 3444142060 ("" (subtype-tcc) nil nil) nil nil))
(Omega_gs_critical 0
(Omega_gs_critical-1 nil 3443205728
("" (skeep)
(("" (expand "Omega_gs")
(("" (expand "o")
(("" (expand "Vgs")
(("" (lemma "omega_v2_critical_points")
(("" (inst?)
(("" (assert)
(("" (expand "gs_critical?")
(("" (flatten)
(("" (split -1)
(("1" (flatten)
(("1" (assert)
(("1" (lemma "gs_line_complete")
(("1" (inst?) (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (lemma "gs_only_circle_complete")
(("2"
(inst - "Entry" "gs2v2(vo)(gsp)" "s" "T" "vi"
"vo")
(("2" (assert) nil nil)) nil))
nil)
("3" (flatten)
(("3" (lemma "gs_only_circle_complete")
(("3"
(inst - "Exit" "gs2v2(vo)(gsp)" "s" "B"
"vi" "vo")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Omega_gs const-decl "({f | continuous?(f)})" gs_bands_2D nil)
(Vgs const-decl "Vect2" gs_bands_2D nil)
(gs2v2 const-decl "Vect2" bands_util nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(gs_critical? const-decl "bool" gs_bands_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(gs_line_complete formula-decl nil gs_line nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers 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)
(gs_only_circle_complete formula-decl nil gs_only nil)
(gs2v2_gs_only application-judgement "(gs_only?(vo2))" bands_util
nil)
(gs2v2_continuous application-judgement "continuous_rv_fun"
gs_bands_2D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(omega_v2_critical_points formula-decl nil omega_v2 nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" gs_bands_2D nil)
(nnreal type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" gs_bands_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" gs_bands_2D nil)
(O const-decl "[T -> real]" vect2_cont_comp "vect_analysis/"))
nil))
(gs_green_two_parallel 0
(gs_green_two_parallel-1 nil 3443208598
("" (skeep)
(("" (expand "two_parallel?")
(("" (flatten)
(("" (skeep -2)
(("" (expand "gs_green?")
(("" (expand "Vgs")
(("" (expand "gs2v2")
(("" (skeep 1)
((""
(name-replace "cr" "tangent_line(sp,eps)" :hide?
nil)
(("" (case "det(gso * ^(vo) - vi,cr)=0")
(("1" (hide -3 -4)
(("1" (rewrite "parallel_det_0" :dir rl)
(("1" (expand "parallel?")
(("1" (skolem -1 "kk")
(("1"
(lemma "tangent_line_independence")
(("1"
(inst -1 "eps" "sp" "cr")
(("1"
(split -1)
(("1"
(lemma
"horizontal_conflict_ever_scal")
(("1"
(inst -1 "kk" "sp" "cr")
(("1"
(assert)
(("1"
(hide 2)
(("1"
(expand "conflict_2D?")
(("1"
(expand
"horizontal_conflict_ever?")
(("1"
(skeep -3)
(("1"
(inst 1 "t")
(("1"
(replaces
-1
:dir
rl)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "tangent_line?")
(("2"
(inst 1 "1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replaces -1)
(("2"
(expand "conflict_2D?")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -4)
(("2" (rewrite "det_asym")
(("2" (rewrite "det_sub_right")
(("2" (expand "^")
(("2"
(rewrite "scal_assoc")
(("2"
(rewrite "det_scal_right")
(("2"
(rewrite "det_asym" 1)
(("2"
(replace -2)
(("2"
(assert)
(("2"
(rewrite
"parallel_det_0"
:dir
rl)
(("2"
(rewrite
"parallel_det_0"
:dir
rl)
(("2"
(lemma
"vectors_2D.parallel_trans")
(("2"
(inst
-1
"vi"
"vo"
"cr")
(("2"
(assert)
(("2"
(hide-all-but
(-1 1))
(("2"
(rewrite
"parallel_det_0")
(("2"
(rewrite
"det_asym")
(("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))
nil))
nil))
nil)
((two_parallel? const-decl "bool" gs_line nil)
(Vgs const-decl "Vect2" gs_bands_2D nil)
(det const-decl "real" det_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(set type-eq-decl nil sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(Connected type-eq-decl nil connected_set "reals/")
(ConnectedGt type-eq-decl nil connected_set "reals/")
(Nz_vector type-eq-decl nil vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(Normalized type-eq-decl nil vectors_2D "vectors/")
(^ const-decl "Normalized" vectors_2D "vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(parallel_det_0 formula-decl nil parallel_2D "vectors/")
(tangent_line? const-decl "bool" tangent_line nil)
(scal_1 formula-decl nil vectors_2D "vectors/")
(horizontal_conflict_ever_scal formula-decl nil horizontal nil)
(conflict_2D? const-decl "bool" cd2d nil)
(B formal-const-decl "nnreal" gs_bands_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" gs_bands_2D nil)
(Lookahead type-eq-decl nil Lookahead nil)
(horizontal_conflict_ever? const-decl "bool" horizontal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(tangent_line_independence formula-decl nil tangent_line nil)
(parallel? const-decl "bool" vectors_2D "vectors/")
(scal_zero formula-decl nil vectors_2D "vectors/")
(add_zero_right formula-decl nil vectors_2D "vectors/")
(det_asym formula-decl nil det_2D "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(det_scal_right formula-decl nil det_2D "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(parallel_trans formula-decl nil vectors_2D "vectors/")
(minus_even_is_even application-judgement "even_int" integers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(scal_assoc formula-decl nil vectors_2D "vectors/")
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(det_sub_right formula-decl nil det_2D "vectors/")
(tangent_line const-decl "Nz_vect2" tangent_line nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal 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)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" gs_bands_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)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(gs2v2 const-decl "Vect2" bands_util nil)
(gs_green? const-decl "bool" gs_bands_2D nil))
shostak))
(gs_line_color 0
(gs_line_color-1 nil 3460208057
("" (skeep)
(("" (expand "Q")
(("" (rewrite "dot_add_left")
(("" (lemma "vectors_2D.dot_comm")
(("" (inst -1 "perpR(ss)" "vo")
(("" (replaces -1)
(("" (rewrite "det_perpR" :dir rl)
(("" (lemma "det_asym")
(("" (inst?)
(("" (replaces -1)
((""
(case-replace
"pm*(alpha(ss) * (ss * vo) + beta(ss) * -det(ss, vo) * eps) > 0 = pm*(alpha(ss) * (ss * vo)) > pm*(beta(ss) * det(ss, vo) * eps)")
(("1" (hide -1)
(("1" (expand "alpha")
(("1" (expand "beta")
(("1"
(case-replace
" pm*(sq(D) / sqv(ss) * (ss * vo)) >
pm*(det(ss, vo) * (D * sqrt(sqv(ss) - sq(D)) / sqv(ss)) * eps) = pm*(sq(D)*(ss*vo)) > pm*(det(ss, vo) * (D * sqrt(sqv(ss) - sq(D))) *eps)")
(("1"
(hide -1)
(("1"
(case-replace
"pm*(sq(D) * (ss * vo)) > pm*(det(ss, vo) * (D * sqrt(sqv(ss) - sq(D))) * eps) = pm*(D* (ss * vo)) > pm*(det(ss, vo) * sqrt(sqv(ss) - sq(D)) * eps)")
(("1"
(hide -1)
(("1"
(lift-if)
(("1"
(split 1)
(("1"
(flatten)
(("1"
(split)
(("1"
(flatten)
(("1"
(split 1)
(("1"
(mult-by
-2
"sqrt(sqv(ss) - sq(D))")
(("1"
(mult-by 1 "D")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(case
"pm * (det(ss, vo) * sqrt(sqv(ss) - sq(D)) * eps) > 0")
(("1"
(both-sides-f
-2
"sq")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(lemma
"sq_eps")
(("1"
(inst-cp
-1
"pm")
(("1"
(inst
-1
"eps")
(("1"
(replaces
(-1
-2))
(("1"
(rewrite
"sq_det")
(("1"
(assert)
(("1"
(move-terms
-1
r
1)
(("1"
(case-replace
"sq(D) * sq((ss * vo)) - sq(ss * vo) * sq(D) = 0")
(("1"
(hide
-1)
(("1"
(mult-by
1
"sqv(ss)")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "sq_gt")
(("2"
(inst? -1)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(mult-by
-2
"sqrt(sqv(ss) - sq(D))")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(mult-by -1 "D")
(("2"
(mult-by
-3
"sqrt(sqv(ss)-sq(D))")
(("2"
(both-sides-f
1
"sq")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(lemma
"sq_eps")
(("1"
(inst-cp
-1
"pm")
(("1"
(inst
-1
"eps")
(("1"
(replaces
(-1
-2))
(("1"
(mult-by
-2
"sqv(ss)")
(("1"
(lemma
"sq_det")
(("1"
(inst
-1
"ss"
"vo")
(("1"
(move-terms
-1
r
2)
(("1"
(mult-by
-1
"sq(D)")
(("1"
(replaces
-1
:dir
rl)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "sq_gt")
(("2"
(inst?)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(case "pm*(ss*vo) > 0")
(("1"
(assert)
(("1"
(case
"pm*(sqrt(sqv(ss) - sq(D)) * det(ss, vo) * eps) <= 0")
(("1"
(mult-by -2 "D")
(("1"
(assert)
nil
nil))
nil)
("2"
(mult-by
2
"sqrt(sqv(ss)-sq(D))")
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(split 3)
(("1"
(flatten)
(("1"
(assert)
(("1"
(neg-formula -1)
(("1"
(both-sides-f
-1
"sq")
(("1"
(rewrite
"sq_neg")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(lemma
"sq_eps")
(("1"
(inst-cp
-1
"pm")
(("1"
(inst
-1
"eps")
(("1"
(rewrite
"sq_neg")
(("1"
(rewrite
"sq_times")
(("1"
(replaces
(-1
-2))
(("1"
(mult-by
2
"sqv(ss)")
(("1"
(lemma
"sq_det")
(("1"
(inst
-1
"ss"
"vo")
(("1"
(move-terms
-1
r
2)
(("1"
(mult-by
-1
"sq(D)")
(("1"
(replaces
-1
:dir
rl)
(("1"
(rewrite
"sq_times")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"sq_gt")
(("1"
(mult-by
5
"D")
(("1"
(assert)
nil
nil))
nil)
("2"
(mult-by
6
"sqrt(sqv(ss)-sq(D))")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(neg-formula 1)
(("2"
(mult-by 2 "D")
(("2"
(mult-by
3
"sqrt(sqv(ss)-sq(D))")
(("2"
(both-sides-f
3
"sq")
(("1"
(rewrite
"sq_neg")
(("1"
(rewrite
"sq_neg")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(rewrite
"sq_times")
(("1"
(lemma
"sq_eps")
(("1"
(inst-cp
-1
"pm")
(("1"
(inst
-1
"eps")
(("1"
(replaces
(-1
-2))
(("1"
(assert)
(("1"
(mult-by
-1
"sqv(ss)")
(("1"
(lemma
"sq_det")
(("1"
(inst
-1
"ss"
"vo")
(("1"
(move-terms
-1
r
2)
(("1"
(mult-by
-1
"sq(D)")
(("1"
(replaces
-1
:dir
rl)
(("1"
(assert)
nil
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.66 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.
|
