|
(subset_algebra_def
(sigma_union_implies_subset_union 0
(sigma_union_implies_subset_union-1 nil 3313473197
("" (expand "subset_algebra_union?")
(("" (expand "sigma_algebra_union?")
(("" (skosimp*)
(("" (typepred "x!1")
(("" (typepred "y!1")
(("" (name "U" "union(singleton(x!1),singleton(y!1))")
(("" (inst - "U")
((""
(case-replace
"(FORALL (x: (extend[setof[T], (S!1), bool, FALSE](U))):
member(x, S!1))")
(("1" (split -5)
(("1" (expand "member")
(("1" (expand "extend")
(("1" (expand "Union")
(("1" (expand "union")
(("1" (assert)
(("1"
(case-replace
"{x: T |
EXISTS (a:
(LAMBDA (t: setof[T]):
IF (S!1)(t) THEN U(t) ELSE FALSE ENDIF)):
a(x)} = {x: T | member(x, x!1) OR member(x, y!1)}")
(("1"
(hide 2)
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(expand "member")
(("1"
(case-replace "x!1(x!2)")
(("1"
(inst + "x!1")
(("1"
(expand "U")
(("1"
(expand "singleton")
(("1"
(expand "union")
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case-replace "y!1(x!2)")
(("1"
(inst + "y!1")
(("1"
(expand "U")
(("1"
(expand "singleton")
(("1"
(expand "union")
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(assert)
(("2"
(expand "U" -1)
(("2"
(expand
"singleton")
(("2"
(expand
"union")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "extend")
(("2" (expand "is_countable[set[T]]")
(("2"
(inst +
"lambda (x:setof[T]): IF x = x!1 THEN 0 ELSE 1 ENDIF")
(("2" (expand "injective?")
(("2"
(skosimp*)
(("2"
(expand "restrict")
(("2"
(typepred "x1!1")
(("2"
(typepred "x2!1")
(("2"
(assert)
(("2"
(expand "U")
(("2"
(expand "singleton")
(("2"
(expand "union")
(("2"
(expand "member")
(("2"
(hide-all-but
(-1 -3 -5 1))
(("2"
(split -1)
(("1"
(split -2)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(split -2)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (typepred "x!2")
(("2" (expand "extend")
(("2" (case-replace "S!1(x!2)")
(("1" (expand "member")
(("1" (propax) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(nonempty_finite_union1 application-judgement
"non_empty_finite_set[T]" countable_props "sets_aux/")
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" countable_props "sets_aux/")
(member const-decl "bool" sets nil)
(is_countable const-decl "bool" countability "sets_aux/")
(restrict const-decl "R" restrict nil)
(injective? const-decl "bool" functions nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(number nonempty-type-decl nil numbers nil)
(Union const-decl "set" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(y!1 skolem-const-decl "(S!1)" subset_algebra_def nil)
(S!1 skolem-const-decl "setofsets[T]" subset_algebra_def nil)
(U skolem-const-decl "non_empty_finite_set[(S!1)]"
subset_algebra_def nil)
(x!1 skolem-const-decl "(S!1)" subset_algebra_def nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(subset_algebra_union? const-decl "bool" subset_algebra_def nil))
shostak))
(sigma_algebra_implies_subset_algebra 0
(sigma_algebra_implies_subset_algebra-1 nil 3313474506
("" (skosimp*)
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra?")
(("" (flatten)
(("" (assert)
(("" (rewrite "sigma_union_implies_subset_union") nil nil))
nil))
nil))
nil))
nil))
nil)
((sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_union_implies_subset_union formula-decl nil
subset_algebra_def nil)
(T formal-type-decl nil subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil))
shostak))
(trivial_subset_algebra_TCC1 0
(trivial_subset_algebra_TCC1-1 nil 3426521314
("" (expand "subset_algebra?")
(("" (expand "emptyset")
(("" (expand "fullset")
(("" (expand "singleton")
(("" (expand "union")
(("" (expand "member")
(("" (expand "subset_algebra_empty?")
(("" (expand "subset_algebra_complement?")
(("" (expand "complement")
(("" (expand "subset_algebra_union?")
(("" (expand "union")
(("" (expand "member")
(("" (expand "emptyset")
(("" (split)
(("1"
(skosimp*)
(("1"
(apply-extensionality :hide? t)
(("1"
(apply-extensionality :hide? t)
(("1"
(typepred "x!1")
(("1"
(split)
(("1"
(replace -1)
(("1" (assert) nil nil))
nil)
("2"
(replace -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(apply-extensionality :hide? t)
(("2"
(apply-extensionality :hide? t)
(("2"
(typepred "x!1")
(("2"
(typepred "y!1")
(("2"
(split -1)
(("1"
(replace -1)
(("1"
(assert)
(("1"
(split -2)
(("1" (assert) nil nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(split -2)
(("1" (assert) nil nil)
("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)
((emptyset const-decl "set" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(member const-decl "bool" sets nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(subset_algebra_union? const-decl "bool" subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(complement const-decl "set" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(union const-decl "set" sets nil)
(fullset const-decl "set" sets nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(nonempty_finite_union1 application-judgement
"non_empty_finite_set[T]" countable_props "sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(sigma_algebra_TCC1 0
(sigma_algebra_TCC1-1 nil 3426521314
("" (expand "trivial_subset_algebra")
(("" (expand "emptyset")
(("" (expand "fullset")
(("" (expand "singleton")
(("" (expand "union")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (expand "emptyset")
(("" (expand "member")
(("" (expand "subset_algebra_complement?")
(("" (expand "complement")
(("" (expand "sigma_algebra_union?")
(("" (expand "Union")
(("" (expand "member")
((""
(split)
(("1"
(skosimp*)
(("1"
(apply-extensionality :hide? t)
(("1"
(apply-extensionality :hide? t)
(("1"
(typepred "x!1")
(("1"
(split)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(apply-extensionality :hide? t)
(("2"
(apply-extensionality :hide? t)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(inst - "a!1")
(("2"
(split -4)
(("1" (assert) nil nil)
("2"
(inst + "a!1")
(("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)
((emptyset const-decl "set" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(TRUE const-decl "bool" booleans nil)
(FALSE const-decl "bool" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(Union const-decl "set" sets nil)
(complement const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(union const-decl "set" sets nil)
(fullset const-decl "set" sets nil)
(trivial_subset_algebra const-decl "(subset_algebra?)"
subset_algebra_def nil)
(nonempty_finite_union1 application-judgement
"non_empty_finite_set[T]" countable_props "sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(sigma_algebra_is_subset_algebra 0
(sigma_algebra_is_subset_algebra-1 nil 3426521314
("" (skolem + ("A"))
(("" (typepred "A")
(("" (expand "subset_algebra?")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (replace -1)
(("" (replace -2)
(("" (expand "subset_algebra_union?")
(("" (expand "sigma_algebra_union?")
(("" (skosimp)
((""
(inst -
"add[set[T]](x!1,singleton[set[T]](y!1))")
((""
(case-replace
"Union(add[set[T]](x!1, singleton[set[T]](y!1)))=union(x!1, y!1)")
(("1" (split -4)
(("1" (propax) nil nil)
("2" (rewrite "finite_countable[set[T]]")
nil nil)
("3" (hide-all-but 1)
(("3"
(skosimp)
(("3"
(typepred "x!2")
(("3"
(expand "singleton")
(("3"
(expand "add")
(("3"
(expand "member")
(("3"
(split)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality :hide? t)
(("2"
(expand "union")
(("2"
(expand "singleton")
(("2"
(expand "add")
(("2"
(expand "member")
(("2"
(expand "Union")
(("2"
(case-replace "x!1(x!2)")
(("1" (inst + "x!1") nil nil)
("2"
(case-replace "y!1(x!2)")
(("1"
(inst + "y!1")
nil
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(split)
(("1"
(assert)
nil
nil)
("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)
((sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset_algebra_union? const-decl "bool" subset_algebra_def nil)
(union const-decl "set" sets nil) (Union const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" countable_props "sets_aux/")
(member const-decl "bool" sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_countable judgement-tcc nil countable_props "sets_aux/")
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" countable_props "sets_aux/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil))
nil))
(powerset_is_sigma_algebra 0
(powerset_is_sigma_algebra-1 nil 3426523512
("" (expand "sigma_algebra?")
(("" (split)
(("1" (expand "subset_algebra_empty?") (("1" (grind) nil nil))
nil)
("2" (grind) nil nil) ("3" (grind) nil nil))
nil))
nil)
((emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(powerset const-decl "setofsets" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(complement const-decl "set" sets nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(is_countable const-decl "bool" countability "sets_aux/")
(Union const-decl "set" sets nil)
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(nonempty_powerset application-judgement "(nonempty?[set[T]])"
sets_lemmas nil))
shostak))
(generated_sigma_algebra_TCC1 0
(generated_sigma_algebra_TCC1-1 nil 3426521314
("" (skosimp)
(("" (expand "Intersection")
(("" (expand "sigma_algebra?")
(("" (split)
(("1" (expand "subset_algebra_empty?")
(("1" (expand "member")
(("1" (skosimp)
(("1" (typepred "a!1")
(("1" (expand "sigma_algebra?")
(("1" (flatten)
(("1" (expand "subset_algebra_empty?")
(("1" (expand "member")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "subset_algebra_complement?")
(("2" (skosimp)
(("2" (expand "member")
(("2" (skosimp)
(("2" (typepred "a!1")
(("2" (expand "sigma_algebra?")
(("2" (flatten)
(("2" (expand "subset_algebra_complement?")
(("2" (expand "member")
(("2" (typepred "x!1")
(("2"
(inst - "a!1")
(("2" (inst - "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "sigma_algebra_union?")
(("3" (skosimp)
(("3" (expand "member")
(("3" (skosimp)
(("3" (typepred "a!1")
(("3" (expand "sigma_algebra?")
(("3" (flatten)
(("3" (expand "sigma_algebra_union?")
(("3" (inst - "X!2")
(("3" (assert)
(("3"
(expand "member")
(("3"
(skosimp)
(("3"
(typepred "x!1")
(("3"
(expand "subset?")
(("3"
(inst - "x!1")
(("3"
(assert)
(("3"
(expand "member")
(("3"
(inst - "x!1")
(("3"
(inst - "a!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Intersection const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(X!1 skolem-const-decl "setofsets[T]" subset_algebra_def nil)
(a!1 skolem-const-decl
"({Y | sigma_algebra?(Y) AND subset?[setof[T]](X!1, Y)})"
subset_algebra_def nil)
(x!1 skolem-const-decl "({x |
FORALL (a: ({Y | sigma_algebra?(Y) AND subset?[setof[T]](X!1, Y)})):
a(x)})" subset_algebra_def nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil))
nil))
(generated_sigma_algebra_subset1 0
(generated_sigma_algebra_subset1-1 nil 3426523538
("" (skosimp)
(("" (expand "generated_sigma_algebra")
(("" (expand "subset?")
(("" (expand "Intersection")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "a!1")
(("" (inst - "x!1")
(("" (expand "member") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((generated_sigma_algebra const-decl "sigma_algebra"
subset_algebra_def nil)
(Intersection const-decl "set" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
shostak))
(generated_sigma_algebra_subset2 0
(generated_sigma_algebra_subset2-1 nil 3426523636
("" (skosimp)
(("" (expand "generated_sigma_algebra")
(("" (expand "Intersection")
(("" (expand "subset?" 1 1)
(("" (expand "member")
(("" (skosimp)
(("" (inst - "Y!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((generated_sigma_algebra const-decl "sigma_algebra"
subset_algebra_def nil)
(subset? const-decl "bool" sets nil)
(Y!1 skolem-const-decl "setofsets[T]" subset_algebra_def nil)
(X!1 skolem-const-decl "setofsets[T]" subset_algebra_def nil)
(set type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(Intersection const-decl "set" sets nil))
shostak))
(generated_sigma_algebra_idempotent 0
(generated_sigma_algebra_idempotent-1 nil 3426523706
("" (skosimp)
((""
(lemma "generated_sigma_algebra_subset2" ("X" "A!1" "Y" "A!1"))
(("" (assert)
(("" (rewrite "subset_reflexive")
(("" (lemma "generated_sigma_algebra_subset1" ("X" "A!1"))
((""
(lemma "subset_antisymmetric"
("a" "generated_sigma_algebra(A!1)" "b" "A!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(generated_sigma_algebra_subset2 formula-decl nil
subset_algebra_def nil)
(subset_reflexive formula-decl nil sets_lemmas nil)
(set type-eq-decl nil sets nil)
(subset_antisymmetric formula-decl nil sets_lemmas nil)
(generated_sigma_algebra const-decl "sigma_algebra"
subset_algebra_def nil)
(generated_sigma_algebra_subset1 formula-decl nil
subset_algebra_def nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
shostak))
(intersection_sigma_algebra 0
(intersection_sigma_algebra-1 nil 3426523790
("" (skosimp)
(("" (typepred "A!1")
(("" (typepred "B!1")
(("" (expand "intersection")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (expand "member")
(("" (split)
(("1" (expand "subset_algebra_empty?")
(("1" (expand "member") (("1" (assert) nil nil))
nil))
nil)
("2" (expand "subset_algebra_complement?")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2" (inst - "x!1")
(("2" (inst - "x!1")
(("2" (expand "member")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "sigma_algebra_union?")
(("3" (skosimp)
(("3" (expand "member")
(("3" (inst -5 "X!1")
(("3" (inst -8 "X!1")
(("3" (assert)
(("3"
(split -5)
(("1"
(split -8)
(("1" (assert) nil nil)
("2"
(skosimp)
(("2"
(inst - "x!1")
(("2" (flatten) nil nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(inst - "x!1")
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(intersection const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(member const-decl "bool" sets nil))
shostak))
(sigma_member 0
(sigma_member-1 nil 3426524135
("" (expand "member")
(("" (skosimp)
(("" (expand "sigma")
(("" (expand "extend")
(("" (expand "Union")
(("" (expand "generated_sigma_algebra")
(("" (expand "Intersection")
(("" (expand "subset?")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "a!1")
(("" (expand "subset?")
(("" (expand "member")
(("" (inst - "x!1")
((""
(split -2)
(("1" (propax) nil nil)
("2" (inst + "A!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extend const-decl "R" extend nil)
(generated_sigma_algebra const-decl "sigma_algebra"
subset_algebra_def nil)
(subset? const-decl "bool" sets nil)
(I!1 skolem-const-decl "set[sigma_algebra]" subset_algebra_def nil)
(A!1 skolem-const-decl "sigma_algebra" subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(FALSE const-decl "bool" booleans nil)
(Intersection const-decl "set" sets nil)
(Union const-decl "set" sets nil)
(sigma const-decl "sigma_algebra" subset_algebra_def nil)
(member const-decl "bool" sets nil))
shostak))
(powerset_is_subset_algebra 0
(powerset_is_subset_algebra-1 nil 3449732914
("" (lemma "powerset_is_sigma_algebra")
(("" (lemma "sigma_algebra_is_subset_algebra")
(("" (inst - "powerset(fullset[T])") nil nil)) nil))
nil)
((sigma_algebra_is_subset_algebra judgement-tcc nil
subset_algebra_def nil)
(fullset const-decl "set" sets nil)
(powerset const-decl "setofsets" sets nil)
(set type-eq-decl nil sets nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(nonempty_powerset application-judgement "(nonempty?[set[T]])"
sets_lemmas nil)
(powerset_is_sigma_algebra formula-decl nil subset_algebra_def
nil))
shostak))
(generated_subset_algebra_TCC1 0
(generated_subset_algebra_TCC1-1 nil 3449732913
("" (subtype-tcc) nil nil)
((a!1 skolem-const-decl "({Y |
(Y(emptyset[T]) AND
(FORALL (x: (Y)): Y(complement(x))) AND
(FORALL (x, y: (Y)): Y(union(x, y))))
AND (FORALL (x: setof[T]): X!1(x) => Y(x))})" subset_algebra_def
nil)
(x!1 skolem-const-decl "(Intersection[setof[T]]
({Y |
(Y(emptyset[T]) AND
(FORALL (x: (Y)): Y(complement(x))) AND
(FORALL (x, y: (Y)): Y(union(x, y))))
AND (FORALL (x: setof[T]): X!1(x) => Y(x))}))"
subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(emptyset const-decl "set" sets nil)
(complement const-decl "set" sets nil)
(union const-decl "set" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(X!1 skolem-const-decl "setofsets[T]" subset_algebra_def nil)
(a!1 skolem-const-decl "({Y |
(Y(emptyset[T]) AND
(FORALL (x: (Y)): Y(complement(x))) AND
(FORALL (x, y: (Y)): Y(union(x, y))))
AND (FORALL (x: setof[T]): X!1(x) => Y(x))})" subset_algebra_def
nil)
(x!1 skolem-const-decl "(Intersection[setof[T]]
({Y |
(Y(emptyset[T]) AND
(FORALL (x: (Y)): Y(complement(x))) AND
(FORALL (x, y: (Y)): Y(union(x, y))))
AND (FORALL (x: setof[T]): X!1(x) => Y(x))}))"
subset_algebra_def nil)
(y!1 skolem-const-decl "(Intersection[setof[T]]
({Y |
(Y(emptyset[T]) AND
(FORALL (x: (Y)): Y(complement(x))) AND
(FORALL (x, y: (Y)): Y(union(x, y))))
AND (FORALL (x: setof[T]): X!1(x) => Y(x))}))"
subset_algebra_def nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(subset_algebra_union? const-decl "bool" subset_algebra_def nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(subset? const-decl "bool" sets nil)
(Intersection const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/"))
nil))
(generated_subset_algebra_subset1 0
(generated_subset_algebra_subset1-1 nil 3449732987
("" (skosimp)
(("" (expand "subset?")
(("" (expand "member")
(("" (skosimp)
(("" (expand "generated_subset_algebra")
(("" (expand "Intersection")
(("" (skosimp)
(("" (typepred "a!1")
(("" (expand "subset?")
(("" (inst - "x!1")
(("" (expand "member") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(Intersection const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(generated_subset_algebra const-decl "subset_algebra"
subset_algebra_def nil)
(member const-decl "bool" sets nil))
shostak))
(generated_subset_algebra_subset2 0
(generated_subset_algebra_subset2-1 nil 3449733118
("" (skosimp)
(("" (expand "subset?" +)
(("" (expand "member")
(("" (skosimp)
(("" (expand "generated_subset_algebra")
(("" (expand "Intersection")
(("" (inst - "Y!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(Intersection const-decl "set" sets nil)
(Y!1 skolem-const-decl "setofsets[T]" subset_algebra_def nil)
(X!1 skolem-const-decl "setofsets[T]" subset_algebra_def nil)
(set type-eq-decl nil sets nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(generated_subset_algebra const-decl "subset_algebra"
subset_algebra_def nil)
(member const-decl "bool" sets nil))
shostak))
(generated_subset_algebra_idempotent 0
(generated_subset_algebra_idempotent-1 nil 3449733211
("" (skosimp)
(("" (typepred "B!1")
(("" (lemma "generated_subset_algebra_subset1" ("X" "B!1"))
((""
(lemma "generated_subset_algebra_subset2"
("X" "B!1" "Y" "B!1"))
(("" (assert)
(("" (rewrite "subset_reflexive")
((""
(lemma "subset_antisymmetric"
("a" "generated_subset_algebra(B!1)" "b" "B!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(generated_subset_algebra_subset2 formula-decl nil
subset_algebra_def nil)
(set type-eq-decl nil sets nil)
(subset_reflexive formula-decl nil sets_lemmas nil)
(generated_subset_algebra const-decl "subset_algebra"
subset_algebra_def nil)
(subset_antisymmetric formula-decl nil sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(generated_subset_algebra_subset1 formula-decl nil
subset_algebra_def nil))
shostak))
(intersection_subset_algebra 0
(intersection_subset_algebra-1 nil 3449733399
("" (skosimp)
(("" (typepred "A!1")
(("" (typepred "B!1")
(("" (expand "subset_algebra?")
(("" (flatten)
(("" (split)
(("1" (expand "subset_algebra_empty?")
(("1" (expand "member")
(("1" (expand "intersection")
(("1" (expand "member") (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "subset_algebra_complement?")
(("2" (skosimp)
(("2" (expand "complement")
(("2" (expand "member")
(("2" (expand "intersection")
(("2" (expand "member")
(("2" (inst - "x!1")
(("1" (inst - "x!1")
(("1" (assert) nil nil)
("2"
(typepred "x!1")
(("2"
(expand "intersection")
(("2"
(flatten)
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "x!1")
(("2"
(expand "intersection")
(("2"
(expand "member")
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "subset_algebra_union?")
(("3" (skosimp)
(("3" (typepred "x!1")
(("3" (typepred "y!1")
(("3" (expand "intersection")
(("3" (expand "member")
(("3" (flatten)
(("3" (inst - "x!1" "y!1")
(("3"
(inst - "x!1" "y!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(B!1 skolem-const-decl "subset_algebra" subset_algebra_def nil)
(set type-eq-decl nil sets nil)
(A!1 skolem-const-decl "subset_algebra" subset_algebra_def nil)
(x!1 skolem-const-decl "(intersection(A!1, B!1))"
subset_algebra_def nil)
(complement const-decl "set" sets nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(x!1 skolem-const-decl "(intersection(A!1, B!1))"
subset_algebra_def nil)
(y!1 skolem-const-decl "(intersection(A!1, B!1))"
subset_algebra_def nil)
(subset_algebra_union? const-decl "bool" subset_algebra_def nil))
shostak))
(subset_member 0
(subset_member-1 nil 3449733630
("" (skosimp)
(("" (expand "subset?")
(("" (skosimp)
(("" (expand "member")
(("" (expand "subset")
(("" (expand "generated_subset_algebra")
(("" (expand "Intersection")
(("" (skosimp)
(("" (typepred "a!1")
(("" (expand "subset?")
(("" (expand "member")
(("" (inst - "x!1")
(("" (assert)
(("" (hide 2)
((""
(expand "extend")
((""
(expand "Union")
(("" (inst + "B!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(generated_subset_algebra const-decl "subset_algebra"
subset_algebra_def nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil subset_algebra_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil) (Union const-decl "set" sets nil)
(subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(Intersection const-decl "set" sets nil)
(subset const-decl "subset_algebra" subset_algebra_def nil))
shostak))
(card_TCC1 0
(card_TCC1-1 nil 3455341025
("" (skosimp)
(("" (typepred "a!1")
(("" (expand "finite_disjoint_union?")
(("" (skosimp)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst -4 "n!1")
(("" (expand "member")
(("" (inst + "E!1")
(("" (expand "finite_disjoint_union_of?")
(("" (assert)
(("" (skosimp)
(("" (inst - "i!1")
(("" (flatten)
((""
(assert)
((""
(expand "member")
((""
(replace -3)
((""
(expand "empty?")
((""
(expand "member")
(("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_disjoint_union? const-decl "bool" subset_algebra_def 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 subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(finite_disjoint_union_of? const-decl "bool" subset_algebra_def
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(number nonempty-type-decl nil numbers nil)
(nonempty? const-decl "bool" sets nil))
nil))
(disjoint_algebra_construction 0
(disjoint_algebra_construction-1 nil 3450336806
("" (skosimp*)
((""
(case "subset?(finite_disjoint_unions(NX!1),generated_subset_algebra(NX!1))")
(("1"
(lemma "generated_subset_algebra_subset2"
("X" "NX!1" "Y" "finite_disjoint_unions(NX!1)"))
(("1" (split -1)
(("1"
(lemma "subset_antisymmetric"
("a" "generated_subset_algebra(NX!1)" "b"
"finite_disjoint_unions(NX!1)"))
(("1" (assert) nil nil)) nil)
("2" (hide-all-but 1)
(("2" (expand "finite_disjoint_unions")
(("2" (expand "fullset")
(("2" (expand "extend")
(("2" (expand "subset?")
(("2" (expand "member")
(("2" (skosimp)
(("2" (assert)
(("2" (prop)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.63 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.
|
