|
(cd2d_ever
(cd2d_ever_def 0
(cd2d_ever_def-2 nil 3519742926
("" (skeep)
(("" (case "v /= zero")
(("1" (label "vnz" -1)
(("1" (hide "vnz")
(("1" (name "aa" "sqv(v)")
(("1" (name "bb" "2*(s*v)")
(("1" (name "cc" "sqv(s)-sq(D)")
(("1" (name "qq" "quadratic(aa,bb,cc)")
(("1" (label "qqname" -1)
(("1" (hide -)
(("1" (name "gg" "sq(s*v)-sqv(v)*(sqv(s)-sq(D))")
(("1" (label "ggname" -1)
(("1" (hide "ggname")
(("1" (case "NOT discr(aa,bb,cc) = 4*gg")
(("1"
(hide 2)
(("1"
(expand "aa")
(("1"
(expand "bb")
(("1"
(expand "cc")
(("1"
(expand "gg")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(label "discrlem" -1)
(("2"
(hide "discrlem")
(("2"
(case
"NOT (horizontal_conflict?[D](s,v) IFF (EXISTS (t:nnreal): qq(t)<0))")
(("1"
(case
"NOT (horizontal_conflict?[D](s,v) IFF (EXISTS (t:nnreal): sqv(s+t*v))
(("1"
(hide-all-but 1)
(("1"
(expand
"horizontal_conflict?")
(("1" (propax) nil nil))
nil))
nil)
("2"
(replace -1)
(("2"
(hide -1)
(("2"
(hide-all-but 1)
(("2"
(ground)
(("1"
(skosimp*)
(("1"
(inst + "t!1")
(("1"
(expand "qq")
(("1"
(expand "aa")
(("1"
(expand "bb")
(("1"
(expand "cc")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst + "t!1")
(("2"
(expand "qq")
(("2"
(expand "aa")
(("2"
(expand "bb")
(("2"
(expand "cc")
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(hide -1)
(("2"
(expand "cd2d_ever")
(("2"
(lift-if)
(("2"
(split +)
(("1"
(flatten)
(("1"
(reveal "ggname")
(("1"
(replace -1)
(("1"
(hide "ggname")
(("1"
(split +)
(("1"
(flatten)
(("1"
(case
"aa>0")
(("1"
(case
"-bb/(2*aa)>=0")
(("1"
(inst
+
"-bb/(2*aa)")
(("1"
(reveal
"discrlem")
(("1"
(case
"discr(aa,bb,cc)>0")
(("1"
(mult-by
-1
"1/aa")
(("1"
(hide-all-but
(-1
-4
1))
(("1"
(expand
"qq")
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(case
"1/aa>0")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(cross-mult
1)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(cross-mult
1)
(("2"
(expand
"bb")
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(assert)
nil
nil))
nil)
("2"
(expand
"aa")
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(reveal
"vnz")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(skosimp*)
(("2"
(expand
"qq")
(("2"
(lemma
"a_gt_0_discr_gt_0")
(("2"
(inst
-
"aa"
"bb"
"cc"
"t!1")
(("1"
(expand
"quadratic")
(("1"
(assert)
(("1"
(split
-)
(("1"
(reveal
"discrlem")
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"aa"
1)
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(reveal
"vnz")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(expand
"aa")
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(reveal
"vnz")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(split)
(("1"
(flatten)
(("1"
(inst + "0")
(("1"
(expand "qq")
(("1"
(expand
"quadratic")
(("1"
(expand
"cc")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(skosimp*)
(("2"
(lemma
"quad_min_mono_inc")
(("2"
(inst
-
"aa"
"bb"
"cc"
"t!1"
"0")
(("1"
(assert)
(("1"
(split -)
(("1"
(expand
"qq")
(("1"
(expand
"quadratic")
(("1"
(expand
"aa")
(("1"
(expand
"bb")
(("1"
(expand
"cc")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"t!1 = 0")
(("1"
(replace
-1)
(("1"
(expand
"qq")
(("1"
(expand
"aa")
(("1"
(expand
"bb")
(("1"
(expand
"cc")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("3"
(case
"aa > 0")
(("1"
(cross-mult
1)
(("1"
(expand
"bb")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"aa")
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(reveal
"vnz")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(expand
"aa")
(("4"
(lemma
"sqv_eq_0")
(("4"
(inst?)
(("4"
(reveal
"vnz")
(("4"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(expand
"aa")
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(reveal
"vnz")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(flatten)
(("3"
(expand "aa")
(("3"
(lemma "sqv_eq_0")
(("3"
(inst?)
(("3"
(reveal "vnz")
(("3" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2" (hide -)
(("2" (expand "horizontal_conflict?")
(("2" (expand "cd2d_ever")
(("2" (assert)
(("2" (case "sqv(s))
(("1" (ground) nil nil)
("2" (hide 2)
(("2" (lemma "sqrt_sqv_norm")
(("2" (inst?)
(("2" (replace -1 :dir rl)
(("2" (lemma "sqrt_lt")
(("2"
(inst - "sqv(s)" "sq(D)")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(quadratic const-decl "real" quadratic "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(discr const-decl "real" quadratic "reals/")
(aa skolem-const-decl "nnreal" cd2d_ever nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(cc skolem-const-decl "real" cd2d_ever nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(gg skolem-const-decl "real" cd2d_ever nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(bb skolem-const-decl "real" cd2d_ever nil)
(cd2d_ever const-decl "bool" cd2d_ever nil)
(a_gt_0_discr_gt_0 formula-decl nil quadratic "reals/")
(sqv_eq_0 formula-decl nil vectors_2D "vectors/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(sq_0 formula-decl nil sq "reals/")
(div_mult_pos_ge2 formula-decl nil real_props nil)
(quad_min_mono_inc formula-decl nil quad_minmax "reals/")
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(qq skolem-const-decl "[real -> real]" cd2d_ever nil)
(< const-decl "bool" reals nil)
(horizontal_conflict? const-decl "bool" horizontal nil)
(IFF const-decl "[bool, bool -> bool]" booleans 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 "[numfield, numfield -> numfield]" number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(scal_zero formula-decl nil vectors_2D "vectors/")
(add_zero_right formula-decl nil vectors_2D "vectors/")
(sqrt_lt formula-decl nil sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/"))
nil)
(cd2d_ever_def-1 nil 3519653201
("" (skeep)
(("" (case "v /= zero")
(("1" (label "vnz" -1)
(("1" (hide "vnz")
(("1" (name "aa" "sqv(v)")
(("1" (name "bb" "2*(s*v)")
(("1" (name "cc" "sqv(s)-sq(D)")
(("1" (name "qq" "quadratic(aa,bb,cc)")
(("1" (label "qqname" -1)
(("1" (hide -)
(("1" (name "gg" "sq(s*v)-sqv(v)*(sqv(s)-sq(D))")
(("1" (label "ggname" -1)
(("1" (hide "ggname")
(("1" (case "NOT discr(aa,bb,cc) = 4*gg")
(("1"
(hide 2)
(("1"
(expand "aa")
(("1"
(expand "bb")
(("1"
(expand "cc")
(("1"
(expand "gg")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(label "discrlem" -1)
(("2"
(hide "discrlem")
(("2"
(case
"NOT (horizontal_conflict?(D,s,v) IFF (EXISTS (t:nnreal): qq(t)<0))")
(("1"
(case
"NOT (horizontal_conflict?(D,s,v) IFF (EXISTS (t:nnreal): sqv(s+t*v))
(("1"
(hide-all-but 1)
(("1"
(expand
"horizontal_conflict?")
(("1"
(ground)
(("1"
(lemma "sq_lt")
(("1"
(skosimp*)
(("1"
(inst + "t!1")
(("1"
(inst?)
(("1"
(rewrite
"sq_norm")
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst + "t!1")
(("2"
(lemma "sqrt_lt")
(("2"
(inst?)
(("2"
(rewrite
"sqrt_sqv_norm")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(hide -1)
(("2"
(hide-all-but 1)
(("2"
(ground)
(("1"
(skosimp*)
(("1"
(inst + "t!1")
(("1"
(expand "qq")
(("1"
(expand "aa")
(("1"
(expand "bb")
(("1"
(expand "cc")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst + "t!1")
(("2"
(expand "qq")
(("2"
(expand "aa")
(("2"
(expand "bb")
(("2"
(expand "cc")
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(hide -1)
(("2"
(expand "cd2d_ever")
(("2"
(lift-if)
(("2"
(split +)
(("1"
(flatten)
(("1"
(reveal "ggname")
(("1"
(replace -1)
(("1"
(hide "ggname")
(("1"
(split +)
(("1"
(flatten)
(("1"
(case
"aa>0")
(("1"
(case
"-bb/(2*aa)>=0")
(("1"
(inst
+
"-bb/(2*aa)")
(("1"
(reveal
"discrlem")
(("1"
(case
"discr(aa,bb,cc)>0")
(("1"
(mult-by
-1
"1/aa")
(("1"
(hide-all-but
(-1
-4
1))
(("1"
(expand
"qq")
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(case
"1/aa>0")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(cross-mult
1)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(cross-mult
1)
(("2"
(expand
"bb")
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(assert)
nil
nil))
nil)
("2"
(expand
"aa")
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(reveal
"vnz")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(skosimp*)
(("2"
(expand
"qq")
(("2"
(lemma
"a_gt_0_discr_gt_0")
(("2"
(inst
-
"aa"
"bb"
"cc"
"t!1")
(("1"
(expand
"quadratic")
(("1"
(assert)
(("1"
(split
-)
(("1"
(reveal
"discrlem")
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"aa"
1)
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(reveal
"vnz")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(expand
"aa")
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(reveal
"vnz")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(split)
(("1"
(flatten)
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.79 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.
|
