|
(parallel_2D
(abs_det_par 0
(abs_det_par-1 nil 3430221694
("" (skeep)
(("" (case-replace "det(nzu, nzv) = 0 IFF sq(det(nzu, nzv)) = 0")
(("1" (hide -1)
(("1" (rewrite "sq_det")
(("1" (rewrite "sq_norm" :dir rl)
(("1" (rewrite "sq_norm" :dir rl)
(("1" (split)
(("1" (flatten) (("1" (grind) nil nil)) nil)
("2" (flatten)
(("2" (lemma "sq_eq_abs")
(("2" (inst -1 "^(nzu)*^(nzv)" "1")
(("2" (rewrite "sq_1")
(("2" (expand "abs" -1 2)
(("2" (replaces -1 :dir rl)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "sq_eq_0") (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def 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)
(det const-decl "real" det_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(sq_det formula-decl nil det_2D nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(Normalized type-eq-decl nil vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(sq_1 formula-decl nil sq "reals/")
(sq_eq_abs formula-decl nil sq "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(^ const-decl "Normalized" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(sq_norm formula-decl nil vectors_2D nil)
(sq_eq_0 formula-decl nil sq "reals/"))
nil))
(parallel_dot_1 0
(parallel_dot_1-2 nil 3430222307
("" (skeep)
(("" (expand "parallel?")
(("" (prop)
(("1" (skeep -1)
(("1" (replaces -1)
(("1" (lemma "norm_scal")
(("1" (inst?)
(("1" (expand "^")
(("1" (replaces -1)
(("1" (rewrite "dot_scal_canon")
(("1" (cross-mult 1)
(("1" (lemma "dot_sq_norm")
(("1" (inst -1 "nzv")
(("1" (replaces -1)
(("1"
(expand "sq")
(("1"
(rewrite "abs_div")
(("1"
(rewrite "abs_mult")
(("1"
(rewrite "abs_abs")
(("1"
(rewrite "abs_div")
(("1"
(rewrite "abs_mult")
(("1"
(rewrite "abs_mult")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "abs_det_par")
(("2" (inst?)
(("2" (assert)
(("2" (hide -2)
(("2" (expand "det")
(("2" (typepred "nzv")
(("2" (rewrite "nzv_xy_neq_0")
(("2" (expand "*")
(("2" (typepred "nzu")
(("2" (rewrite "nzv_xy_neq_0")
(("2" (split -2)
(("1"
(inst 1 "nzu`x/nzv`x")
(("1" (decompose-equality 1) nil nil)
("2" (grind-reals) nil nil))
nil)
("2"
(inst 1 "nzu`y/nzv`y")
(("1" (decompose-equality 1) nil nil)
("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((parallel? const-decl "bool" vectors_2D nil)
(abs_det_par formula-decl nil parallel_2D nil)
(det const-decl "real" det_2D nil)
(nzv_xy_neq_0 formula-decl nil vectors_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzu skolem-const-decl "Nz_vector" parallel_2D nil)
(nzv skolem-const-decl "Nz_vector" parallel_2D nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(norm_scal formula-decl nil vectors_2D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(^ const-decl "Normalized" vectors_2D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(dot_scal_canon formula-decl nil vectors_2D 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 "[numfield, numfield -> 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)
(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_2D nil)
(* const-decl "Vector" vectors_2D nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(dot_sq_norm formula-decl nil vectors_2D nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(abs_div formula-decl nil real_props nil)
(abs_abs formula-decl nil real_props nil)
(abs_mult formula-decl nil real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(times_div2 formula-decl nil real_props nil)
(* const-decl "real" vectors_2D nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div1 formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D 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))
nil)
(parallel_dot_1-1 nil 3430221756
("" (skeep)
(("" (prop)
(("1" (expand "paral?")
(("1" (skeep -1)
(("1" (replaces -1)
(("1" (lemma "norm_scal")
(("1" (inst?)
(("1" (expand "^")
(("1" (replaces -1)
(("1" (rewrite "dot_scal_canon")
(("1" (cross-mult 1)
(("1" (lemma "dot_sq_norm")
(("1" (inst -1 "nzv")
(("1" (replaces -1)
(("1"
(expand "sq")
(("1"
(rewrite "abs_div")
(("1"
(rewrite "abs_mult")
(("1"
(rewrite "abs_abs")
(("1"
(rewrite "abs_div")
(("1"
(rewrite "abs_mult")
(("1"
(rewrite "abs_mult")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "paral?")
(("2" (lemma "abs_det_par")
(("2" (inst?)
(("2" (assert)
(("2" (hide -2)
(("2" (expand "det")
(("2" (typepred "nzv")
(("2" (flatten)
(("2" (rewrite "norm_xy_eq_0")
(("2" (typepred "nzu")
(("2" (flatten)
(("2" (rewrite "norm_xy_eq_0")
(("2"
(expand "*")
(("2"
(split 2)
(("1"
(inst 3 "nzu`x/nzv`x")
(("1"
(decompose-equality 3)
nil
nil)
("2" (grind-reals) nil nil)
("3" (grind-reals) nil nil))
nil)
("2"
(inst 3 "nzu`y/nzv`y")
(("1"
(decompose-equality 3)
nil
nil)
("2" (grind-reals) nil nil)
("3" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_scal formula-decl nil vectors_2D nil)
(^ const-decl "Normalized" vectors_2D nil)
(dot_scal_canon formula-decl nil vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(dot_sq_norm formula-decl nil vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(* const-decl "real" vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(det const-decl "real" det_2D nil)
(norm_xy_eq_0 formula-decl nil vectors_2D nil))
nil))
(parallel_det_0 0
(parallel_det_0-1 nil 3430222402
("" (skeep)
(("" (lemma "parallel_dot_1")
(("" (inst?)
(("" (lemma "abs_det_par")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((parallel_dot_1 formula-decl nil parallel_2D nil)
(abs_det_par formula-decl nil parallel_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(dot_perpL_parallel 0
(dot_perpL_parallel-1 nil 3476105424
("" (skosimp*)
(("" (expand "parallel?")
(("" (expand "perpL")
(("" (expand "*")
(("" (typepred "nzu!1")
(("" (typepred "nzv!1")
(("" (flatten)
(("" (case-replace "nzv!1`y = 0")
(("1" (assert)
(("1" (mult-cases -2)
(("1" (inst + "-nzu!1`y/nzv!1`x")
(("1" (assert) nil nil)
("2" (assert)
(("2" (flatten)
(("2" (cross-mult -1)
(("2"
(reveal 1)
(("2"
(apply-extensionality 2 :hide? t)
(("2"
(apply-extensionality 3 :hide? t)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3" (flatten)
(("3" (apply-extensionality :hide? t) nil
nil))
nil))
nil)
("2" (apply-extensionality 1 :hide? t) nil nil))
nil))
nil)
("2" (case-replace "nzv!1`x = 0")
(("1" (assert)
(("1" (mult-cases -2)
(("1" (inst + "nzu!1`x/nzv!1`y")
(("1" (assert) nil nil)
("2" (flatten)
(("2" (cross-mult -1)
(("2"
(assert)
(("2"
(apply-extensionality 2 :hide? t)
(("2"
(apply-extensionality 3 :hide? t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "-nzu!1`y/nzv!1`x")
(("1" (assert) nil nil)
("2" (flatten)
(("2" (cross-mult -1)
(("2" (assert)
(("2" (case-replace "nzu!1`y = 0")
(("1"
(assert)
(("1"
(apply-extensionality 4 :hide? t)
nil
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((parallel? const-decl "bool" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(zero_times3 formula-decl nil real_props 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)
(div_cancel3 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nzu!1 skolem-const-decl "Nz_vector" parallel_2D nil)
(- const-decl "[numfield -> numfield]" number_fields 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)
(nzv!1 skolem-const-decl "Nz_vector" parallel_2D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_even_is_even application-judgement "even_int" integers 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)
(Vector type-eq-decl nil vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil))
nil))
(dot_perpR_parallel 0
(dot_perpR_parallel-1 nil 3476105449
("" (skosimp*)
(("" (expand "parallel?")
(("" (expand "perpR")
(("" (expand "*")
(("" (typepred "nzu!1")
(("" (typepred "nzv!1")
(("" (flatten)
(("" (case-replace "nzv!1`y = 0")
(("1" (assert)
(("1" (mult-cases -2)
(("1" (inst + "nzu!1`y/nzv!1`x")
(("1" (assert) nil nil)
("2" (flatten)
(("2" (cross-mult -1)
(("2" (assert)
(("2"
(apply-extensionality 1 :hide? t)
(("2"
(apply-extensionality 2 :hide? t)
nil
nil))
nil))
nil))
nil))
nil)
("3" (assert)
(("3" (flatten)
(("3" (apply-extensionality 1 :hide? t) nil
nil))
nil))
nil))
nil)
("2" (apply-extensionality 1 :hide? t) nil nil))
nil))
nil)
("2" (case-replace "nzv!1`x = 0")
(("1" (assert)
(("1" (mult-cases -2)
(("1" (inst + "-nzu!1`x/nzv!1`y")
(("1" (assert) nil nil)
("2" (flatten)
(("2" (cross-mult -1)
(("2"
(assert)
(("2"
(apply-extensionality 2 :hide? t)
(("2"
(apply-extensionality 3 :hide? t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "nzu!1`y/nzv!1`x")
(("1" (assert) nil nil)
("2" (flatten)
(("2" (cross-mult -1)
(("2" (assert)
(("2" (apply-extensionality 3 :hide? t)
(("1"
(apply-extensionality 4 :hide? t)
nil
nil)
("2"
(apply-extensionality 4 :hide? t)
nil
nil))
nil))
nil))
nil))
nil)
("3" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((parallel? const-decl "bool" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(zero_times3 formula-decl nil real_props 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)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_cancel3 formula-decl nil real_props nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nzu!1 skolem-const-decl "Nz_vector" parallel_2D 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)
(nzv!1 skolem-const-decl "Nz_vector" parallel_2D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields 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)
(Vector type-eq-decl nil vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil))
nil)))
¤ Dauer der Verarbeitung: 0.34 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.
|
