| products/sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: trig_doc.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(tca_3D
(IMP_metric_space_real_fun_TCC1 0 (IMP_metric_space_real_fun_TCC1-1 nil 3563728619 ("" (lemma "real_metric_space") (("" (inst?) nil nil)) nil) ((fullset const-decl "set" sets nil) (set type-eq-decl nil sets 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_metric_space formula-decl nil real_metric_space "analysis/")) nil)) (cyl_norm_sq_diff_cont 0 (cyl_norm_sq_diff_cont-1 nil 3487000249 ("" (skeep) (("" (lemma "diff_continuous[real,real_dist]") (("" (inst - "fullset[real]" "(LAMBDA (t:real): sqv(vect2(s) + t * vect2(v)) / sq(D))" "(LAMBDA (t:real): sq(s`z + t * v`z) / sq(H))") (("" (expand "-" -) (("" (assert) (("" (hide 2) (("" (lemma "vectors_2D.sqv_add") (("" (name "hf1" "(LAMBDA (t:real): sqv(vect2(s))/sq(D))") (("" (name "hf2" "(LAMBDA (t:real): t*(2*vect2(s)*vect2(v)/sq(D)))") (("" (name "hf3" "(LAMBDA (t:real): t*(sqv(vect2(v))/sq(D)))") (("" (name "hf4" "(LAMBDA (t:real): t)") (("" (case "NOT (LAMBDA (t: real): sqv(vect2(s) + t * vect2(v)) / sq(D)) = hf1 + hf2 + (("1" (hide 2) (("1" (hide -5) (("1" (decompose-equality +) (("1" (hide -) (("1" (expand "hf1" +) (("1" (expand "hf2" +) (("1" (expand "hf3" +) (("1" (expand "hf4" +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (name "vf1" "(LAMBDA (t:real): sq(s`z)/sq(H))") (("2" (name "vf2" "(LAMBDA (t:real): t*(2*s`z*v`z/sq(H)))") (("2" (name "vf3" "(LAMBDA (t:real): t*(sq(v`z)/sq(H)))") (("2" (name "vf4" "(LAMBDA (t:real): t)") (("2" (case "NOT (LAMBDA (t: real): sq(s`z + t * v`z) / sq(H)) = vf1 + vf2 + vf3*vf4") (("1" (hide 2) (("1" (decompose-equality +) (("1" (hide -) (("1" (expand "vf1" +) (("1" (expand "vf2" +) (("1" (expand "vf3" +) (("1" (expand "vf4" +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (split +) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst - "fullset[real]" "hf1 + hf2" "hf3*hf4") (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (expand "continuous?") (("1" (skosimp*) (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst + "1") (("1" (skosimp*) (("1" (expand "member" +) (("1" (expand "ball" +) (("1" (expand "real_dist") (("1" (expand "hf1" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "hf2") (("2" (name "cc" "2*vect2(s)*vect2(v)/sq(D)") (("2" (replace -1) (("2" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prod_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split +) (("1" (expand "hf3") (("1" (name "cc" "sqv(vect2(v))/sq(D)") (("1" (replace -1) (("1" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "hf4") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sum_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split) (("1" (expand "vf1") (("1" (grind :exclude ("fullset" "sq")) nil nil)) nil) ("2" (expand "vf2") (("2" (name "cc" "(2 * (s`z * v`z) / sq(H))") (("2" (replace -1) (("2" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prod_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split) (("1" (expand "vf3") (("1" (name "cc" "sq(v`z)/sq(H)") (("1" (replace -1) (("1" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.128 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 |
