|
(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?(A)(difference(a, IUnion(n,E)))")
(("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),difference(b,c))")
(("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.42 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.
|
