| products/sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: opt_trk_gs.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(opt_trk_gs
(k_opt_tangent 0 (k_opt_tangent-2 nil 3434118271 ("" (skeep) (("" (assert) (("" (rewrite "dot_sub_right") (("" (expand "k_opt") (("" (rewrite "sqv" :dir rl) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (k_opt const-decl "real" opt_trk_gs nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (* const-decl "Vector" 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) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (dot_sub_right formula-decl nil vectors_2D "vectors/")) nil) (k_opt_tangent-1 nil 3434118248 ("" (postpone) nil nil) nil shostak)) (opt_trk_gs_line_TCC1 0 (opt_trk_gs_line_TCC1-2 nil 3445701811 ("" (skeep) (("" (expand "optimal?") (("" (skeep) (("" (lemma "le_rel") (("" (inst? -1) (("" (inst -1 "vi") (("" (assert) (("" (hide 2) (("" (expand "le?") (("" (both-sides-f 1 "sq") (("1" (rewrite "sq_norm") (("1" (rewrite "sq_norm") (("1" (case "sqv(vo2 - vi - (vo - vi)) = sqv(k * nzv - (vo - vi)) + sqv(vo2-vi-k*nzv)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (name-replace "a" "k * nzv - (vo - vi)" :hide? nil) (("2" (name-replace "b" "vo2 - vi - k * nzv" :hide? nil) (("2" (case-replace "vo2 - vi - (vo - vi) = a+b") (("1" (hide -1) (("1" (rewrite "sqv_add") (("1" (assert) (("1" (cancel-by 1 "2") (("1" (hide 1) (("1" (expand "parallel?") (("1" (skeep -4) (("1" (lemma "k_opt_tangent") (("1" (inst?) (("1" (assert) (("1" (replaces -4 :dir rl) (("1" (replace -3) (("1" (case-replace " vo2 - vi - k * nzv = vo2 - (k * nzv + vi)") (("1" (hide -1) (("1" (replaces -2) (("1" (replaces -3) (("1" (rewrite "dot_scal_right") (("1" (lemma "dot_comm") (("1" (inst?) (("1" (replaces -1) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) 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) ("2" (replaces (-1 -2) :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sq_le") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((optimal? const-decl "bool" definitions nil) (le_rel formula-decl nil definitions nil) (NOT const-decl "[bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (nzreal nonempty-type-eq-decl nil reals nil) (dot_scal_right formula-decl nil vectors_2D "vectors/") (dot_comm formula-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (k_opt_tangent formula-decl nil opt_trk_gs nil) (parallel? const-decl "bool" vectors_2D "vectors/") (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (both_sides_times1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sqv_add formula-decl nil vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_norm formula-decl nil vectors_2D "vectors/") (sq_le formula-decl nil sq "reals/") (le? const-decl "bool" definitions nil) (add_cancel_neg2 formula-decl nil vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (* const-decl "Vector" 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (+ const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil) (opt_trk_gs_line_TCC1-1 nil 3445701764 ("" (subtype-tcc) nil nil) nil nil)) (opt_trk_gs_line_TCC2 0 (opt_trk_gs_line_TCC2-2 nil 3445701838 ("" (skeep) (("" (hide -1) (("" (grind) nil nil)) nil)) nil) ((* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) nil) (opt_trk_gs_line_TCC2-1 nil 3445701764 ("" (subtype-tcc) nil nil) nil nil)) (opt_trk_gs_dot_TCC1 0 (opt_trk_gs_dot_TCC1-2 nil 3445702005 ("" (skeep) (("" (name-replace "opto" "opt_trk_gs_line(Vdir(u, vo - vi), vo, vi + W0(u, j))") (("" (typepred "opto") (("" (case "W0(u,j) + opto`1 * Vdir(u, vo - vi) = opto`2 - vi") (("1" (replaces -1 :dir rl) (("1" (rewrite "W_dot") nil nil)) nil) ("2" (replaces -1) (("2" (hide-all-but 1) (("2" (grind :exclude "W0") nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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/") (bool nonempty-type-eq-decl nil booleans nil) (optimal? const-decl "bool" definitions nil) (Vdir const-decl "Nz_vect2" definitions nil) (- const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "Vector" vectors_2D "vectors/") (opt_trk_gs_line const-decl "{k: real, nvo: (optimal?(vo, nzv)) | k * nzv = nvo - vi}" opt_trk_gs nil) (+ const-decl "Vector" vectors_2D "vectors/") (W0 const-decl "Vect2" definitions nil) (W_dot formula-decl nil definitions nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil) (opt_trk_gs_dot_TCC1-1 nil 3445701764 ("" (subtype-tcc) nil nil) nil nil)) (opt_trk_gs_vertical_TCC1 0 (opt_trk_gs_vertical_TCC1-1 nil 3471177879 ("" (skeep) (("" (assert) (("" (lemma "Delta_gt_0_nzv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Delta_gt_0_nzv formula-decl nil horizontal 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" opt_trk_gs nil)) nil)) (opt_trk_gs_vertical_TCC2 0 (opt_trk_gs_vertical_TCC2-2 nil 3471178012 ("" (skeep) (("" (skeep) (("" (lemma "scal_eq_zero") (("" (inst?) (("" (assert) (("" (rewrite "sqv_eq_0" :dir rl) (("" (replaces -5) (("" (lemma "Theta_D_on_D") (("" (inst?) (("" (assert) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (Theta_D_on_D formula-decl nil horizontal nil) (D formal-const-decl "posreal" opt_trk_gs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "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) (/= const-decl "boolean" notequal 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (scal_eq_zero formula-decl nil vectors_2D "vectors/")) nil) (opt_trk_gs_vertical_TCC2-1 nil 3471177879 ("" (subtype-tcc) nil nil) nil nil)) (opt_trk_gs_vertical_on_D 0 (opt_trk_gs_vertical_on_D-1 nil 3471178124 ("" (skeep) (("" (beta) (("" (flatten) (("" (expand "opt_trk_gs_vertical?") (("" (flatten) (("" (expand "opt_trk_gs_vertical") (("" (lift-if) (("" (split -1) (("1" (flatten) (("1" (assert) (("1" (typepred "opt_trk_gs_dot(t * (s + Theta_D(s, vo - vi, dir) * (vo - vi)), vo, vi, sq(D) - s * (s + Theta_D(s, vo - vi, dir) * (vo - vi)))") (("1" (replaces -5 :dir rl) (("1" (hide-all-but (-2 2)) (("1" (grind :exclude "Theta_D") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((opt_trk_gs_vertical? const-decl "bool" opt_trk_gs nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (opt_trk_gs_vertical const-decl "Vect2" opt_trk_gs nil) (real_minus_real_is_real application-judgement "real" reals 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_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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/") (optimal? const-decl "bool" definitions nil) (Vdir const-decl "Nz_vect2" definitions 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) (* const-decl "Vector" vectors_2D "vectors/") (>= 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) (+ const-decl "Vector" vectors_2D "vectors/") (D formal-const-decl "posreal" opt_trk_gs nil) (Delta const-decl "real" horizontal 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/") (Theta_D const-decl "real" horizontal nil) (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (opt_trk_gs_dot const-decl "{nvo: (optimal?(vo, Vdir(u, vo - vi))) | u * (nvo - vi) = j}" opt_trk_gs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/")) nil))) ¤ Dauer der Verarbeitung: 0.28 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.Bot Zugriff |
