|
(parallel_3D
(abs_cross_par 0
(abs_cross_par-1 nil 3431708775
("" (skosimp*)
(("" (rewrite "sq_dot_eq_0" :dir rl)
(("" (rewrite "Lagrange_Identity")
(("" (expand "^")
(("" (real-props)
(("" (expand "abs" 1 (2 3))
(("" (real-props)
(("" (expand "norm")
(("" (rewrite "sqrt_times" :dir rl)
(("" (ground)
(("1"
(transform-both -1 "sq(%1)" nil (replace -1))
(("1" (rewrite "sq_sqrt")
(("1" (rewrite "sq_abs")
(("1" (grind) nil nil)) nil))
nil))
nil)
("2" (isolate -1 l 1)
(("2" (expand "sqv")
(("2" (replace -1 :hide? t)
(("2" (assert)
(("2"
(lemma "dot_comm")
(("2"
(inst - "nzv!1" "nzu!1")
(("2"
(replace -1 :hide? t)
(("2"
(expand "abs")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(use "sqrt_sq_neg")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_dot_eq_0 formula-decl nil vectors_3D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_3D nil)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(cross const-decl "Vector" cross_3D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D nil)
(Nz_vector type-eq-decl nil vectors_3D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_3D nil)
(^ const-decl "Normalized" vectors_3D nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(norm const-decl "nnreal" vectors_3D nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq_abs formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq "reals/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_3D nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sqrt_square formula-decl nil sqrt "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(sqrt_sq_neg formula-decl nil sqrt "reals/")
(dot_comm formula-decl nil vectors_3D nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_3D nil)
(sqrt_times formula-decl nil sqrt "reals/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_3D nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_nzv application-judgement "Nz_vector" vectors_3D nil)
(div_times formula-decl nil real_props nil)
(times_div2 formula-decl nil real_props nil)
(dot_scal_canon formula-decl nil vectors_3D nil)
(abs_nat formula-decl nil abs_lems "reals/")
(abs_mult formula-decl nil real_props nil)
(abs_div formula-decl nil real_props nil)
(both_sides_times2 formula-decl nil real_props nil)
(div_cancel3 formula-decl nil real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Lagrange_Identity formula-decl nil cross_3D nil))
nil))
(parallel_dot_1 0
(parallel_dot_1-1 nil 3431442707
("" (skosimp*)
(("" (rewrite "abs_cross_par")
(("" (use "lin_indep_cross")
(("" (replace -1 :dir rl :hide? t)
(("" (expand "parallel?")
(("" (expand "linearly_dependent?")
(("" (ground)
(("1" (skosimp*)
(("1" (replace -1)
(("1" (inst 1 "1" "-nzk!1") (("1" (grind) nil nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (case "k1!1 = 0")
(("1" (replace -1 :hide? t)
(("1" (ground)
(("1" (typepred "nzv!1")
(("1" (flatten)
(("1" (grind)
(("1"
(rewrite "zero_times3")
(("1"
(rewrite "zero_times3")
(("1"
(rewrite "zero_times3")
(("1"
(apply-extensionality 1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "k2!1 = 0")
(("1" (replace -1 :hide? t)
(("1" (ground)
(("1" (typepred "nzu!1")
(("1" (flatten)
(("1"
(grind)
(("1"
(rewrite "zero_times3")
(("1"
(rewrite "zero_times3")
(("1"
(rewrite "zero_times3")
(("1"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "add_move_right")
(("2"
(equate "nzu!1" " (-k2!1/k1!1) * nzv!1" t)
(("1" (inst?) (("1" (grind) nil nil)) nil)
("2" (grind)
(("1" (apply-extensionality 1) nil nil)
("2" (apply-extensionality 1) nil nil))
nil)
("3" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_cross_par formula-decl nil parallel_3D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_3D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D nil)
(Nz_vector type-eq-decl nil vectors_3D nil)
(linearly_dependent? const-decl "bool" cross_3D nil)
(add_zero_right formula-decl nil vectors_3D nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(k1!1 skolem-const-decl "real" parallel_3D nil)
(k2!1 skolem-const-decl "real" parallel_3D nil)
(minus_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "Vector" vectors_3D nil)
(sub_zero_left formula-decl nil vectors_3D nil)
(add_move_right formula-decl nil vectors_3D nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(zero_times3 formula-decl nil real_props nil)
(scal_0 formula-decl nil vectors_3D nil)
(add_zero_left formula-decl nil vectors_3D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(+ const-decl "Vector" vectors_3D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nz_nzv application-judgement "Nz_vector" vectors_3D nil)
(parallel? const-decl "bool" vectors_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(lin_indep_cross formula-decl nil cross_3D nil))
shostak))
(parallel_cross_zero 0
(parallel_cross_zero-1 nil 3431342290
("" (skosimp*)
(("" (rewrite "parallel_dot_1")
(("" (rewrite "abs_cross_par") nil nil)) nil))
nil)
((parallel_dot_1 formula-decl nil parallel_3D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_3D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D nil)
(Nz_vector type-eq-decl nil vectors_3D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_cross_par formula-decl nil parallel_3D 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.
|
