| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 490 kB |
|
SSL tca_3D.prf Sprache: Lisp |
|||||||||
|
(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.49 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28