|
(horizontal_los
(sDs_TCC1 0
(sDs_TCC1-2 nil 3527334876
("" (skeep)
(("" (typepred "s")
(("" (case "norm(s)*D - sqv(s) > 0")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (rewrite "sq_norm" :dir rl)
(("2" (rewrite "sq_lt")
(("2" (expand "sq" 1)
(("2" (cancel-by 1 "norm(s)") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((LoS_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_los nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (< const-decl "bool" 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)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sq_lt formula-decl nil sq "reals/")
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(zero_div formula-decl nil extra_tegies nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq_norm formula-decl nil vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(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)
(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)
(norm const-decl "nnreal" vectors_2D "vectors/"))
nil)
(sDs_TCC1-1 nil 3527334792 ("" (subtype-tcc) nil nil) nil nil))
(gs_los_TCC1 0
(gs_los_TCC1-2 nil 3443981844
("" (skeep)
(("" (lemma "max_segment_point_in_slice_def")
(("" (inst?)
(("" (assert)
(("" (rewrite "intersects_segment_fun_def")
(("" (assert)
(("" (flatten)
(("" (expand "on_segment_in_wedge?")
(("" (replace -5 :dir rl)
(("" (skeep -1)
(("" (assert)
(("" (replace -3 2)
(("" (assert)
(("" (split +)
(("1"
(expand "gs_only?")
(("1"
(inst + "t/norm(vo)")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(split +)
(("1" (cross-mult 1) nil nil)
("2" (cross-mult 1) nil nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "norm_scal")
(("2"
(rewrite "abs_mult")
(("2"
(rewrite "abs_div")
(("2"
(expand "abs")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3"
(rewrite "norm_scal")
(("3"
(rewrite "abs_mult")
(("3"
(rewrite "abs_div")
(("3"
(expand "abs")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((max_segment_point_in_slice_def formula-decl nil wedge_optimum_2D
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(neg_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(sub_zero_right formula-decl nil vectors_2D "vectors/")
(on_segment_in_wedge? const-decl "bool" wedge_optimum_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(t skolem-const-decl "real" horizontal_los nil)
(vo skolem-const-decl "Nz_vect2" horizontal_los nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(gs_only? const-decl "bool" definitions nil)
(abs_mult formula-decl nil real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(abs_nat formula-decl nil abs_lems "reals/")
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(abs_div formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(norm_scal formula-decl nil vectors_2D "vectors/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(add_cancel_neg formula-decl nil vectors_2D "vectors/")
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(scal_assoc formula-decl nil vectors_2D "vectors/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(intersects_segment_fun_def formula-decl nil wedge_optimum_2D nil)
(- const-decl "Vector" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(* const-decl "Vector" vectors_2D "vectors/")
(LoS_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_los nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-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)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil)
(gs_los_TCC1-1 nil 3443981813 ("" (subtype-tcc) nil nil) nil nil))
(gs_los_TCC2 0
(gs_los_TCC2-1 nil 3447153768
("" (skeep) (("" (rewrite "gs_only_id") nil nil)) nil) nil nil))
(gs_los_def 0
(gs_los_def-2 nil 3531498662
("" (skeep)
(("" (assert)
(("" (lemma "max_segment_point_in_slice_def")
((""
(inst - "MinGS" "MaxGS" "s" "irt*perpR(s)" "zero"
"(1/norm(vo))*vo" "-vi")
((""
(name "vv" "max_segment_point_in_slice(zero,
-vi,
(1 / norm(vo)) * vo,
MinGS,
MaxGS,
s,
irt * perpR(s))")
(("" (replace -1)
(("" (assert)
(("" (flatten)
(("" (expand "gs_los")
(("" (replace -1)
(("" (assert)
(("" (case "NOT norm(vv)>=MinRelSpeed")
(("1" (assert)
(("1" (skeep 2)
(("1"
(inst - "nvo2-vi")
(("1"
(assert)
(("1"
(hide (-1 -2))
(("1"
(expand "on_segment_in_wedge?")
(("1"
(expand "gs_only?")
(("1"
(skeep -1)
(("1"
(replace -1)
(("1"
(rewrite "norm_scal")
(("1"
(expand "abs")
(("1"
(inst + "l*norm(vo)")
(("1"
(assert)
(("1"
(replace
-1
:dir
rl)
(("1"
(split +)
(("1"
(hide-all-but
1)
(("1"
(grind)
nil
nil))
nil)
("2"
(rewrite
"dot_nneg_divergent"
-
:dir
rl)
(("1"
(hide-all-but
(-4 1))
(("1"
(grind)
nil
nil))
nil)
("2"
(flatten)
(("2"
(replace
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(hide-all-but
(-5 1))
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(case "intersects_segment_fun?(zero,
-vi,
(1 / norm(vo)) * vo,
MinGS,
MaxGS,
s,
irt * perpR(s))")
(("1"
(assert)
(("1"
(split +)
(("1"
(flatten)
(("1"
(rewrite
"intersects_segment_fun_def")
(("1"
(assert)
(("1"
(expand
"on_segment_in_wedge?"
-
1)
(("1"
(skeep -4)
(("1"
(assert)
(("1"
(split +)
(("1"
(expand "gs_only?")
(("1"
(inst
+
"(t * (1 / norm(vo)))")
(("1"
(replace -6 +)
(("1"
(assert)
nil
nil))
nil)
("2"
(case
"FORALL (rgp1:real): rgp1>0 IMPLIES (rgp1>=0 AND rgp1>0)")
(("1"
(rewrite -1)
(("1"
(cross-mult
1)
nil
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(skosimp*)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -6 1)
(("2"
(assert)
(("2"
(rewrite
"norm_scal"
+)
(("2"
(rewrite
"abs_mult")
(("2"
(rewrite
"abs_div")
(("2"
(expand
"abs"
+)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(replace -6 1)
(("3"
(assert)
(("3"
(rewrite
"norm_scal"
+)
(("3"
(rewrite
"abs_mult")
(("3"
(rewrite
"abs_div")
(("3"
(expand
"abs"
+)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(hide-all-but (-7 1))
(("4"
(grind)
nil
nil))
nil)
("5"
(rewrite
"dot_nneg_divergent"
1
:dir
rl)
(("1"
(hide-all-but
(-7 1))
(("1"
(grind)
nil
nil))
nil)
("2"
(flatten)
(("2"
(replace -1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("6"
(hide-all-but (-8 1))
(("6"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"intersects_segment_fun_def")
(("2"
(assert)
(("2"
(skeep)
(("2"
(inst - "nvo2-vi")
(("2"
(assert)
(("2"
(split -)
(("1"
(split +)
(("1" (propax) nil nil)
("2"
(expand
"on_segment_in_wedge?"
-12)
(("2"
(skeep -12)
(("2"
(replace -14 -1)
(("2"
(assert)
(("2"
(case
"t > 0")
(("1"
(hide-all-but
(-1 -2))
(("1"
(lemma
"norm_eq_0")
(("1"
(inst
-
"(t*(1/norm(vo)))*vo")
(("1"
(assert)
(("1"
(rewrite
"norm_scal")
(("1"
(rewrite
"abs_mult")
(("1"
(rewrite
"abs_div")
(("1"
(expand
"abs")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"on_segment_in_wedge?"
+)
(("2"
(expand "gs_only?")
(("2"
(skeep -1)
(("2"
(inst
+
"l*norm(vo)")
(("2"
(assert)
(("2"
(replace -1)
(("2"
(rewrite
"norm_scal")
(("2"
(expand
"abs")
(("2"
(assert)
(("2"
(replace
-1
:dir
rl)
(("2"
(split
+)
(("1"
(hide-all-but
1)
(("1"
(grind)
nil
nil))
nil)
("2"
(rewrite
"dot_nneg_divergent"
-
:dir
rl)
(("1"
(hide-all-but
(-4
1))
(("1"
(grind)
nil
nil))
nil)
("2"
(flatten)
(("2"
(replace
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(hide-all-but
(-5
1))
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skeep 2)
(("2"
(lemma
"max_segment_point_in_slice_complete")
(("2"
(inst?)
(("2"
(replace -3)
(("2"
(assert)
(("2"
(rewrite
"intersects_segment_fun_def")
(("2"
(assert)
(("2"
(inst - "nvo2-vi")
(("2"
(split -1)
(("1"
(hide-all-but
(-1 1))
(("1"
(expand
"on_segment_in_wedge?")
(("1"
(skeep -1)
(("1"
(expand
"intersects_segment?")
(("1"
(inst
+
"t")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide (-2 -3 -4))
(("2"
(expand
"gs_only?")
(("2"
(skeep -2)
(("2"
(expand
"on_segment_in_wedge?")
(("2"
(inst
+
"l*norm(vo)")
(("2"
(replace
-2)
(("2"
(rewrite
"norm_scal")
(("2"
(expand
"abs")
(("2"
(assert)
(("2"
(replace
-2
:dir
rl)
(("2"
(split
+)
(("1"
(hide-all-but
1)
(("1"
(grind)
nil
nil))
nil)
("2"
(rewrite
"dot_nneg_divergent"
-
:dir
rl)
(("1"
(hide-all-but
(-5
1))
(("1"
(grind)
nil
nil))
nil)
("2"
(flatten)
(("2"
(replace
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(hide-all-but
(-6
1))
(("3"
(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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(< const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(D formal-const-decl "posreal" horizontal_los nil)
(LoS_vect2 type-eq-decl nil horizontal nil)
(* const-decl "Vector" vectors_2D "vectors/")
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(NOT const-decl "[bool -> bool]" booleans nil)
(on_segment_in_wedge? const-decl "bool" wedge_optimum_2D nil)
(norm_scal formula-decl nil vectors_2D "vectors/")
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(det const-decl "real" det_2D "vectors/")
(dot_nneg_divergent formula-decl nil definitions nil)
(* const-decl "real" vectors_2D "vectors/")
(dot_zero_left formula-decl nil vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(scal_assoc formula-decl nil vectors_2D "vectors/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(gs_only? const-decl "bool" definitions nil)
(- const-decl "Vector" vectors_2D "vectors/")
(norm_neg formula-decl nil vectors_2D "vectors/")
(sub_zero_left formula-decl nil vectors_2D "vectors/")
(intersects_segment_fun? const-decl "bool" wedge_optimum_2D nil)
(intersects_segment_fun_def formula-decl nil wedge_optimum_2D nil)
(add_zero_left formula-decl nil vectors_2D "vectors/")
(abs_div formula-decl nil real_props nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(abs_nat formula-decl nil abs_lems "reals/")
(abs_mult formula-decl nil real_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div1 formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(add_cancel_neg formula-decl nil vectors_2D "vectors/")
(vo skolem-const-decl "Nz_vect2" horizontal_los nil)
(t skolem-const-decl "real" horizontal_los nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(add_cancel_neg2 formula-decl nil vectors_2D "vectors/")
(intersects_segment? const-decl "bool" wedge_optimum_2D nil)
(max_segment_point_in_slice_complete formula-decl nil
wedge_optimum_2D nil)
(norm_zero formula-decl nil vectors_2D "vectors/")
(gs_los const-decl "{nvo |
nvo /= zero =>
gs_only?(vo)(nvo) AND MinGS <= norm(nvo) AND norm(nvo) <= MaxGS}"
horizontal_los nil)
(sub_zero_right formula-decl nil vectors_2D "vectors/")
(neg_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(max_segment_point_in_slice const-decl "Vect2" wedge_optimum_2D
nil)
(max_segment_point_in_slice_def formula-decl nil wedge_optimum_2D
nil))
nil)
(gs_los_def-1 nil 3531498583
("" (skeep)
(("" (assert)
(("" (lemma "max_segment_point_in_slice_def")
((""
(inst - "MinGS" "MaxGS" "s" "irt*perpR(s)" "zero"
"(1/norm(vo))*vo" "-vi")
((""
(name "vv" "max_segment_point_in_slice(zero,
-vi,
(1 / norm(vo)) * vo,
MinGS,
MaxGS,
s,
irt * perpR(s))")
(("" (replace -1)
(("" (assert)
(("" (flatten)
(("" (expand "gs_los_new")
(("" (replace -1)
(("" (assert)
(("" (case "NOT norm(vv)>=MinRelSpeed")
(("1" (assert)
(("1" (skeep 2)
(("1"
(inst - "nvo2-vi")
(("1"
(assert)
(("1"
(hide (-1 -2))
(("1"
(expand "on_segment_in_wedge?")
(("1"
(expand "gs_only?")
(("1"
(skeep -1)
(("1"
(replace -1)
(("1"
(rewrite "norm_scal")
(("1"
(expand "abs")
(("1"
(inst + "l*norm(vo)")
(("1"
(assert)
(("1"
(replace
-1
:dir
rl)
(("1"
(split +)
(("1"
(hide-all-but
1)
(("1"
(grind)
nil
nil))
nil)
("2"
(rewrite
"dot_nneg_divergent"
-
:dir
rl)
(("1"
(hide-all-but
(-4 1))
(("1"
(grind)
nil
nil))
nil)
("2"
(flatten)
(("2"
(replace
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(hide-all-but
(-5 1))
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(case "intersects_segment_fun?(zero,
-vi,
(1 / norm(vo)) * vo,
MinGS,
MaxGS,
s,
irt * perpR(s))")
(("1"
(assert)
(("1"
(split +)
(("1"
(flatten)
(("1"
(rewrite
"intersects_segment_fun_def")
(("1"
(assert)
(("1"
(expand
"on_segment_in_wedge?"
-
1)
(("1"
(skeep -4)
(("1"
(assert)
(("1"
(split +)
(("1"
(expand "gs_only?")
(("1"
(inst
+
"(t * (1 / norm(vo)))")
(("1"
(replace -6 +)
(("1"
(assert)
nil
nil))
nil)
("2"
(case
"FORALL (rgp1:real): rgp1>0 IMPLIES (rgp1>=0 AND rgp1>0)")
(("1"
(rewrite -1)
(("1"
(cross-mult
1)
nil
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(skosimp*)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.112 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.
|
