| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 901 kB |
|
Quelle ast_def.prf Sprache: Lisp |
|||||||||
|
(ast_def
(A_empty 0 (A_empty-1 nil 3457694307 ("" (postpone) nil nil) nil shostak)) (IMP_generalized_measure_def_TCC1 0 (IMP_generalized_measure_def_TCC1-1 nil 3458454898 ("" (rewrite "A_empty") nil nil) ((A_empty formula-decl nil ast_def nil)) nil)) (A_difference_union 0 (A_difference_union-1 nil 3457883471 ("" (case "forall (a:(A),E:disjoint_indexed_measurable,n:nat): finite_disjoint_union? (("1" (skosimp) (("1" (expand "finite_disjoint_union?" -3) (("1" (skosimp) (("1" (case-replace "n!1=0") (("1" (assert) (("1" (case-replace "b!1=emptyset") (("1" (rewrite "difference_emptyset1") (("1" (expand "finite_disjoint_union?") (("1" (inst + "lambda (i:nat): if i=0 then a!1 else emptyset endif" "1") (("1" (hide -1 -2 -3 -5 -6 -7) (("1" (split) (("1" (expand "disjoint?") (("1" (skosimp) (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp) (("1" (expand "emptyset") (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (case-replace "a!1(x!1)") (("1" (inst + "0") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (case-replace "i!1=0") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "empty?") (("2" (expand "member") (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -5) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst -7 "i!1") (("2" (expand "empty?") (("2" (inst -7 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!1>0") (("1" (hide 1) (("1" (case "b!1=IUnion(n!1-1,E!1)") (("1" (case "FORALL (i:nat): A(E!1(i))") (("1" (hide -7 -8) (("1" (inst -4 "a!1" "E!1" "n!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (expand "disjoint_indexed_measurable?") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -7 "i!1") (("2" (flatten) (("2" (case "i!1 (("1" (assert) nil nil) ("2" (assert) (("2" (rewrite "emptyset_is_empty?") (("2" (replace -7) (("2" (rewrite "A_empty") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (apply-extensionality :hide? t) (("2" (case-replace "b!1(x!1)") (("1" (replace -5 -1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst -6 "i!1") (("1" (expand "image") (("1" (expand "Union") (("1" (inst + "E!1(i!1)") (("1" (flatten) (("1" (case-replace "i!1 < n!1") (("1" (inst + "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (rewrite "emptyset_is_empty?") (("2" (replace -6) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -5) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!2") (("2" (skosimp) (("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (rewrite "IUnion_0_def") (("1" (lemma "A_difference" ("a" "a!1" "b" "E!1(0)")) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (rewrite "IUnion_n_def") (("2" (rewrite "union_commutative" 1) (("2" (rewrite "difference_difference1" 1 :dir rl) (("2" (lemma "A_difference" ("a" "a!1" "b" "E!1(1+j!1)")) (("2" (expand "finite_disjoint_union?" -1) (("2" (skosimp) (("2" (case "forall (a,b,c:set[T]): difference(union(a,b),c)=union(difference(a,c),diff (("1" (case-replace "n!1=0") (("1" (assert) (("1" (case-replace "IUnion(E!2)=emptyset") (("1" (replace -5) (("1" (rewrite "difference_emptyset2") (("1" (hide-all-but 1) (("1" (expand "finite_disjoint_union?") (("1" (inst + "lambda (i:nat): emptyset" "0") (("1" (split) (("1" (grind) nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (expand "member") (("3" (expand "empty?") (("3" (expand "member") (("3" (expand "emptyset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -5)) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst - "i!1") (("2" (expand "empty?") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!1>0") (("1" (hide 1) (("1" (case-replace "IUnion(E!2)=IUnion(n!1-1,E!2)") (("1" (replace -5) (("1" (hide -1 -5) (("1" (case "forall (n:nat): finite_disjoint_union?(A) (difference(IUnion(n, E!2), IUnion(j!1, E!1)))") (("1" (inst - "n!1-1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (rewrite "IUnion_0_def") (("1" (inst -5 "E!2(0)" "E!1") (("1" (assert) (("1" (inst -4 "0") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "IUnion_n_def") (("2" (inst - "IUnion(j!2, E!2)" "E!2(1 + j!2)" "IUnion(j!1, E!1)") (("2" (replace -3) (("2" (inst -6 "E!2(1 + j!2)" "E!1") (("1" (hide -3 -5 -2) (("1" (name-replace "AA" "difference(IUnion(j!2, E!2), IUnion(j!1, E!1))") (("1" (name-replace "BB" "difference(E!2(1 + j!2), IUnion(j!1, E!1))") (("1" (case "disjoint?(AA,BB)") (("1" (expand "finite_disjoint_union?") (("1" (skosimp*) (("1" (inst + "lambda (i:nat): if i "n!2+n!3") (("1" (split) (("1" (expand "disjoint?" 1) (("1" (skosimp) (("1" (case-replace "i!1 < n!2") (("1" (case-replace "j!3 < n!2") (("1" (expand "disjoint?" -4) (("1" (inst - "i!1" "j!3") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "disjoint?" (-2 3)) (("2" (expand "intersection") (("2" (expand "empty?" (-2 3)) (("2" (skosimp) (("2" (expand "member") (("2" (flatten) (("2" (inst - "x!1") (("2" (replace -5) (("2" (split) (("1" (expand "IUnion" 1) (("1" (inst + "i!1") nil nil)) nil) ("2" (replace -9) (("2" (expand "IUnion") (("2" (inst + "j!3-n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "j!3 < n!2") (("1" (expand "disjoint?" (3 -2)) (("1" (expand "intersection") (("1" (expand "empty?" (3 -2)) (("1" (expand "member") (("1" (skosimp) (("1" (inst -4 "x!1") (("1" (split 3) (("1" (replace -5) (("1" (expand "IUnion") (("1" (inst + "j!3") nil nil)) nil)) nil) ("2" (replace -9) (("2" (expand "IUnion") (("2" (inst + "i!1-n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "disjoint?" -6) (("2" (inst -6 "i!1 - n!2" "j!3 - n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (expand "union") (("1" (expand "disjoint?" -1) (("1" (expand "intersection") (("1" (expand "empty?" -1) (("1" (expand "member") (("1" (inst - "x!1") (("1" (case-replace "AA(x!1)") (("1" (replace -3 -1) (("1" (expand "IUnion" (-1 1)) (("1" (skosimp) (("1" (inst -4 "i!1") (("1" (inst + "i!1") (("1" (case-replace "i!1 < n!2") (("1" (assert) (("1" (expand "empty?") (("1" (inst -4 "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "BB(x!1)") (("1" (replace -7) (("1" (expand "IUnion" (-1 2)) (("1" (skosimp) (("1" (inst + "n!2+i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 3) (("2" (replace -3) (("2" (replace -7) (("2" (expand "IUnion" (1 2 -1)) (("2" (skosimp) (("2" (case-replace "i!1 < n!2") (("1" (inst 2 "i!1") nil nil) ("2" (assert) (("2" (inst 2 "i!1-n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (expand "member") (("3" (assert) (("3" (case-replace "i!1 < n!2") (("1" (assert) (("1" (inst -5 "i!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -8 "i!1-n!2") (("2" (flatten) (("2" (assert) (("2" (case "i!1 - n!2 < n!3") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "disjoint?" 1) (("2" (expand "intersection") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (flatten) (("2" (expand "AA") (("2" (expand "BB") (("2" (expand "difference") (("2" (expand "member") (("2" (flatten) (("2" (hide 1 2) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!2") (("2" (skolem - "i!1") (("2" (replace -1) (("2" (hide -1) (("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.56 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28