|
(basis_2D
(orthogonal_basis_TCC1 0
(orthogonal_basis_TCC1-1 nil 3476700907
("" (skosimp*)
(("" (expand "orthogonal?")
(("" (lemma "sqv_eq_0")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((orthogonal? const-decl "bool" vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(sqv_eq_0 formula-decl nil vectors_2D nil))
nil))
(orthogonal_basis_TCC2 0
(orthogonal_basis_TCC2-1 nil 3476700907
("" (skosimp*)
(("" (lemma "sqv_eq_0") (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil)
((sqv_eq_0 formula-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(orthogonal_basis 0
(orthogonal_basis-1 nil 3476701148
("" (skosimp*)
(("" (lemma "posreal_times_posreal_is_posreal")
(("" (inst - "sqv(e1!1)" "sqv(e2!1)")
(("1" (expand "orthogonal?")
(("1"
(case "sqv(e1!1)*sqv(e2!1)*w!1 = (w!1*e1!1*sqv(e2!1))*e1!1 + (w!1*e2!1*sqv(e1!1))*e2!1")
(("1" (decompose-equality 3)
(("1" (mult-by 1 "sqv(e1!1)*sqv(e2!1)")
(("1" (grind :exclude "sqv") nil nil)) nil)
("2" (mult-by 1 "sqv(e1!1)*sqv(e2!1)")
(("2" (grind :exclude "sqv") nil nil)) nil))
nil)
("2" (hide 4) (("2" (grind) nil nil)) nil))
nil))
nil)
("2" (hide 4)
(("2" (lemma "sqv_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (lemma "sqv_eq_0")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(sqv_eq_0 formula-decl nil vectors_2D nil)
(orthogonal? const-decl "bool" vectors_2D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(* const-decl "real" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "Vector" vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(e2!1 skolem-const-decl "Vect2" basis_2D 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)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(e1!1 skolem-const-decl "Vect2" basis_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(orthonormal_basis 0
(orthonormal_basis-1 nil 3476547366
("" (skosimp*)
(("" (expand "orthonormal?")
(("" (flatten)
(("" (lemma "orthogonal_basis")
(("" (inst - "e1!1" "e2!1" "w!1")
(("" (assert)
(("" (case-replace "sqv(e1!1) = 1")
(("1" (case-replace "sqv(e2!1) = 1")
(("1" (assert) nil nil)
("2" (hide -2 -3 4)
(("2" (expand "norm")
(("2" (lemma "sqrt_eq")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -2 -4 4)
(("2" (expand "norm")
(("2" (lemma "sqrt_eq")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((orthonormal? const-decl "bool" basis_2D nil)
(orthogonal_basis formula-decl nil basis_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal 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)
(Vector type-eq-decl nil vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(basis_two_dot_zero 0
(basis_two_dot_zero-1 nil 3481475499
("" (skeep)
(("" (case "orthogonal?(w,e1)")
(("1" (lemma "orthogonal_basis")
(("1" (inst - "w" "e1" "e2")
(("1" (assert)
(("1" (copy -4)
(("1" (case "e2*w = 0")
(("1" (replace -3 -2)
(("1" (replace -1)
(("1" (assert)
(("1" (inst + "(e2*e1)/sqv(e1)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide-all-but (-5 1)) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "orthogonal?") (("2" (propax) nil nil)) nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def nil)
(orthogonal? const-decl "bool" vectors_2D nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(scal_0 formula-decl nil vectors_2D nil)
(add_zero_left formula-decl nil vectors_2D nil)
(dot_scal_right formula-decl nil vectors_2D 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities 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 "real" vectors_2D nil)
(orthogonal_basis formula-decl nil basis_2D nil))
shostak))
(basis_add 0
(basis_add-1 nil 3476530662
("" (skosimp*) (("" (grind) nil nil)) 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_2D nil)
(* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil))
shostak))
(basis_sub 0
(basis_sub-1 nil 3476530735
("" (skosimp*) (("" (grind) nil nil)) nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil))
shostak))
(basis_sqv 0
(basis_sqv-1 nil 3476707207
("" (skeep)
(("" (replace -2)
(("" (hide -2)
(("" (rewrite "sqv_add")
(("" (expand "orthonormal?")
(("" (flatten)
(("" (expand "orthogonal?")
(("" (replace -1)
(("" (assert)
(("" (rewrite "sqv_scal")
(("" (rewrite "sqv_scal")
(("" (case-replace "sqv(e1) = 1")
(("1" (case-replace "sqv(e2) = 1")
(("1" (assert) nil nil)
("2" (hide -1 -2 4)
(("2"
(expand "norm")
(("2"
(lemma "sqrt_eq")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -3 4)
(("2" (expand "norm")
(("2"
(lemma "sqrt_eq")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqv_add formula-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D 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 "Vector" vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(scal_assoc formula-decl nil vectors_2D nil)
(dot_scal_right formula-decl nil vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(sqv_scal formula-decl nil vectors_2D nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(orthogonal? const-decl "bool" vectors_2D nil)
(orthonormal? const-decl "bool" basis_2D nil))
nil))
(basis_dot 0
(basis_dot-1 nil 3477648577
("" (skosimp*)
(("" (expand "orthonormal?")
(("" (flatten)
(("" (expand "orthogonal?")
(("" (assert)
(("" (lemma "dot_add_left")
((""
(inst - "(c!1 * e1!1 + d!1 * e2!1)" "a!1 * e1!1"
"b!1 * e2!1")
(("" (hide 2)
(("" (rewrite "add_dot_add")
(("" (hide -1)
(("" (replace -1)
(("" (assert)
(("" (case-replace "e1!1 * e1!1 = 1")
(("1" (case-replace "e2!1 * e2!1 = 1")
(("1"
(assert)
(("1"
(hide -1 -2)
(("1"
(lemma "dot_comm")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 -2 3)
(("2"
(expand "norm")
(("2"
(expand "sqv")
(("2"
(lemma "sqrt_eq")
(("2"
(inst?)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -3 3)
(("2"
(expand "norm")
(("2"
(expand "sqv")
(("2"
(lemma "sqrt_eq")
(("2"
(inst?)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((orthonormal? const-decl "bool" basis_2D nil)
(orthogonal? const-decl "bool" vectors_2D nil)
(dot_add_left formula-decl nil vectors_2D nil)
(e1!1 skolem-const-decl "Vect2" basis_2D nil)
(dot_comm formula-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(e2!1 skolem-const-decl "Vect2" basis_2D nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqv const-decl "nnreal" vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "real" vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(dot_scal_right formula-decl nil vectors_2D nil)
(add_dot_add formula-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(* const-decl "Vector" vectors_2D 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_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(basis_perpR 0
(basis_perpR-1 nil 3477648600
("" (skeep)
(("" (assert)
(("" (rewrite "perpR_add")
(("" (rewrite "perpR_scal")
(("" (rewrite "perpR_scal")
(("" (assert) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((perpR_scal formula-decl nil perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals 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)
(- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(* const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D 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)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil)
(perpR_add formula-decl nil perpendicular_2D nil))
nil))
(vh_vp_orthon 0
(vh_vp_orthon-1 nil 3476551747
("" (skosimp*)
(("" (skoletin 1)
(("" (skoletin 1)
(("" (expand "^")
(("" (expand "perpR")
(("" (expand "orthonormal?")
(("" (typepred "v!1")
(("" (flatten)
(("" (split +)
(("1" (expand "orthogonal?")
(("1" (grind) nil nil)) nil)
("2" (flatten)
(("2" (replace -1) (("2" (assert) nil nil)) nil))
nil)
("3" (replace -2)
(("3" (rewrite "norm_scal")
(("3" (expand "abs") (("3" (assert) nil nil))
nil))
nil))
nil)
("4" (flatten) (("4" (assert) nil nil)) nil)
("5" (replace -1)
(("5" (replace -2)
(("5" (hide -)
(("5" (lemma "norm_scal")
(("5" (inst - "1 / norm(v!1)" "perpR(v!1)")
(("5"
(case-replace
"norm(perpR(v!1)) = norm(v!1)")
(("1"
(hide -1)
(("1"
(expand "perpR")
(("1"
(expand "*")
(("1"
(assert)
(("1"
(expand "abs")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 2)
(("2"
(expand "norm")
(("2"
(lemma "sqrt_eq")
(("2"
(inst?)
(("2"
(flatten)
(("2"
(hide -1)
(("2"
(split -1)
(("1" (propax) nil nil)
("2"
(hide 2)
(("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))
nil))
nil)
((IFF const-decl "[bool, bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(Normalized type-eq-decl nil vectors_2D nil)
(^ const-decl "Normalized" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(orthonormal? const-decl "bool" basis_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(norm_scal 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)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D nil)
(orthogonal? const-decl "bool" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(orthogonal_basis_sqv 0
(orthogonal_basis_sqv-1 nil 3481620928
("" (skeep)
(("" (replace -2)
(("" (expand "sqv")
(("" (rewrite "dot_add_left")
(("" (rewrite "dot_add_right")
(("" (expand "orthogonal?")
(("" (case "e2*e1 = 0")
(("1" (grind) nil nil)
("2" (hide-all-but (-1 1)) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dot_add_left formula-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D 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 "Vector" vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(orthogonal? const-decl "bool" vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(* const-decl "real" vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(dot_scal_right formula-decl nil vectors_2D nil)
(dot_add_right formula-decl nil vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil))
shostak))
(orthonormal_basis_sqv 0
(orthonormal_basis_sqv-1 nil 3481621043
("" (skeep)
(("" (lemma "orthogonal_basis_sqv")
(("" (inst?)
(("" (assert)
(("" (split -)
(("1" (case "sqv(e1) = 1 AND sqv(e2) = 1")
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (expand "orthonormal?")
(("2" (flatten)
(("2" (lemma "sqrt_sqv_norm")
(("2" (inst-cp - "e1")
(("2" (inst - "e2") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "orthonormal?") (("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((orthogonal_basis_sqv formula-decl nil basis_2D nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(sqrt_sqv_norm formula-decl nil vectors_2D nil)
(orthonormal? const-decl "bool" basis_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def 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))
shostak))
(orthogonal_basis_norm 0
(orthogonal_basis_norm-1 nil 3481623256
("" (skeep)
(("" (lemma "orthogonal_basis_sqv")
(("" (inst?)
(("" (assert)
(("" (lemma "sqrt_sqv_norm")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((orthogonal_basis_sqv formula-decl nil basis_2D nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Vector type-eq-decl nil vectors_2D nil)
(sqrt_sqv_norm formula-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def 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))
shostak))
(orthonormal_basis_norm 0
(orthonormal_basis_norm-1 nil 3481623341
("" (skeep)
(("" (lemma "orthonormal_basis_sqv")
(("" (inst?)
(("" (assert)
(("" (lemma "sqrt_sqv_norm")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((orthonormal_basis_sqv formula-decl nil basis_2D nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Vector type-eq-decl nil vectors_2D nil)
(sqrt_sqv_norm formula-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def 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))
shostak))
(orthogonal_basis_norm_ge 0
(orthogonal_basis_norm_ge-1 nil 3481623463
("" (skeep)
(("" (lemma "orthogonal_basis_sqv")
(("" (inst?)
(("" (assert)
(("" (lemma "sq_ge")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (rewrite "sq_times")
((""
(case "FORALL (pz: Vect2): sq(norm(pz)) = sqv(pz)")
(("1" (inst-cp - "w")
(("1" (inst - "e1")
(("1" (replace -1)
(("1" (replace -2) (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (lemma "sqrt_sqv_norm")
(("2" (inst - "pz")
(("2" (replace -1 :dir rl)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((orthogonal_basis_sqv formula-decl nil basis_2D nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D nil)
(sqrt_sqv_norm formula-decl nil vectors_2D nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_abs formula-decl nil sq "reals/")
(sq_times formula-decl nil sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_ge formula-decl nil sq "reals/")
(Vect2 type-eq-decl nil vectors_2D_def 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))
shostak))
(orthonormal_basis_norm_ge 0
(orthonormal_basis_norm_ge-1 nil 3481623598
("" (skeep)
(("" (lemma "orthogonal_basis_norm_ge")
(("" (inst?)
(("" (assert)
(("" (split -)
(("1" (expand "orthonormal?")
(("1" (flatten) (("1" (assert) nil nil)) nil)) nil)
("2" (expand "orthogonal?")
(("2" (expand "orthonormal?")
(("2" (flatten)
(("2" (expand "orthogonal?") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((orthogonal_basis_norm_ge formula-decl nil basis_2D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(orthogonal? const-decl "bool" vectors_2D nil)
(orthonormal? const-decl "bool" basis_2D nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def 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))
shostak))
(orthogonal_basis_dot 0
(orthogonal_basis_dot-1 nil 3529142458
("" (skeep)
(("" (expand "orthogonal?")
(("" (mult-by -1 "(a1*b2 + b1*a2)")
(("" (replaces -2)
(("" (replaces -2) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((orthogonal? const-decl "bool" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(real_times_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 "[numfield, numfield -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(orthonormal_basis_dot 0
(orthonormal_basis_dot-1 nil 3529142540
("" (skeep)
(("" (lemma "orthogonal_basis_dot")
(("" (inst - "a1" "a2" "b1" "b2" "e1" "e2" "w1" "w2")
(("" (assert)
(("" (split -)
(("1" (case "sqv(e1) = 1 AND sqv(e2) = 1")
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (hide-all-but (-2 1))
(("2" (expand "orthonormal?")
(("2" (assert)
(("2"
(case "FORALL (egrtzp:Vect2): norm(egrtzp) = 1 IMPLIES sqv(egrtzp) = 1")
(("1" (flatten)
(("1" (inst-cp - "e1")
(("1" (inst - "e2") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (skeep)
(("2" (rewrite "sq_eq" -1 :dir rl)
(("2" (rewrite "sq_norm") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "orthonormal?") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((orthogonal_basis_dot formula-decl nil basis_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(orthonormal? const-decl "bool" basis_2D nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(norm const-decl "nnreal" vectors_2D nil)
(sq_norm formula-decl nil vectors_2D nil)
(sq_1 formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_eq formula-decl nil sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def 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))
shostak)))
¤ Dauer der Verarbeitung: 0.64 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.
|
