Impressum cd3d_si.prf
Sprache: Lisp
(cd3d_sinil 3472912840 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3473066751 ("" (subtype-tcc) nil nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3473066751 ("" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_si nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"int" integers nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3473066751"" (skeep)"" "lambda (jj: below[N]): (# time:=(to+B) + (T-B)/2 + jj,position:=zero #)" )"" (split) (("1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3482764106"" (skeep)"" (assert )"" "lambda (jj: below[N]): (# time:=(to+B) + (T-B)/2 + jj,position:=zero #)" )"" (assert )"" (split) (("1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"real" cd3d_si nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"{AB: posreal | AB > B}" cd3d_si nil )"nnreal" cd3d_si nil )nil real_types nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil nat_types nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans 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 )"real" reals nil )"real" reals nil )"nnreal" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3482764106 ("" (subtype-tcc) nil nil ) nil nil ))nil 3482764106 ("" (subtype-tcc) nil nil ) nil nil ))nil 3477825885 ("" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_si nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil ))nil ))nil 3477826332"" (skeep)"" (typepred "flpl" )"" (inst - "j+1" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )"nnreal" cd3d_si nil )nil real_types nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil flightplan nil )nil vectors_3D_def "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil 3473002468"" (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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil int_types nil )"above[1]" cd3d_si nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" cd3d_si nil )"nnreal" cd3d_si nil ))nil ))nil 3473002469"" (skeep)"" (typepred "flpl" )"" (expand "seg_lh_top" )"" (expand "seg_lh_bottom" )"" (case "k = N-1" )"1" (replace -1)"1" (hide 1)"1" (assert )"1" (expand "min" )"1" (expand "max" )"1" (lift-if)"1" (ground)"1" (inst - "N-1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "k = 0" )"1" (replace -1)"1" (hide 3)"1" (assert )"1" (expand "max" )"1" (expand "min" )"1" (lift-if)"1" (ground)"1" (inst - "1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "max" 3)"2" (expand "min" 4)"2" (case "flpl(k)`time = to+T" )"1" (inst - "k" )"1" (expand "max" )"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (inst - "k+1" )"2" (expand "min" )"2" (lift-if) (("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )"nnreal" cd3d_si nil )nil real_types nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil flightplan nil )nil vectors_3D_def "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nnreal" cd3d_si nil )"even_int" integersnil )"posint" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(total_order?[real])" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"real" cd3d_si nil )"real" reals nil ))nil 3473074224 ("" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_si nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"real" reals nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nnreal" cd3d_si nil )"real" cd3d_si nil ))nil ))nil 3475844668"" (skeep)"" (ground)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (typepred "tt!1" )"1" (expand "end_time" )"1" (expand "start_time" )"1" case "EXISTS (kk: below[N]): tt!1 = flpl(kk)`time" )"1" (skosimp*)"1" (lemma "nontrivial_lookahead" )"1" (inst - "kk!1" "to" "flpl" )"1" (assert )"1" (split -1)"1" (flatten)"1" "kk!1" )"1" assert )"1" "seg_lh_bottom(flpl, to)(kk!1)" )"1" "location_at_check" )"1" "flpl" "kk!1" )"1" replace -4 :dir rl)"1" replace -1)"1" case "seg_lh_bottom(flpl,to)(kk!1) = 0" )"1" replace -1)"1" assert )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "seg_lh_bottom" )"2" expand "max" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "kk!1-1" )"1" assert )"1" "seg_lh_top(flpl, to)(kk!1 - 1)" )"1" "location_at_check" )"1" "flpl" "kk!1" )"1" replace -4 :dir rl)"1" replace -1)"1" "1" "cv1" "(so + (flpl(kk!1 - 1)`time - to) * vo) - ") "1" "cv2" "(so + (tt!1 - to) * vo) - flpl(kk!1)`position" )"1" case "cv1 = cv2" )"1" case "vect2(cv1) = vect2(cv2) AND cv1`z = cv2`z" )"1" "1" replace "1" replace "1" rewrite "vect2_sub" )"1" rewrite "vect2_add" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_scal" )"1" rewrite "vect2_add" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_scal" )"1" rewrite "vect2_add" )"1" rewrite "vect2_scal" )"1" assert )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_scal" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_scal" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" 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" assert )nil nil ))nil )"2" replace "2" replace "2" "2" "velocity_def" )"2" "flpl" "kk!1-1" )"2" assert )"2" expand "seg_lh_top" )"2" expand "min" )"2" "2" "velocity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name "jj" "segment(flpl)(tt!1)" )"2" (label "jjname" -1)"2" (inst 2 "jj" )"1" (lemma "segment_def" )"1" (inst - "flpl" "tt!1" )"1" (flatten)"1" case "jj < N-1" )"1" assert )"1" case "flpl(jj)`time < tt!1" )"1" case "seg_lh_bottom(flpl,to)(jj) < seg_lh_top(flpl,to)(jj)" )"1" assert )"1" "newt" "tt!1-flpl(jj)`time" )"1" "newt" )"1" "cv1" "(so + (flpl(jj)`time - to) * vo) - flpl(jj)`position + ") "1" "cv2" "(so + (tt!1 - to) * vo) - location_at(flpl)(tt!1)" )"1" case "cv1 = cv2" )"1" case "vect2(cv1) = vect2(cv2) AND cv1`z = cv2`z" )"1" "1" replace "1" replace "1" rewrite "vect2_sub" )"1" rewrite "vect2_add" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_scal" )"1" rewrite "vect2_add" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_scal" )"1" rewrite "vect2_add" )"1" rewrite "vect2_scal" )"1" assert )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_scal" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_scal" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" 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" assert )nil nil ))nil )"2" "2" replace "2" replace "2" expand "location_at" )"2" replace "jjname" )"2" "jjname" )"2" "2" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "seg_lh_bottom" )"2" expand "max" )"2" "2" assert )"2" expand "seg_lh_top" )"2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "seg_lh_bottom" )"2" expand "seg_lh_top" )"2" expand "max" )"2" expand "min" )"2" "2" "2" assert )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jj" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" case "jj = N-1" )"1" replace -1)"1" "1" "1" "N-1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "N-1" )"1" (expand "segment" )"1" "segment_max(extend[nat, below[N], bool, FALSE] ") "1" replace "jjname" )"1" expand "extend" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (rewrite "conflict_3D_on_open_interval" )"2" (skosimp*)"2" (name "t!1" "topen!1" )"2" (replace -1)"2" (hide -1)"2" (name "newt" "flpl(j!1)`time+t!1" )"2" "cv1" "(so + (newt - to) * vo) - location_at(flpl)(newt)" )"1" "cv2" "(so + (flpl(j!1)`time - to) * vo) - flpl(j!1)`position + ") "1" (case "NOT cv1 = cv2" )"1" (hide 2)"1" (replace -1 :dir rl)"1" replace -2 :dir rl)"1" "1" "1" case "segment(flpl)(newt) = j!1" )"1" replace -2 :dir rl)"1" expand "location_at" )"1" assert )"1" replace -1)"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "pj" "segment(flpl)(newt)" )"2" replace -1)"2" case "newt >= flpl(j!1)`time AND newt < flpl(j!1+1)`time" )"1" "1" "1" expand "segment" "1" "segment_max(extend[nat, below[N], bool, FALSE] ") "1" replace -3)"1" expand "extend" )"1" assert )"1" case "pj < 1+j!1" )"1" "j!1" )"1" "1" assert )nil nil ))nil ))nil )"2" "flight_plan_ascending_time" )"2" "flpl" "pj" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "seg_lh_bottom" )"2" expand "seg_lh_top" )"2" expand "min" )"2" expand "max" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "conflict_3D?" )"2" (inst + "newt" )"1" case "vect2(cv1) = vect2(cv2) AND cv1`z = cv2`z" )"1" "1" replace -4 :dir rl)"1" replace -5 :dir rl)"1" rewrite "vect2_sub" )"1" rewrite "vect2_add" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_scal" )"1" rewrite "vect2_add" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_scal" )"1" rewrite "vect2_add" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_scal" )"1" assert )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_scal" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_scal" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_scal" )"1" 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 )"2" (assert ) nil nil ))nil )"2" expand "seg_lh_bottom" )"2" expand "seg_lh_top" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "start_time" )"2" (expand "end_time" )"2" (expand "seg_lh_bottom" )"2" (expand "seg_lh_top" )"2" "flight_plan_ascending_time" )"2" "flpl" "j!1" "0" )"2" "flpl" "N-1" "j!1+1" )"2" assert )"2" "1" assert )"1" "1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" assert )"2" expand "min" )"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 )"[T, T -> boolean]" equalities nil )nil cd3d_si nil )"(total_order?[real])" nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"int" integers nil )nil flightplan nil )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vect_3D_2D "vectors/" )nil vect_3D_2D "vectors/" )nil vect_3D_2D "vectors/" )"Vect3" flightplan nil )"Vector" vectors_3D "vectors/" )"below[N]" cd3d_si nil )"(strict_total_order?[real])" real_props nil )nil flightplan nil )"odd_int" integers nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"nnreal" cd3d_si nil )"real" cd3d_si nil )nil Lookahead nil )"bool" booleans nil )"R" extend nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )"[SS: non_empty_finite_set[nat] -> AND (FORALL (x: nat): SS(x) IMPLIES x <= a)}]" nil )nil flightplan nil )"posint" nil )"nzreal" nil )"Vect3" flightplan nil )"FlightPlanRelevant(to)" cd3d_si nil )"real" cd3d_si nil )"real" cd3d_si nil )"posint" nil )"below[N]" cd3d_si nil )"below[N]" flightplan 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_si nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )"real" flightplan nil )nil flightplan nil )nil cd3d_si nil )"bool" cd3d_si nil )"bool" cd3d nil )"real" reals nil )"real" reals nil )"real" reals nil )nil cd3d nil )"posreal" cd3d_si nil )"posreal" cd3d_si nil )nil flightplan nil )"real" cd3d_si nil ))nil )nil 3475844455"" (skeep)"" (ground)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (typepred "tt!1" )"1" (expand "end_time" )"1" (expand "start_time" )"1" case "EXISTS (kk: below[N]): tt!1 = flpl(kk)`time" )"1" (skosimp*)"1" (lemma "nontrivial_lookahead" )"1" (inst - "T" "kk!1" "to" "flpl" )"1" (assert )"1" (split -1)"1" (flatten)"1" "kk!1" )"1" assert )"1" "0" )"1" assert )"1" "location_at_check" )"1" "flpl" "kk!1" )"1" replace -4 :dir rl)"1" replace -1)"1" case "seg_lh_bottom(flpl,to,T)(kk!1) = tt!1" )"1" replace -1)"1" case "flpl(kk!1)`position = lh_start_position(flpl,to,T)(kk!1)" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" assert )nil )))))))"2" "2" expand "lh_start_position" )"2" replace -1)"2" replace "2" assert )nil )))))))))))))"2" "2" expand "seg_lh_bottom" "2" expand "max" )"2" assert )nil )))))))))))))))))))))))))))"2" (flatten)"2" "kk!1-1" )"1" assert )"1" "seg_lh_top(flpl,to,T)(kk!1 - 1) - ") "1" "location_at_check" )"1" "flpl" "kk!1" )"1" replace -4 :dir rl)"1" replace -1)"1" "1" case "(so + (seg_lh_bottom(flpl,to,T)(kk!1 - 1) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to,T)(kk!1 - 1) - to) * vo) - AND vect2((so + (seg_lh_bottom(flpl,to,T)(kk!1 - 1) - to) * vo) -") "1" "1" assert )nil )))"2" "2" "lsp" "lh_start_position(flpl,to,T)(kk!1 - 1)" )"2" replace -1)"2" "slb" "seg_lh_bottom(flpl,to,T)(kk!1 - 1)" )"2" replace "2" "slt" "seg_lh_top(flpl,to,T)(kk!1 - 1)" )"2" replace "2" "velc" "velocity(flpl)(kk!1-1)" )"2" replace "2" "2" "2" "2" "2" nil )))))))))))))))))))))))))))))"2" "2" "velocity_def" )"2" "flpl" "kk!1-1" )"2" assert )"2" case "flpl(kk!1-1)`time >= to" )"1" case "seg_lh_bottom(flpl,to,T)(kk!1-1) = flpl(kk!1-1)`time" )"1" replace "1" case "flpl(kk!1)`time <= to+T" )"1" case "seg_lh_top(flpl,to,T)(kk!1-1) = flpl(kk!1)`time" )"1" replace "1" expand "lh_start_position" )"1" replace "1" assert )"1" replace "1" "1" nil )))))))))))))"2" "2" nil )))))"2" assert )nil )))))"2" "2" expand "seg_lh_bottom" )"2" expand "max" )"2" "2" assert )nil )))))))))))"2" case "NOT seg_lh_bottom(flpl,to,T)(kk!1-1) = to" )"1" expand "seg_lh_bottom" "1" expand "max" )"1" "1" nil )))))))"2" expand "lh_start_position" )"2" replace "2" assert )"2" expand "seg_lh_top" )"2" expand "min" )"2" "2" nil )))))))))))))))))))))))))))))))))))))))))"2" (assert ) nil )))))))))))))))"2" (name "jj" "segment(flpl)(tt!1)" )"2" (label "jjname" -1)"2" (name "jjname" -1)"2" (inst 2 "jj" )"1" (lemma "segment_def" )"1" (inst - "flpl" "tt!1" )"1" "1" case "jj < N-1" )"1" assert )"1" case "flpl(jj)`time < tt!1" )"1" case "seg_lh_bottom(flpl,to,T)(jj) < seg_lh_top(flpl,to,T)(jj)" )"1" assert )"1" "newt" "tt!1-seg_lh_bottom(flpl,to,T)(jj)" )"1" "newt" )"1" case "(so + (seg_lh_bottom(flpl,to,T)(jj) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to,T)(jj) - to) * vo) - AND 1))") "1" "1" assert )nil )))"2" "2" "slb1" "seg_lh_bottom(flpl,to,T)(jj)" )"2" "lsp" "lh_start_position(flpl,to,T)(jj)" )"2" "lal" "location_at(flpl)(tt!1)" )"2" "v1" "velocity(flpl)(jj)" )"2" replace "2" "2" replace "2" "2" replace "2" "2" replace "2" "2" nil )))))))))))))))))))))))))))))"2" "2" expand "location_at" )"2" replace "jjname" )"2" "jjname" )"2" "2" "2" nil )))))))))))))))"2" case "seg_lh_bottom(flpl,to,T)(jj) <= tt!1 AND tt!1 <= seg_lh_top(flpl,to,T)(jj)" )"1" "1" (assert ) nil )))"2" "2" expand "seg_lh_bottom" "2" expand "seg_lh_top" "2" expand "max" )"2" expand "min" )"2" "2" "2" assert )nil )))))))))))))))))))))))"2" "2" expand "seg_lh_bottom" )"2" expand "seg_lh_top" )"2" expand "max" )"2" expand "min" )"2" "2" "2" assert )nil )))))))))))))))))"2" "jj" )"2" (assert ) nil )))))))"2" case "jj = N-1" )"1" replace -1)"1" "1" "1" "N-1" )"1" (assert ) nil )"2" (assert ) nil )))))))))"2" (assert ) nil )))))))))))"2" (inst + "N-1" )"1" (expand "segment" )"1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace "jjname" )"1" expand "extend" )"1" (assert ) nil )))))))))"2" (assert ) nil )))))))))))))))))))))))"2" (skosimp*)"2" (expand "conflict_3D?" )"2" (skosimp*)"2" (typepred "t!1" )"2" (name "newt" "seg_lh_bottom(flpl,to,T)(j!1) + t!1" )"2" (case "to<=newt AND newt<=to+T" )"1" (flatten)"1" (inst + "newt" )"1" case "(so + (seg_lh_bottom(flpl,to,T)(j!1) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to,T)(j!1) - to) * vo) - AND t))") "1" (flatten) (("1" (assert ) nil )))"2" (hide 2)"2" (hide-all-but (-1 1))"2" "slb1" "seg_lh_bottom(flpl,to,T)(j!1)" )"2" "lsp" "lh_start_position(flpl,to,T)(j!1)" )"2" "sltop" "seg_lh_top(flpl,to,T)(j!1)" )"2" "loc1" "location_at(flpl)(newt)" )"2" "velc" "velocity(flpl)(j!1)" )"2" replace -1)"2" "2" replace -1)"2" "2" "2" replace -1)"2" "2" replace -1)"2" "2" nil )))))))))))))))))))))))))))))))))))"2" (hide 2)"2" (hide -7)"2" (hide -7)"2" case "t!1 < seg_lh_top(flpl,to,T)(j!1) - seg_lh_bottom(flpl,to,T)(j!1)" )"1" case "segment(flpl)(newt) = j!1" )"1" expand "location_at" )"1" replace -1)"1" "1" assert )"1" "1" nil )))))))))))"2" "2" "pj" "segment(flpl)(newt)" )"2" replace -1)"2" case "newt >= flpl(j!1)`time AND newt < flpl(j!1+1)`time" )"1" "1" "1" expand "segment" -1)"1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace -3)"1" expand "extend" )"1" assert )"1" case "pj < 1+j!1" )"1" "j!1" )"1" "1" assert )nil )))))"2" "flight_plan_ascending_time" )"2" "flpl" "pj" "1+j!1" )"2" assert )nil )))))))))))))))))))))"2" case "seg_lh_top(flpl,to,T)(j!1) <= flpl(j!1+1)`time AND seg_lh_bottom(flpl,to,T)(j!1) >= flpl(j!1)`time" )"1" "1" (assert ) nil )))"2" "2" expand "seg_lh_top" 1)"2" expand "seg_lh_bottom" "2" expand "min" )"2" expand "max" )"2" "2" "2" assert )nil )))))))))))))))))))))))))))"2" case "newt = seg_lh_top(flpl,to,T)(j!1)" )"1" case "to+T < flpl(j!1+1)`time" )"1" case "segment(flpl)(newt) = j!1" )"1" expand "location_at" )"1" replace -1)"1" "1" assert )"1" case "seg_lh_top(flpl,to,T)(j!1) = to+T" )"1" replace -1)"1" "1" "1" nil )))))))"2" expand "seg_lh_top" "2" expand "min" )"2" nil )))))))))))))))"2" "2" "pj" "segment(flpl)(newt)" )"2" replace -1)"2" case "newt >= flpl(j!1)`time AND newt < flpl(j!1+1)`time" )"1" "1" "1" expand "segment" "1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace -3)"1" expand "extend" )"1" assert )"1" case "pj < 1+j!1" )"1" "j!1" )"1" "1" assert )nil )))))"2" "flight_plan_ascending_time" )"2" "flpl" "pj" "1+j!1" )"2" assert )nil )))))))))))))))))))))"2" "2" "2" nil )))))))))))))))"2" case "newt = flpl(j!1+1)`time" )"1" "location_at_check" )"1" "flpl" "j!1+1" )"1" replace -2 :dir rl)"1" replace -1)"1" replace -2)"1" "1" expand "lh_start_position" )"1" "velocity_def" )"1" "flpl" "j!1" )"1" "vel11" "velocity(flpl)(j!1)" )"1" replace "1" "1" nil )))))))))))))))))))))))))"2" "2" expand "seg_lh_top" -1)"2" expand "min" )"2" "2" nil )))))))))))))"2" (assert ) nil )))))))))))"3" (hide 2)"3" case "seg_lh_bottom(flpl,to,T)(j!1) >= start_time(flpl) AND seg_lh_top(flpl,to,T)(j!1) <= end_time(flpl)" )"1" (flatten) (("1" (assert ) nil )))"2" (hide 2)"2" expand "seg_lh_bottom" )"2" expand "start_time" )"2" expand "end_time" )"2" expand "seg_lh_top" )"2" "flight_plan_ascending_time" )"2" "flpl" "N-1" "1+j!1" )"2" "flpl" "j!1" "0" )"2" expand "max" )"2" expand "min" )"2" "2" "2" nil )))))))))))))))))))))))))))))))"2" (assert )"2" case "seg_lh_bottom(flpl,to,T)(j!1) >= start_time(flpl) AND seg_lh_top(flpl,to,T)(j!1) <= end_time(flpl)" )"1" (flatten) (("1" (assert ) nil )))"2" (hide 2)"2" (expand "seg_lh_bottom" )"2" expand "start_time" )"2" expand "end_time" )"2" expand "seg_lh_top" )"2" "flight_plan_ascending_time" )"2" "flpl" "N-1" "1+j!1" )"2" "flpl" "j!1" "0" )"2" expand "max" )"2" expand "min" )"2" "2" "2" nil )))))))))))))))))))))))))))))))))"2" case "seg_lh_bottom(flpl,to,T)(j!1) >= to AND seg_lh_top(flpl,to,T)(j!1) <= to+T" )"1" (flatten) (("1" (assert ) nil )))"2" (hide 3)"2" (hide-all-but 1)"2" (grind) nil ))))))))))))))))))))))nil )nil nil )nil 3475844390"" (skeep)"" (ground)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (typepred "tt!1" )"1" (expand "end_time" )"1" (expand "start_time" )"1" case "EXISTS (kk: below[N]): tt!1 = flpl(kk)`time" )"1" (skosimp*)"1" (lemma "nontrivial_lookahead" )"1" (inst - "T" "kk!1" "to" "flpl" )"1" (assert )"1" (split -1)"1" (flatten)"1" "kk!1" )"1" assert )"1" "0" )"1" assert )"1" "location_at_check" )"1" "flpl" "kk!1" )"1" replace -4 :dir rl)"1" replace -1)"1" case "seg_lh_bottom(flpl,to)(kk!1) = tt!1" )"1" replace -1)"1" case "flpl(kk!1)`position = lh_start_position(flpl,to)(kk!1)" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" assert )nil )))))))"2" "2" expand "lh_start_position" )"2" replace -1)"2" replace "2" assert )nil )))))))))))))"2" "2" expand "seg_lh_bottom" "2" expand "max" )"2" assert )nil )))))))))))))))))))))))))))"2" (flatten)"2" "kk!1-1" )"1" assert )"1" "seg_lh_top(flpl,to)(kk!1 - 1) - ") "1" "location_at_check" )"1" "flpl" "kk!1" )"1" replace -4 :dir rl)"1" replace -1)"1" "1" case "(so + (seg_lh_bottom(flpl,to)(kk!1 - 1) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to)(kk!1 - 1) - to) * vo) - AND vect2((so + (seg_lh_bottom(flpl,to)(kk!1 - 1) - to) * vo) -") "1" "1" assert )nil )))"2" "2" "lsp" "lh_start_position(flpl,to)(kk!1 - 1)" )"2" replace -1)"2" "slb" "seg_lh_bottom(flpl,to)(kk!1 - 1)" )"2" replace "2" "slt" "seg_lh_top(flpl,to)(kk!1 - 1)" )"2" replace "2" "velc" "velocity(flpl)(kk!1-1)" )"2" replace "2" "2" "2" "2" "2" nil )))))))))))))))))))))))))))))"2" "2" "velocity_def" )"2" "flpl" "kk!1-1" )"2" assert )"2" case "flpl(kk!1-1)`time >= to" )"1" case "seg_lh_bottom(flpl,to)(kk!1-1) = flpl(kk!1-1)`time" )"1" replace "1" case "flpl(kk!1)`time <= to+T" )"1" case "seg_lh_top(flpl,to)(kk!1-1) = flpl(kk!1)`time" )"1" replace "1" expand "lh_start_position" )"1" replace "1" assert )"1" replace "1" "1" nil )))))))))))))"2" "2" nil )))))"2" assert )nil )))))"2" "2" expand "seg_lh_bottom" )"2" expand "max" )"2" "2" assert )nil )))))))))))"2" case "NOT seg_lh_bottom(flpl,to)(kk!1-1) = to" )"1" expand "seg_lh_bottom" "1" expand "max" )"1" "1" nil )))))))"2" expand "lh_start_position" )"2" replace "2" assert )"2" expand "seg_lh_top" )"2" expand "min" )"2" "2" nil )))))))))))))))))))))))))))))))))))))))))"2" (assert ) nil )))))))))))))))"2" (name "jj" "segment(flpl)(tt!1)" )"2" (label "jjname" -1)"2" (name "jjname" -1)"2" (inst 2 "jj" )"1" (lemma "segment_def" )"1" (inst - "flpl" "tt!1" )"1" "1" case "jj < N-1" )"1" assert )"1" case "flpl(jj)`time < tt!1" )"1" case "seg_lh_bottom(flpl,to)(jj) < seg_lh_top(flpl,to)(jj)" )"1" assert )"1" "newt" "tt!1-seg_lh_bottom(flpl,to)(jj)" )"1" "newt" )"1" case "(so + (seg_lh_bottom(flpl,to)(jj) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to)(jj) - to) * vo) - AND 1))") "1" "1" assert )nil )))"2" "2" "slb1" "seg_lh_bottom(flpl,to)(jj)" )"2" "lsp" "lh_start_position(flpl,to)(jj)" )"2" "lal" "location_at(flpl)(tt!1)" )"2" "v1" "velocity(flpl)(jj)" )"2" replace "2" "2" replace "2" "2" replace "2" "2" replace "2" "2" nil )))))))))))))))))))))))))))))"2" "2" expand "location_at" )"2" replace "jjname" )"2" "jjname" )"2" "2" "2" nil )))))))))))))))"2" case "seg_lh_bottom(flpl,to)(jj) <= tt!1 AND tt!1 <= seg_lh_top(flpl,to)(jj)" )"1" "1" (assert ) nil )))"2" "2" expand "seg_lh_bottom" "2" expand "seg_lh_top" "2" expand "max" )"2" expand "min" )"2" "2" "2" assert )nil )))))))))))))))))))))))"2" "2" expand "seg_lh_bottom" )"2" expand "seg_lh_top" )"2" expand "max" )"2" expand "min" )"2" "2" "2" assert )nil )))))))))))))))))"2" "jj" )"2" (assert ) nil )))))))"2" case "jj = N-1" )"1" replace -1)"1" "1" "1" "N-1" )"1" (assert ) nil )"2" (assert ) nil )))))))))"2" (assert ) nil )))))))))))"2" (inst + "N-1" )"1" (expand "segment" )"1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace "jjname" )"1" expand "extend" )"1" (assert ) nil )))))))))"2" (assert ) nil )))))))))))))))))))))))"2" (skosimp*)"2" (expand "conflict_3D?" )"2" (skosimp*)"2" (typepred "t!1" )"2" (name "newt" "seg_lh_bottom(flpl,to)(j!1) + t!1" )"2" (case "to<=newt AND newt<=to+T" )"1" (flatten)"1" (inst + "newt" )"1" case "(so + (seg_lh_bottom(flpl,to)(j!1) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to)(j!1) - to) * vo) - AND t))") "1" (flatten) (("1" (assert ) nil )))"2" (hide 2)"2" (hide-all-but (-1 1))"2" "slb1" "seg_lh_bottom(flpl,to)(j!1)" )"2" "lsp" "lh_start_position(flpl,to)(j!1)" )"2" "sltop" "seg_lh_top(flpl,to)(j!1)" )"2" "loc1" "location_at(flpl)(newt)" )"2" "velc" "velocity(flpl)(j!1)" )"2" replace -1)"2" "2" replace -1)"2" "2" "2" replace -1)"2" "2" replace -1)"2" "2" nil )))))))))))))))))))))))))))))))))))"2" (hide 2)"2" (hide -7)"2" (hide -7)"2" case "t!1 < seg_lh_top(flpl,to)(j!1) - seg_lh_bottom(flpl,to)(j!1)" )"1" case "segment(flpl)(newt) = j!1" )"1" expand "location_at" )"1" replace -1)"1" "1" assert )"1" "1" nil )))))))))))"2" "2" "pj" "segment(flpl)(newt)" )"2" replace -1)"2" case "newt >= flpl(j!1)`time AND newt < flpl(j!1+1)`time" )"1" "1" "1" expand "segment" -1)"1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace -3)"1" expand "extend" )"1" assert )"1" case "pj < 1+j!1" )"1" "j!1" )"1" "1" assert )nil )))))"2" "flight_plan_ascending_time" )"2" "flpl" "pj" "1+j!1" )"2" assert )nil )))))))))))))))))))))"2" case "seg_lh_top(flpl,to)(j!1) <= flpl(j!1+1)`time AND seg_lh_bottom(flpl,to)(j!1) >= flpl(j!1)`time" )"1" "1" (assert ) nil )))"2" "2" expand "seg_lh_top" 1)"2" expand "seg_lh_bottom" "2" expand "min" )"2" expand "max" )"2" "2" "2" assert )nil )))))))))))))))))))))))))))"2" case "newt = seg_lh_top(flpl,to)(j!1)" )"1" case "to+T < flpl(j!1+1)`time" )"1" case "segment(flpl)(newt) = j!1" )"1" expand "location_at" )"1" replace -1)"1" "1" assert )"1" case "seg_lh_top(flpl,to)(j!1) = to+T" )"1" replace -1)"1" "1" "1" nil )))))))"2" expand "seg_lh_top" "2" expand "min" )"2" nil )))))))))))))))"2" "2" "pj" "segment(flpl)(newt)" )"2" replace -1)"2" case "newt >= flpl(j!1)`time AND newt < flpl(j!1+1)`time" )"1" "1" "1" expand "segment" "1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace -3)"1" expand "extend" )"1" assert )"1" case "pj < 1+j!1" )"1" "j!1" )"1" "1" assert )nil )))))"2" "flight_plan_ascending_time" )"2" "flpl" "pj" "1+j!1" )"2" assert )nil )))))))))))))))))))))"2" "2" "2" nil )))))))))))))))"2" case "newt = flpl(j!1+1)`time" )"1" "location_at_check" )"1" "flpl" "j!1+1" )"1" replace -2 :dir rl)"1" replace -1)"1" replace -2)"1" "1" expand "lh_start_position" )"1" "velocity_def" )"1" "flpl" "j!1" )"1" "vel11" "velocity(flpl)(j!1)" )"1" replace "1" "1" nil )))))))))))))))))))))))))"2" "2" expand "seg_lh_top" -1)"2" expand "min" )"2" "2" nil )))))))))))))"2" (assert ) nil )))))))))))"3" (hide 2)"3" case "seg_lh_bottom(flpl,to)(j!1) >= start_time(flpl) AND seg_lh_top(flpl,to)(j!1) <= end_time(flpl)" )"1" (flatten) (("1" (assert ) nil )))"2" (hide 2)"2" expand "seg_lh_bottom" )"2" expand "start_time" )"2" expand "end_time" )"2" expand "seg_lh_top" )"2" "flight_plan_ascending_time" )"2" "flpl" "N-1" "1+j!1" )"2" "flpl" "j!1" "0" )"2" expand "max" )"2" expand "min" )"2" "2" "2" nil )))))))))))))))))))))))))))))))"2" (assert )"2" case "seg_lh_bottom(flpl,to)(j!1) >= start_time(flpl) AND seg_lh_top(flpl,to)(j!1) <= end_time(flpl)" )"1" (flatten) (("1" (assert ) nil )))"2" (hide 2)"2" (expand "seg_lh_bottom" )"2" expand "start_time" )"2" expand "end_time" )"2" expand "seg_lh_top" )"2" "flight_plan_ascending_time" )"2" "flpl" "N-1" "1+j!1" )"2" "flpl" "j!1" "0" )"2" expand "max" )"2" expand "min" )"2" "2" "2" nil )))))))))))))))))))))))))))))))))"2" case "seg_lh_bottom(flpl,to)(j!1) >= to AND seg_lh_top(flpl,to)(j!1) <= to+T" )"1" (flatten) (("1" (assert ) nil )))"2" (hide 3)"2" (hide-all-but 1)"2" (grind) nil ))))))))))))))))))))))nil )nil nil )nil 3473074365"" (skeep)"" (ground)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (typepred "tt!1" )"1" (expand "end_time" )"1" (expand "start_time" )"1" case "EXISTS (kk: below[N]): tt!1 = flpl(kk)`time" )"1" (skosimp*)"1" (lemma "nontrivial_lookahead" )"1" (inst - "T" "kk!1" "to" "flpl" )"1" (assert )"1" (split -1)"1" (flatten)"1" "kk!1" )"1" assert )"1" "0" )"1" assert )"1" "location_at_check" )"1" "flpl" "kk!1" )"1" replace -4 :dir rl)"1" replace -1)"1" case "seg_lh_bottom(flpl,to,T)(kk!1) = tt!1" )"1" replace -1)"1" case "flpl(kk!1)`position = lh_start_position(flpl,to,T)(kk!1)" )"1" rewrite "vz_distr_sub" )"1" rewrite "vz_distr_add" )"1" rewrite "vz_scal" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "lh_start_position" )"2" replace -1)"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "seg_lh_bottom" "2" expand "max" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "kk!1-1" )"1" assert )"1" "seg_lh_top(flpl,to,T)(kk!1 - 1) - ") "1" "location_at_check" )"1" "flpl" "kk!1" )"1" replace -4 :dir rl)"1" replace -1)"1" "1" case "(so + (seg_lh_bottom(flpl,to,T)(kk!1 - 1) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to,T)(kk!1 - 1) - to) * vo) - AND vect2((so + (seg_lh_bottom(flpl,to,T)(kk!1 - 1) - to) * vo) -") "1" "1" assert )nil nil ))nil )"2" "2" "lsp" "lh_start_position(flpl,to,T)(kk!1 - 1)" )"2" replace -1)"2" "slb" "seg_lh_bottom(flpl,to,T)(kk!1 - 1)" )"2" replace "2" "slt" "seg_lh_top(flpl,to,T)(kk!1 - 1)" )"2" replace "2" "velc" "velocity(flpl)(kk!1-1)" )"2" replace "2" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "velocity_def" )"2" "flpl" "kk!1-1" )"2" assert )"2" case "flpl(kk!1-1)`time >= to" )"1" case "seg_lh_bottom(flpl,to,T)(kk!1-1) = flpl(kk!1-1)`time" )"1" replace "1" case "flpl(kk!1)`time <= to+T" )"1" case "seg_lh_top(flpl,to,T)(kk!1-1) = flpl(kk!1)`time" )"1" replace "1" expand "lh_start_position" )"1" replace "1" assert )"1" replace "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" expand "seg_lh_bottom" )"2" expand "max" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT seg_lh_bottom(flpl,to,T)(kk!1-1) = to" )"1" expand "seg_lh_bottom" "1" expand "max" )"1" "1" nil nil ))nil ))nil ))nil )"2" expand "lh_start_position" )"2" replace "2" assert )"2" expand "seg_lh_top" )"2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name "jj" "segment(flpl)(tt!1)" )"2" (label "jjname" -1)"2" (name "jjname" -1)"2" (inst 2 "jj" )"1" (lemma "segment_def" )"1" (inst - "flpl" "tt!1" )"1" "1" case "jj < N-1" )"1" assert )"1" case "flpl(jj)`time < tt!1" )"1" case "seg_lh_bottom(flpl,to,T)(jj) < seg_lh_top(flpl,to,T)(jj)" )"1" assert )"1" "newt" "tt!1-seg_lh_bottom(flpl,to,T)(jj)" )"1" "newt" )"1" case "(so + (seg_lh_bottom(flpl,to,T)(jj) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to,T)(jj) - to) * vo) - AND 1))") "1" "1" assert )nil nil ))nil )"2" "2" "slb1" "seg_lh_bottom(flpl,to,T)(jj)" )"2" "lsp" "lh_start_position(flpl,to,T)(jj)" )"2" "lal" "location_at(flpl)(tt!1)" )"2" "v1" "velocity(flpl)(jj)" )"2" replace "2" "2" replace "2" "2" replace "2" "2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "location_at" )"2" replace "jjname" )"2" "jjname" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "seg_lh_bottom(flpl,to,T)(jj) <= tt!1 AND tt!1 <= seg_lh_top(flpl,to,T)(jj)" )"1" "1" assert )nil nil ))nil )"2" "2" expand "seg_lh_bottom" "2" expand "seg_lh_top" "2" expand "max" )"2" expand "min" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "seg_lh_bottom" )"2" expand "seg_lh_top" )"2" expand "max" )"2" expand "min" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jj" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" case "jj = N-1" )"1" replace -1)"1" "1" "1" "N-1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "N-1" )"1" (expand "segment" )"1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace "jjname" )"1" expand "extend" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "conflict_3D?" )"2" (skosimp*)"2" (typepred "t!1" )"2" (name "newt" "seg_lh_bottom(flpl,to,T)(j!1) + t!1" )"2" (case "to<=newt AND newt<=to+T" )"1" (flatten)"1" (inst + "newt" )"1" case "(so + (seg_lh_bottom(flpl,to,T)(j!1) - to) * vo) - ") "1" case "((so + (seg_lh_bottom(flpl,to,T)(j!1) - to) * vo) - AND t))") "1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" (hide-all-but (-1 1))"2" "slb1" "seg_lh_bottom(flpl,to,T)(j!1)" )"2" "lsp" "lh_start_position(flpl,to,T)(j!1)" )"2" "sltop" "seg_lh_top(flpl,to,T)(j!1)" )"2" "loc1" "location_at(flpl)(newt)" )"2" "velc" "velocity(flpl)(j!1)" )"2" replace -1)"2" "2" replace -1)"2" "2" "2" replace -1)"2" "2" replace -1)"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -7)"2" (hide -7)"2" case "t!1 < seg_lh_top(flpl,to,T)(j!1) - seg_lh_bottom(flpl,to,T)(j!1)" )"1" case "segment(flpl)(newt) = j!1" )"1" expand "location_at" )"1" replace -1)"1" "1" assert )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "pj" "segment(flpl)(newt)" )"2" replace -1)"2" case "newt >= flpl(j!1)`time AND newt < flpl(j!1+1)`time" )"1" "1" "1" expand "segment" -1)"1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace -3)"1" expand "extend" )"1" assert )"1" case "pj < 1+j!1" )"1" "j!1" )"1" "1" assert )nil nil ))nil ))nil )"2" "flight_plan_ascending_time" )"2" "flpl" "pj" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "seg_lh_top(flpl,to,T)(j!1) <= flpl(j!1+1)`time AND seg_lh_bottom(flpl,to,T)(j!1) >= flpl(j!1)`time" )"1" "1" (assert ) nil nil ))nil )"2" "2" expand "seg_lh_top" 1)"2" expand "seg_lh_bottom" "2" expand "min" )"2" expand "max" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "newt = seg_lh_top(flpl,to,T)(j!1)" )"1" case "to+T < flpl(j!1+1)`time" )"1" case "segment(flpl)(newt) = j!1" )"1" expand "location_at" )"1" replace -1)"1" "1" assert )"1" case "seg_lh_top(flpl,to,T)(j!1) = to+T" )"1" replace -1)"1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand "seg_lh_top" "2" expand "min" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "pj" "segment(flpl)(newt)" )"2" replace -1)"2" case "newt >= flpl(j!1)`time AND newt < flpl(j!1+1)`time" )"1" "1" "1" expand "segment" "1" "max(extend[nat, below[N], bool, FALSE] ") "1" replace -3)"1" expand "extend" )"1" assert )"1" case "pj < 1+j!1" )"1" "j!1" )"1" "1" assert )nil nil ))nil ))nil )"2" "flight_plan_ascending_time" )"2" "flpl" "pj" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "newt = flpl(j!1+1)`time" )"1" "location_at_check" )"1" "flpl" "j!1+1" )"1" replace -2 :dir rl)"1" replace -1)"1" replace -2)"1" "1" expand "lh_start_position" )"1" "velocity_def" )"1" "flpl" "j!1" )"1" "vel11" "velocity(flpl)(j!1)" )"1" replace "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "seg_lh_top" -1)"2" expand "min" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" case "seg_lh_bottom(flpl,to,T)(j!1) >= start_time(flpl) AND seg_lh_top(flpl,to,T)(j!1) <= end_time(flpl)" )"1" (flatten) (("1" (assert ) nil nil ))nil )"2" (hide 2)"2" expand "seg_lh_bottom" )"2" expand "start_time" )"2" expand "end_time" )"2" expand "seg_lh_top" )"2" "flight_plan_ascending_time" )"2" "flpl" "N-1" "1+j!1" )"2" "flpl" "j!1" "0" )"2" expand "max" )"2" expand "min" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" case "seg_lh_bottom(flpl,to,T)(j!1) >= start_time(flpl) AND seg_lh_top(flpl,to,T)(j!1) <= end_time(flpl)" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" (expand "seg_lh_bottom" )"2" expand "start_time" )"2" expand "end_time" )"2" expand "seg_lh_top" )"2" "flight_plan_ascending_time" )"2" "flpl" "N-1" "1+j!1" )"2" "flpl" "j!1" "0" )"2" expand "max" )"2" expand "min" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "seg_lh_bottom(flpl,to,T)(j!1) >= to AND seg_lh_top(flpl,to,T)(j!1) <= to+T" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide 3)"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )nil finite_sets nil )nil finite_sets nil )"bool" finite_sets nil )nil vectors_3D_def "vectors/" )"bool" cd3d nil ))nil )nil 3473074224 ("" (postpone) nil nil ) nil nil 3483460389"" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_si nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )"bool" reals nil )"real" flightplan nil )"real" flightplan nil )nil flightplan nil )nil cd3d_si nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3483369488"" (skeep)"" (split)"1" (flatten)"1" (lemma "conflict_3D_rew" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (name "lhb" "seg_lh_bottom(flpl, to)(j!1)" )"1" (replace -1)"1" (name "lht" "seg_lh_top(flpl, to)(j!1)" )"1" (replace -1)"1" "conflict_3D_on_open_interval[D, H, seg_lh_bottom(flpl, to)(j!1), seg_lh_top(flpl, to)(j!1)]" )"1" (inst?)"1" (assert )"1" replace -2)"1" replace -3)"1" "1" "ttp" "topen!1 + flpl(j!1)`time" )"1" case "NOT (start_time[N](flpl) <= flpl(j!1)`time + topen!1 AND ") "1" "1" case "topen!1 > 0" )"1" expand "start_time" )"1" "flight_plan_ascending_time" )"1" "flpl" "j!1" "0" )"1" assert )"1" case "j!1 /= 0" )"1" assert )"1" expand "end_time" )"1" case "flpl(j!1)`time + topen!1 < flpl(j!1+1)`time" )"1" "flight_plan_ascending_time" )"1" "flpl" "N-1" "j!1+1" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "lht" "2" expand "seg_lh_top" "2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "end_time" )"2" case "flpl(j!1)`time + topen!1 < flpl(j!1+1)`time" )"1" case "j!1+1 = N-1" )"1" assert )nil nil )"2" "flight_plan_ascending_time" )"2" "flpl" "N-1" "j!1+1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "lht" "2" expand "seg_lh_top" "2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "lhb" -2)"2" expand "seg_lh_bottom" "2" expand "max" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ttp" )"1" case "NOT B+to<ttp" )"1" "1" "1" replace "1" "1" expand "lht" "1" expand "lhb" "1" expand "seg_lh_bottom" "1" expand "max" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "NOT ttp < T+to" )"1" "1" "1" expand "lht" "1" expand "seg_lh_top" "1" expand "min" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "(so + (flpl(j!1)`time - to) * vo) - flpl(j!1)`position + ") "1" case "vect2((so + (flpl(j!1)`time - to) * vo) - flpl(j!1)`position) + tp)) AND ((so + (flpl(j!1)`time - to) * vo) - flpl(j!1)`position)`z +z") "1" "1" assert )"1" "1" expand "end_time" )"1" expand "start_time" )"1" assert )"1" case "flpl(j!1)`time + lht <= flpl(j!1+1)`time" )"1" "1" "N-1" "j!1+1" )"1" assert )nil nil ))nil ))nil )"2" expand "seg_lh_top" )"2" expand "seg_lh_bottom" )"2" expand "min" )"2" expand "max" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" "2" "flpl" "position" "velocity" "location_at" "ttp" ))nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" expand "location_at" )"2" case "segment(flpl)(flpl(j!1)`time + topen!1) = j!1" )"1" replace "1" case "j!1 < N-1" )"1" assert )"1" "1" "velocity" )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" "segment_index" )"2" "flpl" "j!1" "flpl(j!1)`time + topen!1" )"2" assert )"2" "2" expand "lht" "2" expand "seg_lh_top" "2" expand "min" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -3 + :dir rl)"2" expand "lhb" -4)"2" expand "lht" -5)"2" expand "seg_lh_bottom" "2" expand "seg_lh_top" "2" expand "max" )"2" expand "min" )"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" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "conflict_3D?" )"2" (inst + "tt!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil cd3d_si nil )"[T, T -> boolean]" equalities nil )"nnreal" cd3d_si nil )"real" cd3d_si nil )nil cd3d nil )"posreal" cd3d_si nil )"posreal" cd3d_si nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil Lookahead nil )"Vect3" flightplan nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"below[N]" flightplan nil )nil flightplan nil )nil flightplan nil )nil cd3d_si nil )"real" cd3d_si nil )"FlightPlanRelevant(to)" cd3d_si nil )"real" cd3d_si nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"nnreal" cd3d_si nil )"boolean" notequal nil )"posint" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" cd3d_si nil )"int" integers nil )"posint" nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )"(total_order?[real])" nil )nil flightplan nil )"real" flightplan nil )"real" flightplan nil )NOT const-decl "[bool -> bool]" booleans nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vect3" flightplan nil )nil cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )"nnreal" cd3d_si nil )nil real_types nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_3D_def "vectors/" )nil reals nil )"bool" cd3d_si nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3481469113"" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_si nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" nil )"real" reals nil )"nnreal" cd3d_si nil )"real" cd3d_si nil ))nil ))nil 3481469113"" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_si nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" nil )"real" reals nil )"nnreal" cd3d_si nil )"real" cd3d_si nil ))nil ))nil 3481469114"" (skeep)"" (lemma "conflict_3D_rew" )"" (inst?)"" (replace -1)"" (hide -1)"" (ground)"1" (skeep -1)"1" (inst?)"1" (assert )"1" (expand conflict_3D?)"1" (skeep -2)"1" (inst + "t+flpl(j)`time-to" )"1" (assert )"1" case "NOT vect2(so - - flpl(j)`position) +") "1" "1" "velocity" ))nil nil ))nil )"2" assert )"2" case "NOT (so - ") "1" "1" "velocity" ))nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (typepred t)"2" assert )"2" expand "seg_lh_bottom" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep -1)"2" (inst?)"2" (assert )"2" (expand "conflict_3D?" )"2" (skeep -2)"2" (inst + "t+to-flpl(j)`time" )"2" (assert )"2" (hide -1)"2" "velocity" "abs" "sqv" "sq" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cd3d_si nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )"bool" cd3d nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" cd3d_si nil )"FlightPlanRelevant(to)" cd3d_si nil )"below[N - 1]" cd3d_si nil )"bool" reals nil )"nnreal" cd3d_si nil )"real" cd3d_si nil )nil Lookahead nil )"Lookahead[seg_lh_bottom(flpl, to)(j), seg_lh_top(flpl, to)(j)]" nil )NOT const-decl "[bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vect3" flightplan nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )"(strict_total_order?[real])" real_props nil )nil cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )"nnreal" cd3d_si nil )nil real_types nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_3D_def "vectors/" )nil reals nil ))nil 3472981403 ("" (subtype-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nnreal" cd3d_si nil )"real" cd3d_si nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals nil )nil booleans 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 )"Vect3" flightplan nil )"real" reals nil )"real" reals nil )"nzreal" nil )"real" reals nil )"nzreal" real_typesnil ))nil ))nil 3472981403 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3473095354"" (skeep)"" (induct "i" )"1" (flatten)"1" (inst + "0" )"1" (assert )"1" (expand "cd3d_ind?" )"1" (flatten)"1" (assert ) (("1" (rewrite "cd3d" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (expand "cd3d_ind?" -3)"2" (split -3)"1" (flatten)"1" (inst + "1+jb" )"1" (assert ) (("1" (rewrite "cd3d" ) nil nil )) nil ))nil ))nil )"2" (assert )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep) (("3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (assert ) nil nil ) ("5" (assert ) nil nil ))nil ))nil )"real" reals nil )"bool" reals nil )"real" cd3d_si nil )"nnreal" cd3d_si nil )"FlightPlanRelevant(to)" cd3d_si nil )"real" cd3d_si nil )"Vect3" cd3d_si nil )"Vect3" cd3d_si nil )"bool" cd3d_si nil )nil cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )"nnreal" cd3d_si nil )nil real_types nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil flightplan nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )nil defined_types nil )"posreal" cd3d_si nil )"posreal" cd3d_si nil )"bool" cd3d nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vect3" flightplan nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals nil )nil booleans 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 )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bounded_nat_inductions nil )"int" integers nil )"(total_order?[real])" nil )"bool" reals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil cd3d nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil ))nil 3473096278"" (skeep)"" (induct "i" )"1" (ground)"1" (skolem -2 "jjj" )"1" (ground)"1" (expand "cd3d_ind?" )"1" (rewrite "cd3d" :dir rl)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (inst + "t!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skosimp*)"2" (expand "cd3d_ind?" 1)"2" (flatten)"2" (assert )"2" (inst + "j!1" )"2" (assert )"2" (case "j!1 = 1+jb" )"1" (replace -1)"1" (rewrite "cd3d" :dir rl)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" "t!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (assert ) nil nil ) ("5" (assert ) nil nil ))nil ))nil )"real" reals nil )"bool" reals nil )"real" cd3d_si nil )"FlightPlanRelevant(to)" cd3d_si nil )nil cd3d_si nil )"real" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )"nnreal" cd3d_si nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" cd3d_si nil )nil real_types nil )nil flightplan nil )nil vectors_3D_def "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )nil defined_types nil )"posreal" cd3d_si nil )"posreal" cd3d_si nil )"bool" cd3d nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vect3" flightplan nil )"bool" cd3d_si nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals nil )nil booleans 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 )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bounded_nat_inductions nil )"int" integers nil )"(total_order?[real])" nil )"bool" reals nil )"posint" nil )"real" reals nil )"real" reals nil )nil Lookahead nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )nil cd3d nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"posint" nil ))nil 3473096044"" (skeep)"" (expand "cd3d_si?" )"" (lemma "cd3d_ind_correct" )"" (inst - "so" "vo" "to" "flpl" "N-2" )"1" (assert )"1" (lemma "conflict_3D_rew" )"1" (inst - "so" "vo" "to" "flpl" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"bool" cd3d_si nil )"(total_order?[real])" nil )"int" integers nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals 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 )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 vectors_3D_def "vectors/" )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )nil cd3d_si nil )nil cd3d_si nil ))nil 3473097139"" (skeep)"" (expand "cd3d_si?" )"" (lemma "cd3d_ind_complete" )"" (inst - "so" "vo" "to" "flpl" "N-2" )"1" (assert )"1" (lemma "conflict_3D_rew" )"1" (inst - "so" "vo" "to" "flpl" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"int" integers nil )"bool" cd3d_si nil )"(total_order?[real])" nil )"above[1]" cd3d_si nil )nil int_types nil )"bool" reals 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 )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 vectors_3D_def "vectors/" )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_types nil )"nnreal" cd3d_si nil )"{AB: posreal | AB > B}" cd3d_si nil )nil cd3d_si nil )nil cd3d_si nil )nil cd3d_si 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.399Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
