Quelle lines_3D.prf
Sprache: unbekannt
|
|
(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)))
[ Verzeichnis aufwärts0.30unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
2026-03-28
|
