| products/Sources/formale Sprachen/PVS/trig_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: lnexp_fnd.summary Sprache: LispOriginal von: PVS© |
|
||||||
|
(law_cosines
(distance_refl 0 (distance_refl-1 nil 3269434431 ("" (skosimp*) (("" (expand "dist") (("" (expand "sq_dist") (("" (assert) (("" (expand "sq") (("" (rewrite "sqrt_0") nil nil)) nil)) nil)) nil)) nil)) nil) ((dist const-decl "nonneg_real" law_cosines nil) (sq_0 formula-decl nil sq "reals/") (sqrt_0 formula-decl nil sqrt "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_dist const-decl "nonneg_real" law_cosines nil)) nil)) (distance_symm 0 (distance_symm-1 nil 3269434431 ("" (skolem 1 ("x0" "y0" "x1" "y1")) (("" (expand "dist") (("" (expand "sq_dist") (("" (grind) nil nil)) nil)) nil)) nil) ((dist const-decl "nonneg_real" law_cosines nil) (sq const-decl "nonneg_real" sq "reals/") (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) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_dist const-decl "nonneg_real" law_cosines nil)) nil)) (distance_trans 0 (distance_trans-1 nil 3269668543 ("" (skosimp*) (("" (expand "dist") (("" (expand "sq_dist") (("" (propax) nil nil)) nil)) nil)) nil) ((dist const-decl "nonneg_real" law_cosines nil) (sq_dist const-decl "nonneg_real" law_cosines nil)) shostak)) (distance_scale 0 (distance_scale-1 nil 3269668008 ("" (skosimp*) (("" (expand "dist") (("" (expand "sq_dist") (("" (lemma "sq_times") (("" (inst-cp - "pz!1" "x0!1-x1!1") (("" (inst - "pz!1" "y0!1-y1!1") (("" (lemma "sqrt_times") (("" (inst - "sq(pz!1)" "sq(x0!1 - x1!1) + sq(y0!1 - y1!1)") (("" (rewrite "sqrt_sq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((dist const-decl "nonneg_real" law_cosines nil) (sq_times formula-decl nil sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt_sq formula-decl nil sqrt "reals/") (sqrt_times formula-decl nil sqrt "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (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) (real_minus_real_is_real application-judgement "real" reals nil) (sq_dist const-decl "nonneg_real" law_cosines nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (distance_rot 0 (distance_rot-1 nil 3269668867 ("" (skosimp*) (("" (expand "dist") (("" (expand "sq_dist") (("" (name "KX" "x0!1 - x1!1") (("" (name "KY" "y0!1 - y1!1") (("" (case "(cos(ac!1) * x0!1 + sin(ac!1) * y1!1 - cos(ac!1) * x1!1 - sin(ac!1) * y0!1) = cos(ac!1)*KX - sin(ac!1)*KY") (("1" (replace -1) (("1" (case "(cos(ac!1) * y0!1 + sin(ac!1) * x0!1 - cos(ac!1) * y1!1 - sin(ac!1) * x1!1) = sin(ac!1)*KX +cos(ac!1)*KY") (("1" (replace -1) (("1" (replace -3) (("1" (replace -4) (("1" (hide-all-but 1) (("1" (lemma "sin2_cos2" ("a" "ac!1")) (("1" (name-replace "SIN" "sin(ac!1)") (("1" (name-replace "COS" "cos(ac!1)") (("1" (expand "sq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "KX") (("2" (expand "KY") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "KY") (("2" (expand "KX") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sin_range application-judgement "trig_range" sincos_def nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" sincos_def nil) (dist const-decl "nonneg_real" law_cosines 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) (- 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (cos const-decl "real" sincos_def nil) (sin const-decl "real" sincos_def nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (trig_range type-eq-decl nil sincos_def nil) (- const-decl "[numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (sq const-decl "nonneg_real" sq "reals/") (sin2_cos2 formula-decl nil trig_basic nil) (KX skolem-const-decl "real" law_cosines nil) (KY skolem-const-decl "real" law_cosines nil) (sq_dist const-decl "nonneg_real" law_cosines nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (dot_product 0 (dot_product-2 nil 3286013993 ("" (stop-rewrite "sq_sqrt") (("" (skosimp*) (("" (lemma "distance_trans" ("x2" "-x1!1" "y2" "-y1!1")) (("" (inst-cp - "x1!1" "x0!1" "y1!1" "y0!1") (("" (replace -2) (("" (inst-cp - "x2!1" "x0!1" "y2!1" "y0!1") (("" (replace -2) (("" (inst - "x2!1" "x1!1" "y2!1" "y1!1") (("" (replace -1) (("" (hide-all-but 1) (("" (name-replace "X0" "x0!1 - x1!1") (("" (name-replace "Y0" "y0!1 - y1!1") (("" (name-replace "X2" "x2!1 - x1!1") (("" (name-replace "Y2" "y2!1 - y1!1") (("" (assert) (("" (expand "dist") (("" (expand "sq_dist") (("" (lemma "sq_neg") (("" (inst-cp - "X0") (("" (inst-cp - "Y0") (("" (replace -2) (("" (replace -3) (("" (lemma "sqrt_times") (("" (inst - "sq(X0) + sq(Y0)" "sq(X2) + sq(Y2)") (("" (case "-1 * -x1!1 - x1!1 = 0") (("1" (simplify -2) (("1" (case "abs(X0 * X2 + Y0 * Y2) <= sqrt(sq(X0) + sq(Y0)) * sqrt(sq(X2) + sq(Y2))") (("1" (typepred "sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + (sq(X2) * sq(Y0) + sq(Y0) * sq(Y2)))") (("1" (expand ">=" -1) (("1" (expand "<=" -1) (("1" (split -1) (("1" (case "-1<= (X0 * X2 + Y0 * Y2)/sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) + sq(Y0) * sq(Y2))") (("1" (case "(X0 * X2 + Y0 * Y2) / sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) + sq(Y0) * sq(Y2)) <= 1") (("1" (name-replace "DEN" "sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) + sq(Y0) * sq(Y2))") (("1" (name-replace "NUM" "X0 * X2 + Y0 * Y2") (("1" (inst + "acos(NUM/DEN)") (("1" (lemma "div_cancel4" ("y" "cos(acos(NUM / DEN))" "n0z" "sqrt(sq(X0) + sq(Y0)) * sqrt(sq(X2) + sq(Y2))" "x" "NUM")) (("1" (hide-all-but (-2 -3 -4 1)) (("1" (name-replace "K10" "NUM / DEN") (("1" (hide -3) (("1" (typepred "acos(K10)") (("1" (expand "cos") (("1" (case "floor(acos(K10) / (2 * pi))=0") (("1" (replace -1) (("1" (simplify 1) (("1" (expand "<=" -3) (("1" (split -3) (("1" (hide -2) (("1" (lemma "phase_cos_q1" ("x" "acos(K10)")) (("1" (expand "cos_phase") (("1" (expand ">=") (("1" (replace -2) (("1" (replace -3) (("1" (flatten -1) (("1" (replace -1) (("1" (lemma "cos_value_acos" ("xa" "K10")) (("1" (replaces -1) (("1" (expand "K10") (("1" (cross-mult 1) (("1" (cancel-by 1 "NUM") (("1" (expand "DEN" 2) (("1" (both-sides-f 2 "sq") (("1" (grind) nil nil) ("2" (rewrite "sq_eq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "cos_phase_pi") (("2" (lemma "acos_bij") (("2" (lemma "acos_minus1") (("2" (expand "bijective?") (("2" (expand "injective?") (("2" (flatten -2) (("2" (inst - "K10" "-1") (("2" (assert) (("2" (expand "K10") (("2" (cross-mult -2) (("2" (replaces -2) (("2" (neg-formula 1) (("2" (expand "DEN" 1) (("2" (both-sides-f 1 "sq") (("1" (grind) nil nil) ("2" (rewrite "sq_eq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name-replace "K11" "acos(K10)") (("2" (hide -3 -4 2) (("2" (lemma "floor_def" ("x" "K11 / (2 * pi)")) (("2" (rewrite "div_mult_pos_lt1") (("2" (rewrite "div_mult_pos_le2") (("2" (flatten -1) (("2" (name-replace "K12" "floor(K11 / (2 * pi))") (("2" (case "K12>=1") (("1" (lemma "both_sides_times_pos_ge1" ("x" "K12" "y" "1" "pz" "2*pi")) (("1" (assert) nil nil)) nil) ("2" (case "K12<=-1") (("1" (lemma "both_sides_times_pos_le1" ("x" "K12" "y" "-1" "pz" "2*pi")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NUM / DEN < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "abs") (("2" (case "NUM / DEN < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (rewrite "div_mult_pos_le1" 1) (("2" (expand "abs" -3) (("2" (case "X0 * X2 + Y0 * Y2 < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -5 -3 rl) (("2" (rewrite "div_mult_pos_le2" 1) (("2" (expand "abs" -3) (("2" (case "X0 * X2 + Y0 * Y2 < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (inst + "0") (("2" (rewrite "cos_0") (("2" (replace -5 1 rl) (("2" (hide-all-but (-5 1)) (("2" (lemma "zero_times3" ("x" "sqrt(sq(X0) + sq(Y0))" "y" "sqrt(sq(X2) + sq(Y2))")) (("2" (replace -2 -1 rl) (("2" (flatten -1) (("2" (hide -2) (("2" (split -1) (("1" (lemma "sqrt_eq" ("nny" "sq(X0) + sq(Y0)" "nnz" "0")) (("1" (rewrite "sqrt_0") (("1" (replace -2) (("1" (flatten) (("1" (hide -2) (("1" (lemma "sq_plus_eq_0" ("a" "X0" "b" "Y0")) (("1" (assert) (("1" (flatten -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_plus_eq_0" ("a" "X2" "b" "Y2")) (("2" (lemma "sqrt_eq" ("nny" "sq(X2) + sq(Y2)" "nnz" "0")) (("2" (rewrite "sqrt_0") (("2" (replace -3) (("2" (replace -1 -2 rl) (("2" (flatten -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "sq_le" :dir rl) (("2" (replace -2 1 rl) (("2" (rewrite "sq_sqrt") (("2" (case "FORALL (x:real): sq(abs(x)) = sq(x)") (("1" (inst - --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.37 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.Bot Zugriff |
