|
(ECEF
(spherical2xyz_TCC1 0
(spherical2xyz_TCC1-2 nil 3521211413
("" (skeep)
(("" (name "theta" "pi/2-lat")
(("" (name "phi" "pi-lon")
(("" (name "xx" "r*sin(theta)*cos(phi)")
(("" (name "yy" "r*sin(theta)*sin(phi)")
(("" (name "zz" "r*cos(theta)")
(("" (replace -4)
(("" (replace -5)
(("" (assert)
(("" (replace -1)
(("" (replace -3)
(("" (replace -2)
((""
(case "sq(xx) + sq(yy) + sq(zz) = sq(r)")
(("1"
(case "NOT (xx=0 AND yy = 0 AND zz=0)")
(("1"
(hide-all-but (-7 1))
(("1"
(expand "zero")
(("1" (grind) nil nil))
nil))
nil)
("2"
(flatten)
(("2"
(replace -1)
(("2"
(replace -2)
(("2"
(replace -3)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "sq(xx) + sq(yy) = sq(r*sin(theta))")
(("1"
(replace -1)
(("1"
(lemma "sin2_cos2")
(("1"
(inst - "theta")
(("1"
(mult-by -1 "sq(r)")
(("1"
(expand "zz" +)
(("1"
(hide-all-but (-1 1))
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(expand "xx")
(("2"
(expand "yy")
(("2"
(lemma "sin2_cos2")
(("2"
(inst - "phi")
(("2"
(mult-by
-1
"sq(r*sin(theta))")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(< const-decl "bool" reals nil)
(pi_lb const-decl "posreal" trig_basic "trig/")
(AND const-decl "[bool, bool -> bool]" booleans 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)
(- const-decl "[numfield, numfield -> numfield]" 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin const-decl "real" trig_basic "trig/")
(cos const-decl "real" trig_basic "trig/")
(sin2_cos2 formula-decl nil trig_basic "trig/")
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(zz skolem-const-decl "real" ECEF nil)
(xx skolem-const-decl "real" ECEF nil)
(yy skolem-const-decl "real" ECEF nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(zero const-decl "Vector" vectors_3D nil)
(mk_vect3 macro-decl "Vect3" vectors_3D_def nil)
(sq_0 formula-decl nil sq "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/"))
nil)
(spherical2xyz_TCC1-1 nil 3521211363 ("" (subtype-tcc) nil nil) nil
nil))
(spherical2xyz_TCC2 0
(spherical2xyz_TCC2-3 nil 3521211666
("" (skeep)
(("" (name "theta" "pi/2-lat")
(("" (name "phi" "pi-lon")
(("" (name "xx" "r*sin(theta)*cos(phi)")
(("" (name "yy" "r*sin(theta)*sin(phi)")
(("" (name "zz" "r*cos(theta)")
(("" (replace -4)
(("" (replace -5)
(("" (assert)
(("" (replace -1)
(("" (replace -3)
(("" (replace -2)
((""
(case "sq(xx) + sq(yy) + sq(zz) = sq(r)")
(("1"
(case "NOT (xx=0 AND yy = 0 AND zz=0)")
(("1"
(hide-all-but (-7 1))
(("1"
(expand "zero")
(("1" (propax) nil nil))
nil))
nil)
("2"
(flatten)
(("2"
(replace -1)
(("2"
(replace -2)
(("2"
(replace -3)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "sq(xx) + sq(yy) = sq(r*sin(theta))")
(("1"
(replace -1)
(("1"
(lemma "sin2_cos2")
(("1"
(inst - "theta")
(("1"
(mult-by -1 "sq(r)")
(("1"
(expand "zz" +)
(("1"
(hide-all-but (-1 1))
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(expand "xx")
(("2"
(expand "yy")
(("2"
(lemma "sin2_cos2")
(("2"
(inst - "phi")
(("2"
(mult-by
-1
"sq(r*sin(theta))")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(< const-decl "bool" reals nil)
(pi_lb const-decl "posreal" trig_basic "trig/")
(AND const-decl "[bool, bool -> bool]" booleans 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)
(- const-decl "[numfield, numfield -> numfield]" 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin const-decl "real" trig_basic "trig/")
(cos const-decl "real" trig_basic "trig/")
(sin2_cos2 formula-decl nil trig_basic "trig/")
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(zz skolem-const-decl "real" ECEF nil)
(xx skolem-const-decl "real" ECEF nil)
(yy skolem-const-decl "real" ECEF nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(zero const-decl "Vector" vectors_3D nil)
(sq_0 formula-decl nil sq "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/"))
nil)
(spherical2xyz_TCC2-2 nil 3521211418
("" (skeep)
(("" (skoletin 1)
(("" (name "theta" "pi/2-ll`lat")
(("" (name "phi" "pi-ll`lon")
(("" (name "xx" "r*sin(theta)*cos(phi)")
(("" (name "yy" "r*sin(theta)*sin(phi)")
(("" (name "zz" "r*cos(theta)")
(("" (case "vv = (xx,yy,zz)")
(("1" (case "sq(xx) + sq(yy) = sq(r*sin(theta))")
(("1" (case "sqv(vv) = sq(r)")
(("1" (hide-all-but (-1 1))
(("1" (lemma "sqrt_eq")
(("1" (inst?)
(("1" (assert)
(("1"
(rewrite "sqrt_sqv_norm")
nil)))))))))
("2" (hide 2)
(("2"
(case "sqv(vv) = sq(xx) + sq(yy) + sq(zz)")
(("1" (replace -1)
(("1" (hide -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(replace -2 :dir rl)
(("1"
(hide-all-but 1)
(("1"
(lemma "sin2_cos2")
(("1"
(inst - "theta")
(("1"
(mult-by -1 "sq(r)")
(("1"
(grind)
nil)))))))))))))))))))
("2" (replace -2 +)
(("2" (hide-all-but 1)
(("2" (grind) nil)))))))))))
("2" (hide-all-but 1)
(("2" (expand "xx")
(("2" (expand "yy")
(("2" (lemma "sin2_cos2")
(("2" (inst - "phi")
(("2"
(mult-by -1 "sq(r*sin(theta))")
(("2" (grind) nil)))))))))))))))
("2" (hide-all-but 1)
(("2" (expand "vv")
(("2" (expand "spherical2xyz")
(("2" (expand "xx")
(("2" (expand "yy")
(("2" (expand "zz")
(("2"
(expand "theta")
(("2"
(expand "phi")
(("2"
(propax)
nil))))))))))))))))))))))))))))))))
nil)
nil nil)
(spherical2xyz_TCC2-1 nil 3521211363 ("" (subtype-tcc) nil nil) nil
nil))
(spherical2xyz_norm 0
(spherical2xyz_norm-1 nil 3521203582
("" (skeep)
(("" (skoletin 1)
(("" (name "theta" "pi/2-lat")
(("" (name "phi" "pi-lon")
(("" (name "xx" "r*sin(theta)*cos(phi)")
(("" (name "yy" "r*sin(theta)*sin(phi)")
(("" (name "zz" "r*cos(theta)")
(("" (case "vv = (xx,yy,zz)")
(("1" (case "sq(xx) + sq(yy) = sq(r*sin(theta))")
(("1" (case "sqv(vv) = sq(r)")
(("1" (hide-all-but (-1 1))
(("1" (lemma "sqrt_eq")
(("1" (inst?)
(("1" (assert)
(("1" (rewrite "sqrt_sqv_norm") nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(case "sqv(vv) = sq(xx) + sq(yy) + sq(zz)")
(("1" (replace -1)
(("1" (hide -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(replace -2 :dir rl)
(("1"
(hide-all-but 1)
(("1"
(lemma "sin2_cos2")
(("1"
(inst - "theta")
(("1"
(mult-by -1 "sq(r)")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -2 +)
(("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "xx")
(("2" (expand "yy")
(("2" (lemma "sin2_cos2")
(("2" (inst - "phi")
(("2"
(mult-by -1 "sq(r*sin(theta))")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "vv")
(("2" (expand "spherical2xyz")
(("2" (expand "xx")
(("2" (expand "yy")
(("2" (expand "zz")
(("2"
(expand "theta")
(("2"
(expand "phi")
(("2" (propax) 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_3D nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(spherical2xyz const-decl "Nz_vect3" ECEF nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_3D nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_3D nil)
(yy skolem-const-decl "real" ECEF nil)
(xx skolem-const-decl "real" ECEF nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_3D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv const-decl "nnreal" vectors_3D nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_sqv_norm formula-decl nil vectors_3D nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(sin2_cos2 formula-decl nil trig_basic "trig/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(real_plus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_3D nil)
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(vv skolem-const-decl "Nz_vect3" ECEF nil)
(zz skolem-const-decl "real" ECEF nil)
(phi skolem-const-decl "real" ECEF nil)
(theta skolem-const-decl "real" ECEF nil)
(cos const-decl "real" trig_basic "trig/")
(sin const-decl "real" trig_basic "trig/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pi_lb const-decl "posreal" trig_basic "trig/")
(< const-decl "bool" reals nil)
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/"))
shostak)))
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
