Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
reduce_walks.prf
Sprache: Unknown
|
(vect3_basis
(vect3_orthog_toy_def 0
(vect3_orthog_toy_def-1 nil 3512138075 ("" (grind) nil nil)
((minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(zero const-decl "Vector" vectors_3D nil)
(/= const-decl "boolean" notequal nil)
(vect3_orthog_toy const-decl "Vect3" vect3_basis nil)
(* const-decl "real" vectors_3D nil)
(orthogonal? const-decl "bool" vectors_3D nil))
shostak))
(vect3_orthog_toz_def 0
(vect3_orthog_toz_def-1 nil 3512138242 ("" (grind) nil nil)
((/= const-decl "boolean" notequal nil)
(vect3_orthog_toy const-decl "Vect3" vect3_basis nil)
(cross const-decl "Vector" cross_3D nil)
(vect3_orthog_toz const-decl "Vect3" vect3_basis nil)
(* const-decl "real" vectors_3D nil)
(orthogonal? const-decl "bool" vectors_3D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(vect3_orthonorm_toy_TCC1 0
(vect3_orthonorm_toy_TCC1-1 nil 3512137853 ("" (subtype-tcc) nil 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_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(minus_real_is_real application-judgement "real" reals nil)
(/= const-decl "boolean" notequal nil)
(vect3_orthog_toy const-decl "Vect3" vect3_basis nil)
(zero const-decl "Vector" vectors_3D nil))
nil))
(vect3_orthonorm_toz_TCC1 0
(vect3_orthonorm_toz_TCC1-1 nil 3512137853
("" (skeep)
(("" (expand "vect3_orthog_toz")
(("" (lemma "lin_indep_cross")
(("" (inst?)
(("1" (assert)
(("1" (hide -2)
(("1"
(case "FORALL (w:Nz_vect3): linearly_dependent?(nzv,w) IMPLIES EXISTS (c:nzreal): nzv = c*w")
(("1" (inst?)
(("1" (assert)
(("1" (hide -2)
(("1" (skosimp*)
(("1" (lemma "sqv_eq_0")
(("1" (inst - "nzv")
(("1" (assert)
(("1"
(lemma "nzreal_times_nzreal_is_nzreal")
(("1"
(inst - "sqv(nzv)" "c!1")
(("1"
(flatten)
(("1"
(hide 2)
(("1"
(case
"nzv*vect3_orthog_toy(nzv) = 0")
(("1" (grind) nil nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1) (("2" (grind) nil nil)) nil))
nil)
("2" (hide -1)
(("2" (skosimp*)
(("2" (expand "linearly_dependent?")
(("2" (skosimp*)
(("2" (case "k1!1/=0 AND k2!1/=0")
(("1" (hide -2)
(("1" (flatten)
(("1"
(inst + "-k2!1/k1!1")
(("1"
(expand "zero")
(("1"
(decompose-equality -1)
(("1"
(decompose-equality 3)
(("1" (grind) nil nil)
("2" (grind) nil nil)
("3" (grind) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil)
("2" (ground)
(("1" (replace -1)
(("1"
(assert)
(("1"
(hide 2)
(("1"
(lemma "sqv_eq_0")
(("1"
(inst - "w!1")
(("1"
(assert)
(("1"
(lemma
"nzreal_times_nzreal_is_nzreal")
(("1"
(inst - "k2!1" "k2!1")
(("1"
(mult-by 1 "k2!1*k2!1")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(replace -1)
(("2"
(assert)
(("2"
(lemma "sqv_eq_0")
(("2"
(inst - "nzv")
(("2"
(assert)
(("2"
(lemma
"nzreal_times_nzreal_is_nzreal")
(("2"
(inst - "k1!1" "k1!1")
(("2"
(mult-by 1 "k1!1*k1!1")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((vect3_orthog_toz const-decl "Vect3" vect3_basis nil)
(nzv skolem-const-decl "Nz_vect3" vect3_basis nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(zero const-decl "Vector" vectors_3D nil)
(vect3_orthog_toy const-decl "Vect3" vect3_basis nil)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_3D nil)
(real nonempty-type-from-decl nil reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "Vector" vectors_3D nil)
(k2!1 skolem-const-decl "real" vect3_basis 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)
(k1!1 skolem-const-decl "real" vect3_basis nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(add_zero_right formula-decl nil vectors_3D nil)
(both_sides_times1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(add_zero_left formula-decl nil vectors_3D nil)
(scal_0 formula-decl nil vectors_3D nil)
(sqv_eq_0 formula-decl nil vectors_3D nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_3D nil)
(sqv const-decl "nnreal" vectors_3D nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_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)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(* const-decl "real" vectors_3D nil)
(nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil)
(nz_nzv application-judgement "Nz_vector" vectors_3D nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(linearly_dependent? const-decl "bool" cross_3D 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "Vector" vectors_3D nil)
(lin_indep_cross formula-decl nil cross_3D nil))
nil))
(vect3_orthonorm_basis 0
(vect3_orthonorm_basis-1 nil 3512137883
("" (skeep) (("" (assert) (("" (grind) nil nil)) nil)) nil)
((sqrt_1 formula-decl nil sqrt "reals/")
(vect3_orthonorm_toy const-decl "Normalized" vect3_basis nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_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_plus_real_is_real application-judgement "real" reals nil)
(nz_nzv application-judgement "Nz_vector" vectors_3D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_3D nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_3D nil)
(orthogonal? const-decl "bool" vectors_3D nil)
(vect3_orthonorm_tox const-decl "Normalized" vect3_basis nil)
(vect3_orthonorm_toz const-decl "Normalized" vect3_basis nil)
(^ const-decl "Normalized" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(norm const-decl "nnreal" vectors_3D nil)
(sqv const-decl "nnreal" vectors_3D nil)
(* const-decl "real" vectors_3D nil)
(vect3_orthog_toz const-decl "Vect3" vect3_basis nil)
(cross const-decl "Vector" cross_3D nil)
(vect3_orthog_toy const-decl "Vect3" vect3_basis nil)
(/= const-decl "boolean" notequal nil))
shostak))
(Equator_map_def 0
(Equator_map_def-1 nil 3512139740
("" (skeep)
(("" (lemma "vect3_orthonorm_basis")
(("" (inst - "nzv")
(("" (case "sqv(nzv) = 1")
(("1" (hide -3) (("1" (grind) nil nil)) nil)
("2" (hide-all-but (-2 1))
(("2" (lemma "sqrt_eq_1")
(("2" (inst?)
(("2" (assert)
(("2" (hide 2)
(("2" (lemma "sqrt_sqv_norm")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((vect3_orthonorm_basis formula-decl nil vect3_basis nil)
(sqv const-decl "nnreal" vectors_3D 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_3D nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(nz_norm_gt_0 application-judgement "posreal" vectors_3D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_nzv application-judgement "Nz_vector" vectors_3D nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(* const-decl "real" vectors_3D nil)
(vect3_orthog_toy const-decl "Vect3" vect3_basis nil)
(norm const-decl "nnreal" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(^ const-decl "Normalized" vectors_3D nil)
(vect3_orthonorm_toy const-decl "Normalized" vect3_basis nil)
(cross const-decl "Vector" cross_3D nil)
(vect3_orthog_toz const-decl "Vect3" vect3_basis nil)
(vect3_orthonorm_toz const-decl "Normalized" vect3_basis nil)
(orthogonal? const-decl "bool" vectors_3D nil)
(vect3_orthonorm_tox const-decl "Normalized" vect3_basis nil)
(Equator_map const-decl "Vect3" vect3_basis nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(sqrt_eq_1 formula-decl nil sqrt "reals/")
(sqrt_sqv_norm formula-decl nil vectors_3D nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(zero const-decl "Vector" vectors_3D nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_3D nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(Equator_map_inv_def 0
(Equator_map_inv_def-1 nil 3512203957
("" (skeep)
(("" (expand "Equator_map_inv")
(("" (expand "Equator_map")
(("" (name "nvx" "vect3_orthonorm_tox(nzv)")
(("" (name "nvy" "vect3_orthonorm_toy(nzv)")
(("" (name "nvz" "vect3_orthonorm_toz(nzv)")
(("" (replace -1)
(("" (replace -2)
(("" (replace -3)
(("" (lemma "vect3_orthonorm_basis")
(("" (inst - "nzv")
(("" (assert)
(("" (replace -2)
(("" (hide -2)
((""
(replace -2)
((""
(hide -2)
((""
(replace -2)
((""
(hide -2)
((""
(flatten)
((""
(expand "orthogonal?")
((""
(case
"FORALL (vvzzv:Normalized): sqv(vvzzv) = 1")
(("1"
(inst-cp - "nvx")
(("1"
(inst-cp - "nvy")
(("1"
(inst - "nvz")
(("1"
(copy -1)
(("1"
(copy -1)
(("1"
(copy -1)
(("1"
(mult-by
-1
"w`x")
(("1"
(mult-by
-2
"w`y")
(("1"
(mult-by
-3
"w`z")
(("1"
(copy
-5)
(("1"
(copy
-1)
(("1"
(copy
-1)
(("1"
(mult-by
-1
"w`x")
(("1"
(mult-by
-2
"w`y")
(("1"
(mult-by
-3
"w`z")
(("1"
(copy
-9)
(("1"
(copy
-1)
(("1"
(copy
-1)
(("1"
(mult-by
-1
"w`x")
(("1"
(mult-by
-2
"w`y")
(("1"
(mult-by
-3
"w`z")
(("1"
(copy
-13)
(("1"
(copy
-1)
(("1"
(copy
-1)
(("1"
(mult-by
-1
"w`x")
(("1"
(mult-by
-2
"w`y")
(("1"
(mult-by
-3
"w`z")
(("1"
(copy
-17)
(("1"
(copy
-1)
(("1"
(copy
-1)
(("1"
(mult-by
-1
"w`x")
(("1"
(mult-by
-2
"w`y")
(("1"
(mult-by
-3
"w`z")
(("1"
(copy
-21)
(("1"
(copy
-1)
(("1"
(copy
-1)
(("1"
(mult-by
-1
"w`x")
(("1"
(mult-by
-2
"w`y")
(("1"
(label
"hyp"
-)
(("1"
(expand
"sqv")
(("1"
(assert)
(("1"
(expand
"*")
(("1"
(assert)
(("1"
(decompose-equality)
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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2"
(typepred "vvzzv")
(("2"
(lemma "sqrt_eq")
(("2"
(inst
-
"sqv(vvzzv)"
"1")
(("2"
(assert)
(("2"
(lemma
"sqrt_sqv_norm")
(("2"
(inst?)
(("2"
(assert)
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))
nil))
nil))
nil))
nil))
nil))
nil)
((Equator_map_inv const-decl "Vect3" vect3_basis nil)
(vect3_orthonorm_tox const-decl "Normalized" vect3_basis nil)
(Normalized type-eq-decl nil vectors_3D nil)
(norm const-decl "nnreal" vectors_3D 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)
(number nonempty-type-decl nil numbers nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(zero const-decl "Vector" vectors_3D nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_3D nil)
(real nonempty-type-from-decl nil reals nil)
(vect3_orthonorm_toz const-decl "Normalized" vect3_basis nil)
(vect3_orthonorm_basis formula-decl nil vect3_basis nil)
(orthogonal? const-decl "bool" vectors_3D nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqrt_sqv_norm formula-decl nil vectors_3D nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(nz_norm_gt_0 application-judgement "posreal" vectors_3D nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sqrt_eq formula-decl nil sqrt "reals/")
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(* const-decl "real" vectors_3D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sqv const-decl "nnreal" vectors_3D nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_3D nil)
(vect3_orthonorm_toy const-decl "Normalized" vect3_basis nil)
(Equator_map const-decl "Vect3" vect3_basis nil))
shostak)))
[ zur Elbe Produktseite wechseln0.16Quellennavigators
Analyse erneut starten
]
|
|
