Quelle cd3d_inf.prf
Sprache: Lisp
(cd3d_infnil 3483961475"" (skeep)"" (lemma "posreal_times_posreal_is_posreal" )"" (inst - "D" "abs(v`z)" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil real_types nil )nil sign "reals/" )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"Vect3" cd3d_inf nil )nil vectors_3D_def "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" cd3d_inf 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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"nzreal" real_typesnil ))nil ))nil 3483961475"" (subtype-tcc) nil nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"real" reals nil )"nzreal" real_typesnil )"real" reals nil ))nil ))nil 3563274460"" (subtype-tcc) nil nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"real" reals nil )"nzreal" real_typesnil )"real" reals nil ))nil ))nil 3483961513"" (skeep)"" (split)"1" (flatten)"1" (expand "conflict?" )"1" (skosimp*)"1" (lemma "vertical_los_inside_Theta" )"1" (inst - "abs(v`z)" "sign(v`z)*s`z" "nnt!1" )"1" (flatten)"1" (hide -1)"1" (split -1)"1" (flatten)"1" (expand "Theta_H" )"1" (case "sign(abs(v`z)) = 1" )"1" (replace -1)"1" "1" assert )"1" "1" "1" expand "conflict_2D?" )"1" "nnt!1*abs(v`z)" )"1" rewrite "vect2_scal" )"1" case "abs(v`z) * vect2(s) + nnt!1 * abs(v`z) * vect2(v) = abs(v`z)*(vect2(s)+nnt!1*vect2(v))" )"1" replace -1)"1" "1" rewrite "sqv_scal" )"1" rewrite "sq_times" )"1" "sq(v`z)" )"1" "sq_eq_0" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" expand "max" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "sign" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "conflict_2D_on_open_interval[D *abs( v`z), max (-H - sign(v`z) * s`z, 0),") "1" (inst?)"1" (assert )"1" (replace -2)"1" (assert )"1" (skosimp*)"1" (name "t!2" "topen!1/abs(v`z)" )"1" case "max(Theta_H[H](sign(v`z)*s`z,abs(v`z),-1),0)< t!2 AND t!2 < Theta_H[H](sign(v`z)*s`z,abs(v`z),1)" )"1" (flatten)"1" (expand "conflict?" )"1" (inst + "t!2" )"1" "1" "vertical_los_inside_Theta" )"1" "abs(v`z)" "sign(v`z)*s`z" "t!2" )"1" "1" "1" "1" "1" (grind) nil nil ))nil )"2" "2" "Theta_H" )nil nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "vect2_scal" )"2" case "abs(v`z) * vect2(s) + topen!1 * vect2(v) = abs(v`z)*(vect2(s) + t!2*vect2(v))" )"1" replace -1)"1" rewrite "sqv_scal" )"1" rewrite "sq_times" )"1" "sq(v`z)" )nil nil ))nil ))nil ))nil )"2" replace -3 :dir rl)"2" "2" "abs" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Theta_H" )nil nil ))nil ))nil ))nil ))nil )"2" (replace -1 1 :dir rl)"2" (hide-all-but (-2 -3 -6 1))"2" (split)"1" "1" "nneg_mult_max" )"1" "abs(v`z)" "Theta_H[H](sign(v`z) * s`z, abs(v`z), -1)" "0" )"1" replace -1)"1" expand "Theta_H" )"1" case "v`z>0" )"1" expand "abs" )"1" expand "sign" )"1" (assert ) nil nil ))nil ))nil )"2" case "v`z < 0" )"1" expand "abs" )"1" expand "sign" )"1" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Theta_H" )"2" case "v`z>0" )"1" expand "abs" )"1" expand "sign" )"1" (assert ) nil nil ))nil ))nil )"2" case "v`z < 0" )"1" expand "abs" )"1" expand "sign" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-2 1)) (("2" (assert ) nil nil )) nil )"3" (lemma "posreal_times_posreal_is_posreal" )"3" (inst - "D" "abs(v`z)" )"1" (assert ) nil nil )"2" (lemma "abs_eq_0" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"4" (lemma "posreal_times_posreal_is_posreal" )"4" (inst - "D" "abs(v`z)" ) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" space_3D nil )"posreal" cd3d_inf 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 vertical nil )nil abs_lems "reals/" )"nzreal" nil )"real" vertical nil )"real" reals nil )"(total_order?[real])" nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(strict_total_order?[real])" real_props nil )"posreal" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"bool" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"Vect3" cd3d_inf nil )"nnreal" cd3d_inf nil )nil Lookahead nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"posreal" cd3d_inf nil )nil sq "reals/" )nil sq "reals/" )nil reals nil )nil extra_real_props nil )nil extra_real_props nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_props nil )nil sq "reals/" )nil vectors_2D "vectors/" )"real" reals nil )nil vect_3D_2D "vectors/" )"bool" cd2d nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_props nil )nil real_types nil )"Sign" sign "reals/" )nil sign "reals/" )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"Vect3" cd3d_inf nil )nil vectors_3D_def "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"nnreal" nil )"(total_order?[real])" nil )nil omega_2D nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil min_max "reals/" )nil real_props nil )"real" cd3d_inf nil )"bool" reals nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil sign "reals/" )nil abs_lems "reals/" )nil real_types nil )"real" reals nil )"nzreal" real_typesnil ))nil ))nil 3483962172"" (skeep)"" (split)"1" (flatten)"1" (expand "conflict?" )"1" (skosimp*)"1" (inst + "nnt!1" )"1" (assert )"1" (expand "abs" )"1" (lift-if) (("1" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "conflict?" )"2" (skosimp*)"2" (inst + "nnt!1" )"2" (assert )"2" (expand "abs" )"2" (lift-if) (("2" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"real" reals nil )"bool" space_3D nil )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 )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil vect_3D_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" ))nil )nil 3483962156 ("" (postpone) nil nil ) nil nil 3483962247"" (skeep)"" (split)"1" (flatten)"1" (expand "conflict?" )"1" (skosimp*)"1" case "exists (epH:posreal): FORALL (th: real): abs(th-nnt!1))"1" (skeep -1)"1" case "exists (epD:posreal): FORALL (td: real): abs(td-nnt!1))"1" (skeep -1)"1" (name "newt" "min(epD/2,epH/2)" )"1" (case "newt > 0" )"1" (case "nnt!1 = 0" )"1" (replace -1)"1" (hide -1)"1" "newt" )"1" assert )"1" "newt" )"1" "newt" )"1" case "abs(newt))"1" "1" (assert ) nil nil ))nil )"2" "2" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (inst + "nnt!1" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (case "vect2(v) = zero" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (hide -1)"2" (hide -1)"2" (hide 3)"2" (lemma "sqv_cont" )"2" (expand "continuous_vr?" )"2" "vect2(s) + nnt!1 * vect2(v)" )"2" expand "continuous_vr?" )"2" "sq(D) - sqv(vect2(s)+nnt!1*vect2(v))" )"1" "1" "delta!1/norm(vect2(v))" )"1" "1" "vect2(s) + td!1*vect2(v)" )"1" "1" "const1" "sqv(vect2(s) + td!1*vect2(v))" )"1" replace -1)"1" "const2" "sqv(vect2(s) + nnt!1*vect2(v))" )"1" replace -1)"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vect2(s) + td!1 * vect2(v) - (vect2(s) + nnt!1 * vect2(v)) = (td!1-nnt!1)*vect2(v)" )"1" replace -1)"1" rewrite "norm_scal" )"1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "posreal_div_posreal_is_posreal" )"2" "delta!1" "norm(vect2(v))" )"1" (assert ) nil nil )"2" "vectors_2D.norm_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "vectors_2D.norm_eq_0" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "v`z = 0" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (inst + "(H-abs(s`z+nnt!1*v`z))/abs(v`z)" )"1" (skosimp*)"1" (cross-mult -1)"1" (hide-all-but (-1 -2 2))"1" (rewrite "abs_mult" :dir rl)"1" "+" "abs(s`z+nnt!1*v`z)" -1)"1" (assert )"1" "triangle" )"1" "v`z * th!1 - v`z * nnt!1" "s`z + nnt!1 * v`z" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (split 1)"1" (cross-mult 1) (("1" (assert ) nil nil )) nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil )"3" (expand "abs" 1)"3" (lift-if) (("3" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp*)"2" (expand "conflict?" )"2" (inst + "topen!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" space_3D nil )"posreal" cd3d_inf nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[bool, bool -> bool]" booleans 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 )"real" reals nil )"posreal" cd3d_inf nil )"nonneg_real" sq "reals/" )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"posreal" nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"{y: posreal | y >= x}" nil )"bool" cont_vect2_real "vect_analysis/" )"bool" cont_vect2_real "vect_analysis/" )nil real_types nil )nil vectors_2D "vectors/" )"odd_int" integers nil )"posreal" nil )nil real_props nil )"nnreal" nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"posreal" cd3d_inf nil )"nnreal" vectors_2D "vectors/" )"nzreal" nil )"Vect3" cd3d_inf nil )"nnreal" cd3d_inf nil )"Vect3" cd3d_inf nil )nil vect_cont_2D "vect_analysis/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" reals nil )nil real_props nil )nil real_props nil )"real" reals nil )"(total_order?[real])" nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"nnreal" nil )nil extra_real_props nil )nil real_props nil )nil abs_lems "reals/" )"real" reals nil )"real" reals nil ))nil ))nil 3483961475"" (skeep)"" (typepred "nzv" )"" (hide -3)"" (expand "zero" )"" (grind) (("" (decompose-equality) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"boolean" notequal nil )nil vectors_3D "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" ))nil ))nil 3483961475"" (skeep)"" (lemma "Delta_gt_0_nzv" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )"posreal" cd3d_inf 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 horizontal nil )"(total_order?[real])" nil )"odd_int" integers nil )"(total_order?[real])" nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(strict_total_order?[real])" real_props nil )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )"boolean" notequal nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" ))nil ))nil 3563274460 ("" (subtype-tcc) nil nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"boolean" notequal nil )nil vectors_3D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posreal" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"posreal" cd3d_inf 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 )"real" vertical nil )"real" reals nil )"nzreal" nil )"real" reals nil )"real" reals nil ))nil ))nil 3563274460"" (skeep)"" (assert )"" (flatten)"" (assert )"" (replace -2)"" (expand "Delta" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"posreal" sq "reals/" )"real" horizontal nil )"real" reals nil )"nnreal" nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )nil vectors_2D "vectors/" ))nil ))nil 3563274460 ("" (subtype-tcc) nil nil )nil vectors_3D_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 )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"nonneg_real" sq "reals/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"real" det_2D "vectors/" )"real" horizontal nil )"real" quadratic_2b "reals/" )"real" quadratic_2b "reals/" )"real" horizontal nil )"boolean" notequal nil )"posreal" cd3d_inf 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 )"real" vertical nil )"real" reals nil )"real" reals nil )"real" reals nil )"posreal" nil )"odd_int" integers nil )"real" reals nil )"nnreal" nil )"nzreal" nil ))nil ))nil 3563274460 ("" (subtype-tcc) nil nil )nil vectors_3D_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 )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"nonneg_real" sq "reals/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"real" det_2D "vectors/" )"real" horizontal nil )"real" quadratic_2b "reals/" )"real" quadratic_2b "reals/" )"real" horizontal nil )"boolean" notequal nil )"posreal" cd3d_inf 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 )"real" vertical nil )"real" reals nil )"real" reals nil )"real" reals nil )"posreal" nil )"odd_int" integers nil )"real" reals nil )"nnreal" nil )"nzreal" nil ))nil ))nil 3483963292"" (skeep)"" (skoletin 1)"" (flatten)"" (expand "detection_inf" )"" (lift-if)"" (split -)"1" (flatten)"1" (assert )"1" (replace -1)"1" (assert )"1" (lemma "vertical_los_inside_Theta" )"1" (inst?)"1" (assert )"1" (grind :exclude "Theta_H" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (split -1)"1" (flatten)"1" (assert )"1" (split -2)"1" (flatten)"1" (assert )"1" "1" "1" (assert ) nil nil ))nil )"2" "2" "vertical_los_inside_Theta" )"2" "2" assert )"2" "horizontal_los_inside_Theta" )"2" "2" assert )"2" "sqv" "vect2" "Theta_D" "Theta_H" "Delta" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (split -2)"1" "1" assert )"1" "1" "1" (assert ) nil nil ))nil )"2" "2" "horizontal_los_inside_Theta" )"2" "2" assert )"2" "sqv" "vect2" "Theta_D" "Theta_H" "Delta" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil reals nil )nil vectors_3D_def "vectors/" )nil vectors_3D "vectors/" )"boolean" notequal nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"[nnreal, nnreal]" cd3d_inf nil )"posreal" cd3d_inf nil )"nonneg_real" sq "reals/" )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"posreal" cd3d_inf nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"odd_int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" vectors_2D "vectors/" )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil vertical nil )nil horizontal nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" reals nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"real" reals nil )"real" reals nil ))nil ))nil 3483963425"" (skeep)"" (skoletin 1)"" (flatten)"" (expand "detection_inf" )"" (lift-if)"" (split -)"1" (flatten)"1" (assert )"1" (lemma "vertical_los_inside_Theta" )"1" (inst? -1)"1" (assert )"1" "sqv" "vect2" "Theta_D" "Theta_H" "Delta" ))nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (split -)"1" (flatten)"1" (split -)"1" (flatten)"1" (assert )"1" (split -)"1" "1" (assert ) nil nil ))nil )"2" "2" assert )"2" "vertical_los_inside_Theta" )"2" "2" assert )"2" "horizontal_los_inside_Theta" )"2" "2" assert )"2" "sqv" "vect2" "Theta_D" "Theta_H" "Delta" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))quality 100%
¤ Dauer der Verarbeitung: 0.32 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
