|
(horizontal_criterion_line
(horizontal_criterion_rewrite 0
(horizontal_criterion_rewrite-2 nil 3470043336
("" (skeep)
(("" (expand "horizontal_criterion?")
(("" (assert)
((""
(case "NOT FORALL (bb1,bb2,bb3:bool): (bb1 IFF bb2) IMPLIES ((bb1 AND bb3) IFF (bb2 AND bb3))")
(("1" (hide 2) (("1" (grind) nil nil)) nil)
("2" (inst?)
(("2" (replace 1)
(("2" (hide 2)
(("2"
(name "G"
"(LAMBDA (vvvv: Vector): eps * det(vvvv, tangent_line(sp, eps)))")
(("2" (label "Gname" -1)
(("2"
(name "H"
"(LAMBDA (vvvv: Vector): R(sp) * det(sp, vvvv) * eps - sp * vvvv)")
(("2" (label "Hname" -1)
(("2" (name "VT" "tangent_line(sp,eps)")
(("2" (label "hokie" -1)
(("2" (replace -1)
(("2"
(name "UV" "-eps*perpR(VT)")
(("2"
(label "UVname" -1)
(("2"
(lemma
"linear_functional_perp_signs_unique")
(("2"
(inst - "H" "G" "UV" "VT")
(("2"
(assert)
(("2"
(split -1)
(("1"
(inst - "v")
(("1"
(case
"H(v) /= 0 AND G(v) /= 0")
(("1"
(flatten)
(("1"
(ground)
(("1"
(case "H(v) < 0")
(("1"
(case "G(v) < 0")
(("1"
(replace
"Gname"
-
rl)
(("1"
(assert)
nil
nil))
nil)
("2"
(div-by
-3
"-H(v)")
(("2"
(field -3)
nil
nil))
nil))
nil)
("2"
(replace
"Hname"
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil)
("2"
(case "G(v) < 0")
(("1"
(case "H(v) < 0")
(("1"
(replace
"Hname"
:dir
rl)
(("1"
(assert)
nil
nil))
nil)
("2"
(div-by
-3
"-G(v)")
(("2"
(assert)
nil
nil))
nil))
nil)
("2"
(replace
"Gname"
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(case "G(v) = 0")
(("1"
(hide 1)
(("1"
(replace
"Gname"
-
rl)
(("1"
(assert)
(("1"
(lemma
"parallel_det_0")
(("1"
(inst
-
"v"
"tangent_line(sp,eps)")
(("1"
(case
"det(v,VT) = 0")
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(expand
"parallel?")
(("1"
(skosimp*)
(("1"
(lemma
"line_solution_tangent_line")
(("1"
(inst
-
"eps"
"sp")
(("1"
(expand
"line_solution?")
(("1"
(flatten)
(("1"
(replace
-3
1)
(("1"
(replace
"hokie")
(("1"
(hide-all-but
(-1
1))
(("1"
(rewrite
"det_scal_right")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"eps")
(("2"
(assert)
nil
nil))
nil))
nil)
("2"
(flatten)
(("2"
(replace
-1)
(("2"
(assert)
(("2"
(expand
"det")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "H(v) = 0")
(("1"
(replace
"Hname"
:dir
rl)
(("1"
(assert)
(("1"
(case
"line_solution?(sp,v,eps)")
(("1"
(lemma
"tangent_line_solution")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"tangent_line?")
(("1"
(skosimp*)
(("1"
(replace
"hokie")
(("1"
(replace
-1)
(("1"
(hide-all-but
2)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"line_solution?")
(("2"
(case
"line_solution?(sp,-v,eps)")
(("1"
(lemma
"tangent_line_solution")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"tangent_line?")
(("1"
(skosimp*)
(("1"
(case
"v = (-nnk!1)*tangent_line(sp,eps)")
(("1"
(replace
-1)
(("1"
(replace
"hokie")
(("1"
(hide-all-but
3)
(("1"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(replace
"hokie")
(("2"
(hide-all-but
(-1
1))
(("2"
(expand
"*")
(("2"
(expand
"-")
(("2"
(flatten)
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"line_solution?")
(("2"
(split)
(("1"
(hide-all-but
(-1
1))
(("1"
(grind)
nil
nil))
nil)
("2"
(lemma
"det_scal_right")
(("2"
(inst
-
"-1"
"sp"
"v")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"linear_functional?")
(("2"
(skosimp*)
(("2"
(replace "Hname" + rl)
(("2"
(assert)
(("2"
(hide-all-but 1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(replace "Gname" + rl)
(("3"
(hide-all-but 1)
(("3" (grind) nil nil))
nil))
nil)
("4"
(hide 2)
(("4"
(replace "Hname" + rl)
(("4"
(replace "Gname" + rl)
(("4"
(assert)
(("4"
(replace
"UVname"
+
rl)
(("4"
(rewrite
"det_scal_left")
(("4"
(assert)
(("4"
(rewrite
"det_scal_right")
(("4"
(assert)
(("4"
(case
"R(sp) * det(perpR(VT), VT) * det(sp, perpR(VT)) * -eps * -eps * eps *
eps = R(sp) * det(perpR(VT), VT) * det(sp, perpR(VT)) AND (sp * perpR(VT)) * det(perpR(VT), VT) * -eps * -eps * eps = (sp * perpR(VT)) * det(perpR(VT), VT) * eps")
(("1"
(flatten)
(("1"
(replace
-1)
(("1"
(replace
-2)
(("1"
(factor
1)
(("1"
(case
"det(perpR(VT),VT) > 0 AND (R(sp) * det(sp, perpR(VT)) - sp * perpR(VT) * eps) > 0")
(("1"
(flatten)
(("1"
(lemma
"posreal_times_posreal_is_posreal")
(("1"
(inst?)
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(split)
(("1"
(rewrite
"det_perpR")
(("1"
(typepred
"sqv(perpR(VT))")
(("1"
(expand
"sqv")
(("1"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(split)
(("1"
(rewrite
"det_perpR")
(("1"
(typepred
"sqv(perpR(VT))")
(("1"
(expand
"sqv")
(("1"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(case
"sp * perpR(VT) * eps < 0 AND R(sp) * det(sp, perpR(VT)) >= 0")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide
2)
(("2"
(split)
(("1"
(lemma
"line_solution_det")
(("1"
(inst
-
"eps"
"sp"
"VT")
(("1"
(assert)
(("1"
(lemma
"line_solution_tangent_line")
(("1"
(inst
-
"eps"
"sp")
(("1"
(assert)
(("1"
(flatten)
(("1"
(rewrite
"det_perpR")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"nnreal_times_nnreal_is_nnreal")
(("2"
(inst
-
"R(sp)"
"det(sp,perpR(VT))")
(("2"
(hide
2)
(("2"
(lemma
"line_solution_tangent_line")
(("2"
(inst
-
"eps"
"sp")
(("2"
(lemma
"line_solution_det")
(("2"
(inst
-
"eps"
"sp"
"VT")
(("2"
(assert)
(("2"
(flatten)
(("2"
(rewrite
"det_perpR")
(("2"
(rewrite
"det_perpR")
(("2"
(rewrite
"perpR_perpR")
(("2"
(hide-all-but
(-2
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)
("2"
(hide-all-but
1)
(("2"
(typepred
"eps")
(("2"
(split)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5"
(replace "Hname" + rl)
(("5"
(assert)
(("5"
(lemma
"line_solution_tangent_line")
(("5"
(inst?)
(("5"
(expand
"line_solution?")
(("5"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("6"
(replace "Gname" + rl)
(("6" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_cancel3 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(H skolem-const-decl "[Vector -> real]" horizontal_criterion_line
nil)
(v skolem-const-decl "Vect2" horizontal_criterion_line nil)
(both_sides_div_pos_ge1 formula-decl nil real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(< const-decl "bool" reals nil)
(G skolem-const-decl "[Vector -> real]" horizontal_criterion_line
nil)
(scal_neg_1 formula-decl nil vectors_2D "vectors/")
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(- const-decl "Vector" vectors_2D "vectors/")
(tangent_line_solution formula-decl nil tangent_line nil)
(tangent_line? const-decl "bool" tangent_line nil)
(parallel? const-decl "bool" vectors_2D "vectors/")
(line_solution_tangent_line formula-decl nil tangent_line nil)
(line_solution? const-decl "bool" line_solutions nil)
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(det_scal_right formula-decl nil det_2D "vectors/")
(nzreal nonempty-type-eq-decl nil reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(parallel_det_0 formula-decl nil parallel_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(linear_functional? const-decl "bool" linear_transformations_2D
"vectors/")
(det_scal_left formula-decl nil det_2D "vectors/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(line_solution_det formula-decl nil line_solutions nil)
(perpR_perpR formula-decl nil perpendicular_2D "vectors/")
(neg_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil)
(VT skolem-const-decl "Nz_vect2" horizontal_criterion_line nil)
(sp skolem-const-decl "Sp_vect2[D]" horizontal_criterion_line nil)
(eps skolem-const-decl "Sign" horizontal_criterion_line nil)
(det_perpR formula-decl nil det_2D "vectors/")
(posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(det_eq_0 formula-decl nil det_2D "vectors/")
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(linear_functional_perp_signs_unique formula-decl nil
linear_transformations_2D "vectors/")
(Nz_vector type-eq-decl nil vectors_2D "vectors/")
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(sign_neg_clos application-judgement "Sign" sign "reals/")
(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/")
(<= const-decl "bool" reals nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" 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)
(/= 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)
(det const-decl "real" det_2D "vectors/")
(R const-decl "nnreal" horizontal_criteria nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_criterion_line 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil)
(horizontal_criterion_rewrite-1 nil 3469886798
("" (skeep)
(("" (ground)
(("1" (lemma "horiz_criteria_implies_half_plane")
(("1" (expand "horizontal_half_plane?")
(("1" (inst - "eps" "v" "sp" "zero") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "horizontal_criterion?")
(("2" (case "eps * det(v, tangent_line(sp, eps)) < 0")
(("1" (hide -2)
(("1"
(name "G"
"(LAMBDA (vvvv: Vector): eps * det(vvvv, tangent_line(sp, eps)))")
(("1" (label "Gname" -1)
(("1"
(name "H"
"(LAMBDA (vvvv: Vector): R(sp) * det(sp, vvvv) * eps - sp * vvvv)")
(("1" (label "Hname" -1)
(("1" (name "VT" "tangent_line(sp,eps)")
(("1" (label "hokie" -1)
(("1" (replace -1)
(("1" (name "UV" "-eps*perpR(VT)")
(("1" (label "UVname" -1)
(("1"
(case
"H(UV) < 0 AND G(UV) < 0 AND H(VT) = 0 AND G(VT) = 0")
(("1"
(flatten)
(("1"
(label "HUV" -1)
(("1"
(label "GUV" -2)
(("1"
(label "HVT" -3)
(("1"
(label "GVT" -4)
(("1"
(lemma
"linear_functional_perp_signs_unique")
(("1"
(inst
-
"H"
"G"
"UV"
"VT")
(("1"
(assert)
(("1"
(split -1)
(("1"
(inst - "v")
(("1"
(case "G(v) < 0")
(("1"
(div-by
-2
"-G(v)")
(("1"
(replace
"Hname"
-2
rl)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(replace
"Gname"
+
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"linear_functional?")
(("2"
(skosimp*)
(("2"
(replace
"Hname"
+
rl)
(("2"
(assert)
(("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(replace
"Gname"
+
rl)
(("3"
(hide-all-but 1)
(("3"
(grind)
nil
nil))
nil))
nil)
("4"
(lemma
"negreal_times_negreal_is_posreal")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.116 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.
|
