|
(vertical_los_criterion
(time_vertical_exit_by_TCC1 0
(time_vertical_exit_by_TCC1-1 nil 3519732687
("" (skeep)
(("" (lemma "vertical_los_inside_Theta")
(("" (inst - "eps*MinRelVertSpeed" "sz" "0")
(("" (assert) nil nil)) nil))
nil))
nil)
((H formal-const-decl "posreal" vertical_los_criterion 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)
(>= 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)
(vertical_los_inside_Theta formula-decl nil vertical nil)
(real_plus_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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
nil))
(time_vertical_exit_by_TCC2 0
(time_vertical_exit_by_TCC2-1 nil 3519732687
("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(real nonempty-type-from-decl nil reals nil)
(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/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(/= const-decl "boolean" notequal nil))
nil))
(time_vertical_exit_by_TCC3 0
(time_vertical_exit_by_TCC3-1 nil 3519732687
("" (skeep)
(("" (lemma "vertical_los_inside_Theta")
(("" (inst-cp - "eps*MinRelVertSpeed" "sz" "0")
(("" (inst - "vz" "sz" "0")
(("" (assert)
(("" (flatten)
(("" (expand "min")
(("" (lift-if) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((H formal-const-decl "posreal" vertical_los_criterion 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)
(>= 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)
(vertical_los_inside_Theta formula-decl nil vertical nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
nil))
(time_vertical_exit_by_symm 0
(time_vertical_exit_by_symm-1 nil 3531579993
("" (skeep)
(("" (expand "time_vertical_exit_by")
(("" (case "-eps*MinRelVertSpeed = -(eps*MinRelVertSpeed)")
(("1" (replace -1)
(("1" (rewrite "Theta_H_symm")
(("1" (rewrite "Theta_H_symm")
(("1" (hide -1)
(("1" (lift-if)
(("1" (lift-if)
(("1" (lift-if) (("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((sign_neg_clos application-judgement "Sign" sign "reals/")
(time_vertical_exit_by const-decl
"{x: real | MinRelVertSpeed > 0 AND abs(sz) < H IMPLIES x > 0}"
vertical_los_criterion nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Theta_H_symm formula-decl nil vertical nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(H formal-const-decl "posreal" vertical_los_criterion nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" 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)
(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)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Sign type-eq-decl nil sign "reals/")
(>= 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)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(min_rel_vert_speed_TCC1 0
(min_rel_vert_speed_TCC1-1 nil 3531562642 ("" (subtype-tcc) nil nil)
nil nil))
(min_rel_vert_speed_TCC2 0
(min_rel_vert_speed_TCC2-1 nil 3531562642 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(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/")
(>= 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)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(min_rel_vert_speed_symm 0
(min_rel_vert_speed_symm-1 nil 3531562675
("" (skeep)
(("" (expand "min_rel_vert_speed")
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (assert)
(("" (ground) (("" (rewrite "abs_neg") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sign_neg_clos application-judgement "Sign" sign "reals/")
(min_rel_vert_speed const-decl
"{x: nnreal | abs(sz) < H IMPLIES x > 0}" vertical_los_criterion
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_neg formula-decl nil abs_lems "reals/")
(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)
(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)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(vs_bound_crit_indep_TCC1 0
(vs_bound_crit_indep_TCC1-1 nil 3562942251
("" (skeep) (("" (replace -4) (("" (assert) nil nil)) nil)) nil)
((dot_zero_right formula-decl nil vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(vs_bound_crit_indep_TCC2 0
(vs_bound_crit_indep_TCC2-1 nil 3562942251
("" (skeep) (("" (replace -4) (("" (assert) nil nil)) nil)) nil)
((dot_zero_right formula-decl nil vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(vs_bound_crit_indep 0
(vs_bound_crit_indep-1 nil 3562941990
("" (skeep)
(("" (lemma "sq_gt")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (rewrite "sq_norm")
(("" (rewrite "sq_norm")
(("" (assert)
(("" (case "eps*v`z > 0")
(("1" (expand "vs_bound_crit?")
(("1" (assert)
(("1" (flatten)
(("1"
(case "eps * horizontal_tca(vect2(s), vect2(nv)) * nv`z >=
eps * horizontal_tca(vect2(s), vect2(v)) * v`z")
(("1" (grind :exclude "horizontal_tca") nil
nil)
("2" (hide 3)
(("2"
(case
"NOT sqv(horizontal_tca(s,nv)*vect2(nv)) >= sqv(horizontal_tca(s,v)*vect2(v))")
(("1"
(rewrite "vect2_add")
(("1"
(rewrite "vect2_add")
(("1"
(rewrite "vect2_scal")
(("1"
(rewrite "vect2_scal")
(("1"
(rewrite
"horizontal_sq_dtca_eq"
:dir
rl)
(("1"
(rewrite
"horizontal_sq_dtca_eq"
:dir
rl)
(("1"
(expand
"horizontal_sq_dtca")
(("1"
(rewrite "sqv_scal")
(("1"
(rewrite "sqv_scal")
(("1"
(assert)
(("1"
(assert)
(("1"
(expand
"horizontal_tca"
1)
(("1"
(rewrite
"sq_div")
(("1"
(rewrite
"sq_div")
(("1"
(case
"FORALL (ap1:posreal,b:real): b/sq(ap1) * ap1 = b/ap1")
(("1"
(rewrite
-1)
(("1"
(rewrite
-1)
(("1"
(lemma
"orthogonal_basis")
(("1"
(inst-cp
-
"nv"
"perpR(nv)"
"s")
(("1"
(assert)
(("1"
(case
"vect2(nv) /= zero AND
perpR(vect2(nv)) /= zero AND
orthogonal?(vect2(nv), perpR(vect2(nv)))")
(("1"
(flatten)
(("1"
(assert)
(("1"
(inst
-
"v"
"perpR(v)"
"s")
(("1"
(case
"vect2(v) /= zero AND
perpR(vect2(v)) /= zero AND orthogonal?(vect2(v), perpR(vect2(v)))")
(("1"
(flatten)
(("1"
(assert)
(("1"
(lemma
"orthogonal_basis_sqv")
(("1"
(inst
-
_
_
"v"
"perpR(v)"
"s")
(("1"
(inst?)
(("1"
(assert)
(("1"
(lemma
"orthogonal_basis_sqv")
(("1"
(inst
-
_
_
"nv"
"perpR(nv)"
"s")
(("1"
(inst?)
(("1"
(assert)
(("1"
(rewrite
"sqv_perpR")
(("1"
(rewrite
"sqv_perpR")
(("1"
(assert)
(("1"
(rewrite
"det_perpR"
:dir
rl)
(("1"
(rewrite
"det_perpR"
:dir
rl)
(("1"
(assert)
(("1"
(rewrite
"sq_neg")
(("1"
(rewrite
"sq_neg")
(("1"
(assert)
(("1"
(rewrite
"sq_div")
(("1"
(rewrite
"sq_div")
(("1"
(rewrite
"sq_div")
(("1"
(rewrite
"sq_div")
(("1"
(assert)
(("1"
(rewrite
-7)
(("1"
(rewrite
-7)
(("1"
(rewrite
-7)
(("1"
(rewrite
-7)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(lemma
"vectors_2D.sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(lemma
"vectors_2D.sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"vectors_2D.sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(lemma
"vectors_2D.sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(split)
(("1"
(flatten)
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(flatten)
(("2"
(lemma
"perpR_perpR")
(("2"
(inst?)
(("2"
(replace
-2)
(("2"
(assert)
(("2"
(case
"--vect2(v) = zero")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(replace
-1
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but
1)
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(split)
(("1"
(flatten)
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(flatten)
(("2"
(lemma
"perpR_perpR")
(("2"
(inst
-
"nv")
(("2"
(replace
-2)
(("2"
(assert)
(("2"
(case
"--vect2(nv) = zero")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(replace
-1
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but
1)
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"vectors_2D.sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(replace
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(lemma
"vectors_2D.sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(replace
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "sqv_scal")
(("2"
(rewrite "sqv_scal")
(("2"
(expand "horizontal_tca" -1)
(("2"
(rewrite "sq_div")
(("1"
(rewrite "sq_div")
(("1"
(case
"FORALL (ap1:posreal,b:real): b/sq(ap1) * ap1 = b/ap1")
(("1"
(rewrite -1)
(("1"
(rewrite -1)
(("1"
(hide -1)
(("1"
(cross-mult -1)
(("1"
(invoke
(case "%1")
(! -1 1))
(("1"
(assert)
(("1"
(cross-mult
-2)
(("1"
(invoke
(case
"%1")
(!
-2
1))
(("1"
(assert)
(("1"
(case
"NOT nv`z * horizontal_tca(vect2(s), vect2(nv)) * eps <
v`z * horizontal_tca(vect2(s), vect2(v)) * eps")
(("1"
(assert)
nil
nil)
("2"
(expand
"horizontal_tca"
-1)
(("2"
(cross-mult
-1)
(("2"
(cross-mult
-1)
(("2"
(case
"(sq(-(vect2(s) * vect2(v))) * sqv(vect2(nv))) > 0")
(("1"
(case
"nv`z * sqv(vect2(v)) * -(vect2(s) * vect2(nv)) * eps > 0")
(("1"
(mult-ineq
-3
-6)
(("1"
(name
"K1"
"sqv(vect2(v))*(-(vect2(s)*vect2(nv)))*(-vect2(s)*vect2(v))*sqv(vect2(nv))")
(("1"
(case
"K1 > 0")
(("1"
(mult-by
-12
"K1")
(("1"
(hide
1)
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(hide
(-1
-2
2))
(("2"
(hide
(-1
-2
-3
-6))
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.895 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.
|
