| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 145 kB |
|
Quelle vertical_los_criterion.prf Sprache: Lisp |
|||||||||
|
(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.34 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28