| products/Sources/formale Sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: borel.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(borel
(borel_TCC1 0 (borel_TCC1-1 nil 3384845712 ("" (subtype-tcc) nil nil) ((member const-decl "bool" sets nil) (T formal-type-decl nil borel nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (subset_algebra_complement? const-decl "bool" subset_algebra_def nil) (is_countable const-decl "bool" countability "sets_aux/") (sigma_algebra_union? const-decl "bool" subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (S formal-const-decl "topology" borel nil) (topology nonempty-type-eq-decl nil topology_prelim "topology/") (topology? const-decl "bool" topology_prelim "topology/") (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) (open? const-decl "bool" topology "topology/") (subset? const-decl "bool" sets nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (borel? const-decl "sigma_algebra" borel nil) (Intersection const-decl "set" sets nil) (emptyset_is_compact name-judgement "compact[T, S]" borel nil) (emptyset_is_clopen name-judgement "clopen[T, S]" borel nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)) nil)) (emptyset_is_borel 0 (emptyset_is_borel-1 nil 3384845734 ("" (expand "borel?") (("" (expand "fullset") (("" (expand "extend") (("" (expand "generated_sigma_algebra") (("" (expand "Intersection") (("" (skosimp) (("" (typepred "a!1") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_empty?") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset const-decl "set" sets nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (member const-decl "bool" 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 borel 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) (subset? const-decl "bool" sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (topology? const-decl "bool" topology_prelim "topology/") (topology nonempty-type-eq-decl nil topology_prelim "topology/") (S formal-const-decl "topology" borel nil) (open? const-decl "bool" topology "topology/") (TRUE const-decl "bool" booleans nil) (FALSE const-decl "bool" booleans nil) (Intersection const-decl "set" sets nil) (extend const-decl "R" extend nil) (borel? const-decl "sigma_algebra" borel nil) (emptyset_is_compact name-judgement "compact[T, S]" borel nil) (emptyset_is_clopen name-judgement "clopen[T, S]" borel nil) (subset_algebra_emptyset name-judgement "(S)" borel nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (fullset_is_borel 0 (fullset_is_borel-1 nil 3384845770 ("" (expand "borel?") (("" (expand "extend") (("" (expand "generated_sigma_algebra") (("" (expand "Intersection") (("" (skosimp) (("" (typepred "a!1") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_empty?") (("" (expand "subset_algebra_complement?") (("" (expand "member") (("" (inst - "emptyset[T]") (("" (rewrite "complement_emptyset") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extend const-decl "R" extend nil) (Intersection const-decl "set" sets nil) (FALSE const-decl "bool" booleans nil) (fullset const-decl "set" sets nil) (open nonempty-type-eq-decl nil topology "topology/") (open? const-decl "bool" topology "topology/") (S formal-const-decl "topology" borel nil) (topology nonempty-type-eq-decl nil topology_prelim "topology/") (topology? const-decl "bool" topology_prelim "topology/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (subset? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans 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 borel 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_complement? const-decl "bool" subset_algebra_def nil) (emptyset_is_compact name-judgement "compact[T, S]" borel nil) (emptyset_is_clopen name-judgement "clopen[T, S]" borel nil) (subset_algebra_emptyset name-judgement "(S)" borel nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (a!1 skolem-const-decl "({Y | sigma_algebra?(Y) AND subset?(LAMBDA (t: setof[T]): IF open?(t) THEN fullset[open](t) ELSE FALSE ENDIF, Y)})" borel nil) (emptyset const-decl "set" sets nil) (complement_emptyset formula-decl nil sets_lemmas nil) (member const-decl "bool" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (borel? const-decl "sigma_algebra" borel nil) (fullset_is_clopen name-judgement "clopen[T, S]" borel nil) (subset_algebra_fullset name-judgement "(S)" borel nil)) shostak)) (open_is_borel 0 (open_is_borel-1 nil 3357878377 ("" (skosimp) (("" (expand "borel?") (("" (expand "extend") (("" (expand "generated_sigma_algebra") (("" (expand "Intersection") (("" (skosimp) (("" (typepred "a!1") (("" (typepred "X!1") (("" (expand "subset?") (("" (expand "member") (("" (expand "fullset") (("" (inst - "X!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((borel? const-decl "sigma_algebra" borel nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (member const-decl "bool" 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 borel 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) (subset? const-decl "bool" sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (topology? const-decl "bool" topology_prelim "topology/") (topology nonempty-type-eq-decl nil topology_prelim "topology/") (S formal-const-decl "topology" borel nil) (open? const-decl "bool" topology "topology/") (open nonempty-type-eq-decl nil topology "topology/") (fullset const-decl "set" sets nil) (FALSE const-decl "bool" booleans nil) (Intersection const-decl "set" sets nil) (extend const-decl "R" extend nil)) nil)) (closed_is_borel 0 (closed_is_borel-1 nil 3357878377 ("" (skosimp) (("" (typepred "Y!1") (("" (expand "borel?") (("" (expand "extend") (("" (expand "generated_sigma_algebra") (("" (expand "Intersection") (("" (skosimp) (("" (typepred "a!1") (("" (expand "closed?") (("" (expand "member") (("" (lemma "open_is_borel" ("X" "complement(Y!1)")) (("" (expand "borel?") (("" (expand "extend") (("" (expand "generated_sigma_algebra") (("" (expand "Intersection") (("" (inst - "a!1") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_complement?") (("" (inst - "complement(Y!1)") (("" (rewrite "complement_complement") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (S formal-const-decl "topology" borel nil) (topology nonempty-type-eq-decl nil topology_prelim "topology/") (topology? const-decl "bool" topology_prelim "topology/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil borel nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (extend const-decl "R" extend nil) (Intersection const-decl "set" sets nil) (FALSE const-decl "bool" booleans nil) (fullset const-decl "set" sets nil) (open nonempty-type-eq-decl nil topology "topology/") (open? const-decl "bool" topology "topology/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (subset? const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (member const-decl "bool" sets nil) (a!1 skolem-const-decl "({Y | sigma_algebra?(Y) AND subset?(LAMBDA (t: setof[T]): IF open?(t) THEN fullset[open](t) ELSE FALSE ENDIF, Y)})" borel nil) (Y!1 skolem-const-decl "closed[T, S]" borel nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (complement_complement formula-decl nil sets_lemmas nil) (subset_algebra_complement? const-decl "bool" subset_algebra_def nil) (complement const-decl "set" sets nil) (open_is_borel formula-decl nil borel nil) (complement_closed_is_open application-judgement "open[T, S]" borel nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (borel? const-decl "sigma_algebra" borel nil)) nil)) (complement_is_borel 0 (complement_is_borel-1 nil 3384845885 ("" (skosimp) (("" (expand "borel?") (("" (expand "extend") (("" (expand "generated_sigma_algebra") (("" (expand "Intersection") (("" (skosimp*) (("" (typepred "a!2") (("" (typepred "a!1") (("" (expand "borel?") (("" (expand "extend") (("" (expand "generated_sigma_algebra") (("" (expand "Intersection") (("" (inst - "a!2") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_complement?") (("" (inst - "a!1") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset_algebra_complement application-judgement "(S)" borel nil) (borel? const-decl "sigma_algebra" borel nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (borel nonempty-type-eq-decl nil borel nil) (subset_algebra_complement? const-decl "bool" subset_algebra_def nil) (member const-decl "bool" sets nil) (a!1 skolem-const-decl "borel" borel nil) (a!2 skolem-const-decl "({Y | sigma_algebra?(Y) AND subset?(LAMBDA (t: setof[T]): IF open?(t) THEN fullset[open](t) ELSE FALSE ENDIF, Y)})" borel 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 borel 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) (subset? const-decl "bool" sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (topology? const-decl "bool" topology_prelim "topology/") (topology nonempty-type-eq-decl nil topology_prelim "topology/") (S formal-const-decl "topology" borel nil) (open? const-decl "bool" topology "topology/") (open nonempty-type-eq-decl nil topology "topology/") (fullset const-decl "set" sets nil) (FALSE const-decl "bool" booleans nil) (Intersection const-decl "set" sets nil) (extend const-decl "R" extend nil)) shostak)) (union_is_borel 0 (union_is_borel-1 nil 3384846934 ("" (skosimp) (("" (typepred "borel?") (("" (lemma "sigma_algebra_implies_subset_algebra" ("S" "borel?")) (("" (split -1) (("1" (hide -2) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((borel? const-decl "sigma_algebra" borel 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 borel 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 application-judgement "(S)" borel nil) (sigma_algebra_implies_subset_algebra formula-decl nil subset_algebra_def nil)) shostak)) (intersection_is_borel 0 (intersection_is_borel-1 nil 3384846540 ("" (skosimp) (("" (typepred "a!1") (("" (typepred "b!1") (("" (lemma "complement_is_borel") (("" (inst-cp - "a!1") (("" (inst-cp - "b!1") (("" (lemma "union_is_borel" ("a" "complement(a!1)" "b" "complement(b!1)")) (("" (inst - "union(complement(a!1), complement(b!1))") (("" (rewrite "demorgan2" -2 :dir rl) (("" (rewrite "complement_complement") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((borel nonempty-type-eq-decl nil borel nil) (borel? const-decl "sigma_algebra" borel 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 borel nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (complement_is_borel formula-decl nil borel nil) (subset_algebra_union application-judgement "(S)" borel nil) (union const-decl "set" sets nil) (intersection const-decl "set" sets nil) (complement_complement formula-decl nil sets_lemmas nil) (subset_algebra_intersection application-judgement "(S)" borel nil) (demorgan2 formula-decl nil sets_lemmas nil) (subset_algebra_complement application-judgement "(S)" borel nil) (union_is_borel formula-decl nil borel nil) (set type-eq-decl nil sets nil) (complement const-decl "set" sets nil)) shostak)) (difference_is_borel 0 (difference_is_borel-1 nil 3384846714 ("" (skosimp) (("" (rewrite "difference_intersection") (("" (typepred "a!1") (("" (typepred "b!1") (("" (lemma "complement_is_borel" ("a" "b!1")) (("" (rewrite "intersection_is_borel") nil nil)) nil)) nil)) nil)) nil)) nil) ((difference_intersection formula-decl nil sets_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets 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) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (borel? const-decl "sigma_algebra" borel nil) (borel nonempty-type-eq-decl nil borel nil) (T formal-type-decl nil borel nil) (subset_algebra_complement application-judgement "(S)" borel nil) (subset_algebra_intersection application-judgement "(S)" borel nil) (complement const-decl "set" sets nil) (intersection_is_borel formula-decl nil borel nil) (complement_is_borel formula-decl nil borel nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (Union_is_borel 0 (Union_is_borel-1 nil 3391050828 ("" (skosimp) (("" (typepred "borel?") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "sigma_algebra_union?") (("" (inst - "extend[setof[T], borel, bool, FALSE](A!1)") (("" (split -3) (("1" (assert) nil nil) ("2" (typepred "A!1") (("2" (hide-all-but (-1 1)) (("2" (expand "extend") (("2" (expand "is_countable") (("2" (skosimp*) (("2" (typepred "f!1") (("2" (inst + "f!1") (("2" (split) (("1" (skosimp) (("1" (case-replace "A!1(x!1)") (("1" (assert) (("1" (case-replace "borel?(x!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("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) ("3" (skosimp) (("3" (typepred "x!1") (("3" (expand "extend") (("3" (expand "member") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((borel? const-decl "sigma_algebra" borel 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 borel nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (borel nonempty-type-eq-decl nil borel nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (set type-eq-decl nil sets nil) (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (f!1 skolem-const-decl "(injective?[(A!1), nat])" borel nil) (A!1 skolem-const-decl "countable_set[borel]" borel nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (sigma_algebra_union? const-decl "bool" subset_algebra_def nil)) shostak)) (Complement_is_borel 0 (Complement_is_borel-1 nil 3391054293 ("" (expand "extend") (("" (expand "Complement") (("" (expand "every") (("" (skosimp*) (("" (typepred "x!1") (("" (skosimp) (("" (typepred "b!1") (("" (assert) (("" (lemma "complement_is_borel" ("a" "b!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Complement const-decl "setofsets[T]" sets_lemmas nil) (complement_is_borel formula-decl nil borel nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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 borel nil) (setof type-eq-decl nil defined_types nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (borel? const-decl "sigma_algebra" borel nil) (borel nonempty-type-eq-decl nil borel nil) (set type-eq-decl nil sets nil) (FALSE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (complement const-decl "set" sets nil) (every const-decl "bool" sets nil) (extend const-decl "R" extend nil)) shostak)) (Intersection_is_borel 0 (Intersection_is_borel-1 nil 3391054364 ("" (skosimp) (("" (typepred "A!1") (("" (case "FORALL (S:sigma_algebra[T],X:setofsets[T]): is_countable(X) AND (FORALL (x:(X)): member(x,S)) IMPLIES member(Intersection(X),S)") (("1" (inst - "borel?" "A!1") (("1" (expand "member") (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "extend") (("2" (expand "is_countable") (("2" (skosimp*) (("2" (typepred "f!1") (("2" (inst + "f!1") (("2" (split) (("1" (skosimp) (("1" (split) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (prop) nil nil)) nil)) nil)) nil)) nil) ("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) ("3" (hide -1 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "S!1") (("2" (expand "sigma_algebra?") (("2" (flatten) (("2" (case "is_countable(Complement(X!1))") (("1" (case "FORALL (x: (Complement(X!1))): member(x, S!1)") (("1" (hide -6 -7) (("1" (expand "sigma_algebra_union?") (("1" (inst -5 "Complement(X!1)") (("1" (assert) (("1" (replace -1 -5) (("1" (hide -1 -2 -3) (("1" (rewrite "Demorgan2" -2 :dir rl) (("1" (expand "subset_algebra_complement?") (("1" (inst - "complement(Intersection(X!1))") (("1" (rewrite "complement_complement") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -6 1)) (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "Complement") (("2" (skosimp) (("2" (expand "subset_algebra_complement?") (("2" (typepred "b!1") (("2" (inst -4 "b!1") (("2" (assert) (("2" (inst - "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (expand "is_countable") (("2" (skosimp*) (("2" (typepred "f!1") (("2" (inst + "lambda (x:(Complement(X!1))): f!1(complement(x))") (("1" (expand "injective?") (("1" (skosimp*) (("1" (inst - "complement[T](x1!1)" "complement[T](x2!1)") (("1" (rewrite "complement_equal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "Complement") (("2" (skosimp) (("2" (typepred "b!1") (("2" (replace -2) (("2" (rewrite "complement_complement") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (borel nonempty-type-eq-decl nil borel nil) (borel? const-decl "sigma_algebra" borel 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 borel nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (f!1 skolem-const-decl "(injective?[(X!1), nat])" borel nil) (complement_equal formula-decl nil sets_lemmas nil) (sigma_algebra_union? const-decl "bool" subset_algebra_def nil) (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Complement_bijective name-judgement "(bijective?[setofsets[T], setofsets[T]])" sets_lemmas nil) (subset_algebra_complement? const-decl "bool" subset_algebra_def nil) (complement_complement formula-decl nil sets_lemmas nil) (X!1 skolem-const-decl "setofsets[T]" borel nil) (complement const-decl "set" sets nil) (S!1 skolem-const-decl "sigma_algebra[T]" borel nil) (Demorgan2 formula-decl nil sets_lemmas nil) (Complement const-decl "setofsets[T]" sets_lemmas nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (A!1 skolem-const-decl "countable_set[borel]" borel nil) (f!1 skolem-const-decl "(injective?[(A!1), nat])" borel 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) (injective? const-decl "bool" functions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (Intersection const-decl "set" sets nil)) shostak)) (open_is_borel_judge 0 (open_is_borel_judge-1 nil 3384845712 ("" (lemma "open_is_borel") (("" (propax) nil nil)) nil) ((open_is_borel formula-decl nil borel nil)) nil)) (closed_is_borel_judge 0 (closed_is_borel_judge-1 nil 3384845712 ("" (skosimp) (("" (typepred "x!1") (("" (expand "closed?") (("" (expand "member") (("" (lemma "open_is_borel" ("X" "complement(x!1)")) (("" (lemma "complement_is_borel" ("a" "complement(x!1)")) (("" (rewrite "complement_complement") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (S formal-const-decl "topology" borel nil) (topology nonempty-type-eq-decl nil topology_prelim "topology/") (topology? const-decl "bool" topology_prelim "topology/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil borel nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (complement_is_borel formula-decl nil borel nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (borel? const-decl "sigma_algebra" borel nil) (borel nonempty-type-eq-decl nil borel nil) (complement_complement formula-decl nil sets_lemmas nil) (complement_closed_is_open application-judgement "open[T, S]" borel nil) (open_is_borel formula-decl nil borel nil) (open? const-decl "bool" topology "topology/") (open nonempty-type-eq-decl nil topology "topology/") (complement const-decl "set" sets nil)) nil)) (borel_basis 0 (borel_basis-1 nil 3384849051 ("" (skosimp) (("" (expand "borel?") (("" (expand "fullset") (("" (expand "extend") (("" (expand "generated_sigma_algebra") (("" (expand "Intersection") (("" (skosimp) (("" (typepred "a!1") (("" (inst - "a!1") (("" (hide 2) (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (typepred "B!1") (("" (expand "base?") (("" (flatten) (("" (expand "subset?") (("" (expand "member") (("" (inst - "x!1") (("" (inst -5 "x!1") (("" (expand "open?") (("" (expand "member") (("" (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) ((borel? const-decl "sigma_algebra" borel nil) (extend const-decl "R" extend nil) (Intersection const-decl "set" sets nil) (FALSE const-decl "bool" booleans nil) (TRUE const-decl "bool" booleans nil) (open? const-decl "bool" topology "topology/") (S formal-const-decl "topology" borel nil) (topology nonempty-type-eq-decl nil topology_prelim "topology/") (topology? const-decl "bool" topology_prelim "topology/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (subset? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans 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 borel nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (a!1 skolem-const-decl "({Y | sigma_algebra?(Y) AND subset?(LAMBDA (t: setof[T]): IF open?(t) THEN TRUE ELSE FALSE ENDIF, Y)})" borel nil) (B!1 skolem-const-decl "(base?[T](S))" borel nil) (base? const-decl "bool" basis "topology/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (fullset const-decl "set" sets nil)) shostak)) (borel_countable_basis 0 (borel_countable_basis-1 nil 3384849248 ("" (skosimp) (("" (apply-extensionality 1 :hide? t) (("" (case-replace "borel?(x!1)") (("1" (expand "borel?") (("1" (expand "fullset") (("1" (expand "extend") (("1" (expand "generated_sigma_algebra") (("1" (expand "Intersection") (("1" (skosimp) (("1" (typepred "a!1") (("1" (typepred "B!1") (("1" (inst - "a!1") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) (("1" (prop) (("1" (hide 2) (("1" (expand "base?") (("1" (flatten) (("1" (expand "open?") (("1" (expand "member") (("1" (inst - "x!2") (("1" (skosimp) (("1" (lemma "countable_subset" ("S" "V!1" "Count" "B!1")) (("1" (assert) (("1" (expand "sigma_algebra?") (("1" (flatten) (("1" (expand "sigma_algebra_union?") (("1" (inst -8 "V!1") (("1" (replace -5) (("1" (replace -1) (("1" (expand "member") (("1" (skosimp) (("1" (typepred "x!3") (("1" (expand "subset?") (("1" (inst -5 "x!3") (("1" (inst -9 "x!3") (("1" (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)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "borel_basis" ("B" "B!1" "Z" "x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil borel 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) (S formal-const-decl "topology" borel nil) (base? const-decl "bool" basis "topology/") (topology nonempty-type-eq-decl nil topology_prelim "topology/") (topology? const-decl "bool" topology_prelim "topology/") (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (borel? const-decl "sigma_algebra" borel nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (borel_basis formula-decl nil borel nil) (extend const-decl "R" extend nil) (Intersection const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (FALSE const-decl "bool" booleans nil) (TRUE const-decl "bool" booleans nil) (open? const-decl "bool" topology "topology/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (B!1 skolem-const-decl "(base?[T](S))" borel nil) (a!1 skolem-const-decl "({Y | sigma_algebra?(Y) AND subset?(B!1, Y)})" borel nil) (member const-decl "bool" sets nil) (x!2 skolem-const-decl "setof[T]" borel nil) (countable_subset formula-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (sigma_algebra_union? const-decl "bool" subset_algebra_def nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (fullset const-decl "set" sets nil)) shostak))) ¤ Dauer der Verarbeitung: 0.64 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.Bot Zugriff |
