|
(criteria_flightplan
(hconflictever_rew 0
(hconflictever_rew-1 nil 3511624351
("" (case "FORALL (vvv:Vect2): sq(norm(vvv)) = sqv(vvv)")
(("1" (skeep)
(("1" (expand "horizontal_conflict_ever_traj?")
(("1" (ground)
(("1" (skosimp*)
(("1" (inst + "t!1")
(("1" (rewrite "sq_lt" :dir rl)
(("1" (rewrite -2) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst + "t!1")
(("2" (rewrite "sq_lt" + :dir rl)
(("2" (rewrite -2) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skeep)
(("2" (rewrite "sqrt_eq" :dir rl)
(("2" (assert) (("2" (rewrite "sqrt_sqv_norm") nil nil))
nil))
nil))
nil))
nil))
nil)
((sqrt_eq formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
(sqrt_sq formula-decl nil sqrt "reals/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(B formal-const-decl "nnreal" criteria_flightplan nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(T formal-const-decl "{AB: posreal | AB > B}" criteria_flightplan
nil)
(Lookahead type-eq-decl nil Lookahead nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_lt formula-decl nil sq "reals/")
(Trajectory type-eq-decl nil criteria_flightplan nil)
(D formal-const-decl "posreal" criteria_flightplan nil)
(horizontal_conflict_ever_traj? const-decl "bool"
criteria_flightplan nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/"))
shostak))
(repulisve_criterion_independent 0
(repulisve_criterion_independent-1 nil 3511709952
("" (skeep)
(("" (lemma "dot_nneg_divergent")
(("" (expand "repulsive?")
(("" (expand "repulsive_criterion?")
(("" (ground)
(("1" (skeep)
(("1" (case "(newrtraj(t) - rtraj(t)) /= zero")
(("1" (inst - "t")
(("1" (flatten)
(("1" (assert)
(("1" (skeep 3)
(("1"
(inst - "newrtraj(t) - rtraj(t)" "rtraj(t)")
(("1" (assert)
(("1" (expand "divergent?")
(("1"
(inst - "p")
(("1"
(expand "dist")
(("1"
(rewrite "sq_dist_norm")
(("1"
(rewrite "sq_dist_norm")
(("1"
(assert)
(("1"
(assert)
(("1"
(hide-all-but (-2 3))
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "p = 0")
(("1"
(replace -1)
(("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (flatten)
(("2" (inst - "t")
(("2" (flatten)
(("2" (assert)
(("2" (case "newrtraj(t) = rtraj(t)")
(("1" (replace -1)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(hide-all-but 2)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2"
(expand "zero")
(("2"
(decompose-equality -)
(("2"
(rewrite "vx_distr_sub")
(("2"
(rewrite "vy_distr_sub")
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (inst - "t")
(("2" (flatten)
(("2" (assert)
(("2" (case "(newrtraj(t) - rtraj(t)) /= zero")
(("1" (flatten)
(("1"
(case "EXISTS (p:posreal): norm(p * newrtraj(t) + (1 - p) * rtraj(t)) = norm(rtraj(t))")
(("1"
(case "(FORALL (p: nnreal):
sqv(p * newrtraj(t) + (1 - p) * rtraj(t)) >= sqv(rtraj(t))) AND (EXISTS (p: posreal):
sqv(p * newrtraj(t) + (1 - p) * rtraj(t)) = sqv(rtraj(t)))")
(("1" (hide (-2 -3))
(("1"
(flatten)
(("1"
(skolem -2 "pp")
(("1"
(name
"ff"
"quadratic(sqv(newrtraj(t) - rtraj(t)),2*(rtraj(t) * (newrtraj(t) - rtraj(t))),0)")
(("1"
(case
"NOT (FORALL (qq:real): ff(qq) = sqv(qq * newrtraj(t) + (1 - qq) * rtraj(t)) - sqv(rtraj(t)))")
(("1"
(skeep)
(("1"
(replace -1 :dir rl)
(("1"
(hide-all-but 1)
(("1" (grind) nil nil))
nil))
nil))
nil)
("2"
(lemma "quad_min_eq_intv")
(("2"
(inst?)
(("1"
(inst - "pp/2" "0" "pp")
(("1"
(assert)
(("1"
(case
"ff(0) = 0 AND ff(pp) = 0")
(("1"
(split -2)
(("1"
(flatten)
(("1"
(inst-cp
-
"pp/2")
(("1"
(replace -6)
(("1"
(inst
-7
"pp/2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(flatten)
(("3"
(assert)
nil
nil))
nil))
nil)
("2"
(hide -1)
(("2"
(inst-cp - "0")
(("2"
(inst - "pp")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "sqv_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 -2 1))
(("2"
(split +)
(("1"
(hide -1)
(("1"
(skosimp*)
(("1"
(inst - "p!1")
(("1"
(rewrite "sqrt_ge" :dir rl)
(("1"
(rewrite "sqrt_sqv_norm")
(("1"
(rewrite "sqrt_sqv_norm")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -2)
(("2"
(skosimp*)
(("2"
(inst + "p!1")
(("2"
(rewrite "sqrt_eq" :dir rl)
(("2"
(rewrite "sqrt_sqv_norm")
(("2"
(rewrite "sqrt_sqv_norm")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst -2 "newrtraj(t) - rtraj(t)"
"rtraj(t)")
(("1" (assert)
(("1"
(expand "divergent?")
(("1"
(skolem 5 "pp")
(("1"
(inst - "pp")
(("1"
(inst + "pp")
(("1"
(expand "dist")
(("1"
(rewrite "sq_dist_norm")
(("1"
(rewrite "sq_dist_norm")
(("1"
(assert)
(("1"
(assert)
(("1"
(hide-all-but
(-1 1 5))
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dot_nneg_divergent formula-decl nil definitions nil)
(repulsive_criterion? const-decl "bool" criteria_flightplan nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
(sqrt_ge formula-decl nil sqrt "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(sq const-decl "nonneg_real" sq "reals/")
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(sqv_eq_0 formula-decl nil vectors_2D "vectors/")
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(quad_min_eq_intv formula-decl nil quad_minmax "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(quadratic const-decl "real" quadratic "reals/")
(vy_distr_sub formula-decl nil vectors_2D "vectors/")
(vx_distr_sub formula-decl nil vectors_2D "vectors/")
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(sub_eq_args formula-decl nil vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(divergent? const-decl "bool" closest_approach_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(scal_0 formula-decl nil vectors_2D "vectors/")
(scal_1 formula-decl nil vectors_2D "vectors/")
(odd_minus_even_is_odd application-judgement "odd_int" integers
nil)
(dist const-decl "nnreal" distance_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(scal_zero formula-decl nil vectors_2D "vectors/")
(add_zero_left formula-decl nil vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sqrt_sq formula-decl nil sqrt "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sub_zero_right formula-decl nil vectors_2D "vectors/")
(sq_dist_norm formula-decl nil distance_2D "vectors/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(B formal-const-decl "nnreal" criteria_flightplan nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(T formal-const-decl "{AB: posreal | AB > B}" criteria_flightplan
nil)
(Lookahead type-eq-decl nil Lookahead nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Trajectory type-eq-decl nil criteria_flightplan nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(repulsive? const-decl "bool" criteria_flightplan nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(repulsive_criterion_coordinated 0
(repulsive_criterion_coordinated-1 nil 3511709628
("" (skeep)
(("" (expand "repulsive_criterion?")
(("" (skosimp*)
(("" (inst - "t!1")
(("" (inst - "t!1") (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((repulsive_criterion? const-decl "bool" criteria_flightplan nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(B formal-const-decl "nnreal" criteria_flightplan nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(T formal-const-decl "{AB: posreal | AB > B}" criteria_flightplan
nil)
(Lookahead type-eq-decl nil Lookahead nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D "vectors/")
(rel_traj const-decl "Vect2" criteria_flightplan nil))
nil))
(horizontal_criterion_repulsive 0
(horizontal_criterion_repulsive-1 nil 3511692238
("" (skeep)
(("" (expand "repulsive_criterion?")
(("" (expand "horizontal_criterion?")
(("" (skosimp*)
(("" (inst - "t!1") (("" (grind :exclude "norm") nil nil))
nil))
nil))
nil))
nil))
nil)
((repulsive_criterion? const-decl "bool" criteria_flightplan nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(Lookahead type-eq-decl nil Lookahead nil)
(T formal-const-decl "{AB: posreal | AB > B}" criteria_flightplan
nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" criteria_flightplan nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(horizontal_criterion? const-decl "bool" criteria_flightplan nil))
shostak))
(horizontal_criterion_independent 0
(horizontal_criterion_independent-2 nil 3511710317
("" (skeep)
(("" (expand "horizontal_conflict_ever_traj?")
(("" (skeep -2)
(("" (expand "horizontal_criterion?")
(("" (inst - "t")
(("" (flatten)
(("" (lemma "max_le")
(("" (inst?)
(("" (inst - "rtraj(t) * newrtraj(t)")
(("" (ground)
(("" (hide (-1 -2))
(("" (hide -2)
(("" (lemma "cauchy_schwarz")
(("" (inst - "rtraj(t)" "newrtraj(t)")
((""
(case
"rtraj(t) * newrtraj(t) <= norm(rtraj(t)) * norm(newrtraj(t))")
(("1"
(case "norm(rtraj(t))>0")
(("1"
(mult-by -5 "norm(rtraj(t))")
(("1" (assert) nil nil))
nil)
("2"
(lemma "norm_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(rewrite "sq_le" :dir rl)
(("2"
(rewrite "sq_times")
(("2"
(case
"FORALL (vv:Vect2): sq(norm(vv)) = sqv(vv)")
(("1"
(inst-cp -1 "rtraj(t)")
(("1"
(inst - "newrtraj(t)")
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2"
(rewrite "sqrt_eq" :dir rl)
(("2"
(rewrite "sqrt_sqv_norm")
(("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)
((horizontal_conflict_ever_traj? const-decl "bool"
criteria_flightplan nil)
(horizontal_criterion? const-decl "bool" criteria_flightplan nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Trajectory type-eq-decl nil criteria_flightplan nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(D formal-const-decl "posreal" criteria_flightplan nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq_le formula-decl nil sq "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_eq formula-decl nil sqrt "reals/")
(sq_times formula-decl nil sq "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(cauchy_schwarz formula-decl nil vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(max_le formula-decl nil real_defs nil)
(Lookahead type-eq-decl nil Lookahead nil)
(T formal-const-decl "{AB: posreal | AB > B}" criteria_flightplan
nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" criteria_flightplan nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil)
(horizontal_criterion_independent-1 nil 3511710046
("" (skeep)
(("" (expand "repulsive_criterion?")
(("" (expand "horizontal_criterion?")
(("" (skosimp*)
(("" (inst - "t!1")
(("" (grind :exclude "norm") nil))))))))))
nil)
nil nil))
(horizontal_criterion_coordinated 0
(horizontal_criterion_coordinated-1 nil 3511690762
("" (skeep)
((""
(case "repulsive_criterion?(rel_traj(so, si))(rel_traj(newso, si)) AND
repulsive_criterion?(rel_traj(si, so))(rel_traj(newsi, so))")
(("1" (flatten)
(("1" (expand "horizontal_criterion?")
(("1" (skeep)
(("1" (inst - "t")
(("1" (inst - "t")
(("1" (flatten)
(("1" (assert)
(("1" (lemma "max_le")
(("1" (inst?)
(("1"
(inst -
"rel_traj(so, si)(t) * rel_traj(newso, newsi)(t)")
(("1" (assert)
(("1" (hide 4)
(("1"
(lemma
"repulsive_criterion_coordinated")
(("1"
(inst - "newsi" "newso" "si" "so")
(("1"
(assert)
(("1"
(hide (-2 -3))
(("1"
(expand "repulsive_criterion?")
(("1"
(inst - "t")
(("1"
(split +)
(("1"
(flatten)
(("1"
(hide-all-but (-1 1))
(("1" (grind) nil nil))
nil))
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(case
"NOT rel_traj(so, si)(t) * rel_traj(so,newsi)(t) >=
max(sqv(rel_traj(so, si)(t)), norm(rel_traj(so, si)(t)) * D)")
(("1"
(hide-all-but
(-3 1))
(("1"
(case
"norm(rel_traj(so, si)(t)) = norm(rel_traj(si,so)(t))")
(("1"
(case
"sqv(rel_traj(so, si)(t)) = sqv(rel_traj(si,so)(t))")
(("1"
(replace
-1
:dir
rl)
(("1"
(replace
-2
:dir
rl)
(("1"
(hide
(-1 -2))
(("1"
(grind
:exclude
("max"
"norm"))
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(rewrite
"sqv_neg"
:dir
rl)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(rewrite
"norm_neg"
:dir
rl)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide -4)
(("2"
(hide -2)
(("2"
(case
"rel_traj(newso, newsi)(t) = rel_traj(newso, si)(t) + rel_traj(so, newsi)(t) - rel_traj(so, si)(t)")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(grind
:exclude
("norm"
"rel_traj"))
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "repulsive_criterion?")
(("2" (expand "horizontal_criterion?")
(("2" (split +)
(("1" (skosimp*)
(("1" (inst -1 "t!1")
(("1" (hide -2)
(("1" (grind :exclude "norm") nil nil)) nil))
nil))
nil)
("2" (hide -1)
(("2" (skosimp*)
(("2" (inst - "t!1")
(("2" (grind :exclude "norm") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rel_traj const-decl "Vect2" criteria_flightplan nil)
(repulsive_criterion? const-decl "bool" criteria_flightplan nil)
(Trajectory type-eq-decl nil criteria_flightplan nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Lookahead type-eq-decl nil Lookahead nil)
(T formal-const-decl "{AB: posreal | AB > B}" criteria_flightplan
nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" criteria_flightplan nil)
(<= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(horizontal_criterion? const-decl "bool" criteria_flightplan nil)
(max_le formula-decl nil real_defs nil)
(* const-decl "real" vectors_2D "vectors/")
(NOT const-decl "[bool -> bool]" booleans nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sqv_neg formula-decl nil vectors_2D "vectors/")
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(norm_neg formula-decl nil vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(repulsive_criterion_coordinated formula-decl nil
criteria_flightplan nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(D formal-const-decl "posreal" criteria_flightplan nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(horizontal_flightplan_criterion 0
(horizontal_flightplan_criterion-1 nil 3511710740
("" (skeep)
(("" (expand "horizontal_criterion?")
(("" (expand "flightplan_criterion?")
(("" (skeep)
(("" (inst - "t")
(("" (flatten)
(("" (assert)
(("" (expand "safe_vect?")
(("" (case "norm(rtraj(t)) >= D")
(("1"
(case "sqv(rtraj(t)) >= norm(rtraj(t)) * (norm(rtraj(t)) / 2) +
norm(rtraj(t)) * (D / 2)")
(("1" (expand "max")
(("1" (lift-if) (("1" (ground) nil nil)) nil))
nil)
("2" (hide (-2 3))
(("2"
(case "sqv(rtraj(t)) = sq(norm(rtraj(t)))")
(("1"
(case "sqv(rtraj(t)) >= norm(rtraj(t))*D")
(("1" (expand "sq")
(("1" (assert) nil nil)) nil)
("2" (hide 2)
(("2"
(replace -1)
(("2"
(expand "sq" +)
(("2"
(mult-by -2 "norm(rtraj(t))")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (rewrite "sqrt_eq" :dir rl)
(("2"
(lemma "sqrt_sqv_norm")
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "max" +)
(("2" (lift-if)
(("2" (ground)
(("2" (hide (-1 2))
(("2" (mult-by 2 "norm(rtraj(t))/2")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((horizontal_criterion? const-decl "bool" criteria_flightplan nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(safe_vect? const-decl "bool" criteria_flightplan nil)
(both_sides_times_pos_ge1 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq "reals/")
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
(D formal-const-decl "posreal" criteria_flightplan nil)
(Trajectory type-eq-decl nil criteria_flightplan nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Lookahead type-eq-decl nil Lookahead nil)
(T formal-const-decl "{AB: posreal | AB > B}" criteria_flightplan
nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" criteria_flightplan nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(flightplan_criterion? const-decl "bool" criteria_flightplan nil))
shostak))
(flightplan_criterion_independent 0
(flightplan_criterion_independent-1 nil 3511710387
("" (skeep)
(("" (expand "horizontal_conflict_ever_traj?")
(("" (skeep -2)
(("" (expand "flightplan_criterion?")
(("" (expand "safe_vect?")
(("" (inst - "t")
(("" (flatten)
(("" (lemma "max_le")
(("" (inst?)
(("" (inst - "rtraj(t) * newrtraj(t)")
(("" (ground)
(("" (hide (-1 -2))
(("" (hide -2)
(("" (lemma "cauchy_schwarz")
((""
(inst - "rtraj(t)" "newrtraj(t)")
((""
(case
"rtraj(t) * newrtraj(t) <= norm(rtraj(t)) * norm(newrtraj(t))")
(("1"
(case "norm(rtraj(t))>0")
(("1"
(mult-by -5 "norm(rtraj(t))")
(("1" (assert) nil nil))
nil)
("2"
(lemma "norm_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(rewrite "sq_le" :dir rl)
(("2"
(rewrite "sq_times")
(("2"
(case
"FORALL (vv:Vect2): sq(norm(vv)) = sqv(vv)")
(("1"
(inst-cp -1 "rtraj(t)")
(("1"
(inst - "newrtraj(t)")
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2"
(rewrite
"sqrt_eq"
:dir
rl)
(("2"
(rewrite
"sqrt_sqv_norm")
(("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)
((horizontal_conflict_ever_traj? const-decl "bool"
criteria_flightplan nil)
(flightplan_criterion? const-decl "bool" criteria_flightplan nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(B formal-const-decl "nnreal" criteria_flightplan nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(T formal-const-decl "{AB: posreal | AB > B}" criteria_flightplan
nil)
(Lookahead type-eq-decl nil Lookahead nil)
(max_le formula-decl nil real_defs nil)
(* const-decl "real" vectors_2D "vectors/")
(cauchy_schwarz formula-decl nil vectors_2D "vectors/")
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq_times formula-decl nil sq "reals/")
(sqrt_eq formula-decl nil sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(sq_le formula-decl nil sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(D formal-const-decl "posreal" criteria_flightplan nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(Trajectory type-eq-decl nil criteria_flightplan nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(safe_vect? const-decl "bool" criteria_flightplan nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil))
(flightplan_criterion_coordinated 0
(flightplan_criterion_coordinated-1 nil 3511694910
("" (skeep)
(("" (expand "flightplan_criterion?")
(("" (expand "horizontal_conflict_ever_traj?")
(("" (expand "safe_vect?")
(("" (skeep -3)
(("" (case "NOT norm(rel_traj(newso, newsi)(t)) >= D")
(("1" (hide -3)
(("1" (inst - "t")
(("1" (inst - "t")
(("1" (flatten)
(("1" (assert)
(("1"
(case "NOT rel_traj(so,si)(t) * rel_traj(so,newsi)(t) >=
max(norm(rel_traj(so,si)(t)) * (D / 2) +
norm(rel_traj(so,si)(t)) * (norm(rel_traj(so,si)(t)) / 2),
norm(rel_traj(so,si)(t)) * D)")
(("1" (hide-all-but (-2 1))
(("1" (grind) nil nil)) nil)
("2" (hide -3)
(("2" (name "v" "rel_traj(so,si)(t)")
(("2"
(replace -1)
(("2"
(name "w" "rel_traj(newso,si)(t)")
(("2"
(replace -1)
(("2"
(name
"u"
"rel_traj(so,newsi)(t)")
(("2"
(replace -1)
(("2"
(case
"NOT rel_traj(newso,newsi)(t) = u+w-v")
(("1"
(hide-all-but 1)
(("1"
(expand "u")
(("1"
(expand "w")
(("1"
(expand "v")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(hide (-1 -2 -3 -4))
(("2"
(case "norm(v)>=D")
(("1"
(name
"Kpos"
"norm(v)*D")
(("1"
(case "Kpos > 0")
(("1"
(case
"norm(v) * (D / 2) + norm(v) * (norm(v) / 2) = (Kpos + sqv(v))/2")
(("1"
(replace -1)
(("1"
(replace -3)
(("1"
(hide -1)
(("1"
(case
"NOT v*(u+w-v)>= norm(v)*D")
(("1"
(hide
2)
(("1"
(grind)
nil
nil))
nil)
("2"
(lemma
"cauchy_schwarz")
(("2"
(inst
-
"v"
"u+w-v")
(("2"
(lemma
"sqrt_le")
(("2"
(inst?)
(("2"
(assert)
(("2"
(rewrite
"sqrt_times")
(("2"
(rewrite
"sqrt_sqv_norm")
(("2"
(rewrite
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.74 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
