| products/sources/formale sprachen/PVS/vectors/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: lines_3D.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(lines_3D
(line_from_TCC1 0 (line_from_TCC1-1 nil 3306084266 ("" (skosimp*) (("" (typepred "p2!1") (("" (flatten) (("" (expand "vec_from") (("" (expand "nz_vector?") (("" (lemma "sub_eq_zero") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (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) (vec_from const-decl "Vect3" lines_3D nil) (Vector type-eq-decl nil vectors_3D nil) (sub_eq_zero formula-decl nil vectors_3D nil)) nil)) (vec_from_eq_args 0 (vec_from_eq_args-1 nil 3255275743 ("" (skosimp*) (("" (expand "vec_from") (("" (grind) nil nil)) nil)) nil) ((vec_from const-decl "Vect3" lines_3D nil) (- const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (vel_from_tm_TCC1 0 (vel_from_tm_TCC1-1 nil 3255275743 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (- const-decl "Vector" vectors_3D nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil 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) (* const-decl "Vector" vectors_3D 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) (+ const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (scal_assoc formula-decl nil vectors_3D nil) (scal_1 formula-decl nil vectors_3D nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (line_from_tm_TCC1 0 (line_from_tm_TCC1-1 nil 3306084266 ("" (skosimp* :preds? t) (("" (expand "vel_from_tm") (("" (lemma "scal_eq_zero") (("" (inst?) (("" (assert) (("" (rewrite "sub_eq_zero") nil nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines_3D nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (Vector type-eq-decl nil vectors_3D nil) (- const-decl "Vector" vectors_3D nil) (sub_eq_zero formula-decl nil vectors_3D nil) (scal_eq_zero formula-decl nil vectors_3D 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) (Vect3 type-eq-decl nil vectors_3D_def nil) (/= const-decl "boolean" notequal 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) (nzreal nonempty-type-eq-decl nil reals nil)) nil)) (vel_from_tm_nz 0 (vel_from_tm_nz-1 nil 3255275743 ("" (skosimp*) (("" (typepred "vel_from_tm(p1!1, p2!1, t!1)") (("" (replace -1 +) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines_3D nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (* const-decl "Vector" vectors_3D 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) (+ const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (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) (add_zero_right formula-decl nil vectors_3D nil) (scal_zero formula-decl nil vectors_3D nil) (zero const-decl "Vector" vectors_3D nil)) nil)) (vel_from_tm_lem 0 (vel_from_tm_lem-1 nil 3255275743 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)) (vel_from_tm_rew 0 (vel_from_tm_rew-1 nil 3255275743 ("" (skosimp*) (("" (typepred "vel_from_tm(p1!1, p2!1, t!1)") (("" (apply-extensionality 1 :hide? t) (("1" (expand "*" +) (("1" (cross-mult 1) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "*" +) (("2" (cross-mult 1) (("2" (grind) nil nil)) nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil) ((vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines_3D nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (* const-decl "Vector" vectors_3D 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) (+ const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (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) (real_minus_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_cancel4 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "Vector" vectors_3D nil)) nil)) (vel_from_tm_eq_args 0 (vel_from_tm_eq_args-1 nil 3255275743 ("" (skosimp*) (("" (rewrite "vel_from_tm_rew") (("" (rewrite "sub_eq_args") (("" (grind) nil nil)) nil)) nil)) nil) ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sub_eq_args formula-decl nil vectors_3D nil) (scal_zero formula-decl nil vectors_3D nil) (vel_from_tm_rew formula-decl nil lines_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def 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) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) nil)) (vel_from_tm_length 0 (vel_from_tm_length-1 nil 3255275743 ("" (skosimp*) (("" (lemma "vel_from_tm_rew") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (assert) (("" (rewrite "norm_scal") (("" (rewrite "sq_times") (("" (rewrite "dist_norm" :dir rl) (("" (expand "dist") (("" (rewrite "sq_sqrt") (("" (case-replace "sq(abs(1 / t!1)) = 1/sq(t!1)") (("1" (assert) (("1" (rewrite "sq_dist_sym") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_tm_rew formula-decl nil lines_3D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sq_times formula-decl nil sq "reals/") (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_3D nil) (sq_abs formula-decl nil sq "reals/") (dist const-decl "nnreal" distance_3D nil) (sq const-decl "nonneg_real" sq "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sq_dist_sym formula-decl nil distance_3D nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_sqrt formula-decl nil sqrt "reals/") (sq_dist const-decl "nnreal" distance_3D nil) (dist_norm formula-decl nil distance_3D nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (- const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (norm_scal formula-decl nil vectors_3D nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (Vect3 type-eq-decl nil vectors_3D_def nil) (real nonempty-type-from-decl nil reals nil)) nil)) (vel_from_spd_TCC1 0 (vel_from_spd_TCC1-1 nil 3255275743 ("" (skosimp*) (("" (cross-mult 2) (("" (assert) (("" (lemma "dist_eq_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (dist_eq_0 formula-decl nil distance_3D nil)) nil)) (vel_from_spd_lem_TCC1 0 (vel_from_spd_lem_TCC1-1 nil 3256559321 ("" (skosimp*) (("" (cross-mult -1) (("" (rewrite "dist_eq_0") nil nil)) nil)) nil) ((nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (div_cancel3 formula-decl nil real_props nil) (dist const-decl "nnreal" distance_3D nil) (nnreal type-eq-decl nil real_types nil) (Vect3 type-eq-decl nil vectors_3D_def 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (dist_eq_0 formula-decl nil distance_3D nil)) shostak)) (vel_from_spd_lem 0 (vel_from_spd_lem-1 nil 3255348389 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (assert) (("" (rewrite "vel_from_tm_rew") (("1" (assert) nil nil) ("2" (hide 3) (("2" (lemma "dist_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_spd const-decl "Vect3" lines_3D nil) (vel_from_tm_rew formula-decl nil lines_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def 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) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (dist const-decl "nnreal" distance_3D 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) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (vel_from_spd_norm_TCC1 0 (vel_from_spd_norm_TCC1-1 nil 3255866120 ("" (skeep) (("" (expand "nz_vector?") (("" (lemma "sub_eq_zero") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sub_eq_zero formula-decl nil vectors_3D nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (Vector type-eq-decl nil vectors_3D nil) (real nonempty-type-from-decl nil reals nil)) shostak)) (vel_from_spd_norm 0 (vel_from_spd_norm-1 nil 3255867439 ("" (skosimp*) (("" (expand "^") (("" (expand "vel_from_spd") (("" (rewrite "dist_norm") (("" (assert) (("" (rewrite "norm_sym") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((^ const-decl "Normalized" vectors_3D nil) (dist_norm formula-decl nil distance_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (Vector type-eq-decl nil vectors_3D nil) (norm_sym formula-decl nil vectors_3D nil) (scal_assoc formula-decl nil vectors_3D nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (vel_from_spd const-decl "Vect3" lines_3D nil)) shostak)) (gen_speed_TCC1 0 (gen_speed_TCC1-1 nil 3255275743 ("" (inst 1 "lambda (d: [p1: Vect3, {v | v /= p1}, posreal]) : 1 / d`3 * dist(d`1, d`2)") nil nil) ((dist const-decl "nnreal" distance_3D nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types 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_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) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (real nonempty-type-from-decl nil reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (on_line_lem 0 (on_line_lem-1 nil 3602330096 ("" (skosimp*) (("" (expand "on_line?") (("" (expand "line_from") (("" (split +) (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (inst + "1") (("2" (assert) (("2" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_3D nil) (scal_0 formula-decl nil vectors_3D nil) (add_zero_right formula-decl nil vectors_3D 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) (scal_1 formula-decl nil vectors_3D nil) (- const-decl "Vector" vectors_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (vec_from const-decl "Vect3" lines_3D nil) (+ const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (/= const-decl "boolean" notequal nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (line_from const-decl "Line" lines_3D nil)) nil)) (on_line_neg 0 (on_line_neg-1 nil 3602330131 ("" (skosimp*) (("" (expand "on_line?") (("" (expand "-") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (inst + "-x!1") (("" (assert) (("" (apply-extensionality :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_3D nil) (neg_nzv application-judgement "Nz_vector" vectors_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_3D nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (Nz_vect3 type-eq-decl nil vectors_3D nil) (Line type-eq-decl nil lines_3D nil) (* const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "Line" lines_3D nil)) nil)) (on_line_sym_TCC1 0 (on_line_sym_TCC1-1 nil 3602330075 ("" (subtype-tcc) nil nil) ((- const-decl "Vector" vectors_3D nil) (vec_from const-decl "Vect3" lines_3D nil) (line_from const-decl "Line" lines_3D nil) (* const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D nil) (on_line? const-decl "bool" lines_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (on_line_sym 0 (on_line_sym-1 nil 3602330161 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (inst + "1-x!1") (("" (replace -1) (("" (hide -1) (("" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_3D nil) (real_minus_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "Vector" vectors_3D nil) (vec_from const-decl "Vect3" lines_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_3D nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (/= const-decl "boolean" notequal nil) (Nz_vect3 type-eq-decl nil vectors_3D nil) (Line type-eq-decl nil lines_3D nil) (line_from const-decl "Line" lines_3D nil) (* const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil)) nil)) (gen_line_spd_TCC1 0 (gen_line_spd_TCC1-6 nil 3440254934 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (name-replace "AA" "s!1 / dist(p1!1, p2!1)") (("" (lemma "scal_eq_zero") (("" (inst?) (("" (assert) (("" (rewrite "sub_eq_zero") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_spd const-decl "Vect3" lines_3D nil) (scal_eq_zero formula-decl nil vectors_3D nil) (sub_eq_zero formula-decl nil vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (- const-decl "Vector" vectors_3D nil) (nzreal nonempty-type-eq-decl nil reals nil) (dist const-decl "nnreal" distance_3D nil) (nnreal type-eq-decl nil real_types nil) (Vect3 type-eq-decl nil vectors_3D_def 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil) (gen_line_spd_TCC1-5 nil 3440246180 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (name-replace "AA" "s!1 / dist(p1!1, p2!1)") (("" (lemma "scal_eq_0") (("" (inst?) (("" (assert) (("" (rewrite "sub_eq_zero") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vect3 type-eq-decl nil vectors_3D_def nil) (dist const-decl "nnreal" distance_3D nil) (Vector type-eq-decl nil vectors_3D nil) (sub_eq_zero formula-decl nil vectors_3D nil)) nil) (gen_line_spd_TCC1-4 nil 3430838788 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (name-replace "AA" "s!1 / dist(p1!1, p2!1)") (("" (lemma "scal_eq_zero") (("" (inst?) (("" (assert) (("" (rewrite "sub_eq_zero") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vect3 type-eq-decl nil vectors_3D_def nil) (Vector type-eq-decl nil vectors_3D nil) (sub_eq_zero formula-decl nil vectors_3D nil)) nil) (gen_line_spd_TCC1-3 nil 3430838147 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (typepred "p2!1") (("" (flatten) (("" (grind :exclude "dist") (("" (name-replace "AA" "s!1 / dist(p1!1, p2!1)") (("" (cancel-by -1 "AA") (("" (cancel-by -2 "AA") (("" (cancel-by -3 "AA") (("" (decompose-equality 4) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (Vect3 type-eq-decl nil vectors_3D_def nil)) nil) (gen_line_spd_TCC1-2 nil 3430838136 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (typepred "p2!1") (("" (flatten) (("" (ground) (("" (grind :exclude "dist") (("" (name-replace "AA" "s!1 / dist(p1!1, p2!1)") (("" (apply-extensionality 1 :hide? t) (("" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil) (gen_line_spd_TCC1-1 nil 3303642886 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (name-replace "AA" "s!1 / dist(p1!1, p2!1)") (("1" (typepred "p2!1") (("1" (flatten) (("1" (prop) (("1" (rewrite "norm_scal") (("1" (mult-cases -1) (("1" (rewrite "norm_eq_0") nil nil)) nil)) nil) ("2" (expand "*") (("2" (expand "-") (("2" (apply-extensionality 1 :hide? t) (("2" (factor -1) (("2" (mult-cases -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "p2!1") (("2" (flatten) (("2" (rewrite "dist_eq_0") nil nil)) nil)) nil)) nil)) nil)) nil) ((norm const-decl "nnreal" vectors_3D nil) (norm_zero formula-decl nil vectors_3D nil) (sub_eq_zero formula-decl nil vectors_3D nil) (norm_scal formula-decl nil vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (* const-decl "Vector" vectors_3D nil)) nil)) (test1_TCC1 0 (test1_TCC1-1 nil 3306084266 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (test1 0 (test1-1 nil 3256559090 ("" (skosimp*) (("" (expand "gen_line_tm") (("" (expand "on_line?") (("" (expand "vel_from_tm") (("" (inst + "0") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((gen_line_tm const-decl "Line" lines_3D nil) (vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines_3D nil) (scal_0 formula-decl nil vectors_3D nil) (scal_assoc formula-decl nil vectors_3D nil) (add_zero_right formula-decl nil vectors_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (on_line? const-decl "bool" lines_3D nil)) shostak)) (test2 0 (test2-1 nil 3256559204 ("" (skosimp*) (("" (expand "on_line?") (("" (expand "gen_line_tm") (("" (expand "vel_from_tm") (("" (inst + "t!1") (("" (assert) (("" (apply-extensionality 2 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_3D nil) (vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines_3D nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (scal_1 formula-decl nil vectors_3D nil) (scal_assoc formula-decl nil vectors_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (gen_line_tm const-decl "Line" lines_3D nil)) shostak)) (test3 0 (test3-1 nil 3256559678 ("" (skosimp*) (("" (expand "gen_line_spd") (("" (expand "on_line?") (("" (inst + "0") (("" (expand "vel_from_spd") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((gen_line_spd const-decl "Line" lines_3D 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) (scal_0 formula-decl nil vectors_3D nil) (scal_assoc formula-decl nil vectors_3D nil) (add_zero_right formula-decl nil vectors_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (vel_from_spd const-decl "Vect3" lines_3D nil) (on_line? const-decl "bool" lines_3D nil)) shostak)) (test4 0 (test4-2 nil 3306085315 ("" (skosimp*) (("" (expand "on_line?") (("" (expand "gen_line_spd") (("" (expand "vel_from_spd") (("" (inst + "dist(p1!1,p2!1)/s!1") (("" (apply-extensionality 2 :hide? t) (("1" (expand "+") (("1" (grind :exclude "dist") nil nil)) nil) ("2" (grind :exclude "dist") nil nil) ("3" (grind :exclude "dist") nil nil) ("4" (flatten) (("4" (rewrite "dist_eq_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_3D nil) (vel_from_spd const-decl "Vect3" lines_3D nil) (- const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil) (p2!1 skolem-const-decl "Vect3" lines_3D nil) (p1!1 skolem-const-decl "Vect3" lines_3D nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (scal_assoc formula-decl nil vectors_3D nil) (scal_1 formula-decl nil vectors_3D 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) (dist_eq_0 formula-decl nil distance_3D 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) (dist const-decl "nnreal" distance_3D nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (gen_line_spd const-decl "Line" lines_3D nil)) nil) (test4-1 nil 3256559702 ("" (skosimp*) (("" (expand "on_line?") (("" (expand "gen_line_spd") (("" (expand "vel_from_spd") (("" (inst + "dist(p1!1,p2!1)/s!1") (("" (apply-extensionality 1 :hide? t) (("1" (expand "+") (("1" (grind :exclude "dist") nil nil)) nil) ("2" (grind :exclude "dist") nil nil) ("3" (grind :exclude "dist") nil nil) ("4" (flatten) (("4" (rewrite "dist_eq_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_3D nil) (norm const-decl "nnreal" vectors_3D nil) (* const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D nil)) shostak)) (vel_from_spd_on_line 0 (vel_from_spd_on_line-1 nil 3256567691 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (expand "on_line?") (("" (expand "vel_from_spd") (("" (assert) (("" (lift-if) (("" (ground) (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (rewrite "dist_eq_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" distance_3D nil) (scal_assoc formula-decl nil vectors_3D nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (scal_zero formula-decl nil vectors_3D nil) (add_zero_right formula-decl nil vectors_3D nil) (scal_0 formula-decl nil vectors_3D 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (Vect3 type-eq-decl nil vectors_3D_def nil) (nnreal type-eq-decl nil real_types nil) (dist const-decl "nnreal" distance_3D nil) (vel_from_spd const-decl "Vect3" lines_3D nil)) shostak))) ¤ Dauer der Verarbeitung: 0.19 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 |
