Quelle horizontal_criterion_line.prf
Sprache: Lisp
(horizontal_criterion_linenil 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" "G" "(LAMBDA (vvvv: Vector): eps * det(vvvv, tangent_line(sp, eps)))" )"2" (label "Gname" -1)"2" "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" "UV" "-eps*perpR(VT)" )"2" "UVname" -1)"2" "linear_functional_perp_signs_unique" )"2" "H" "G" "UV" "VT" )"2" assert )"2" "1" "v" )"1" case "H(v) /= 0 AND G(v) /= 0" )"1" "1" "1" case "H(v) < 0" )"1" case "G(v) < 0" )"1" replace "Gname" "1" assert )nil nil ))nil )"2" "-H(v)" )"2" nil nil ))nil ))nil )"2" replace "Hname" "2" assert )nil nil ))nil ))nil )"2" case "G(v) < 0" )"1" case "H(v) < 0" )"1" replace "Hname" "1" assert )nil nil ))nil )"2" "-G(v)" )"2" assert )nil nil ))nil ))nil )"2" replace "Gname" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "G(v) = 0" )"1" "1" replace "Gname" "1" assert )"1" "parallel_det_0" )"1" "v" "tangent_line(sp,eps)" )"1" case "det(v,VT) = 0" )"1" assert )"1" "1" expand "parallel?" )"1" "1" "line_solution_tangent_line" )"1" "eps" "sp" )"1" expand "line_solution?" )"1" "1" replace "1" replace "hokie" )"1" "1" rewrite "det_scal_right" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "eps" )"2" assert )nil nil ))nil ))nil )"2" "2" replace "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" "1" assert )"1" case "line_solution?(sp,v,eps)" )"1" "tangent_line_solution" )"1" "1" assert )"1" expand "tangent_line?" )"1" "1" replace "hokie" )"1" replace "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "line_solution?" )"2" case "line_solution?(sp,-v,eps)" )"1" "tangent_line_solution" )"1" "1" assert )"1" expand "tangent_line?" )"1" "1" case "v = (-nnk!1)*tangent_line(sp,eps)" )"1" replace "1" replace "hokie" )"1" "1" nil nil ))nil ))nil ))nil )"2" replace "hokie" )"2" "2" expand "*" )"2" expand "-" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "line_solution?" )"2" "1" "1" nil nil ))nil )"2" "det_scal_right" )"2" "-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" "2" replace "Hname" + rl)"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" replace "Gname" + rl)"3" "3" (grind) nil nil ))nil ))nil )"4" "4" replace "Hname" + rl)"4" replace "Gname" + rl)"4" assert )"4" replace "UVname" "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 * AND (sp * perpR(VT)) * det(perpR(VT), VT) * -eps * -eps * eps = (sp * perpR(VT)) * det(perpR(VT), VT) * eps") "1" "1" replace "1" replace "1" "1" case "det(perpR(VT),VT) > 0 AND (R(sp) * det(sp, perpR(VT)) - sp * perpR(VT) * eps) > 0" )"1" "1" "posreal_times_posreal_is_posreal" )"1" "1" assert )nil nil )"2" "2" "1" rewrite "det_perpR" )"1" "sqv(perpR(VT))" )"1" expand "sqv" )"1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1" rewrite "det_perpR" )"1" "sqv(perpR(VT))" )"1" expand "sqv" )"1" nil nil ))nil ))nil ))nil )"2" "2" case "sp * perpR(VT) * eps < 0 AND R(sp) * det(sp, perpR(VT)) >= 0" )"1" "1" assert )nil nil ))nil )"2" "2" "1" "line_solution_det" )"1" "eps" "sp" "VT" )"1" assert )"1" "line_solution_tangent_line" )"1" "eps" "sp" )"1" assert )"1" "1" rewrite "det_perpR" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "nnreal_times_nnreal_is_nnreal" )"2" "R(sp)" "det(sp,perpR(VT))" )"2" "2" "line_solution_tangent_line" )"2" "eps" "sp" )"2" "line_solution_det" )"2" "eps" "sp" "VT" )"2" assert )"2" "2" rewrite "det_perpR" )"2" rewrite "det_perpR" )"2" rewrite "perpR_perpR" )"2" "2" 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" "2" "eps" )"2" "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" "line_solution_tangent_line" )"5" "5" expand "line_solution?" )"5" 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" reals nil )"bool" horizontal_criteria nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posreal" sq "reals/" )"posreal" vectors_2D "vectors/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"odd_int" integers nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )"[Vector -> real]" horizontal_criterion_linenil )"Vect2" horizontal_criterion_line nil )nil real_props nil )"real" reals nil )"bool" reals nil )"[Vector -> real]" horizontal_criterion_linenil )nil vectors_2D "vectors/" )"nnreal" nil )"posreal" nil )"Vector" vectors_2D "vectors/" )nil tangent_line nil )"bool" tangent_line nil )"bool" vectors_2D "vectors/" )nil tangent_line nil )"bool" line_solutions nil )nil vectors_2D "vectors/" )nil det_2D "vectors/" )nil reals nil )"real" reals nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil parallel_2D "vectors/" )"Vector" vectors_2D "vectors/" )"bool" linear_transformations_2D"vectors/" )nil det_2D "vectors/" )"posreal" vectors_2D"vectors/" )nil line_solutions nil )nil perpendicular_2D "vectors/" )"Nz_vector" vectors_2D "vectors/" )nil real_types nil )"Nz_vect2" horizontal_criterion_line nil )"Sp_vect2[D]" horizontal_criterion_line nil )"Sign" horizontal_criterion_line nil )nil det_2D "vectors/" )nil real_types nil )nil det_2D "vectors/" )"Nz_vect2" perpendicular_2D"vectors/" )"(strict_total_order?[real])" real_props nil )nil "vectors/" )nil vectors_2D "vectors/" )"Vect2" perpendicular_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Nz_vector" vectors_2D "vectors/" )"Sign" sign "reals/" )"Nz_vect2" tangent_line nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"bool" reals nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" det_2D "vectors/" )"nnreal" horizontal_criteria nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil horizontal nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D_def "vectors/" )"real" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil )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" "G" "(LAMBDA (vvvv: Vector): eps * det(vvvv, tangent_line(sp, eps)))" )"1" (label "Gname" -1)"1" "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" "1" "HUV" -1)"1" "GUV" -2)"1" "HVT" -3)"1" "GVT" -4)"1" "linear_functional_perp_signs_unique" )"1" "H" "G" "UV" "VT" )"1" assert )"1" "1" "v" )"1" case "G(v) < 0" )"1" "-G(v)" )"1" replace "Hname" "1" assert )nil nil ))nil ))nil )"2" replace "Gname" "2" assert )nil nil ))nil ))nil ))nil )"2" expand "linear_functional?" )"2" "2" replace "Hname" "2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" replace "Gname" "3" "3" nil nil ))nil ))nil )"4" "negreal_times_negreal_is_posreal" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" replace "Hname" + rl)"1" assert )"1" "+" "sp*UV" 1)"1" assert )"1" case "R(sp) * det(sp, UV) * eps = R(sp)*(sp*VT)" )"1" replace -1)"1" "1" case "sp*UV = D*norm(VT)" )"1" replace -1)"1" "1" case "R(sp) * (sp*VT) <= 0 AND D*norm(VT) > 0" )"1" assert )nil nil )"2" "2" "1" case "(sp*VT) <= 0" )"1" "nnreal_times_nnreal_is_nnreal" )"1" "R(sp)" "-(sp*VT)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "line_solution_det" )"2" "eps" "sp" "VT" )"2" assert )"2" "line_solution_tangent_line" )"2" "eps" "sp" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "posreal_times_posreal_is_posreal" )"2" "D" "norm(VT)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "line_solution_det" )"2" "eps" "sp" "VT" )"2" case "sp * UV = -eps * det(sp, VT)" )"1" assert )"1" "line_solution_tangent_line" )"1" "eps" "sp" )"1" assert )nil nil ))nil ))nil ))nil )"2" replace "UVname" "2" rewrite "det_perpR" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "det(sp,UV)*eps = sp*VT" )"1" (assert ) nil nil )"2" replace "UVname" + rl)"2" "2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "Gname" + rl)"2" assert )"2" replace "UVname" + rl)"2" rewrite "det_scal_left" )"2" case "eps*eps = 1" )"1" case "det(perpR(VT),VT) > 0" )"1" (assert ) nil nil )"2" rewrite "det_perpR" )"2" "2" "sqv(perpR(VT))" )"2" expand "sqv" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "eps" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace "Hname" + rl)"3" assert )"3" "line_solution_tangent_line" )"3" "3" replace "hokie" - rl)"3" replace "hokie" )"3" expand "line_solution?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" replace "Gname" + rl)"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "det(v,tangent_line(sp,eps)) = 0" )"1" (lemma "parallel_det_0" )"1" (inst - "v" "tangent_line(sp,eps)" )"1" (assert )"1" (expand "parallel?" )"1" (skosimp*)"1" (lemma "line_solution_tangent_line" )"1" (inst - "eps" "sp" )"1" (expand "line_solution?" )"1" (flatten)"1" replace -3 2)"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replace -1)"2" (hide-all-but 2) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" horizontal_criteria nil )"bool" vectors_2D "vectors/" )"{x: posreal | x < 1}" tangent_line nil )"nnreal" tangent_line nil )"Vect2" tangent_line nil )"Vect2" tangent_line nil )nil sqrt "reals/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil parallel_2D "vectors/" )"Sign" sign "reals/" )"Nz_vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" perpendicular_2D "vectors/" )nil vectors_2D "vectors/" )nil "vectors/" )"Nz_vect2" perpendicular_2D"vectors/" )"bool" linear_transformations_2D"vectors/" )"Vector" vectors_2D "vectors/" )"posreal" sq "reals/" )nil det_2D "vectors/" )"bool" line_solutions nil )"Sign" sign "reals/" )"posreal" vectors_2D "vectors/" )nil det_2D "vectors/" )nil det_2D "vectors/" )nil vectors_2D "vectors/" )"posreal" vectors_2D"vectors/" )nil line_solutions nil )nil tangent_line nil )"nnreal" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" horizontal_criteria nil )"real" det_2D "vectors/" )nil vectors_2D "vectors/" )"Nz_vect2" tangent_line nil )nil sign "reals/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" ))nil 3470055284"" (skeep)"" (lemma "horizontal_criterion_independence" )"" (inst?)"" (assert )"" (inst + "eps" )"" (hide -3)"" (lemma "horizontal_criterion_symmetric" )"" (inst - "eps" "sp" "vo-nvi" )"" (case-replace "-(vo-nvi) = nvi-vo" )"1" (hide -1)"1" (assert )"1" (hide -2)"1" (lemma "horizontal_criterion_rewrite" )"1" (inst?)"1" replace -1)"1" "1" "horizontal_criterion_rewrite" )"1" "1" replace -1)"1" "1" "horizontal_criterion_rewrite" )"1" "1" replace -1)"1" "1" "VT" "tangent_line(sp,eps)" )"1" replace -1)"1" "1" 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" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )"Sp_vect2[D]" nil )"real" reals nil )"posreal" vectors_2D "vectors/" )"posreal" sq "reals/" )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" det_2D "vectors/" )"Nz_vect2" tangent_line nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil nil )"Vector" vectors_2D "vectors/" )nil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"Vector" vectors_2D "vectors/" )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" ))nil ))nil 3470051175"" (skeep)"" (lemma "tangent_line_solution" )"" (inst-cp - "eps" "sp" "nvo-vi" )"" (inst - "eps" "sp" "v" )"" (assert )"" (expand "tangent_line?" )"" (skosimp*)"" (lemma "det_add_left" )"" (inst - "vi-nvo" "nvo-nvi" "v" )"" "vi - nvo + (nvo - nvi) = vi-nvi" )"1" (hide -1)"1" (replace -1)"1" (assert )"1" (lemma "det_scal_left" )"1" "-1" "nvo-vi" "v" )"1" assert )"1" "-(nvo-vi) = vi-nvo" )"1" "1" replace -1)"1" replace -3)"1" replace -4)"1" "1" rewrite "det_scal_left" )"1" rewrite "det_scal_right" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil tangent_line nil )"bool" tangent_line nil )nil det_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil det_2D "vectors/" )"real" reals nil )nil vectors_2D "vectors/" )"real" reals nil )"real" reals nil )"posreal" sq "reals/" )"posreal" vectors_2D "vectors/" )nil det_2D "vectors/" )nil det_2D "vectors/" )"nnreal" nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Nz_vect2" tangent_line nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"odd_int" integers nil )"real" reals nil )"Vector" vectors_2D "vectors/" )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil ))nil ))nil 3470051469"" (skeep)"" (lemma "horizontal_criterion_dot_equality" )"" (inst - "eps" "nvi" "nvo" "sp" "tangent_line(sp,eps)" "vi" )"" (lemma "line_solution_tangent_line" )"" (inst?)"" (assert )"" (lemma "horizontal_criterion_rewrite" )"" (inst?)"" (replace -1)"" (hide -1)"" (lemma "horizontal_criterion_rewrite" )"" (inst?)"" (replace -1)"" (replace -3)"" assert )"" "" expand "line_solution?" )"" "" "" (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 tangent_line nil )"Vector" vectors_2D "vectors/" )"posreal" vectors_2D "vectors/" )"posreal" sq "reals/" )"real" det_2D "vectors/" )"real" reals nil )"real" reals nil )"bool" line_solutions nil )"(total_order?[real])" nil )"real" reals nil )nil nil )"Nz_vect2" tangent_line nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil horizontal nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"bool" reals nil )nil vectors_2D_def "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3470052030"" (skeep)"" (lemma "line_solution_meets_horizontal_criterion" )"" (inst - "eps" "-sp" "nvi-vo" )"" (assert )"" (lemma "horizontal_criterion_special_coordination" )"" (inst - "eps" "nvi" "nvo" "sp" "vo" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )nil nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"Sp_vect2[D]" nil ))nil 3524407913"" (skeep)"" (expand "horizontal_criterion_ext?" )"" (ground)"" (lemma "horizontal_criterion_rewrite" )"" (inst - "eps" "sp" _)"" (inst-cp - "v" )"" (inst-cp - "nv" )"" (inst - "nv-(1/2)*v" )"" (assert )"" (flatten)"" (assert )"" (split +)"1" (hide-all-but (-1 -3 1))"1" "perpR" "tangent_line" ))nil nil ))nil )"2" (assert )"2" (hide-all-but (-2 -4 1))"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" nil )nil nil )"posrat" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"posreal" vectors_2D "vectors/" )"posreal" sq "reals/" )"real" reals nil )"real" reals nil )"real" det_2D "vectors/" )"(total_order?[real])" nil )"real" reals nil )nil horizontal nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"bool" reals nil )nil vectors_2D_def "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3524407031"" (skeep)"" (lemma "horizontal_criterion_independence" )"" (inst?)"" (assert )"" (expand "horizontal_criterion_ext?" )"" (lift-if)"" (assert )"" (ground)"1" (inst + "eps" ) nil nil )"2" (inst + "eps" ) nil nil )"3" (inst + "-eps" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )"Sign" sign "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"bool" nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" ))nil 3529935975"" (skeep)"" (lemma "horizontal_criterion_independence" )"" (inst?)"" (assert )"" (expand "horizontal_criterion_ext?" )"" (lift-if)"" (assert )"" (ground)"1" (inst + "eps" ) nil nil )"2" (inst + "eps" ) nil nil )"3" (inst + "-eps" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )"Sign" sign "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"bool" nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" ))nil )nil 3529935901"" (skeep)"" (lemma "horizontal_criterion_independence" )"" (inst?)"" (assert )"" (expand "horizontal_criterion_ext?" )"" (lift-if)"" (assert )"" (ground)"1" (inst + "eps" ) nil nil )"2" (inst + "eps" ) nil nil )"3" (inst + "-eps" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )nil sign "reals/" )"Sign" sign "reals/" )nil nil ))nil )nil 3524407122"" (skeep)"" (lemma "horizontal_criterion_independence" )"" (inst - "sp" "v" )"" (flatten)"" (assert )"" (hide -1)"" (inst + "eps" )"" (expand "horizontal_criterion_ext?" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil sign "reals/" )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" ))nil 3524407240"" (skeep)"" (lemma "horizontal_criterion_independence" )"" (inst - "sp" "nv" )"" (assert )"" (lemma "horizontal_criterion_ext_subset" )"" (inst - "eps" "nv" "sp" "v" )"" (assert ) (("" (inst + "eps" ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" ))nil 3530265833"" (skeep)"" (lemma "horizontal_criterion_independence" )"" (inst - "sp" "vo-vi" )"" (ground)"1" (expand "horizontal_criterion_ext?" )"1" (split -)"1" (flatten)"1" (lemma "horizontal_criterion_symmetric" )"1" (inst-cp - "eps" "sp" "vo-vi" )"1" (inst - "eps" "sp" "-(vo-vi)" )"1" (assert )"1" (case "-(vo-vi) = vi-vo" )"1" (replace -1)"1" (assert )"1" "horizontal_criterion_independence" )"1" "sp" "nvo-nvi" )"1" "1" "1" assert )"1" "1" "eps" )"1" "1" rewrite "horizontal_criterion_rewrite" )"1" rewrite "horizontal_criterion_rewrite" )"1" rewrite "horizontal_criterion_rewrite" )"1" rewrite "horizontal_criterion_rewrite" )"1" "1" "tangent_line_asymm" )"1" "1" replace "1" "1" "1" "1" "tangent_line" )nil nil ))nil )"2" "2" 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" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "horizontal_criterion_symmetric" )"2" (inst?)"2" (case "-(vo-vi) = vi-vo" )"1" (replace -1)"1" (assert )"1" (split -)"1" (flatten)"1" assert )"1" "horizontal_criterion_symmetric" )"1" "eps" "sp" "vi-vo" )"1" case "-(vi-vo) = vo-vi" )"1" replace -1)"1" replace -2 :dir rl)"1" "horizontal_criterion_symmetric" )"1" "-eps" "sp" "vo-vi" )"1" case "-(vo-vi) = vi-vo" )"1" replace -1)"1" replace "1" assert )"1" replace -5)"1" "1" "1" case "eps!1 = eps OR eps!1 = -eps" )"1" assert )"1" replace "1" "horizontal_criterion_symmetric" )"1" "eps" "sp" "vo-nvi" )"1" case "-(vo-nvi) = nvi-vo" )"1" replace "1" replace "1" "1" "horizontal_criterion_independence" )"1" "sp" "nvo-nvi" )"1" assert )"1" "eps" )"1" "1" rewrite "horizontal_criterion_rewrite" )"1" rewrite "horizontal_criterion_rewrite" )"1" rewrite "horizontal_criterion_rewrite" )"1" rewrite "horizontal_criterion_rewrite" )"1" "1" "1" "1" "tangent_line" )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "eps!1" )"2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" case "-(vi-vo) = vo-vi" )"1" "horizontal_criterion_symmetric" )"1" "eps" "sp" "vi-vo" )"1" replace -1 :dir rl)"1" assert )"1" "horizontal_criterion_symmetric" )"1" "-eps" "sp" "vo-vi" )"1" assert )"1" "1" assert )"1" "horizontal_criterion_symmetric" )"1" "eps" "-sp" "nvi - vo - (1 / 2) * (vi - vo)" )"1" assert )"1" case "NOT -(nvi - vo - (1 / 2) * (vi - vo)) = vo-nvi - (1/2)*(vo-vi)" )"1" "1" nil nil ))nil )"2" replace "2" "ww" "vo - nvi - (1 / 2) * (vo - vi)" )"2" "vv" "nvo - vi - (1 / 2) * (vo - vi)" )"2" case "NOT ww+vv = nvo-nvi" )"1" "1" expand "vv" )"1" expand "ww" )"1" nil nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" "2" "horizontal_criterion_independence" )"2" "2" assert )"2" "eps" )"2" "2" rewrite "horizontal_criterion_rewrite" )"2" rewrite "horizontal_criterion_rewrite" )"2" rewrite "horizontal_criterion_rewrite" )"2" "2" "1" "1" "tangent_line" )nil nil ))nil )"2" "2" 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 ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "horizontal_criterion_ext?" )"2" (inst-cp + "eps" )"2" (inst-cp + "-eps" )"2" (assert )"2" (lemma "horizontal_criterion_symmetric" )"2" (inst - "eps" "sp" "vo-vi" )"2" (lemma "horizontal_criterion_symmetric" )"2" (inst - "-eps" "sp" "vo-vi" )"2" (case "-(vo-vi) = vi-vo" )"1" (replaces -1)"1" replace -1 :dir rl)"1" replace -2 :dir rl)"1" assert )"1" "horizontal_criterion_coordination" )"1" "eps" "nvi" "nvo" "sp" "vi" "vo" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))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 )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )"Sp_vect2[D]" nil )nil nil )"Vector" vectors_2D "vectors/" )nil tangent_line nil )"posreal" vectors_2D "vectors/" )"posreal" sq "reals/" )"real" reals nil )"real" reals nil )"Nz_vector" vectors_2D "vectors/" )"real" reals nil )"real" det_2D "vectors/" )"Vector" vectors_2D "vectors/" )"(total_order?[real])" nil )"real" reals nil )nil nil )nil vectors_2D "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"Sign" sign "reals/" )"posrat" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"Vector" vectors_2D "vectors/" )"Vector" horizontal_criterion_line nil )"Vector" horizontal_criterion_line nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )"bool" nil )nil nil )"Vector" vectors_2D "vectors/" )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" ))nil )nil 3524409185"" (lemma "horizontal_criterion_ext_coordinated_criterion" )"" (skeep)"" (inst - "eps" "nvi" "nvo" "sp" "vi" "vo" )"" (assert )"" (lemma "horizontal_criterion_independence" )"" (inst - "sp" "nvo-nvi" )"" (assert ) (("" (inst + "eps" ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil sign "reals/" ))nil 3525080681"" (skeep)"" (expand "horizontal_criterion_ext?" )"" (split +)"1" (flatten)"1" (assert )"1" (rewrite "horizontal_criterion_rewrite" )"1" (rewrite "horizontal_criterion_rewrite" )"1" (rewrite "horizontal_criterion_rewrite" )"1" (rewrite "horizontal_criterion_rewrite" )"1" (flatten)"1" (split +)"1" (hide-all-but (-1 -3 -5 +))"1" (grind :exclude "tangent_line" ) nil nil ))nil )"2" (hide-all-but (-2 -4 -6 +))"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (split +)"1" (flatten)"1" (replace -1)"1" (hide-all-but (-2 -3 1))"1" (rewrite "horizontal_criterion_rewrite" )"1" (rewrite "horizontal_criterion_rewrite" )"1" (rewrite "horizontal_criterion_rewrite" )"1" (flatten)"1" (split +)"1" "1" "tangent_line" )nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (flatten)"2" (split +)"1" (hide-all-but (-2 -4 1))"1" (rewrite "horizontal_criterion_rewrite" )"1" rewrite "horizontal_criterion_rewrite" )"1" rewrite "horizontal_criterion_rewrite" )"1" "1" "1" "1" "tangent_line" )nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 -4 1))"2" (rewrite "horizontal_criterion_rewrite" )"2" rewrite "horizontal_criterion_rewrite" )"2" rewrite "horizontal_criterion_rewrite" )"2" "2" "1" "1" "tangent_line" )nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" nil )"Sign" sign "reals/" )nil nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D_def "vectors/" )"bool" reals nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"nonneg_real" sq "reals/" )"bool" reals nil )nil real_types nil )"posreal" horizontal_criterion_line nil )nil horizontal nil )"real" reals nil )"(total_order?[real])" nil )"real" det_2D "vectors/" )"real" reals nil )"real" reals nil )"posreal" sq "reals/" )"posreal" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" ))nil 3525082075"" (skeep)"" (expand "horizontal_criterion_ext?" )"" (lemma "horizontal_criterion_scal" )"" (inst?)"1" (assert )"1" (ground)"1" (lemma "horizontal_criterion_sum_closed" )"1" (inst - "eps" "sp" "(1/2)*v" "nv - (1 / 2) * v" )"1" (assert )"1" case "(1 / 2) * v + (nv - (1 / 2) * v) = nv" )"1" (split -2)"1" (replace -2)"1" (lemma "horizontal_criterion_scal" )"1" (inst - "eps" "sp" "nv" "c-1" )"1" assert )"1" "horizontal_criterion_sum_closed" )"1" "eps" "sp" "(c-1)*nv" "nv - (1/2)*v" )"1" assert )"1" "1" "horizontal_criterion?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "horizontal_criterion_scal" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1)"2" (decompose-equality)"1" (grind) nil nil ) ("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "horizontal_criterion_sum_closed" )"2" (inst - "eps" "sp" "(c-1)*nv" "nv - (1/2)*v" )"2" (assert )"2" (split -)"1" (hide-all-but (-1 1))"1" (grind :exclude "horizontal_criterion?" )nil nil ))nil )"2" (lemma "horizontal_criterion_scal" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "horizontal_criterion_sum_closed" )"3" (inst - "eps" "sp" "(1/2)*v" "nv - (1 / 2) * v" )"3" (assert )"3" (split -)"1" (hide-all-but (-1 2))"1" case "(1 / 2) * v + (nv - (1 / 2) * v) = nv" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (decompose-equality)"1" (grind) nil nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "horizontal_criterion_scal" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"bool" nil )"(total_order?[real])" nil )"real" horizontal_criterion_line nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"Sign" sign "reals/" )"posrat" nil )"Vector" vectors_2D "vectors/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" sq "reals/" )"real" reals nil )"real" reals nil )nil nil )nil horizontal_criterianil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" horizontal_criterion_line nil ))nil 3525087134"" case "FORALL (eps: Sign, sp: Sp_vect2[D], v, nv1, nv2: Vect2): AND AND t <= 1 IMPLIES") "1" (skeep)"1" (skeep)"1" (expand "horizontal_criterion_ext?" )"1" (assert )"1" (split +)"1" (flatten)"1" (assert )"1" "eps" "sp" "v" "nv1 - (1 / 2) * v" "nv2 - (1 / 2) * v" )"1" (assert )"1" (inst - "t" )"1" case "(1 - t) * (nv1 - (1 / 2) * v) + ") "1" (assert ) nil nil )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (split +)"1" (flatten)"1" (replace -1)"1" (inst - "eps" "sp" "v" "nv1" "nv2" )"1" (assert )"1" (inst - "t" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (flatten)"2" (assert )"2" (flatten)"2" (split +)"1" "eps" "sp" "v" "nv1" "nv2" )"1" assert )"1" "t" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "eps" "sp" "v" "nv1 - (1 / 2) * v" "nv2 - (1 / 2) * v" )"2" assert )"2" "t" )"2" case "(1 - t) * (nv1 - (1 / 2) * v) + ") "1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (skeep)"2" (rewrite "horizontal_criterion_rewrite" )"2" (rewrite "horizontal_criterion_rewrite" )"2" (rewrite "horizontal_criterion_rewrite" )"2" (flatten)"2" (mult-by -1 "(1-t)" )"2" (mult-by -2 "(1-t)" )"2" (mult-by -3 "t" )"2" (mult-by -4 "t" )"2" (split +)"1" (hide (-1 -3))"1" "tangent_line" )nil nil ))nil )"2" (hide (-2 -4))"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" vectors_2D "vectors/" )"(total_order?[real])" nil )"real" horizontal_criterion_line nil )"Nz_vect2" tangent_line nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" det_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_propsnil )nil nil )"bool" nil )"posreal" sq "reals/" )"real" reals nil )"real" reals nil )"Vector" vectors_2D "vectors/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posrat" nil )"Sign" sign "reals/" )"(total_order?[real])" nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D_def "vectors/" )"bool" reals nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"nonneg_real" sq "reals/" )"bool" reals nil )nil real_types nil )"posreal" horizontal_criterion_line nil )nil horizontal nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" horizontal_criteria nil )"bool" reals nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3525087186"" (subtype-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D "vectors/" )nil real_types nil )nil vectors_2D_def "vectors/" )nil horizontal nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" horizontal_criteria nil )"real" det_2D "vectors/" )"bool" horizontal_criteria nil )"boolean" notequal nil )"posreal" nil )"real" reals nil )"real" reals nil )"nnreal" nil )"posreal" sq "reals/" ))nil ))nil 3525081721"" case "FORALL (eps: Sign, sp: Sp_vect2[D], v, sp1, sp2: Vect2): AND AND t <= 1 IMPLIESNOT sqv((1-t)*sp1 + t * sp2) < sq(D))") "1" (skeep)"1" (inst - "eps" "sp" "v" "sp1" "sp2" )"1" (assert )"1" (skeep)"1" (inst - "((t - t1) / (t2 - t1))" )"1" (split -)"1" (name "tz" "(t-t1)/(t2-t1)" )"1" (replace -1)"1" (hide-all-but (-7 1))"1" (grind :exclude ("sqv" "sq" )) nil nil ))nil ))nil ))nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil )"3" (cross-mult 1) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "horizontal_criterion_ext_seg_convex" )"2" (skeep)"2" (inst - "eps" "sp" "v" "sp1-sp" "sp2-sp" )"2" (assert )"2" (skeep)"2" (inst - "t" )"2" (assert )"2" "horizontal_criterion_ext_independence" )"2" "eps" "(1 - t) * (sp1 - sp) + t * (sp2 - sp)" "sp" "v" )"2" (assert )"2" (hide-all-but (-6 1))"2" (expand "horizontal_conflict?" )"2" "1" )"2" "sqv" "sq" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )"bool" horizontal nil )nil nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"posreal" sq "reals/" )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D_def "vectors/" )"bool" reals nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"nonneg_real" sq "reals/" )"bool" reals nil )nil real_types nil )"posreal" horizontal_criterion_line nil )nil horizontal nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" nil )"Vector" vectors_2D "vectors/" )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3525084493"" (subtype-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )"boolean" notequal nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" horizontal_criteria nil )"real" det_2D "vectors/" )"bool" horizontal_criteria nil )"real" reals nil )"posreal" nil )"real" reals nil )"real" reals nil )"nnreal" nil )"posreal" sq "reals/" ))nil ))nil 3525084493"" (subtype-tcc) nil nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"posreal" horizontal_criterion_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" horizontal_criteria nil )"real" det_2D "vectors/" )"bool" horizontal_criteria nil )"boolean" notequal nil )"real" reals nil )"real" reals nil )"real" reals nil )"posreal" nil )"nnreal" nil )"posreal" sq "reals/" ))nil ))nil 3525084495"" case "FORALL (ssp:Sp_vect2,vv,nvv:Vect2,eps:Sign): horizontal_criterion_ext?(ssp,vv,eps)(nvv) IMPLIES horizontal_criterion_ext?(-ssp,-vv,eps)(-nvv)" )"1" (label "lem1" -1)"1" (hide "lem1" )"1" case "FORALL (eps: Sign, nso1, nso2, nsi1, nsi2: Vect2, AND AND horizontal_criterion_ext?(sp, v, eps)(nso2 - sp)AND horizontal_criterion_ext?(-sp, -v, eps)(nsi1 +sp)AND horizontal_criterion_ext?(-sp, -v, eps)(nsi2 +sp)LET time01 = (t - t1) / (t2 - t1),AND t <= t2 IMPLIES") "1" (skeep)"1" "eps" "nso1-si" "nso2-si" "nsi1-so" "nsi2-so" "t1" "t2" "so-si" "vo-vi" )"1" (assert )"1" (split -)"1" (skeep)"1" (inst - "t" )"1" (assert )"1" (name "nt" "(t-t1)/(t2-t1)" )"1" (replace -1)"1" (hide -1)"1" "vvr" "nso1 + nt * (nso2 - nso1) - (nsi1 + nt * (nsi2 - nsi1))" )"1" replace -1)"1" case "NOT (nso1 - si + nt * (nso2 - si - (nso1 - si)) ") "1" "1" expand "vvr" )"1" (grind) nil nil ))nil ))nil )"2" replace -1)"2" "2" "horizontal_criterion_ext_independence" )"2" "2" assert )"2" expand "horizontal_conflict?" )"2" "1" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "sqv" "sq" "horizontal_criterion_ext?" ))nil nil ))nil )"3" (hide 2)"3" "sqv" "sq" "horizontal_criterion_ext?" ))nil nil ))nil )"4" (hide 2)"4" "sqv" "sq" "horizontal_criterion_ext?" ))nil nil ))nil )"5" (hide 2)"5" "sqv" "sq" "horizontal_criterion_ext?" ))nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "horizontal_criterion_ext_seg_convex" )"2" (skeep)"2" (skeep)"2" "eps" "sp" "v" "nso1-nsi1 - 2*sp" "nso2-nsi2-2*sp" )"2" (assert )"2" (split -)"1" (flatten)"1" (assert )"1" (inst - "(t-t1)/(t2-t1)" )"1" "1" "nt" "(t-t1)/(t2-t1)" )"1" replace -1)"1" "1" "1" "horizontal_criterion_ext?" )nil nil ))nil ))nil ))nil ))nil )"2" (cross-mult 1) nil nil )"3" (cross-mult 1) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "horizontal_criterion_ext_sum_closed" )"2" "eps" "nso1-sp" "-(nsi1+sp)" "sp" "v" )"2" assert )"2" "1" "1" "horizontal_criterion_ext?" )nil nil ))nil )"2" "lem1" )"2" "-sp" "-v" "nsi1+sp" "eps" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" "horizontal_criterion_ext_sum_closed" )"3" "eps" "nso2-sp" "-(nsi2+sp)" "sp" "v" )"3" assert )"3" "1" "1" "horizontal_criterion_ext?" )nil nil ))nil )"2" "lem1" )"2" "-sp" "-v" "nsi2+sp" "eps" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skeep) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "horizontal_criterion_ext?" )"2" (rewrite "horizontal_criterion_symmetric" :dir rl)"2" (rewrite "horizontal_criterion_symmetric" :dir rl)"2" (rewrite "horizontal_criterion_symmetric" :dir rl)"2" rewrite "horizontal_criterion_symmetric" :dir rl)"2" (case "-nvv-(1/2)*-vv = -(nvv-(1/2)*vv)" )"1" (replace -1)"1" (hide -1)"1" rewrite "horizontal_criterion_symmetric" nil nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posrat" nil )"Sign" sign "reals/" )nil nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"Vector" vectors_2D "vectors/" )"bool" reals nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )nil nil )"posreal" nil )"real" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"bool" horizontal nil )"real" reals nil )"real" reals nil )"Vector" horizontal_criterion_line nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" sq "reals/" )nil nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil nil )nil real_props nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"Sp_vect2[D]" nil )nil reals nil )nil vectors_2D_def "vectors/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil booleans nil )"bool" reals nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"nonneg_real" sq "reals/" )"bool" reals nil )nil real_types nil )"posreal" horizontal_criterion_line nil )nil horizontal nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"[bool, bool -> bool]" booleans nil )"bool" nil )"Vector" vectors_2D "vectors/" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.196 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
