Impressum vertical_los_criterion.prf
Interaktion und
(vertical_los_criterionnil 3519732687"" (skeep)"" (lemma "vertical_los_inside_Theta" )"" (inst - "eps*MinRelVertSpeed" "sz" "0" )"" (assert ) nil nil )) nil ))nil ))nil )"posreal" vertical_los_criterion 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 )"real" reals nil )"odd_int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" 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 )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )"nzreal" nil ))nil ))nil 3519732687"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers 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 )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/" )"(total_order?[real])" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"boolean" notequal nil ))nil ))nil 3519732687"" (skeep)"" (lemma "vertical_los_inside_Theta" )"" (inst-cp - "eps*MinRelVertSpeed" "sz" "0" )"" (inst - "vz" "sz" "0" )"" (assert )"" (flatten)"" (expand "min" )"" (lift-if) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" vertical_los_criterion 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 )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" 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 )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )"nzreal" nil ))nil ))nil 3531579993"" (skeep)"" (expand "time_vertical_exit_by" )"" (case "-eps*MinRelVertSpeed = -(eps*MinRelVertSpeed)" )"1" (replace -1)"1" (rewrite "Theta_H_symm" )"1" (rewrite "Theta_H_symm" )"1" (hide -1)"1" (lift-if)"1" (lift-if)"1" (lift-if) (("1" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"Sign" sign "reals/" )"{x: real | MinRelVertSpeed > 0 AND abs(sz) < H IMPLIES x > 0}" nil )"(total_order?[real])" nil )"real" reals nil )nil vertical nil )nil reals nil )"posreal" vertical_los_criterion nil )"nzreal" nil )"nzreal" real_typesnil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )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 )nil sign "reals/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" reals nil ))nil 3531562642 ("" (subtype-tcc) nil nil )nil nil ))nil 3531562642 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals 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/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3531562675"" (skeep)"" (expand "min_rel_vert_speed" )"" (lift-if)"" (lift-if)"" (lift-if)"" (assert )"" (ground) (("" (rewrite "abs_neg" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"Sign" sign "reals/" )"{x: nnreal | abs(sz) < H IMPLIES x > 0}" vertical_los_criterionnil )"real" reals nil )"(total_order?[real])" nil )nil abs_lems "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(total_order?[real])" nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )"real" reals nil ))nil 3562942251"" (skeep) (("" (replace -4) (("" (assert ) nil nil )) nil )) nil )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3562942251"" (skeep) (("" (replace -4) (("" (assert ) nil nil )) nil )) nil )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3562941990"" (skeep)"" (lemma "sq_gt" )"" (inst?)"" (assert )"" (hide 2)"" (rewrite "sq_norm" )"" (rewrite "sq_norm" )"" (assert )"" (case "eps*v`z > 0" )"1" (expand "vs_bound_crit?" )"1" (assert )"1" (flatten)"1" case "eps * horizontal_tca(vect2(s), vect2(nv)) * nv`z >= ") "1" (grind :exclude "horizontal_tca" ) nil nil )"2" (hide 3)"2" case "NOT sqv(horizontal_tca(s,nv)*vect2(nv)) >= sqv(horizontal_tca(s,v)*vect2(v))" )"1" rewrite "vect2_add" )"1" rewrite "vect2_add" )"1" rewrite "vect2_scal" )"1" rewrite "vect2_scal" )"1" rewrite "horizontal_sq_dtca_eq" "1" rewrite "horizontal_sq_dtca_eq" "1" expand "horizontal_sq_dtca" )"1" rewrite "sqv_scal" )"1" rewrite "sqv_scal" )"1" assert )"1" assert )"1" expand "horizontal_tca" "1" rewrite "sq_div" )"1" rewrite "sq_div" )"1" case "FORALL (ap1:posreal,b:real): b/sq(ap1) * ap1 = b/ap1" )"1" rewrite "1" rewrite "1" "orthogonal_basis" )"1" "nv" "perpR(nv)" "s" )"1" assert )"1" case "vect2(nv) /= zero AND AND ") "1" "1" assert )"1" "v" "perpR(v)" "s" )"1" case "vect2(v) /= zero AND AND orthogonal?(vect2(v), perpR(vect2(v)))") "1" "1" assert )"1" "orthogonal_basis_sqv" )"1" "v" "perpR(v)" "s" )"1" "1" assert )"1" "orthogonal_basis_sqv" )"1" "nv" "perpR(nv)" "s" )"1" "1" assert )"1" rewrite "sqv_perpR" )"1" rewrite "sqv_perpR" )"1" assert )"1" rewrite "det_perpR" "1" rewrite "det_perpR" "1" assert )"1" rewrite "sq_neg" )"1" rewrite "sq_neg" )"1" assert )"1" rewrite "sq_div" )"1" rewrite "sq_div" )"1" rewrite "sq_div" )"1" rewrite "sq_div" )"1" assert )"1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" assert )nil nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" replace "1" assert )nil nil ))nil ))nil )"2" "2" "perpR_perpR" )"2" "2" replace "2" assert )"2" case "--vect2(v) = zero" )"1" assert )"1" replace "1" assert )nil nil ))nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" replace "1" assert )nil nil ))nil ))nil )"2" "2" "perpR_perpR" )"2" "nv" )"2" replace "2" assert )"2" case "--vect2(nv) = zero" )"1" assert )"1" replace "1" assert )nil nil ))nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sqv_scal" )"2" rewrite "sqv_scal" )"2" expand "horizontal_tca" -1)"2" rewrite "sq_div" )"1" rewrite "sq_div" )"1" case "FORALL (ap1:posreal,b:real): b/sq(ap1) * ap1 = b/ap1" )"1" rewrite -1)"1" rewrite -1)"1" "1" "1" case "%1" )"1" assert )"1" "1" case "%1" )"1" assert )"1" case "NOT nv`z * horizontal_tca(vect2(s), vect2(nv)) * eps < ") "1" assert )nil nil )"2" expand "horizontal_tca" "2" "2" "2" case "(sq(-(vect2(s) * vect2(v))) * sqv(vect2(nv))) > 0" )"1" case "nv`z * sqv(vect2(v)) * -(vect2(s) * vect2(nv)) * eps > 0" )"1" "1" "K1" "sqv(vect2(v))*(-(vect2(s)*vect2(nv)))*(-vect2(s)*vect2(v))*sqv(vect2(nv))" )"1" case "K1 > 0" )"1" "K1" )"1" "1" nil nil ))nil ))nil )"2" "2" "2" expand "K1" )"2" rewrite "posreal_times_posreal_is_posreal" )"2" "2" case "%1" )"1" assert )nil nil )"2" "2" rewrite "posreal_times_posreal_is_posreal" )"1" "1" nil nil ))nil )"2" "2" rewrite "posreal_times_posreal_is_posreal" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "posreal_times_posreal_is_posreal" )"2" "eps*nv`z" "sqv(vect2(v)) * -(vect2(s) * vect2(nv))" )"1" assert )nil nil )"2" case "%1" )"1" assert )nil nil )"2" "2" rewrite "posreal_times_posreal_is_posreal" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "posreal_times_posreal_is_posreal" )"2" "sq_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace -1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace -1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace -1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace -1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "v`z = 0" )"1" (expand "vs_bound_crit?" )"1" (replace -1)"1" (assert )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" rewrite "vz_scal" )"1" replace -1)"1" assert )"1" "horizontal_tca(vect2(s), vect2(nv))" )"1" (assert ) nil nil )"2" "2" expand "horizontal_tca" "2" "2" "2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "NOT eps*v`z < 0" )"1" (typepred "eps" )"1" (ground) nil nil )) nil )"2" (expand "vs_bound_crit?" )"2" (assert )"2" rewrite "vz_distr_add" )"2" rewrite "vz_distr_add" )"2" rewrite "vz_scal" )"2" rewrite "vz_scal" )"2" assert )"2" "horizontal_tca(vect2(s), vect2(v))" )"1" "horizontal_tca(vect2(s), vect2(nv))" )"1" (assert ) nil nil )"2" "2" "2" "2" expand "horizontal_tca" "2" "2" "2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "%1" )"1" (assert ) nil nil )"2" "2" "2" "2" expand "horizontal_tca" "2" "2" "2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sq "reals/" )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )"odd_int" integers nil )nil real_props nil )nil extra_real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"bool" vertical_los_criterion nil )"Vect3" vertical_los_criterion nil )nil extra_real_props nil )nil reals nil )nil real_props nil )"bool" reals nil )nil real_props nil )nil real_props nil )nil real_props nil )"Vect3" vertical_los_criterion nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil extra_real_props nil )"real" vertical_los_criterion nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_propsnil )nil real_types nil )nil sq "reals/" )nil extra_real_props nil )nil vect_3D_2D "vectors/" )nil vect_3D_2D "vectors/" )nil definitions nil )"real" definitions nil )nil sq "reals/" )"real" reals nil )"posreal" sq "reals/" )nil real_types nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )"Vect2" perpendicular_2D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" vectors_2D "vectors/" )"nnreal" nil )nil det_2D "vectors/" )nil vectors_2D "vectors/" )"real" det_2D "vectors/" )nil sq "reals/" )nil perpendicular_2D "vectors/" )nil basis_2D "vectors/" )"rat" rationals nil )nil perpendicular_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil perpendicular_2D "vectors/" )nil vectors_2D "vectors/" )nil sq "reals/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil basis_2D "vectors/" )"Vect3" vertical_los_criterion nil )"posreal" nil )"real" reals nil )"nnreal" nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"nnreal" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"real" 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 )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"real" definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )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 3527436562"" (skeep)"" (expand "vs_bound_crit_vect?" )"" (split +)"1" (flatten)"1" (assert )"1" (split -)"1" (flatten)"1" (assert )"1" case "NOT (eps * (nvo - nvi)`z >= eps * (vo - vi)`z)" )"1" (hide 2)"1" (hide (-3 -6)) (("1" (grind) nil )))))"2" (name "vv" "vo-vi" )"2" (replace -1)"2" (case "vi-vo = -vv" )"1" (replace -1)"1" (name "v1" "nvo-vi" )"1" replace -1)"1" "v2" "nvi-vo" )"1" replace -1)"1" case "NOT nvo-nvi = v1-v2-vv" )"1" "1" expand "v1" )"1" expand "v2" )"1" expand "vv" )"1" nil )))))))))"2" replace -1)"2" "2" rewrite "vz_neg" )"2" assert )"2" case "vv`z * (vect2(- vv) * vect2(vv)) * -eps + ") "1" (grind) nil )"2" "2" case "vect2(-vv)*vect2(vv) = -sqv(vect2(vv))" )"1" replace -1)"1" "sqv(vect2(vv))" )"1" "1" nil )))))))"2" "2" nil )))))))))))))))))))))))))))))"2" (hide-all-but 1)"2" (expand "vv" )"2" (grind) nil )))))))))))))))))"2" (flatten)"2" (assert )"2" (hide-all-but (-2 1))"2" (grind) nil )))))))))))))"2" (flatten)"2" (assert )"2" (split -)"1" (flatten)"1" (hide-all-but (-1 1)) (("1" (grind) nil )))))"2" (flatten) (("2" (grind) nil ))))))))))))))nil )"Sign" sign "reals/" )"Vector" vectors_3D "vectors/" )"Vector" vertical_los_criterion nil )"Vector" vertical_los_criterion nil )"Vector" vertical_los_criterion nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"odd_int" integers nil )"bool" vertical_los_criterion nil )"real" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields 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 )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D_def "vectors/" ))nil ))nil 3527436806"" (skeep)"" (expand "vs_bound_crit?" ) (("" (ground) nil nil )) nil )) nil )"real" reals nil )"bool" vertical_los_criterion nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3527436584"" (skeep)"" (expand "vs_bound_crit_vect?" ) (("" (ground) nil )))) nil )"Sign" sign "reals/" )) nil ))nil 3527436825"" (skeep)"" (expand "vertical_los_criterion?" )"" (flatten)"" (assert )"" (split +)"1" (lemma "vs_bound_crit_coord" )"1" (inst - "eps" "nvi" "nvo" "zero" "s" "vi" "vo" )"1" (assert ) nil nil )) nil ))nil )"2" (case "vi-vo = -(vo-vi)" )"1" (replace -1)"1" (hide -1)"1" (rewrite "vz_neg" )"1" (rewrite "vz_neg" )"1" (rewrite "min_rel_vert_speed_symm" )"1" (expand "min_rel_vert_speed" )"1" (lift-if)"1" (split +)"1" "1" assert )"1" "1" (grind) nil nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "max" +)"2" "2" "2" "2" "1" "1" case "eps = sign((vo-vi)`z)" )"1" replace -1)"1" "1" nil nil ))nil ))nil )"2" "2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" case "eps = sign((vo-vi)`z)" )"1" replace -1)"1" "1" nil nil ))nil ))nil )"2" "2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" case "eps = sign((vo-vi)`z)" )"1" replace -1)"1" "1" nil nil ))nil ))nil )"2" "2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil )"4" "4" case "eps = sign((vo-vi)`z)" )"1" replace -1)"1" "1" nil nil ))nil ))nil )"2" "2" "eps" )"2" 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 )"Sign" sign "reals/" )"bool" vertical_los_criterionnil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"{x: nnreal | abs(sz) < H IMPLIES x > 0}" vertical_los_criterionnil )"{z: posreal | z >= x AND z >= y}" real_defs nil )"(total_order?[real])" nil )"real" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"Sign" sign "reals/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil vertical_los_criterion nil )"real" reals nil )nil vectors_3D "vectors/" )nil vertical_los_criterion nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )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 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 )nil 3527436607"" (skeep)"" (expand "vertical_los_criterion_vect?" )"" (flatten)"" (assert )"" (split +)"1" (lemma "vs_bound_crit_vect_coord" )"1" (inst - "eps" "nvi" "nvo" "zero" "s" "vi" "vo" )"1" (assert ) nil )))))"2" (lemma "time_vertical_exit_by_symm" )"2" (inst - "eps" "s`z" "tr" "vo`z-vi`z" )"2" (rewrite "vz_distr_sub" )"2" (rewrite "vz_distr_sub" )"2" (rewrite "vz_distr_sub" )"2" (rewrite "vz_distr_sub" )"2" (rewrite "vz_distr_sub" )"2" (lemma "time_vertical_exit_by_dist" )"2" (inst - "eps" "s`z" "tr" "vo`z-vi`z" )"2" assert )"2" assert )"2" rewrite "vz_neg" )"2" assert )nil ))))))))))))))))))))))))))))))))))nil )"Sign" sign "reals/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D_def "vectors/" )nil sign "reals/" ))nil ))nil 3519723086"" (skeep)"" (expand "vertical_sep_after" )"" (skeep)"" (case "vz >= 0" )"1" (case "sz + tr*vz >= 0" )"1" (hide -3)"1" (expand "abs" -)"1" (assert )"1" (mult-by -4 "vz" )"1" (expand "abs" +)"1" (lift-if) (("1" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (mult-by -1 "tr" ) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (case "sz + tr*vz <= -H" )"1" (mult-by -4 "-vz" ) (("1" (grind) nil nil )) nil )"2" (hide 3)"2" (mult-by 2 "tr" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vertical_los_criterion 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" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )nil extra_real_propsnil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"real" vertical_los_criterion nil )"(total_order?[real])" nil )"nzreal" real_typesnil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"posreal" vertical_los_criterion nil )"real" reals nil )"real" reals nil ))nil 3527436843"" (skeep)"" (expand "vertical_los_criterion?" )"" (flatten)"" (skoletin 1)"" (typepred "teb" )"" (assert )"" (lemma "vertical_sep_after_def" )"" (inst?)"" (assert )"" (hide 2)"" (case "eps*(s`z + teb*nv`z)>=H" )"1" (hide-all-but (-1 1))"1" (typepred "eps" )"1" (grind) nil nil )) nil ))nil )"2" (hide 2)"2" (expand "time_vertical_exit_by" )"2" (lift-if)"2" "1" expand "min_rel_vert_speed" )"1" "teb" )"1" assert )"1" case "s`z + teb*(eps*MinRelVertSpeed) = eps*H" )"1" assert )"1" "eps" )"1" (ground) nil nil ))nil ))nil )"2" replace -3 1)"2" expand "Theta_H" +)"2" "2" "eps" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min_rel_vert_speed" )"2" expand "min" -1)"2" "2" "1" "1" replace -2)"1" case "eps*(s`z+teb*v`z)>=H" )"1" "1" "teb" )"1" case "eps*nv`z>=eps*v`z" )"1" "teb" )"1" "1" nil nil ))nil ))nil )"2" "2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "teb" )"2" replace -2)"2" "Theta_H_on_H" )"2" "2" assert )"2" "2" "eps" )"2" "Theta_H" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Theta_H_on_H" )"2" "1" "eps*MinRelVertSpeed" "s`z" )"2" assert )"2" replace -2 :dir rl)"2" "eps" )"2" "1" replace -1)"1" assert )"1" expand "abs" "1" "1" assert )"1" "1" "nnreal_times_nnreal_is_nnreal" )"1" "1" "1" nil nil ))nil ))nil ))nil )"2" case "nv`z>=MinRelVertSpeed" )"1" "teb" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" assert )"2" assert )"2" case "-s`z+teb*MinRelVertSpeed = H" )"1" case "-nv`z>=MinRelVertSpeed" )"1" "teb" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" "nnreal_times_nnreal_is_nnreal" )"2" "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 ))nil )"bool" vertical_los_criterionnil )"[bool, bool -> bool]" booleans nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities 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 )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posreal" vertical_los_criterion nil )"{x: real | MinRelVertSpeed > 0 AND abs(sz) < H IMPLIES x > 0}" nil )nil vectors_3D_def "vectors/" )"bool" vertical_los_criterion nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posreal" nil )nil real_types nil )nil real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )"real" reals nil )nil reals nil )nil vertical nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{x: nnreal | abs(sz) < H IMPLIES x > 0}" vertical_los_criterionnil )"Sign" sign "reals/" )"real" vertical nil )"real" reals nil )"real" reals nil )nil extra_real_propsnil )"nzreal" nil )"(total_order?[real])" nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vertical_los_criterion nil )NOT const-decl "[bool -> bool]" booleans nil ))nil )nil 3527436633"" (skeep)"" (expand "vertical_los_criterion_vect?" )"" (flatten)"" (name "teb" "time_vertical_exit_by(s`z, v`z, eps, tr)" )"" (typepred "teb" )"" (assert )"" (case "teb <= tr" )"1" (replace -3)"1" (hide (-5 -3))"1" (expand "vertical_sep_after" )"1" (skeep)"1" (case "eps*(s`z + t*nv`z)>=H" )"1" (hide-all-but (-1 1))"1" (typepred "eps" )"1" (grind) nil )))))"2" (hide 2)"2" (case "eps*s`z < H" )"1" case "eps*nv`z >=0" )"1" "eps*nv`z" )"1" "eps*nv`z" )"1" (grind) nil )))))"2" "teb" )"2" (assert ) nil )))))"2" "2" "eps" )"2" (grind) nil )))))))))))))))))))"2" (hide-all-but 1)"2" (expand "teb" )"2" (grind :exclude "Theta_H" )nil ))))))))))))))))))nil )nil vectors_3D_def "vectors/" )nil sign "reals/" ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.82Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
