Quelle vertical_los_crit_CA.prf
Sprache: Lisp
(vertical_los_crit_CAnil 3519998803"" (inst + "LAMBDA (s,v:Vect3): IF s = zero THEN v ELSE s ENDIF" )"" (skeep)"" (grind)"1" (decompose-equality +) nil nil )"2" (decompose-equality +) nil nil )"3" (decompose-equality +) nil nil )"4" (decompose-equality +)"1" (decompose-equality 2) nil nil )"2" (decompose-equality 2) nil nil )"3" (decompose-equality 2) nil nil ))nil )"5" (decompose-equality 2) nil nil )"6" (decompose-equality 2) nil nil ))nil ))nil ))nil )"real" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"Vector" vectors_3D "vectors/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil vectors_3D_def "vectors/" )nil reals nil ))nil ))nil 3519751927"" (skeep)"" (typepred "dv" )"" (inst - "s" "v" )"" (assert )"" (replace -2)"" (flatten)"" (expand "dv_to_ec" )"" (lemma "break_vz_symm_comm" )"" (inst - "dv(s,v)" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vertical_los_crit_CAnil )"Vector" vectors_3D "vectors/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"Sign" sign "reals/" )nil vertical_los_crit_CA nil )"Sign" vertical_los_crit_CA nil ))nil 3519751654"" (grind :exclude "CA_cyl_conflict_ever?" ) nil nil )"real" reals nil )"Vector" vectors_3D "vectors/" )"nnreal" vectors_3D "vectors/" )"real" vectors_3D "vectors/" )"boolean" notequal nil )"real" reals nil )"nzreal" real_typesnil ))nil ))nil 3519978628"" (subtype-tcc) nil nil )"nonneg_int" nil )"even_int" integersnil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"boolean" notequal nil )"real" vectors_3D "vectors/" )"nnreal" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"bool" vertical_los_crit_CA nil )"real" reals nil )"real" reals nil )"nzreal" real_typesnil ))nil ))nil 3519978628"" (skeep) (("" (replace -3) (("" (assert ) nil nil )) nil )) nil )nil vect_3D_2D "vectors/" )nil vectors_3D "vectors/" ))nil ))nil 3519998803"" (skeep)"" (assert )"" (hide -2)"" (expand "CA_cyl_conflict_ever?" )"" (rewrite "cd3d_ever" :dir rl)"" (expand "conflict?" )"" (inst + "horizontal_tca(s,v)" )"1" (hide-all-but (-2 3))"1" (expand "zero" )"1" (grind :exclude "horizontal_tca" ) nil nil ))nil ))nil )"2" (expand "horizontal_tca" )"2" (cross-mult 1)"2" (ground)"2" (lemma "vectors_2D.sqv_eq_0" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3519998803"" (skeep)"" (assert )"" (expand "CA_cyl_conflict_ever?" )"" (lemma "cd3d_ever" )"" (inst?)"" (assert )"" (expand "conflict?" )"" (inst + "horizontal_tca(s,v)" )"1" (assert )"1" (replace -3)"1" (name "A" "vectors_3D.zero" )"1" (case "A`z = zero`z" )"1" (copy -2)"1" (replace -5 -1 :dir rl)"1" replace -1 -2 :dir rl)"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" replace -2)"1" case "vect2(A) = vect2(zero)" )"1" replace -2 -1 :dir rl)"1" rewrite "vect2_add" )"1" rewrite "vect2_scal" )"1" assert )"1" replace -1)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -3 :dir rl)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (replace -1 :dir rl)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "horizontal_tca" 1)"2" (cross-mult 1)"2" (ground)"1" (lemma "vectors_2D.sqv_eq_0" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" (lemma "vectors_2D.sqv_eq_0" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"posreal" vertical_los_crit_CA nil )"posreal" vertical_los_crit_CA 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 cd3d_ever nil )"(total_order?[real])" nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"real" definitions nil )"Vect2" vect_3D_2D "vectors/" )"Vect3" vertical_los_crit_CA nil )"Vect3" vertical_los_crit_CA nil )nil real_types nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vect_3D_2D "vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )nil vectors_2D "vectors/" )nil abs_lems "reals/" )nil vectors_3D "vectors/" )nil vect_3D_2D "vectors/" )nil vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"[T, T -> boolean]" equalities nil )nil vectors_3D "vectors/" )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil extra_real_props nil )nil reals nil )"nnreal" vectors_2D "vectors/" )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" vectors_2D "vectors/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )"nnreal" nil )"bool" space_3D nil )"real" reals nil )"real" reals nil )nil vectors_3D_def "vectors/" )"bool" vertical_los_crit_CA nil ))nil ))nil 3562954006"" (subtype-tcc) nil nil )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )"bool" vertical_los_crit_CA nil )"real" reals nil )"nzreal" real_typesnil ))nil ))nil 3520001568"" (skeep)"" (split +)"1" (assert )"1" (typepred "vertical_decision_vect(s, v)" )"1" (replace -2) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (expand "vertical_decision_vect" )"2" (case "vect2(v)=zero IFF vect2(-v)=zero" )"1" (replace -1 :dir rl)"1" case "CA_cyl_conflict_ever?(s, v) IFF CA_cyl_conflict_ever?(-s, -v)" )"1" (replace -1 :dir rl)"1" (hide -1)"1" case "vect2(-s) * vect2(-v)=vect2(s) * vect2(v)" )"1" (replace -1)"1" (hide -1)"1" case "NOT vect2(v) = zero IMPLIES (-s + horizontal_tca(vect2(-s), vect2(-v)) * -v) = -(s + horizontal_tca(vect2(s), vect2(v)) * v)" )"1" case "FORALL (vvss:Vect3): vvss=zero IFF -vvss = zero" )"1" (inst-cp - "s" )"1" "v" )"1" "1" replace -1 :dir rl)"1" case "FORALL (vvss:Vect3): vvss/=zero IFF -vvss /= zero" )"1" "s" )"1" "1" replace -1 :dir rl)"1" rewrite "vz_neg" )"1" case "FORALL (vvss:Vect3): vvss=zero IFF -vvss = zero" )"1" "v" )"1" rewrite "vz_neg" )"1" case "v = zero IFF vect2(v) = zero AND v`z = 0" )"1" "1" "1" "1" "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "zero" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" case "vvss = -(-vvss)" )"1" replace "1" replace "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" case "vvss = -(-vvss)" )"1" replace "1" replace "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" case "vvss = -(-vvss)" )"1" replace -1 +)"1" replace -2)"1" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" case "vvss = -(-vvss)" )"1" replace -1 +)"1" replace -2)"1" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "2" "2" "1" case "vvss = -(-vvss)" )"1" replace -1 +)"1" replace -2)"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" case "vvss = -(-vvss)" )"1" replace -1 +)"1" replace -2)"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (flatten)"2" assert )"2" case "horizontal_tca(vect2(-s), vect2(-v))=horizontal_tca(vect2(s), vect2(v))" )"1" replace -1)"1" "1" "horizontal_tca" )nil nil ))nil ))nil )"2" "2" expand "horizontal_tca" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (ground) nil nil )"4" (hide 2) (("4" (ground) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "CA_cyl_conflict_ever?" )"2" (rewrite "cd3d_ever" :dir rl)"2" (rewrite "cd3d_ever" :dir rl)"2" (expand "conflict?" )"2" (ground)"1" (skosimp*)"1" (inst + "nnt!1" )"1" (grind) nil nil )) nil ))nil )"2" (skosimp*)"2" (inst + "nnt!1" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "zero" ) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"{vq: Vect3 | (s /= zero OR v /= zero) IMPLIES vq /= zero}" nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"boolean" notequal nil )nil vectors_3D_def "vectors/" )nil reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"[T, T -> boolean]" equalities nil )nil vectors_2D_def "vectors/" )"[bool, bool -> bool]" booleans nil )"bool" vertical_los_crit_CA nil )"real" definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"real" reals nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil vectors_3D "vectors/" )"nzreal" real_typesnil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil real_props nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil reals nil )nil real_props nil )"real" reals nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"real" vectors_2D "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"posreal" nil )"posreal" sq "reals/" )"(strict_total_order?[real])" real_props nil )"bool" space_3D nil )"posreal" vertical_los_crit_CA nil )"posreal" vertical_los_crit_CA nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil cd3d_ever nil )"even_int" integers nil ))nil )nil 3519752529"" (expand "antisymmetric?" )"" (skeep)"" (expand "vertical_decision_vect" )"" (case "vect2(vo - vi) = zero iFF vect2(vi - vo) = zero" )"1" (replace -1 :dir rl)"1" case "CA_cyl_conflict_ever?(s, vo - vi) IFF CA_cyl_conflict_ever?(-s, vi - vo)" )"1" (replace -1 :dir rl)"1" (hide -1)"1" case "vect2(-s) * vect2(vi - vo)=vect2(s) * vect2(vo - vi)" )"1" (replace -1)"1" (hide -1)"1" case "NOT vect2(vo - vi) = zero IMPLIES -(-s + ") "1" (lift-if)"1" (lift-if)"1" "1" "1" "1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (flatten)"2" assert )"2" "2" case "horizontal_tca(vect2(-s), vect2(vi - vo))=horizontal_tca(vect2(s), vect2(vo - vi))" )"1" replace -1)"1" "1" "horizontal_tca" )nil nil ))nil ))nil )"2" "2" expand "horizontal_tca" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (ground) nil nil )"4" (hide 2) (("4" (ground) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "CA_cyl_conflict_ever?" )"2" (rewrite "cd3d_ever" :dir rl)"2" (rewrite "cd3d_ever" :dir rl)"2" (expand "conflict?" )"2" (ground)"1" (skosimp*)"1" (inst + "nnt!1" )"1" (grind) nil nil )) nil ))nil )"2" (skosimp*)"2" (inst + "nnt!1" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "zero" )"2" (expand "vect2" )"2" (rewrite "vx_distr_sub" )"2" (rewrite "vy_distr_sub" )"2" (rewrite "vy_distr_sub" )"2" (rewrite "vx_distr_sub" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Nz_vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"real" definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"nnreal" vectors_2D "vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"real" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"posreal" sq "reals/" )"bool" space_3D nil )nil cd3d_ever nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" ))nil 3562944353"" (skosimp*) (("" (replace -5) (("" (assert ) nil nil )) nil )) nil )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3562944353"" (skosimp*) (("" (replace -5) (("" (assert ) nil nil )) nil )) nil )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3520096277"" (skeep)"" (lemma "vs_bound_crit_indep" )"" (expand "vertical_los_crit_CA?" )"" (expand "vertical_los_criterion?" )"" (flatten)"" "dv_to_ec(vertical_decision_vect)(s, v)" "nv" "s" "v" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"posreal" vertical_los_crit_CA nil )"posreal" vertical_los_crit_CA 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_los_criterion nil )"bool" vertical_los_criterionnil )"Decision_Vector" vertical_los_crit_CA 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_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_3D "vectors/" )nil vertical_los_crit_CAnil )"Sign" vertical_los_crit_CA nil )"{vq: Vect3 | (s /= zero OR v /= zero) IMPLIES vq /= zero}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"Vertical_Strategy[D, H]" vertical_los_crit_CA nil )"real" reals nil )"(total_order?[real])" nil )"bool" vertical_los_crit_CA nil ))nil 3562945349"" (skosimp*) (("" (replace -4) (("" (assert ) nil nil )) nil )) nil )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3562945349"" (skosimp*) (("" (replace -4) (("" (assert ) nil nil )) nil )) nil )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3562945351"" (skeep)"" (lemma "vertical_los_crit_CA_independent" )"" (inst?)"" (assert )"" (assert )"" (name "epsi" "dv_to_ec(vertical_decision_vect)(s, v)" )"" (replace -1)"" (expand "dv_to_ec" -1)"" (expand "vertical_decision_vect" -1)"" (lift-if)"" (split -1)"1" (flatten)"1" (assert )"1" (invoke (case "NOT %1" ) (! 2 1))"1" "1" (ground) nil nil ))nil )"2" replace -1)"2" assert )"2" case "s`z = 0" )"1" case "sign(s`z) = 1" )"1" replace -1)"1" replace -2)"1" assert )"1" "1" case "NOT v`z>=0" )"1" expand "sign" )"1" assert )nil nil ))nil )"2" assert )"2" expand "sign" )"2" case "v = zero" )"1" replace -1)"1" assert )nil nil ))nil )"2" case "sqv(v)=0" )"1" "vectors_3D.sqv_eq_0" )"1" "1" assert )nil nil ))nil ))nil )"2" assert )"2" case "v`z = 0" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" rewrite "vz_scal" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "NOT v`z > 0" )"1" assert )nil nil )"2" assert )"2" case "NOT epsi = 1" )"1" "break_vz_symm_sz" )"1" "v" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" replace "2" assert )"2" rewrite "vz_distr_add" )"2" rewrite "vz_distr_add" )"2" rewrite "vz_scal" )"2" rewrite "vz_scal" )"2" assert )"2" replace "2" assert )"2" "horizontal_tca(s,v)" )"1" assert )"1" expand "abs" )"1" nil nil ))nil ))nil )"2" case "%1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" (assert ) nil nil ))nil ))nil )"2" assert )"2" case "sign(s`z) = sign(v`z)" )"1" assert )"1" "1" case "epsi * (s + horizontal_tca((vect2(s)), vect2(v)) * v)`z >=0" )"1" "epsi" )"1" expand "abs" )"1" "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (egr:real): sign(egr)*egr >= 0" )"1" "v`z" )"1" "s`z" )"1" assert )"1" "horizontal_tca(s,v)" )"1" assert )"1" "break_vz_symm_sz" )"1" "s" )"1" assert )"1" replace "1" replace "1" replace "1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" rewrite "vz_scal" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "horizontal_tca" "2" "2" "1" "vectors_2D.sqv_eq_0" )"1" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "vectors_2D.sqv_eq_0" )"2" "2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "vectors_2D.sqv_eq_0" )"3" "3" assert )"3" replace "3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "vectors_2D.sqv_eq_0" )"4" "4" assert )"4" replace "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "break_vz_symm_sz" )"2" "s" )"2" assert )"2" replace -4)"2" expand "vertical_los_crit_CA?" )"2" expand "vertical_decision_vect" )"2" expand "dv_to_ec" )"2" assert )"2" replace "2" replace "2" expand "vertical_los_criterion?" )"2" "2" assert )"2" expand "min_rel_vert_speed" )"2" assert )"2" case "NOT epsi*nv`z >= 0" )"1" "1" nil nil ))nil )"2" "2" assert )"2" case "sign(nv`z) = sign(s`z)" )"1" replace "1" case "epsi*nv`z >= 0" )"1" "horizontal_tca(s,nv)" )"1" assert )"1" case "epsi = sign((s + horizontal_tca((vect2(s)), vect2(nv)) * nv)`z)" )"1" case "FORALL (egr:real): sign(egr)*egr = abs(egr)" )"1" "(s + horizontal_tca((vect2(s)), vect2(nv)) * nv)`z" )"1" "s`z" )"1" replace "1" replace "1" assert )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" rewrite "vz_scal" )"1" assert )"1" replace "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" replace "2" replace "2" "2" "horizontal_tca" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "horizontal_tca" "2" "2" "1" "vectors_2D.sqv_eq_0" )"1" "1" assert )"1" replace "1" assert )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 )"3" "vectors_2D.sqv_eq_0" )"3" "3" assert )"3" replace "3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "vectors_2D.sqv_eq_0" )"4" "4" assert )"4" replace "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" nil nil ))nil ))nil ))nil )"2" replace "2" case "NOT nv`z = 0" )"1" "1" nil nil ))nil )"2" rewrite "vz_distr_add" )"2" rewrite "vz_distr_add" )"2" rewrite "vz_scal" )"2" rewrite "vz_scal" )"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 ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide 4)"2" "1" "1" replace -1)"1" (assert ) nil nil ))nil ))nil )"2" "2" "break_vz_symm_sz" )"2" "2" case "%1" ) (! -1 1))"1" assert )"1" "1" replace -2)"1" replace -1)"1" case "FORALL (egr:real): sign(egr)*egr = abs(egr)" )"1" "(s + horizontal_tca((vect2(s)), vect2(v)) * v)`z" )"1" replace "1" assert )"1" replace "1" replace "1" "1" "epsi" )"1" "horizontal_tca" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"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 )"real" reals nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"Decision_Vector" vertical_los_crit_CA nil )"Vertical_Strategy[D, H]" vertical_los_crit_CA nil )"{vq: Vect3 | (s /= zero OR v /= zero) IMPLIES vq /= zero}" nil )"Sign" vertical_los_crit_CA nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil vertical_los_crit_CAnil )"Vector" vectors_3D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"{j: nonneg_int | j >= i}" nil )"bool" vertical_los_crit_CA nil )NOT const-decl "[bool -> bool]" booleans nil )"{x: nnreal | abs(sz) < H IMPLIES x > 0}" vertical_los_criterionnil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"Vect3" vertical_los_crit_CA nil )"bool" vertical_los_criterionnil )"bool" vertical_los_crit_CA nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_3D "vectors/" )nil extra_real_propsnil )nil extra_real_props nil )"nzreal" real_typesnil )"Sign" sign "reals/" )nil vectors_3D "vectors/" )nil vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )nil vertical_los_crit_CA nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"real" reals nil )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil reals nil )nil extra_real_props nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"Vect3" vertical_los_crit_CA nil )"Vect3" vertical_los_crit_CA nil )nil real_props nil )"Vect2" vect_3D_2D "vectors/" )"real" definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"real" reals nil )nil vectors_3D "vectors/" )nil abs_lems "reals/" )nil vectors_3D "vectors/" )"nnreal" vectors_3D "vectors/" )nil real_types nil )"odd_int" integers nil )nil abs_lems "reals/" )nil sign "reals/" )nil vectors_3D_def "vectors/" )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 3562937623"" (skeep)"" (expand "vertical_los_crit_CA?" )"" (expand "vertical_los_criterion?" )"" (expand "dv_to_ec" )"" (flatten)"" (expand "min_rel_vert_speed" )"" (expand "max" )"" (lift-if) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vertical_los_crit_CA nil )"Sign" vertical_los_crit_CA nil )"{x: nnreal | abs(sz) < H IMPLIES x > 0}" vertical_los_criterionnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"Decision_Vector" vertical_los_crit_CA nil )"real" reals nil )"(total_order?[real])" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" vertical_los_criterionnil ))nil ))nil 3562937572"" (skeep)"" (expand "vertical_los_crit_CA?" )"" (lemma "vertical_los_criterion_coord" )"" "MinRelVertSpeedi" "MinRelVertSpeedo" "dv_to_ec(vertical_decision_vect)(s,vo-vi)" "nvi" "nvo" "s" "vi" "vo" )"" (assert )"" (split -)"1" (expand "vertical_los_criterion?" -1)"1" (flatten)"1" (expand "dv_to_ec" )"1" (rewrite "vz_distr_sub" )"1" (expand "min_rel_vert_speed" )"1" (expand "max" )"1" (lift-if)"1" (lift-if)"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "dv_to_ec(vertical_decision_vect)" )"2" (inst - "s" "vo-vi" )"2" (assert )"2" (case "-(vo-vi) = vi-vo" )"1" (assert ) nil nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vertical_los_crit_CA nil )"Decision_Vector" vertical_los_crit_CA 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_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_3D "vectors/" )nil vertical_los_crit_CAnil )"Sign" vertical_los_crit_CA nil )"{vq: Vect3 | (s /= zero OR v /= zero) IMPLIES vq /= zero}" nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"{x: nnreal | abs(sz) < H IMPLIES x > 0}" vertical_los_criterionnil )"bool" vertical_los_criterionnil )"nzreal" real_typesnil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"Vertical_Strategy[D, H]" vertical_los_crit_CA nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"{z: posreal | z >= x AND z >= y}" real_defs 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 )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" vertical_los_crit_CA nil )"posreal" vertical_los_crit_CA nil ))nil ))nil 3563037117"" (skeep)"" (expand "vertical_los_crit_CA?" )"" (lemma "vertical_los_criterion_coord" )"" (inst?)"" (assert )"" (typepred "dv_to_ec(vertical_decision_vect)" )"" (inst - "s" "vo-vi" )"" (assert )"" (case "-(vo-vi) = vi-vo" )"1" (assert ) nil nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vertical_los_crit_CA nil )"Decision_Vector" vertical_los_crit_CA 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_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_3D "vectors/" )nil vertical_los_crit_CAnil )"Sign" vertical_los_crit_CA nil )"{vq: Vect3 | (s /= zero OR v /= zero) IMPLIES vq /= zero}" nil )"Vector" vectors_3D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"real" reals nil )"nzreal" real_typesnil )"Vertical_Strategy[D, H]" vertical_los_crit_CA nil )"{z: posreal | z >= x AND z >= y}" real_defs 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 )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" vertical_los_crit_CA nil )"posreal" vertical_los_crit_CA nil ))nil 3563026818"" (skosimp*) (("" (replace -6) (("" (assert ) nil nil )) nil )) nil )nil vectors_2D "vectors/" )"(total_order?[real])" nil ))nil ))nil 3563026818"" (skosimp*) (("" (replace -6) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" ))nil ))nil 3563026927"" (skeep)"" (skoletin 1 :postfix "aa" )"" (skoletin 1 :postfix "aa" )"" (flatten)"" (lemma "vertical_los_crit_CA_coordinated" )"" "MinRelVertSpeedi" "MinRelVertSpeedo" "nvi" "nvo" "s" "vi" "vo" )"" (assert )"" (lemma "vertical_los_crit_CA_independent_strong" )"" "max(MinRelVertSpeedo,MinRelVertSpeedi)" "nvo-nvi" "s" "vo-vi" )"" (assert )"" (flatten)"" (assert ) (("" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )nil vectors_2D "vectors/" )"real" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_3D "vectors/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" vertical_los_crit_CA nil )"Vector" vectors_3D "vectors/" )"bool" reals nil )"Vector" vectors_2D "vectors/" )"[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 )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"Sign" sign "reals/" )"bool" vertical_los_crit_CA nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_2D "vectors/" )"real" definitions nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[bool, bool -> bool]" booleans nil )nil nil )"(total_order?[real])" nil )nil sign "reals/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{z: posreal | z >= x AND z >= y}" real_defs nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil nil )"(total_order?[real])" nil ))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.166Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
