| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 6 kB |
|
Quelle old_horiz_los_criterion.prf Sprache: Lisp |
|||||||||
|
(old_horiz_los_criterion
(horizontal_los_crit_symm 0 (horizontal_los_crit_symm-1 nil 3488034416 ("" (grind) 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 "bool" reals nil) (nnreal type-eq-decl nil real_types 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/") (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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 "real" vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (horizontal_los_crit? const-decl "bool" old_horiz_los_criterion nil) (- const-decl "Vector" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (horizontal_los_crit_independent 0 (horizontal_los_crit_independent-1 nil 3488118551 ("" (skeep) (("" (lemma "dot_nneg_divergent") (("" (inst?) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (expand "horizontal_los_crit?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil) ((dot_nneg_divergent formula-decl nil definitions nil) (horizontal_los_crit? const-decl "bool" old_horiz_los_criterion nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (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) (- const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nvo skolem-const-decl "Vect2" old_horiz_los_criterion nil) (vi skolem-const-decl "Vect2" old_horiz_los_criterion nil) (zero const-decl "Vector" vectors_2D "vectors/")) shostak)) (horizontal_los_crit_coordinated 0 (horizontal_los_crit_coordinated-1 nil 3488034263 ("" (skeep) (("" (rewrite "dot_nneg_divergent" :dir rl) (("1" (expand "horizontal_los_crit?") (("1" (flatten) (("1" (hide (-2 -3 -5 -6)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "nvo-nvi = (nvo-vi) + (vo-nvi) - (vo-vi)") (("1" (case "s*(nvo-nvi) = 0") (("1" (replace -2 -1) (("1" (rewrite "dot_sub_right") (("1" (rewrite "dot_add_right") (("1" (case "s*(vo-nvi) = -s*(nvi-vo)") (("1" (assert) (("1" (expand "horizontal_los_crit?") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2) (("2" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((dot_nneg_divergent formula-decl nil definitions 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) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (* const-decl "real" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (horizontal_los_crit? const-decl "bool" old_horiz_los_criterion nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "Vector" vectors_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (dot_add_right formula-decl nil vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (dot_sub_right formula-decl nil vectors_2D "vectors/") (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)) shostak))) ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28