| 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 454 kB |
|
Impressum measure_def.prfSprache: Lisp |
|||||||||||||||
|
(measure_def (IMP_generalized_measure_def_TCC1 0 (IMP_generalized_measure_def_TCC1-1 nil 3458457144 ("" (assuming-tcc) nil nil) ((finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (subset_algebra_emptyset name-judgement "(S)" measure_def nil)) nil)) (increasing_indexed_measurable_TCC1 0 (increasing_indexed_measurable_TCC1-1 nil 3450166483 ("" (expand "increasing_indexed_measurable?") (("" (expand "increasing_indexed?") (("" (split) (("1" (apply-extensionality :hide? t) (("1" (expand "fullset") (("1" (expand "IUnion") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "increasing?") (("2" (expand "subset?") (("2" (expand "fullset") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing_indexed? const-decl "bool" nat_indexed_sets "sets_aux/") (increasing? const-decl "bool" fun_preds_partial "structures/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_def nil) (fullset const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (set type-eq-decl nil sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (increasing_indexed_measurable? const-decl "bool" measure_def nil) (subset_algebra_fullset name-judgement "(S)" measure_def nil)) nil)) (sigma_finite_measure_TCC1 0 (sigma_finite_measure_TCC1-1 nil 3396670582 ("" (expand "sigma_finite_measure?") (("" (split) (("1" (lemma "measure_type_TCC1") (("1" (propax) nil nil)) nil) ("2" (expand "measure_sigma_finite?") (("2" (expand "zero_measure") (("2" (inst + "lambda i: if i = 0 then fullset[T] else emptyset[T] endif") (("1" (apply-extensionality :hide? t) (("1" (expand "fullset") (("1" (expand "IUnion") (("1" (inst + "0") nil nil)) nil)) nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (expand "fullset") (("2" (expand "emptyset") (("2" (expand "disjoint?") (("2" (skosimp) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (case-replace "i!1=0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measure_type_TCC1 subtype-tcc nil generalized_measure_def nil) (T formal-type-decl nil measure_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) (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "subset_algebra" measure_def nil) (zero_measure const-decl "extended_nnreal" generalized_measure_def nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/") (IUnion const-decl "set[T]" indexed_sets nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def 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) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (set type-eq-decl nil sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (fullset const-decl "set" sets nil) (emptyset const-decl "set" sets nil) (subset_algebra_fullset name-judgement "(S)" measure_def nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (subset_algebra_emptyset name-judgement "(S)" measure_def nil) (measure_sigma_finite? const-decl "bool" measure_def nil) (sigma_finite_measure? const-decl "bool" measure_def nil)) nil)) (discrete_measure_TCC1 0 (discrete_measure_TCC1-1 nil 3396670582 ("" (expand "measure?") (("" (split) (("1" (expand "measure_empty?") (("1" (rewrite "card_emptyset[T]") nil nil)) nil) ("2" (expand "measure_countably_additive?") (("2" (name-replace "MM" "LAMBDA a: IF is_finite[T](a) THEN (TRUE, card[T](a)) ELSE (FALSE, 0) ENDIF") (("2" (skosimp) (("2" (expand "x_eq") (("2" (expand "o ") (("2" (expand "MM") (("2" (expand "x_sum") (("2" (case-replace "FORALL i: IF is_finite[T](X!1(i)) THEN TRUE ELSE FALSE ENDIF") (("1" (case "FORALL i: is_finite[T](X!1(i))") (("1" (hide -2) (("1" (case-replace "(LAMBDA (i_1: nat): IF is_finite[T](X!1(i_1)) THEN card[T](X!1(i_1)) ELSE 0 ENDIF)=LAMBDA (i_1: nat):card[T](X!1(i_1))") (("1" (hide -1) (("1" (case "FORALL i: series(LAMBDA (i_1: nat): card[T](X!1(i_1)))(i) = card[T](IUnion(lambda (n:na (("1" (case "FORALL i: is_finite[T](IUnion(LAMBDA (n: nat): IF n <= i THEN X!1(n) ELSE emptyset[T] ENDIF))") (("1" (name-replace "CS" "series(LAMBDA (i_1: nat): card[T](X!1(i_1)))") (("1" (case-replace "is_finite[T](IUnion(X!1))") (("1" (assert) (("1" (case-replace "convergent(CS)") (("1" (case "increasing?(CS)") (("1" (case "FORALL i: CS(i) <= card[T](IUnion(X!1))") (("1" (lemma "converges_upto_is_lub" ("u" "CS" "x" "card[T](IUnion(X!1))")) (("1" (expand "converges_upto?" -1) (("1" (replace -3) (("1" (flatten -1) (("1" (hide -1) (("1" (split -1) (("1" (rewrite "convergence_sequences.limit_def") (("1" (hide-all-but (-1 1)) (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (expand "convergence") (("1" (expand "ball") (("1" (expand "member") (("1" (skosimp) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_above?") (("2" (inst + "card[T](IUnion(X!1))") nil nil)) nil)) nil) ("3" (hide 2) (("3" (expand "fullset") (("3" (expand "image") (("3" (expand "least_upper_bound?") (("3" (split) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "upper_bound?") (("2" (case "y!1<card[T](IUnion(X!1))") (("1" (hide 1) (("1" (case "exists i: IUnion(LAMBDA (n: nat): IF n <= i THEN X!1(n) ELSE emptyset[T] ENDIF) = IUnion(X!1)") (("1" (skosimp) (("1" (inst -3 "CS(i!1)") (("1" (inst -9 "i!1") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "i!1") nil nil)) nil)) nil) ("2" (hide -1 -2) (("2" (lemma "convergence_cauchy1" ("u" "CS")) (("2" (assert) (("2" (expand "cauchy") (("2" (inst - "1/2") (("2" (skosimp) (("2" (inst + "n!1") (("2" (apply-extensionality :hide? t) (("2" (inst - "_" "n!1") (("2" (assert) (("2" (case-replace "IUnion(LAMBDA (n: nat): IF n <= n!1 THEN X!1(n) ELSE emptyset[T] ENDIF) (x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (expand "emptyset") (("1" (prop) (("1" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (expand "IUnion") (("2" (skosimp) (("2" (expand "emptyset") (("2" (case "i!1>n!1") (("1" (inst - "i!1") (("1" (assert) (("1" (hide 1) (("1" (expand "increasing?") (("1" (inst -5 "n!1" "i!1") (("1" (assert) (("1" (expand "abs" -3) (("1" (assert) (("1" (expand "<=" -5) (("1" (split -5) (("1" (assert) (("1" (inst-cp -9 "n!1") (("1" (inst -9 "i!1") (("1" (replace -10) (("1" (replace -9) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -4) (("2" (inst-cp -8 "n!1") (("2" (inst -8 "i!1") (("2" (replace -9) (("2" (replace -8) (("2" (hide -9 -8) (("2" (lemma "same_card_subset[T]" ("A" "{x: T | EXISTS (i_1: nat): IF i_1 <= n!1 THEN X!1(i_1)(x) ELSE FALSE ENDIF}" "B" "{x_1: T | EXISTS (i_2: nat): IF i_2 <= i!1 THEN X!1(i_2)(x_1) ELSE FALSE ENDIF}")) (("1" (replace -2) (("1" (hide -2) (("1" (split -1) (("1" (lemma "extensionality_postulate" ("f" "{x_1: T | EXISTS (i_2: nat): IF i_2 <= n!1 THEN X!1(i_2)(x_1) ELSE FALSE ENDIF}" "g" "{x_2: T | EXISTS (i_1: nat): IF i_1 <= i!1 THEN X!1(i_1)(x_2) ELSE FALSE ENDIF}")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (inst - "x!1") (("1" (case-replace "(EXISTS (i_2: nat): IF i_2 <= n!1 THEN X!1(i_2)(x!1) ELSE FALSE ENDIF)") (("1" (skosimp) (("1" (prop) (("1" (typepred "X!1") (("1" (expand "disjoint_indexed_measurable?") (("1" (expand "disjoint?") (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "i!2" "i!1") (("1" (assert) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (assert) (("2" (inst 2 "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) (("2" (inst + "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -7 "i!1") nil nil) ("3" (inst -7 "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "i!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) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (inst -4 "i!1") (("2" (replace -4) (("2" (lemma "card_subset[T]" ("A" "IUnion(LAMBDA (n: nat): IF n <= i!1 THEN X!1(n) ELSE emptyset[T] ENDIF)" "B" "IUnion(X!1)")) (("2" (assert) (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) (("2" (inst + "i!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (inst-cp -4 "i!1") (("2" (inst -4 "j!1") (("2" (replace -4) (("2" (replace -5) (("2" (hide -4 -5) (("2" (lemma "card_subset[T]" ("A" "IUnion(LAMBDA (n_1: nat): IF n_1 <= i!1 THEN X!1(n_1) ELSE emptyset[T] ENDIF)" "B" "IUnion(LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF)")) (("2" (assert) (("2" (hide 2) (("2" (expand "IUnion") (("2" (expand "subset?") (("2" (expand "emptyset") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) (("2" (inst + "i!2") (("2" (assert) 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" (hide 2) (("2" (case "forall i: CS(i) <= card[T](IUnion(X!1))") (("1" (case "increasing?(CS)") (("1" (lemma "converges_upto_is_lub" ("u" "CS" "x" "card[T](IUnion(X!1))")) (("1" (expand "converges_upto?") (("1" (replace -2) (("1" (flatten -1) (("1" (hide -1) (("1" (split -1) (("1" (rewrite "metric_convergence_def") (("1" (hide-all-but (-1 1)) (("1" (expand "metric_converges_to") (("1" (expand "ball") (("1" (expand "member") (("1" (assert) (("1" (expand "convergent?") (("1" (expand "convergence") (("1" (inst + "card[T](IUnion(X!1))") (("1" (skosimp) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_above?") (("2" (inst + "card[T](IUnion(X!1))") nil nil)) nil)) nil) ("3" (hide 2) (("3" (expand "fullset") (("3" (expand "image") (("3" (expand "least_upper_bound?") (("3" (split) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (case "y!1<card[T](IUnion(X!1))") (("1" (hide 1) (("1" (expand "upper_bound?") (("1" (case "exists i: IUnion(LAMBDA (n: nat): IF n <= i THEN X!1(n) ELSE emptyset[T] ENDIF) = IUnion(X!1)") (("1" (skosimp) (("1" (inst -8 "i!1") (("1" (replace -1) (("1" (inst -3 "CS(i!1)") (("1" (assert) nil nil) ("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 -8 1)) (("2" (case "forall (Y:sequence[set[T]],n:nat): (FORALL i: is_finite[T](Y(i)))& is_finite(IUn IUnion(LAMBDA (m: nat): IF m <= i THEN Y(m) ELSE emptyset[T] ENDIF) = IUnion(Y)") (("1" (inst - "X!1" "card(IUnion(X!1))") (("1" (replace -2) (("1" (replace -3) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 2) (("2" (induct "n") (("1" (skosimp) (("1" (inst + "0") (("1" (apply-extensionality :hide? t) (("1" (lemma "card_is_0[T]" ("S" "IUnion(Y!1)")) (("1" (assert) (("1" (replace -1) (("1" (expand "emptyset" 1) (("1" (expand "IUnion" -2) (("1" (skosimp) (("1" (prop) (("1" (rewrite "emptyset_is_empty?" -3 :dir rl) (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (expand "IUnion") (("1" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "nonempty_card[T]" ("S" "IUnion(Y!1)")) (("2" (assert) (("2" (lemma "choose_rest[T]" ("a" "IUnion(Y!1)")) (("2" (expand "nonempty?") (("2" (assert) (("2" (lemma "card_rest[T]" ("S" "IUnion(Y!1)")) (("2" (replace -6) (("2" (assert) (("2" (lemma "choose_member[T]" ("a" "IUnion(Y!1)")) (("2" (name-replace "CC" "choose(IUnion(Y!1))") (("2" (replace 1 -1) (("2" (name "YY" "lambda i: remove[T](CC,Y!1(i))") (("2" (inst -5 "YY") (("2" (case "IUnion(YY)=rest(IUnion(Y!1))") (("1" (replace -1) (("1" (replace -4) (("1" (lemma "finite_rest[T]" ("A" "IUnion(Y!1)")) (("1" (replace -1) (("1" (split -7) (("1" (skosimp) (("1" (expand "member" -5) (("1" (expand "IUnion" -5) (("1" (skosimp) (("1" (inst + "max(i!1,i!2)") (("1" (apply-extensionality :hide? t) (("1" (case-replace "IUnion(Y!1)(x!1)") (("1" (replace -8 -1 rl) (("1" (expand "add" -1) (("1" (split -1) (("1" (expand "IUnion" 1) (("1" (inst + "i!2") (("1" (expand "emptyset") (("1" (assert) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 -1 rl) (("2" (expand "member") (("2" (expand "IUnion" (-1 1)) (("2" (skosimp) (("2" (hide-all-but (-1 -6 1)) (("2" (expand "emptyset") (("2" (prop) (("2" (expand "YY") (("2" (expand "remove") (("2" (flatten) (("2" (expand "member") (("2" (inst + "i!3") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (expand "IUnion" (-1 1)) (("2" (skosimp) (("2" (expand "emptyset") (("2" (prop) (("2" (inst + "i!3") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-7 1 2)) (("2" (skosimp) (("2" (inst - "i!1") (("2" (expand "YY") (("2" (lemma "finite_remove[T]" ("x" "CC" "A" "Y!1(i!1)")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3 -5) (("2" (apply-extensionality :hide? t) (("2" (expand "YY") (("2" (expand "rest" 1) (("2" (expand "CC" 1) (("2" (expand "IUnion" 1) (("2" (expand "remove") (("2" (expand "member") (("2" (case-replace "choose({x: T | EXISTS (i: nat): Y!1(i)(x)}) /= x!1") (("1" (assert) nil nil) ("2" (expand "nonempty?") (("2" (expand "IUnion") (("2" (propax) 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) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (inst-cp -5 "i!1") (("2" (inst -5 "j!1") (("2" (replace -5) (("2" (replace -6) (("2" (hide -5 -6) (("2" (lemma "card_subset[T]" ("A" "IUnion(LAMBDA (n_1: nat): IF n_1 <= i!1 THEN X!1(n_1) ELSE emptyset[T] ENDIF)" "B" "IUnion(LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF)")) (("2" (assert) (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "IUnion") (("2" (expand "member") (("2" (expand "emptyset") (("2" (skosimp*) (("2" (prop) (("2" (inst + "i!2") (("2" (assert) 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" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (replace -3) (("2" (lemma "card_subset[T]" ("A" "IUnion(LAMBDA (n: nat): IF n <= i!1 THEN X!1(n) ELSE emptyset[T] ENDIF)" "B" "IUnion(X!1)")) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide -3 2) (("2" (expand "subset?") (("2" (expand "IUnion") (("2" (expand "member") (("2" (expand "emptyset") (("2" (skosimp*) (("2" (prop) (("2" (inst + "i!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "convergent(CS)") (("1" (lemma "convergence_cauchy1" ("u" "CS")) (("1" (assert) (("1" (expand "cauchy") (("1" (inst - "1/2") (("1" (skosimp) (("1" (case "IUnion(LAMBDA (n: nat): IF n <= n!1 THEN X!1(n) ELSE emptyset[T] ENDIF) = IUnion(X!1)") (("1" (inst -4 "n!1") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "IUnion" 1) (("2" (case-replace "(EXISTS (i: nat): IF i <= n!1 THEN X!1(i)(x!1) ELSE emptyset[T](x!1) ENDIF)") (("1" (skosimp) (("1" (prop) (("1" (inst + "i!1") nil nil) ("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (case "i!1>n!1") (("1" (inst - "i!1" "n!1") (("1" (assert) (("1" (inst-cp -6 "i!1") (("1" (inst -6 "n!1") (("1" (replace -6) (("1" (replace -7) (("1" (hide -6 -7) (("1" (hide 1) (("1" (inst-cp - "i!1") (("1" (inst - "n!1") (("1" (name-replace "IU_n" "IUnion(LAMBDA (n: nat): IF n <= n!1 THEN X!1(n) ELSE emptyset[T] ENDIF)") (("1" (name-replace "IU_i" "IUnion(LAMBDA (n: nat): IF n <= i!1 THEN X!1(n) ELSE emptyset[T] ENDIF)") (("1" (lemma "card_subset[T]" ("A" "IU_n" "B" "IU_i")) (("1" (split -1) (("1" (expand "abs") (("1" (expand "<=" -1) (("1" (split -1) (("1" (assert) nil nil) ("2" (assert) (("2" (typepred "X!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (expand "disjoint?") (("2" (inst - "i!1" "n!1") (("2" (assert) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (inst - "x!1") (("2" (expand "member") (("2" (lemma "same_card_subset[T]" ("A" "IU_n" "B" "IU_i")) (("2" (split) (("1" (lemma "extensionality_postulate" ("f" "IU_n" "g" "IU_i")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (inst - "x!1") (("1" (expand "IU_n" -1) (("1" (expand "IU_i" -1) (("1" (expand "IUnion" -1) (("1" (expand "emptyset") (("1" (case-replace "EXISTS (i: nat): IF i <= n!1 THEN X!1(i)(x!1) ELSE FALSE ENDIF") (("1" (skosimp) (("1" (prop) (("1" (typepred "X!1") (("1" (expand "disjoint_indexed_measurable?") (("1" (expand "disjoint?") (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "i!2" "i!1") (("1" (assert) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (assert) (("2" (inst 2 "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "subset?") (("2" (expand "IU_n") (("2" (expand "IU_i") (("2" (expand "member") (("2" (skosimp) (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (skosimp) (("2" (prop) (("2" (inst + "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "subset?") (("2" (expand "IU_n") (("2" (expand "IU_i") (("2" (expand "member") (("2" (expand "IUnion") (("2" (skosimp*) (("2" (expand "emptyset") (("2" (prop) (("2" (inst + "i!2") (("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) ("2" (inst + "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (copy -1) (("2" (induct "i") (("1" (case-replace "(IUnion(LAMBDA (n: nat): IF n <= 0 THEN X!1(n) ELSE emptyset[T] ENDIF))=X!1(0)") (("1" (inst - "0") nil nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (case-replace "X!1(0)(x!1)") (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case-replace "IUnion(LAMBDA (n: nat): IF n <= j!1 + 1 THEN X!1(n) ELSE emptyset[T] ENDIF)=union(X!1(1+j!1),IUnion(LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF))") (("1" (hide -1) (("1" (lemma "finite_union[T]" ("A" "X!1(1 + j!1)" "B" "IUnion(LAMBDA (n_1: nat): IF n_1 <= j!1 THEN X!1(n_1) ELSE emptyset[T] ENDIF)")) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (inst - "1+j!1") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "union") (("2" (expand "member") (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (case-replace "X!1(1 + j!1)(x!1)") (("1" (inst + "1+j!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (case-replace "EXISTS (i: nat): IF i <= j!1 THEN X!1(i)(x!1) ELSE FALSE ENDIF") (("1" (skosimp) (("1" (prop) (("1" (inst + "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1 3) (("2" (assert) (("2" (skosimp) (("2" (prop) (("2" (expand "<=" -1) (("2" (split -1) (("1" (inst + "i!1") (("1" (assert) nil 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) ("2" (hide 2) (("2" (expand "series") (("2" (copy -1) (("2" (induct "i") (("1" (case-replace "IUnion(LAMBDA (n: nat): IF n <= 0 THEN X!1(n) ELSE emptyset[T] ENDIF) =X!1(0)") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (case-replace "X!1(0)(x!1)") (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (case-replace "IUnion(LAMBDA (n: nat): IF n <= 1 + j!1 THEN X!1(n) ELSE emptyset[T] ENDIF)=union(X!1(1+j!1),IUnion(LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF))") (("1" (hide -1) (("1" (case "disjoint?(X!1(1+j!1),IUnion(LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF))") (("1" (lemma "card_disj_union[T]" ("A" "X!1(1 + j!1)" "B" "IUnion(LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF)")) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (hide-all-but 1) (("2" (typepred "X!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (expand "disjoint?") (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) (("2" (inst - "i!1" "1+j!1") (("2" (assert) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality :hide? t) (("2" (expand "union") (("2" (expand "member") (("2" (expand "IUnion") (("2" (case-replace "X!1(1 + j!1)(x!1)") (("1" (inst + "1+j!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "emptyset") (("2" (case-replace "(EXISTS (i: nat): IF i <= j!1 THEN X!1(i)(x!1) ELSE FALSE ENDIF)") (("1" (skosimp) (("1" (prop) (("1" (inst + "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1 3) (("2" (assert) (("2" (skosimp) (("2" (prop) (("2" (inst + "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (induct "i") (("1" (case-replace "IUnion[nat, T] (LAMBDA (n: nat): IF n <= 0 THEN X!1(n) ELSE emptyset[T] ENDIF)=X!1(0)") (("1" (inst - "0") nil nil) ("2" (hide-all-but 1) (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (apply-extensionality :hide? t) (("2" (case-replace "X!1(0)(x!1)") (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case-replace "IUnion[nat, T] (LAMBDA (n: nat): IF n <= j!1 + 1 THEN X!1(n) ELSE emptyset[T] ENDIF)=union(X!1(1+j!1),IUnion[nat, T] (LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF))") (("1" (hide -1) (("1" (lemma "finite_union[T]" ("A" "X!1(1 + j!1)" "B" "IUnion[nat, T] (LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF)")) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (inst - "1+j!1") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "union") (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (expand "member") (("2" (apply-extensionality :hide? t) (("2" (case-replace "X!1(1 + j!1)(x!1)") (("1" (inst + "1+j!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (case-replace "(EXISTS (i: nat): IF i <= j!1 THEN X!1(i)(x!1) ELSE FALSE ENDIF)") (("1" (skosimp) (("1" (prop) (("1" (inst + "i!2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1 3) (("2" (assert) (("2" (skosimp) (("2" (prop) (("2" (expand "<=" -1) (("2" (split -1) (("1" (inst + "i!2") (("1" (assert) nil 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) ("3" (hide 2) (("3" (induct "i") (("1" (expand "emptyset") (("1" (expand "IUnion") (("1" (case-replace "{x_1: T | EXISTS (i: nat): IF i <= 0 THEN X!1(i)(x_1) ELSE FALSE ENDIF}=X!1(0)") (("1" (inst - "0") nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (case-replace "X!1(0)(x!1)") (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case-replace "(IUnion[nat, T] (LAMBDA (n: nat): IF n <= j!1 + 1 THEN X!1(n) ELSE emptyset[T] ENDIF))=union(X!1(j!1+1),(IUnion[nat, T] (LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF)))") (("1" (hide -1) (("1" (lemma "finite_union[T]" ("A" "X!1(j!1 + 1)" "B" "IUnion[nat, T] (LAMBDA (n: nat): IF n <= j!1 THEN X!1(n) ELSE emptyset[T] ENDIF)")) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (inst - "1+j!1") nil nil)) nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality :hide? t) (("2" (expand "union") (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (expand "member") (("2" (case-replace "X!1(1 + j!1)(x!1)") (("1" (inst + "1+j!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (case-replace "(EXISTS (i: nat): IF i <= j!1 THEN X!1(i)(x!1) ELSE FALSE ENDIF)") (("1" (skosimp) (("1" (prop) (("1" (inst + "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1 3) (("2" (assert) (("2" (skosimp) (("2" (prop) (("2" (expand "<=" -1) (("2" (split -1) (("1" (inst + "i!1") (("1" (assert) nil 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) ("4" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "i!1") (("2" (prop) nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (prop) (("2" (lemma "finite_subset[T]" ("A" "IUnion(X!1)" "s" "X!1(i!1)")) (("1" (assert) (("1" (expand "IUnion") (("1" (expand "subset?") (("1" (skosimp) (("1" (expand "member") (("1" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil measure_def nil) (card_emptyset formula-decl nil finite_sets nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (subset_algebra_emptyset name-judgement "(S)" measure_def nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets 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) (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "subset_algebra" measure_def 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) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (TRUE const-decl "bool" booleans nil) (finite_set type-eq-decl nil finite_sets 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) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (FALSE const-decl "bool" booleans nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (MM skolem-const-decl "[(S) -> [bool, naturalnumber]]" measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (card_disj_union formula-decl nil finite_sets nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (X!1 skolem-const-decl "disjoint_indexed_measurable[T, S]" measure_def nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (converges_upto? const-decl "bool" convergence_aux "metric_space/") (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (ball const-decl "set[T]" metric_space_def "metric_space/") (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (member const-decl "bool" sets nil) (convergence const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (limit_def formula-decl nil convergence_sequences "analysis/") (bounded_above? const-decl "bool" real_fun_preds "reals/") (fullset const-decl "set" sets nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (< const-decl "bool" reals nil) (CS skolem-const-decl "sequence[real]" measure_def nil) (i!1 skolem-const-decl "nat" measure_def nil) (convergence_cauchy1 formula-decl nil convergence_sequences "analysis/") (cauchy const-decl "bool" convergence_sequences "analysis/") (same_card_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (extensionality_postulate formula-decl nil functions nil) (subset_algebra_intersection application-judgement "(S)" measure_def nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (image const-decl "set[R]" function_image nil) (converges_upto_is_lub formula-decl nil convergence_aux "metric_space/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (card_subset formula-decl nil finite_sets nil) (increasing? const-decl "bool" real_fun_preds "reals/") (i!1 skolem-const-decl "nat" measure_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (card_is_0 formula-decl nil finite_sets nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (nonempty_card formula-decl nil finite_sets nil) (choose_rest formula-decl nil sets_lemmas nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (choose_member formula-decl nil sets_lemmas nil) (CC skolem-const-decl "(IUnion(Y!1))" measure_def nil) (finite_rest judgement-tcc nil finite_sets nil) (YY skolem-const-decl "[nat -> set[T]]" measure_def nil) (add const-decl "(nonempty?)" sets nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (finite_remove judgement-tcc nil finite_sets nil) (rest const-decl "set" sets nil) (remove const-decl "set" sets nil) (choose const-decl "(p)" sets nil) (card_rest formula-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (IU_i skolem-const-decl "set[T]" measure_def nil) (IU_n skolem-const-decl "set[T]" measure_def nil) (minus_int_is_int application-judgement "int" integers nil) (finite_union judgement-tcc nil finite_sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (union const-decl "set" sets nil) (emptyset const-decl "set" sets nil) (<= const-decl "bool" reals nil) (IUnion const-decl "set[T]" indexed_sets nil) (series const-decl "sequence[real]" series "series/") (sequence type-eq-decl nil sequences nil) (finite_subset formula-decl nil finite_sets nil) (x_sum const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (O const-decl "T3" function_props nil) (measure_countably_additive? const-decl "bool" generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil)) nil)) (sigma_finite_measure_is_measure 0 (sigma_finite_measure_is_measure-1 nil 3396670582 ("" (judgement-tcc) nil nil) ((NOT const-decl "[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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (sigma_finite_measure? const-decl "bool" measure_def nil) (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil) (measure_sigma_finite? const-decl "bool" measure_def nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (subset_algebra_emptyset name-judgement "(S)" measure_def nil) (S formal-const-decl "subset_algebra" measure_def 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_def nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (O const-decl "T3" function_props nil) (series const-decl "sequence[real]" series "series/") (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (measure_countably_additive? const-decl "bool" generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")) nil)) (complete_sigma_finite_is_complete_measure 0 (complete_sigma_finite_is_complete_measure-1 nil 3421359236 ("" (skolem + ("mu!1")) (("" (typepred "mu!1") (("" (expand "complete_sigma_finite?") (("" (flatten) (("" (expand "complete_measure?") (("" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complete_sigma_finite type-eq-decl nil measure_def nil) (complete_sigma_finite? const-decl "bool" measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (S formal-const-decl "subset_algebra" measure_def 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 measure_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (complete_measure? const-decl "bool" generalized_measure_def nil)) nil)) (complete_sigma_finite_is_sigma_finite_measure 0 (complete_sigma_finite_is_sigma_finite_measure-1 nil 3421359236 ("" (skolem + ("mu!1")) (("" (typepred "mu!1") (("" (expand "complete_sigma_finite?") (("" (expand "sigma_finite_measure?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((complete_sigma_finite type-eq-decl nil measure_def nil) (complete_sigma_finite? const-decl "bool" measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (S formal-const-decl "subset_algebra" measure_def 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 measure_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sigma_finite_measure? const-decl "bool" measure_def nil)) nil)) (measure_monotone 0 (measure_monotone-1 nil 3396804295 ("" (skosimp) (("" (lemma "measure_disjoint_union" ("f" "f!1" "a" "a!1" "b" "difference(b!1,a!1)")) (("" (assert) (("" (split -1) (("1" (case-replace "union(a!1, difference(b!1, a!1)) = b!1") (("1" (hide -1) (("1" (expand "x_add") (("1" (expand "x_eq") (("1" (expand "x_le") (("1" (flatten) (("1" (case-replace "f!1(a!1)`1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (apply-extensionality :hide? t) (("2" (expand "difference") (("2" (expand "union") (("2" (expand "subset?") (("2" (expand "member") (("2" (assert) (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "difference") (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "subset_algebra" measure_def 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (difference const-decl "set" sets nil) (set type-eq-decl nil sets nil) (measure_disjoint_union formula-decl nil generalized_measure_def nil) (subset_algebra_difference application-judgement "(S)" measure_def nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (= const-decl "[T, T -> boolean]" equalities nil) (union const-decl "set" sets nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset_algebra_union application-judgement "(S)" measure_def nil)) shostak)) (measure_union 0 (measure_union-1 nil 3453271429 ("" (skosimp) (("" (lemma "measure_disjoint_union" ("f" "f!1" "a" "a!1" "b" "difference(b!1,a!1)")) (("" (rewrite "union_difference" -1 :dir rl) (("" (replace -2) (("" (rewrite "difference_disjoint") (("" (name-replace "LHS" "f!1(union(a!1, b!1))") (("" (lemma "measure_monotone" ("f" "f!1" "a" "difference(b!1, a!1)" "b" "b!1")) (("" (replace -3) (("" (rewrite "difference_subset") (("" (name-replace "FMID" "f!1(difference(b!1, a!1))") (("" (expand "x_eq") (("" (expand "x_le") (("" (assert) (("" (flatten) (("" (assert) (("" (expand "x_add") (("" (split) (("1" (flatten) (("1" (assert) (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "subset_algebra" measure_def 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (difference const-decl "set" sets nil) (set type-eq-decl nil sets nil) (measure_disjoint_union formula-decl nil generalized_measure_def nil) (subset_algebra_difference application-judgement "(S)" measure_def nil) (union const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (difference_subset formula-decl nil sets_lemmas nil) (measure_monotone formula-decl nil measure_def nil) (difference_disjoint formula-decl nil sets_lemmas nil) (subset_algebra_union application-judgement "(S)" measure_def nil) (union_difference formula-decl nil sets_lemmas nil)) shostak)) (measure_def 0 (measure_def-1 nil 3453287567 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (split) (("1" (expand "measure?") (("1" (flatten) nil nil)) nil) ("2" (skosimp) (("2" (lemma "measure_disjoint_union" ("f" "f!1" "a" "a!1" "b" "b!1")) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (expand "measure?") (("3" (flatten) (("3" (expand "measure_countably_additive?") (("3" (inst - "X!1") (("3" (expand "x_le") (("3" (expand "x_eq") (("3" (assert) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "measure?") (("2" (assert) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (inst - "X!1") (("2" (assert) (("2" (case "x_le(x_sum(f!1 o X!1), f!1(IUnion(X!1)))") (("1" (name-replace "LHS" "x_sum(f!1 o X!1)") (("1" (name-replace "RHS" "f!1(IUnion(X!1))") (("1" (hide-all-but (-1 -4 1)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (case "forall (a,b:(S)): subset?(a,b) => x_le(f!1(a),f!1(b))") (("1" (expand "x_le" 1) (("1" (flatten) (("1" (assert) (("1" (expand "x_sum") (("1" (expand "o ") (("1" (case-replace "FORALL i: f!1(X!1(i))`1") (("1" (case "FORALL (n: nat): S(IUnion[T](n, X!1))") (("1" (case "forall (n:nat): x_eq(f!1(IUnion(n,X!1)),x_sigma(0,n,f!1 o X!1))") (("1" (case "forall (nna:sequence[nnreal],nnb:nnreal): (forall (n:nat): series(nna)(n) <= nnb)=>conv (("1" (inst - "LAMBDA i: f!1(X!1(i))`2" "f!1(IUnion(X!1))`2") (("1" (split -1) (("1" (flatten) (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "n!1") (("2" (expand "series") (("2" (expand "o ") (("2" (inst -2 "n!1") (("2" (inst -4 "IUnion(n!1, X!1)" "IUnion(X!1)") (("2" (split -4) (("1" (name-replace "MID1" "f!1(IUnion(n!1, X!1))") (("1" (expand "x_sigma") (("1" (name-replace "LHS" "sigma(0, n!1, LAMBDA i: f!1(X!1(i))`2)") (("1" (case-replace "FORALL i: i <= n!1 => f!1(X!1(i))`1") (("1" (hide-all-but (-2 -3 1 -6)) (("1" (name-replace "RHS" "f!1(IUnion(X!1))") (("1" (grind) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -5 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (inst + "x!2") (("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) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (case "nonempty?[real](image[nat, real](series(nna!1), fullset[nat])) AND above_bounded[real](image[nat, real](series(nna!1), fullset[nat]))") (("1" (typepred "sup(image(series(nna!1),fullset[nat]))") (("1" (name-replace "LIMIT" "sup(image(series(nna!1), fullset[nat]))") (("1" (expand "least_upper_bound") (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "upper_bound") (("1" (flatten) (("1" (case "LIMIT <= nnb!1") (("1" (case "convergence(series(nna!1),LIMIT)") (("1" (split 1) (("1" (expand "convergent?") (("1" (inst + "LIMIT") nil nil)) nil) ("2" (rewrite "limit_def" -1 :dir rl) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergence") (("2" (skosimp) (("2" (inst -3 "LIMIT-epsilon!1/2") (("2" (assert) (("2" (skosimp) (("2" (typepred "z!1") (("2" (skolem - "n!1") (("2" (replace -1) (("2" (hide -1) (("2" (inst + "n!1") (("2" (skosimp) (("2" (case "LIMIT-series(nna!1)(n!1)<epsilon!1/2") (("1" (hide 2) (("1" (case "series(nna!1)(i!1) <= LIMIT") (("1" (case "LIMIT-series(nna!1)(i!1)<epsilon!1") (("1" (expand "abs") (("1" (expand "<=" -2) (("1" (split -2) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "series(nna!1)(n!1)<=series(nna!1)(i!1)") (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "sigma_split" ("low" "0" "high" "i!1" "z" "n!1" "F" "nna!1")) (("2" (expand "series") (("2" (assert) (("2" (replace -1 1) (("2" (assert) (("2" (hide -1) (("2" (lemma "sigma_ge_0" ("low" "1+n!1" "high" "i!1" "F" "nna!1")) (("2" (split) (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -4 "series(nna!1)(i!1)") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -2 "nnb!1") (("2" (assert) (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (inst -5 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "series(nna!1)(0)") (("1" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (expand "above_bounded") (("2" (inst + "nnb!1") (("2" (expand "image") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (rewrite "IUnion_0_def") (("1" (expand "x_sigma") (("1" (expand "x_eq") (("1" (expand "o ") (("1" (case-replace "FORALL i: i <= 0 => f!1(X!1(i))`1") (("1" (expand "sigma") (("1" (assert) (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (expand "<=" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "IUnion_n_def") (("2" (typepred "X!1") (("2" (inst - "j!1") (("2" (inst -8 "IUnion(j!1, X!1)" "X!1(1 + j!1)") (("2" (split -8) (("1" (name-replace "LHS" "f!1(union(IUnion(j!1, X!1), X!1(1 + j!1)))") (("1" (hide-all-but (-1 -3 1)) (("1" (expand "x_eq") (("1" (expand "x_sigma") (("1" (expand "o ") (("1" (flatten) (("1" (expand "x_add") (("1" (case-replace "FORALL i: i <= 1 + j!1 => f!1(X!1(i))`1") (("1" (case-replace "FORALL i: i <= j!1 => f!1(X!1(i))`1") (("1" (assert) (("1" (expand "sigma" 1) (("1" (assert) (("1" (case-replace "f!1(X!1(1 + j!1))`1") (("1" (assert) nil nil) ("2" (inst -2 "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (skosimp) (("2" (expand "<=" -1) (("2" (split) (("1" (case-replace "FORALL i: i <= j!1 => f!1(X!1(i))`1") (("1" (assert) (("1" (assert) (("1" (inst - "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (hide-all-but (-1 1)) (("2" (expand "disjoint?") (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (skolem - "j!2") (("2" (inst - "1+j!1" "j!2") (("2" (assert) (("2" (inst - "x!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)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (induct "n") (("1" (rewrite "IUnion_0_def") (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (rewrite "IUnion_n_def") (("2" (lemma "subset_algebra_union" ("x" "IUnion[T](j!1, X!1)" "y" "X!1(1 + j!1)")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (skosimp) (("2" (inst - "X!1(i!1)" "IUnion(X!1)") (("2" (split) (("1" (expand "x_le") (("1" (flatten) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "IUnion") (("2" (expand "member") (("2" (skosimp) (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst -3 "a!1" "difference(b!1,a!1)") (("2" (lemma "union_diff_subset" ("a" "a!1" "b" "b!1")) (("2" (assert) (("2" (replace -1) (("2" (rewrite "difference_disjoint") (("2" (hide-all-but (-4 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measure? const-decl "bool" generalized_measure_def nil) (S formal-const-decl "subset_algebra" measure_def 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (measure_disjoint_union formula-decl nil generalized_measure_def nil) (subset_algebra_union application-judgement "(S)" measure_def nil) (measure_countably_additive? const-decl "bool" generalized_measure_def nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (IUnion const-decl "set[T]" indexed_sets nil) (set type-eq-decl nil sets nil) (O const-decl "T3" function_props nil) (x_sum const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (subset_algebra_union judgement-tcc nil subset_algebra nil) (x_sigma const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (nonempty? const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (above_bounded const-decl "bool" bounded_reals "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (TRUE const-decl "bool" booleans nil) (< const-decl "bool" reals nil) (sigma_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs 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) (minus_real_is_real application-judgement "real" reals nil) (i!1 skolem-const-decl "nat" measure_def nil) (nna!1 skolem-const-decl "sequence[nnreal]" measure_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (limit_def formula-decl nil convergence_sequences "analysis/") (convergence const-decl "bool" convergence_sequences "analysis/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (least_upper_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (Union const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (image const-decl "set[R]" function_image nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (AND const-decl "[bool, bool -> bool]" booleans nil) (series const-decl "sequence[real]" series "series/") (<= const-decl "bool" reals nil) (X!1 skolem-const-decl "disjoint_indexed_measurable[T, S]" measure_def nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/") (IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/") (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (union const-decl "set" sets nil) (subset_algebra_intersection application-judgement "(S)" measure_def nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/") (sequence type-eq-decl nil sequences nil) (union_diff_subset formula-decl nil sets_lemmas nil) (difference_disjoint formula-decl nil sets_lemmas nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (difference const-decl "set" sets nil) (subset_algebra_difference application-judgement "(S)" measure_def nil)) shostak)) (finite_measure_def 0 (finite_measure_def-1 nil 3454804407 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (lemma "measure_def" ("f" "to_measure(g!1)")) (("1" (assert) (("1" (flatten) (("1" (split) (("1" (expand "measure_empty?") (("1" (expand "to_measure") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "a!1" "b!1") (("2" (assert) (("2" (expand "to_measure") (("2" (expand "x_add") (("2" (expand "x_eq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -5 "X!1") (("3" (assert) (("3" (expand "to_measure") (("3" (expand "x_le") (("3" (assert) (("3" (expand "o ") (("3" (expand "x_sum") (("3" (replace -2) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (flatten) (("2" (lemma "measure_def" ("f" "lambda a: (TRUE,g!1(a))")) (("2" (flatten -1) (("2" (hide -1) (("2" (split -1) (("1" (hide-all-but (-1 1)) (("1" (expand "measure?") (("1" (expand "finite_measure?") (("1" (flatten) (("1" (expand "measure_empty?") (("1" (assert) (("1" (skosimp) (("1" (expand "measure_countably_additive?") (("1" (inst - "X!1") (("1" (assert) (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (expand "x_sum") (("1" (expand "o") (("1" (prop) (("1" (assert) (("1" (rewrite "limit_def" 1 :dir rl) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measure_empty?") (("2" (propax) nil nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (inst -3 "a!1" "b!1") (("3" (assert) (("3" (expand "x_add") (("3" (expand "x_eq") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (inst -4 "X!1") (("4" (assert) (("4" (hide 2 -3) (("4" (expand "x_sum") (("4" (expand "x_le") (("4" (expand "o ") (("4" (flatten) (("4" (prop) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((to_measure const-decl "measure_type" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (finite_measure nonempty-type-eq-decl nil generalized_measure_def nil) (finite_measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (S formal-const-decl "subset_algebra" measure_def 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_def nil) (measure_def formula-decl nil measure_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (O const-decl "T3" function_props nil) (x_sum const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (subset_algebra_union application-judgement "(S)" measure_def nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (measure_empty? const-decl "bool" generalized_measure_def nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (subset_algebra_emptyset name-judgement "(S)" measure_def nil) (TRUE const-decl "bool" booleans nil) (limit_def formula-decl nil convergence_sequences "analysis/") (set type-eq-decl nil sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (sequence type-eq-decl nil sequences nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (measure_countably_additive? const-decl "bool" generalized_measure_def nil)) shostak)) (A_of_TCC1 0 (A_of_TCC1-1 nil 3431320334 ("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (typepred "f!1") (("" (expand "sigma_finite_measure?") (("" (flatten) (("" (expand "measure_sigma_finite?") (("" (skosimp) (("" (inst -4 "X!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (measure_sigma_finite? const-decl "bool" measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (subset_algebra_fullset name-judgement "(S)" measure_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 measure_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) (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "subset_algebra" measure_def 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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (sigma_finite_measure? const-decl "bool" measure_def nil) (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil) (empty? const-decl "bool" sets nil)) nil)) (P_of_TCC1 0 (P_of_TCC1-1 nil 3453281846 ("" (case "forall (f: sigma_finite_measure, n: nat): S(IUnion(n,A_of(f)))") (("1" (case "forall (f: sigma_finite_measure, n: nat): IUnion[nat, T] (LAMBDA i: IF i <= n THEN A_of(f)(i) ELSE emptyset[T] ENDIF)= IUnion(n, A_of(f))") (("1" (skosimp) (("1" (inst - "f!1" "n!1") (("1" (inst - "f!1" "n!1") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "n") (("1" (skosimp) (("1" (rewrite "IUnion_0_def") (("1" (apply-extensionality :hide? t) (("1" (expand "IUnion") (("1" (case-replace "A_of(f!1)(0)(x!1)") (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "IUnion_n_def" 1) (("2" (apply-extensionality :hide? t) (("2" (expand "union") (("2" (expand "member") (("2" (case-replace "A_of(f!1)(1 + j!1)(x!1)") (("1" (hide -2) (("1" (expand "IUnion") (("1" (inst + "1+j!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "f!1") (("2" (case-replace "IUnion(j!1, A_of(f!1))(x!1)") (("1" (replace -2 -1 rl) (("1" (hide -2) (("1" (expand "IUnion") (("1" (skosimp) (("1" (expand "emptyset") (("1" (prop) (("1" (inst + "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -2 1 rl) (("2" (hide -2) (("2" (expand "IUnion") (("2" (skosimp) (("2" (expand "emptyset") (("2" (prop) (("2" (expand "<=" -1) (("2" (split) (("1" (inst + "i!1") (("1" (assert) nil 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) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (rewrite "IUnion_0_def") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (inst - "f!1") (("2" (rewrite "IUnion_n_def") (("2" (assert) (("2" (typepred "S") (("2" (expand "subset_algebra?") (("2" (flatten) (("2" (expand "subset_algebra_union?") (("2" (inst - "IUnion(j!1, A_of(f!1))" "A_of(f!1)(1 + j!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset_algebra_union? const-decl "bool" subset_algebra_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (emptyset const-decl "set" sets nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IUnion const-decl "set[T]" indexed_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/") (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (union const-decl "set" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T formal-type-decl nil measure_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) (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "subset_algebra" measure_def 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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (sigma_finite_measure? const-decl "bool" measure_def nil) (sigma_finite_measure nonempty-type-eq-decl nil measure_def 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (sequence type-eq-decl nil sequences nil) (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/") (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (A_of const-decl "disjoint_indexed_measurable" measure_def nil)) nil)) (A_of_def1 0 (A_of_def1-1 nil 3459221383 ("" (skosimp) (("" (name "AA" "A_of(mu!1)") (("" (replace -1) (("" (expand "A_of") (("" (case "nonempty?({X | IUnion(X) = fullset[T] AND (FORALL i: mu!1(X(i))`1)})") (("1" (lemma "choose_member" ("a" "{X | IUnion(X) = fullset[T] AND (FORALL i: mu!1(X(i))`1)}")) (("1" (replace -3) (("1" (expand "nonempty?") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "mu!1") (("2" (expand "sigma_finite_measure?") (("2" (flatten) (("2" (expand "measure_sigma_finite?") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst -4 "X!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((A_of const-decl "disjoint_indexed_measurable" measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil) (sigma_finite_measure? const-decl "bool" measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (S formal-const-decl "subset_algebra" measure_def 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 measure_def nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (measure_sigma_finite? const-decl "bool" measure_def nil) (choose_member formula-decl nil sets_lemmas nil) (subset_algebra_fullset name-judgement "(S)" measure_def nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IUnion const-decl "set[T]" indexed_sets nil) (fullset const-decl "set" sets nil)) shostak)) (A_of_def2 0 (A_of_def2-1 nil 3459221692 ("" (skosimp) (("" (name "AA" "A_of(mu!1)") (("" (replace -1) (("" (expand "A_of") (("" (case "nonempty?({X | IUnion(X) = fullset[T] AND (FORALL i: mu!1(X(i))`1)})") (("1" (lemma "choose_member" ("a" "{X | IUnion(X) = fullset[T] AND (FORALL i: mu!1(X(i))`1)}")) (("1" (replace -3) (("1" (expand "nonempty?") (("1" (assert) (("1" (inst - "n!1") nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "mu!1") (("2" (expand "sigma_finite_measure?") (("2" (flatten) (("2" (hide-all-but (-2 1)) (("2" (expand "measure_sigma_finite?") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst -3 "X!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((A_of const-decl "disjoint_indexed_measurable" measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil) (sigma_finite_measure? const-decl "bool" measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (S formal-const-decl "subset_algebra" measure_def 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 measure_def nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (measure_sigma_finite? const-decl "bool" measure_def nil) (empty? const-decl "bool" sets nil) (choose_member formula-decl nil sets_lemmas nil) (member const-decl "bool" sets nil) (subset_algebra_fullset name-judgement "(S)" measure_def nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IUnion const-decl "set[T]" indexed_sets nil) (fullset const-decl "set" sets nil)) shostak)) (P_of_def1 0 (P_of_def1-1 nil 3459221497 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (expand "fullset") (("" (expand "P_of") (("" (expand "IUnion") (("" (lemma "A_of_def1" ("mu" "mu!1")) (("" (lemma "extensionality_postulate" ("f" "IUnion(A_of(mu!1))" "g" "fullset[T]")) (("" (flatten) (("" (hide -1) (("" (split) (("1" (inst - "x!1") (("1" (hide -2) (("1" (expand "emptyset") (("1" (expand "fullset") (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst + "i!1") (("1" (inst + "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil measure_def nil) (boolean nonempty-type-decl nil booleans nil) (fullset const-decl "set" sets nil) (P_of const-decl "(S)" measure_def nil) (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil) (sigma_finite_measure? const-decl "bool" measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (S formal-const-decl "subset_algebra" measure_def 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) (IUnion const-decl "set[T]" indexed_sets nil) (set type-eq-decl nil sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (subset_algebra_fullset name-judgement "(S)" measure_def nil) (A_of_def1 formula-decl nil measure_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (emptyset const-decl "set" sets nil) (extensionality_postulate formula-decl nil functions nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (A_of const-decl "disjoint_indexed_measurable" measure_def nil)) shostak)) (P_of_def2 0 (P_of_def2-1 nil 3459221799 ("" (induct "n") (("1" (skosimp) (("1" (case-replace "P_of(mu!1)(0)=A_of(mu!1)(0)") (("1" (rewrite "A_of_def2") nil nil) ("2" (hide 2) (("2" (expand "P_of") (("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (case-replace "A_of(mu!1)(0)(x!1)") (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (inst - "mu!1") (("2" (case "P_of(mu!1)(j!1 + 1)=union(P_of(mu!1)(j!1),A_of(mu!1)(j!1+1))") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "measure_union" ("a" "P_of(mu!1)(j!1)" "b" "A_of(mu!1)(j!1 + 1)" "f" "mu!1")) (("1" (assert) (("1" (typepred "mu!1") (("1" (expand "sigma_finite_measure?") (("1" (flatten) (("1" (assert) (("1" (lemma "A_of_def2" ("mu" "mu!1" "n" "1+j!1")) (("1" (expand "x_le") (("1" (expand "x_add") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "P_of") (("2" (expand "union") (("2" (expand "member") (("2" (case-replace "IUnion(LAMBDA i: IF i <= 1+j!1 THEN A_of(mu!1)(i) ELSE emptyset[T] ENDIF) (x!1)") (("1" (flatten) (("1" (expand "IUnion") (("1" (skosimp) (("1" (expand "emptyset") (("1" (prop) (("1" (expand "<=" -1) (("1" (split) (("1" (inst + "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (split) (("1" (skosimp) (("1" (inst + "i!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (measure_union formula-decl nil measure_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (subset_algebra_union application-judgement "(S)" measure_def nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (union const-decl "set" sets nil) (emptyset const-decl "set" sets nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IUnion const-decl "set[T]" indexed_sets nil) (set type-eq-decl nil sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (A_of_def2 formula-decl nil measure_def nil) (A_of const-decl "disjoint_indexed_measurable" measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat_induction formula-decl nil naturalnumbers nil) (P_of const-decl "(S)" measure_def nil) (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil) (sigma_finite_measure? const-decl "bool" measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (S formal-const-decl "subset_algebra" measure_def 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 measure_def nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (P_of_def3 0 (P_of_def3-1 nil 3459222257 ("" (skosimp) (("" (expand "subset?") (("" (expand "member") (("" (skosimp) (("" (expand "P_of") (("" (expand "IUnion") (("" (expand "emptyset") (("" (skosimp) (("" (prop) (("" (inst + "i!2") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (emptyset const-decl "set" sets nil) (P_of const-decl "(S)" measure_def nil) (member const-decl "bool" sets nil)) shostak)) (sigma_finite_def1 0 (sigma_finite_def1-1 nil 3453268789 ("" (expand "sigma_finite_measure?") (("" (skosimp) (("" (case-replace "measure?(f!1)") (("1" (expand "measure_sigma_finite?") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((measure_sigma_finite? const-decl "bool" measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (S formal-const-decl "subset_algebra" measure_def 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_def nil) (sigma_finite_measure? const-decl "bool" measure_def nil)) shostak)) (sigma_finite_def2 0 (sigma_finite_def2-1 nil 3453268923 ("" (skosimp) (("" (rewrite "sigma_finite_def1") (("" (case-replace "measure?(f!1)") (("1" (split) (("1" (skosimp*) (("1" (lemma "increasing_IUnion" ("A" "X!1")) (("1" (skosimp) (("1" (case "forall n: S(B!1(n))") (("1" (inst + "B!1") (("1" (assert) (("1" (induct "i") (("1" (inst -7 "0") (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (inst -5 "j!1") (("2" (replace -5) (("2" (inst -8 "1+j!1") (("2" (lemma "measure_union" ("f" "f!1" "a" "B!1(j!1)" "b" "X!1(1 + j!1)")) (("2" (assert) (("2" (expand "x_add") (("2" (expand "x_le") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (expand "increasing_indexed_measurable?") (("2" (expand "increasing_indexed?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (assert) nil nil) ("2" (skosimp) (("2" (inst -4 "j!1") (("2" (replace -4) (("2" (lemma "subset_algebra_union" ("x" "B!1(j!1)" "y" "X!1(j!1+1)")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "disjoint_IUnion" ("A" "P!1")) (("2" (skosimp) (("2" (inst + "B!1") (("1" (assert) (("1" (typepred "P!1") (("1" (skosimp) (("1" (lemma "measure_monotone" ("f" "f!1" "a" "B!1(i!1)" "b" "P!1(i!1)")) (("1" (assert) (("1" (split) (("1" (expand "x_le") (("1" (inst -8 "i!1") nil nil)) nil) ("2" (hide 2) (("2" (expand "increasing_indexed_measurable?") (("2" (expand "increasing_indexed?") (("2" (case "forall n: IUnion(n, P!1)=P!1(n)") (("1" (inst - "i!1") (("1" (case "subset?(B!1(i!1), IUnion(i!1, B!1))") (("1" (inst - "i!1") (("1" (replace -5) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "IUnion") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (expand "image") (("2" (expand "Union") (("2" (inst + "B!1(i!1)") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (case-replace "P!1(n!1)(x!1)") (("1" (inst + "P!1(n!1)") (("1" (inst + "n!1") nil nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skolem - "n!2") (("2" (replace -1) (("2" (hide -1) (("2" (typepred "n!2") (("2" (expand "increasing?") (("2" (inst - "n!2" "n!1") (("2" (assert) (("2" (expand "subset?") (("2" (inst - "x!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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (case "B!1(0)=P!1(0)") (("1" (case "forall n: P!1(n) = IUnion(n, P!1)") (("1" (case "forall n: B!1(n+1)=difference(P!1(n+1),P!1(n))") (("1" (skosimp) (("1" (case-replace "x1!1=0") (("1" (assert) nil nil) ("2" (inst - "x1!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (apply-extensionality :hide? t) (("2" (expand "difference") (("2" (expand "member") (("2" (case-replace "B!1(1 + n!1)(x!1)") (("1" (case-replace "P!1(1 + n!1)(x!1)") (("1" (inst-cp -4 "1+n!1") (("1" (inst -4 "n!1") (("1" (replace -5 -1) (("1" (hide -5) (("1" (expand "IUnion" -1) (("1" (expand "image") (("1" (expand "Union") (("1" (skosimp) (("1" (replace -4 -3) (("1" (hide -4) (("1" (inst -6 "n!1") (("1" (replace -6 -3 :dir rl) (("1" (hide-all-but (-2 -3 -5)) (("1" (expand "IUnion") (("1" (expand "image") (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!2") (("1" (skolem - "n!2") (("1" (typepred "n!2") (("1" (replace -2) (("1" (hide -2) (("1" (expand "disjoint?") (("1" (inst - "n!2" "1+n!1") (("1" (grind) 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" (hide 2) (("2" (inst -2 "1+n!1") (("2" (replace -2) (("2" (hide -2) (("2" (inst -4 "1+n!1") (("2" (replace -4 1 rl) (("2" (hide-all-but (-1 1)) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (inst + "B!1(1+n!1)") (("2" (inst + "1+n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (inst-cp -2 "1+n!1") (("2" (replace -3) (("2" (inst-cp -6 "1+n!1") (("2" (replace -7 -1 rl) (("2" (expand "IUnion" -1) (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (skolem - "n!2") (("2" (replace -1) (("2" (hide -1) (("2" (typepred "n!2") (("2" (expand "<=" -1) (("2" (split) (("1" (inst -7 "n!1") (("1" (inst -3 "n!1") (("1" (replace -3) (("1" (replace -7 2 :dir rl) (("1" (expand "IUnion" 2) (("1" (expand "image") (("1" (expand "Union") (("1" (inst + "B!1(n!2)") (("1" (inst + "n!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (apply-extensionality :hide? t) (("2" (case-replace "P!1(n!1)(x!1)") (("1" (expand "IUnion") (("1" (expand "image") (("1" (expand "Union") (("1" (inst + "P!1(n!1)") (("1" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (skolem - "n!2") (("2" (typepred "n!2") (("2" (typepred "P!1") (("2" (expand "increasing_indexed_measurable?") (("2" (expand "increasing_indexed?") (("2" (flatten) (("2" (expand "increasing?") (("2" (inst - "n!2" "n!1") (("2" (expand "subset?") (("2" (assert) (("2" (inst - "x!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) ("2" (propax) nil nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((sigma_finite_def1 formula-decl nil measure_def nil) (T formal-type-decl nil measure_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) (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "subset_algebra" measure_def 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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (sequence type-eq-decl nil sequences nil) (set type-eq-decl nil sets nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (increasing_IUnion formula-decl nil nat_indexed_sets "sets_aux/") (increasing_indexed? const-decl "bool" nat_indexed_sets "sets_aux/") (subset_algebra_fullset name-judgement "(S)" measure_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (measure_union formula-decl nil measure_def nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (increasing_indexed_measurable nonempty-type-eq-decl nil measure_def nil) (increasing_indexed_measurable? const-decl "bool" measure_def nil) (B!1 skolem-const-decl "sequence[set[T]]" measure_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subset_algebra_union judgement-tcc nil subset_algebra nil) (disjoint_IUnion formula-decl nil nat_indexed_sets "sets_aux/") (B!1 skolem-const-decl "sequence[set[T]]" measure_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (measure_monotone formula-decl nil measure_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/") (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (image const-decl "set[R]" function_image nil) (<= const-decl "bool" reals nil) (i!1 skolem-const-decl "nat" measure_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Union const-decl "set" sets nil) (increasing? const-decl "bool" fun_preds_partial "structures/") (n!1 skolem-const-decl "nat" measure_def nil) (P!1 skolem-const-decl "increasing_indexed_measurable" measure_def nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (n!1 skolem-const-decl "nat" measure_def nil) (subset_algebra_difference application-judgement "(S)" measure_def nil) (difference const-decl "set" sets nil) (int_plus_int_is_int application-judgement "int" integers nil) (x1!1 skolem-const-decl "nat" measure_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (n!1 skolem-const-decl "nat" measure_def nil) (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/") (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (/= const-decl "boolean" notequal nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (n!2 skolem-const-decl "({i | i <= 1 + n!1})" measure_def nil) (measure? const-decl "bool" generalized_measure_def nil)) shostak)))
¤ 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.0.769Bemerkung: (vorverarbeitet am 2026-05-02) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26