|
(partitions
(partition_TCC1 0
(partition_TCC1-1 nil 3390454630
("" (expand "partition?")
(("" (split)
(("1" (apply-extensionality 1 :hide? t)
(("1" (expand "fullset")
(("1" (expand "singleton")
(("1" (expand "Union")
(("1" (inst + "fullset[T]")
(("1" (expand "fullset") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (typepred "x!1")
(("2" (typepred "y!1")
(("2" (expand "singleton") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(TRUE const-decl "bool" booleans nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(set type-eq-decl nil sets nil) (Union const-decl "set" sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(fullset const-decl "set" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil partitions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(partition? const-decl "bool" partitions nil))
nil))
(finite_partition_TCC1 0
(finite_partition_TCC1-1 nil 3390454630
("" (expand "finite_partition?")
(("" (lemma "partition_TCC1") (("" (propax) nil nil)) nil)) nil)
((partition_TCC1 subtype-tcc nil partitions nil)
(finite_partition? const-decl "bool" partitions nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil))
nil))
(join_TCC1 0
(join_TCC1-1 nil 3394989455
("" (skosimp)
(("" (typepred "p2!1")
(("" (typepred "p1!1")
(("" (expand "finite_partition?")
(("" (flatten)
(("" (split)
(("1" (expand "fullset")
(("1" (hide -2 -4)
(("1" (expand "partition?")
(("1" (flatten)
(("1" (split)
(("1" (apply-extensionality 1 :hide? t)
(("1" (hide -2 -4)
(("1"
(lemma "extensionality_postulate"
("f" "Union(p1!1)" "g" "{x: T | TRUE}"))
(("1"
(lemma
"extensionality_postulate"
("f"
"Union(p2!1)"
"g"
"{x: T | TRUE}"))
(("1"
(replace -1 -4 rl)
(("1"
(replace -2 -3 rl)
(("1"
(hide -1 -2)
(("1"
(assert)
(("1"
(expand "Union")
(("1"
(inst - "x!1")
(("1"
(inst - "x!1")
(("1"
(skosimp*)
(("1"
(inst
+
"intersection(a!1,a!2)")
(("1"
(expand
"intersection")
(("1"
(expand "member")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(inst
+
"a!1"
"a!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "x!1")
(("2" (typepred "y!1")
(("2"
(skosimp*)
(("2"
(inst - "a1!1" "a1!2")
(("2"
(inst - "a2!1" "a2!2")
(("2"
(assert)
(("2"
(case-replace "a1!2=a1!1")
(("1"
(assert)
(("1"
(hide -5 -4 -6)
(("1"
(expand "disjoint?")
(("1"
(expand "intersection")
(("1"
(expand "member")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(skosimp)
(("1"
(inst
-
"x!2")
(("1"
(assert)
(("1"
(replace
-3)
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
(("1"
(replace
-2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case-replace "a2!2=a2!1")
(("1"
(expand "disjoint?")
(("1"
(expand "intersection")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(skosimp)
(("1"
(replace -2)
(("1"
(replace -3)
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
(("1"
(inst
-9
"x!2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand "disjoint?")
(("2"
(expand "empty?")
(("2"
(skosimp)
(("2"
(inst - "x!2")
(("2"
(inst - "x!2")
(("2"
(expand
"member")
(("2"
(expand
"intersection")
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(replace
-1)
(("2"
(replace
-2)
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset")
(("2" (expand "partition?")
(("2" (flatten)
(("2" (lemma "is_finite_cross[(p1!1),(p2!1)]")
(("2" (assert)
(("2" (split)
(("1" (hide -4 -7)
(("1"
(case "is_finite({x:[set[T],set[T]] | p1!1(x`1)&p2!1(x`2)})")
(("1"
(hide -2)
(("1"
(rewrite "is_finite_surj" * :dir rl)
(("1"
(rewrite
"is_finite_surj"
*
:dir
rl)
(("1"
(skosimp)
(("1"
(inst
+
"N!1"
"lambda (n:below[N!1]): intersection(f!1(n)`1,f!1(n)`2)")
(("1"
(expand "surjective?")
(("1"
(skosimp)
(("1"
(typepred "y!1")
(("1"
(skosimp)
(("1"
(typepred "a1!1")
(("1"
(typepred "a2!1")
(("1"
(inst
-4
"(a1!1,a2!1)")
(("1"
(skosimp)
(("1"
(inst
+
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(inst
+
"f!1(n!1)`1"
"f!1(n!1)`2")
(("1"
(typepred "f!1(n!1)")
(("1" (propax) nil nil))
nil)
("2"
(typepred "f!1(n!1)")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2"
(expand "is_finite_type")
(("2"
(expand "is_finite")
(("2"
(skosimp)
(("2"
(inst + "N!1" "g!1")
(("2"
(expand "restrict")
(("2"
(expand "injective?")
(("2"
(skosimp)
(("2"
(inst - "x1!1" "x2!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-3 1))
(("2" (expand "is_finite_type")
(("2"
(expand "is_finite")
(("2" (propax) nil nil))
nil))
nil))
nil)
("3" (hide-all-but (-6 1))
(("3" (expand "is_finite_type")
(("3"
(expand "is_finite")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_partition nonempty-type-eq-decl nil partitions nil)
(fullset const-decl "set" sets nil)
(finite_partition? const-decl "bool" partitions nil)
(set type-eq-decl nil sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil partitions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(TRUE const-decl "bool" booleans nil)
(intersection const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Union const-decl "set" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(extensionality_postulate formula-decl nil functions nil)
(p1!1 skolem-const-decl "finite_partition" partitions nil)
(p2!1 skolem-const-decl "finite_partition" partitions nil)
(a!1 skolem-const-decl "(p1!1)" partitions nil)
(a!2 skolem-const-decl "(p2!1)" partitions nil)
(member const-decl "bool" sets nil)
(partition? const-decl "bool" partitions nil)
(is_finite_cross formula-decl nil finite_cross "finite_sets/")
(is_finite const-decl "bool" finite_sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(is_finite_surj formula-decl nil finite_sets nil)
(n!1 skolem-const-decl "below[N!1]" partitions nil)
(surjective? const-decl "bool" functions nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(N!1 skolem-const-decl "nat" partitions nil)
(below type-eq-decl nil nat_types nil)
(f!1 skolem-const-decl
"[below[N!1] -> ({x: [set[T], set[T]] | p1!1(x`1) & p2!1(x`2)})]"
partitions nil)
(is_finite_type const-decl "bool" finite_sets nil)
(injective? const-decl "bool" functions nil)
(restrict const-decl "R" restrict nil))
nil)))
¤ Dauer der Verarbeitung: 0.20 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.
|
