| products/sources/formale Sprachen/PVS/vectors/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: lines.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(lines
(line_from_TCC1 0 (line_from_TCC1-1 nil 3306081175 ("" (skosimp*) (("" (typepred "p2!1") (("" (flatten) (("" (expand "vec_from") (("" (lemma "sub_eq_zero[n]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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 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) (number nonempty-type-decl nil numbers 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 "Vector[n]" lines nil) (sub_eq_zero formula-decl nil vectors 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 "Vector[n]" lines nil) (sub_eq_args formula-decl nil vectors nil)) nil)) (vel_from_tm_TCC1 0 (vel_from_tm_TCC1-1 nil 3255275743 ("" (inst + "(LAMBDA p1,p2,t: (1/t)*(p2-p1))") (("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (n formal-const-decl "posnat" lines nil) (Index type-eq-decl nil vectors nil) (- const-decl "real" vectors 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 nil) (+ const-decl "real" vectors nil) (Vector type-eq-decl nil vectors nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (scal_assoc formula-decl nil vectors nil) (scal_1 formula-decl nil vectors nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (line_from_tm_TCC1 0 (line_from_tm_TCC1-2 nil 3430837655 ("" (skosimp* :preds? t) (("" (expand "vel_from_tm") (("" (lemma "scal_eq_zero[n]") (("" (inst?) (("" (assert) (("" (rewrite "sub_eq_zero") nil nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines 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 "real" vectors nil) (sub_eq_zero formula-decl nil vectors nil) (scal_eq_zero formula-decl nil vectors 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (n formal-const-decl "posnat" lines nil) (Index type-eq-decl nil vectors nil) (Vector type-eq-decl nil vectors nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) nil) (line_from_tm_TCC1-1 nil 3306081175 ("" (skosimp*) (("" (typepred "p2!1") (("" (flatten) (("" (expand "vel_from_tm") (("" (assert) (("" (rewrite "norm_scal") (("" (mult-cases -1) (("" (rewrite "norm_eq_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (norm_scal formula-decl nil vectors nil) (- const-decl "real" vectors nil) (sub_eq_zero formula-decl nil vectors nil) (norm_zero formula-decl nil vectors nil) (norm const-decl "nnreal" vectors 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)") (("1" (replace -1 +) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (* const-decl "Vector" vectors nil) (+ const-decl "real" vectors nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (scal_zero formula-decl nil vectors nil) (add_zero_right formula-decl nil vectors nil) (zero const-decl "Vector" vectors 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) (("" (expand "*" +) (("" (cross-mult 1) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (* const-decl "Vector" vectors nil) (+ const-decl "real" vectors nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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 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) (number nonempty-type-decl nil numbers 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 "real" vectors nil)) nil)) (vel_from_tm_eq_args 0 (vel_from_tm_eq_args-1 nil 3306085151 ("" (skosimp*) (("" (assert) (("" (expand "vel_from_tm") (("" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil) ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (Vector type-eq-decl nil vectors nil) (* const-decl "Vector" vectors nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (- const-decl "real" vectors nil) (zero const-decl "Vector" vectors nil) (comp_zero formula-decl nil vectors nil) (scal_zero formula-decl nil vectors nil) (sub_eq_args formula-decl nil vectors 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (n formal-const-decl "posnat" lines nil) (Index type-eq-decl nil vectors nil) (vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines nil)) shostak)) (vel_from_tm_length 0 (vel_from_tm_length-1 nil 3255275743 ("" (skosimp*) (("" (lemma "vel_from_tm_rew") (("" (inst?) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (assert) (("" (rewrite "norm_scal") (("" (rewrite "sq_times") (("" (rewrite "dist_norm[n]" :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" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_tm_rew formula-decl nil lines 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) (norm_scal formula-decl nil vectors 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 "real" vectors nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (dist_norm formula-decl nil distance nil) (sq_dist const-decl "nnreal" distance nil) (sq_sqrt formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_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_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (sigma_nnreal application-judgement "nnreal" vectors 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) (sq_dist_sym formula-decl nil distance nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sq const-decl "nonneg_real" sq "reals/") (dist const-decl "nnreal" distance nil) (sq_abs formula-decl nil sq "reals/") (norm const-decl "nnreal" vectors nil) (nnreal type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq_times formula-decl nil sq "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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 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)) nil)) (vel_from_spd_TCC1 0 (vel_from_spd_TCC1-1 nil 3255275743 ("" (skosimp*) (("" (assert) (("" (lemma "dist_eq_0[n]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (Index type-eq-decl nil vectors nil) (Vector type-eq-decl nil vectors nil) (dist_eq_0 formula-decl nil distance 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (n formal-const-decl "posnat" lines 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 nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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 nil)) shostak)) (vel_from_spd_lem 0 (vel_from_spd_lem-3 nil 3256922924 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (assert) (("" (rewrite "vel_from_tm_rew") (("1" (assert) nil nil) ("2" (hide 3) (("2" (lemma "dist_eq_0[n]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_spd const-decl "Vector[n]" lines nil) (vel_from_tm_rew formula-decl nil lines 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (n formal-const-decl "posnat" lines nil) (Index type-eq-decl nil vectors nil) (Vector type-eq-decl nil vectors 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) (nnreal type-eq-decl nil real_types nil) (dist const-decl "nnreal" distance nil) (nonneg_real nonempty-type-eq-decl nil real_types 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)) nil) (vel_from_spd_lem-2 nil 3256922896 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (assert) (("" (rewrite "vel_from_tm_rewn[n]") (("1" (assert) nil) ("2" (hide 3) (("2" (lemma "dist_eq_0") (("2" (inst?) (("2" (assert) nil)))))))))))))) nil) nil nil) (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) nil shostak)) (vel_from_spd_norm_TCC1 0 (vel_from_spd_norm_TCC1-1 nil 3255866120 ("" (skeep) (("" (expand "nz_vector?") (("" (lemma "sub_eq_zero[n]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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 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) (sub_eq_zero formula-decl nil vectors nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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 nil) (dist_norm formula-decl nil distance nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (Index type-eq-decl nil vectors nil) (Vector type-eq-decl nil vectors 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (n formal-const-decl "posnat" lines nil) (norm_sym formula-decl nil vectors nil) (scal_assoc formula-decl nil vectors 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 "Vector[n]" lines nil)) shostak)) (gen_speed_TCC1 0 (gen_speed_TCC1-1 nil 3255275743 ("" (inst 1 "lambda (d: [Vector[n], Vector[n], posreal]) : 1 / d`3 * dist[n](d`1, d`2)") nil nil) ((dist const-decl "nnreal" distance nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (gen_line_spd_TCC1 0 (gen_line_spd_TCC1-3 nil 3430838803 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (name-replace "AA" "s!1 / dist(p1!1, p2!1)") (("" (lemma "scal_eq_zero[n]") (("" (inst?) (("" (assert) (("" (rewrite "sub_eq_zero") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vel_from_spd const-decl "Vector[n]" lines nil) (scal_eq_zero formula-decl nil vectors nil) (sub_eq_zero formula-decl nil vectors nil) (- const-decl "real" vectors nil) (nzreal nonempty-type-eq-decl nil reals nil) (dist const-decl "nnreal" distance nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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-2 nil 3430838563 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (typepred "p2!1") (("" (flatten) (("" (grind :exclude "dist") (("" (name-replace "AA" "s!1 / dist(p1!1, p2!1)") (("" (lemma "scal_eq_zero[n]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "real" vectors nil) (sub_eq_zero formula-decl nil vectors nil) (scal_eq_zero formula-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (Vector type-eq-decl nil vectors nil)) nil) (gen_line_spd_TCC1-1 nil 3303642628 ("" (skosimp*) (("" (expand "vel_from_spd") (("" (rewrite "norm_scal") (("1" (typepred "p2!1") (("1" (flatten) (("1" (mult-cases -1) (("1" (rewrite "norm_eq_0") nil nil) ("2" (rewrite "dist_eq_0") nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "dist_eq_0") nil nil)) nil)) nil)) nil)) nil) ((norm const-decl "nnreal" vectors nil) (norm_zero formula-decl nil vectors nil) (sub_eq_zero formula-decl nil vectors nil) (- const-decl "real" vectors nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (norm_scal formula-decl nil vectors nil)) nil)) (test1_TCC1 0 (test1_TCC1-1 nil 3306085048 ("" (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 nil) (vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines nil) (scal_0 formula-decl nil vectors nil) (scal_assoc formula-decl nil vectors nil) (add_zero_right formula-decl nil vectors 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 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) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines nil) (vel_from_tm const-decl "{v | p2 = p1 + t * v}" lines 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 nil) (scal_assoc formula-decl nil vectors nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (- const-decl "real" vectors nil) (+ const-decl "real" vectors nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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 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 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 nil) (scal_assoc formula-decl nil vectors nil) (add_zero_right formula-decl nil vectors 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 "Vector[n]" lines nil) (on_line? const-decl "bool" lines nil)) shostak)) (test4 0 (test4-2 nil 3256922949 ("" (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" (grind :exclude "dist") nil nil) ("2" (flatten) (("2" (rewrite "dist_eq_0[n]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines nil) (vel_from_spd const-decl "Vector[n]" lines nil) (- const-decl "real" vectors nil) (zero const-decl "Vector" vectors nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "Vector" vectors nil) (+ const-decl "real" vectors nil) (p2!1 skolem-const-decl "Vector[n]" lines nil) (p1!1 skolem-const-decl "Vector[n]" lines 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 nil) (scal_1 formula-decl nil vectors nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (dist_eq_0 formula-decl nil distance nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (dist const-decl "nnreal" distance nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors nil) (Index type-eq-decl nil vectors nil) (n formal-const-decl "posnat" lines nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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, 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 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" (grind) nil nil) ("2" (grind) nil nil) ("3" (flatten) (("3" (rewrite "dist_eq_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "Vector" vectors nil) (zero const-decl "Vector" vectors nil) (norm const-decl "nnreal" vectors nil) (* const-decl "Vector" vectors nil) (+ const-decl "real" vectors nil) (Vector type-eq-decl nil vectors nil) (sq const-decl "nonneg_real" sq "reals/")) 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 nil) (scal_assoc formula-decl nil vectors 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 nil) (add_zero_right formula-decl nil vectors nil) (scal_0 formula-decl nil vectors 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (n formal-const-decl "posnat" lines nil) (Index type-eq-decl nil vectors nil) (Vector type-eq-decl nil vectors nil) (nnreal type-eq-decl nil real_types nil) (dist const-decl "nnreal" distance nil) (vel_from_spd const-decl "Vector[n]" lines nil)) shostak))) ¤ Dauer der Verarbeitung: 0.25 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 |
