| 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 901 kB |
|
Quelle ast_def.prfSprache: Lisp |
|||||||||||||||
|
(ast_def (A_empty 0 (A_empty-1 nil 3457694307 ("" (postpone) nil nil) nil shostak)) (IMP_generalized_measure_def_TCC1 0 (IMP_generalized_measure_def_TCC1-1 nil 3458454898 ("" (rewrite "A_empty") nil nil) ((A_empty formula-decl nil ast_def nil)) nil)) (A_difference_union 0 (A_difference_union-1 nil 3457883471 ("" (case "forall (a:(A),E:disjoint_indexed_measurable,n:nat): finite_disjoint_union?(A (("1" (skosimp) (("1" (expand "finite_disjoint_union?" -3) (("1" (skosimp) (("1" (case-replace "n!1=0") (("1" (assert) (("1" (case-replace "b!1=emptyset") (("1" (rewrite "difference_emptyset1") (("1" (expand "finite_disjoint_union?") (("1" (inst + "lambda (i:nat): if i=0 then a!1 else emptyset endif" "1") (("1" (hide -1 -2 -3 -5 -6 -7) (("1" (split) (("1" (expand "disjoint?") (("1" (skosimp) (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp) (("1" (expand "emptyset") (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (case-replace "a!1(x!1)") (("1" (inst + "0") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (case-replace "i!1=0") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "empty?") (("2" (expand "member") (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -5) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst -7 "i!1") (("2" (expand "empty?") (("2" (inst -7 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!1>0") (("1" (hide 1) (("1" (case "b!1=IUnion(n!1-1,E!1)") (("1" (case "FORALL (i:nat): A(E!1(i))") (("1" (hide -7 -8) (("1" (inst -4 "a!1" "E!1" "n!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (expand "disjoint_indexed_measurable?") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -7 "i!1") (("2" (flatten) (("2" (case "i!1<n!1") (("1" (assert) nil nil) ("2" (assert) (("2" (rewrite "emptyset_is_empty?") (("2" (replace -7) (("2" (rewrite "A_empty") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (apply-extensionality :hide? t) (("2" (case-replace "b!1(x!1)") (("1" (replace -5 -1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst -6 "i!1") (("1" (expand "image") (("1" (expand "Union") (("1" (inst + "E!1(i!1)") (("1" (flatten) (("1" (case-replace "i!1 < n!1") (("1" (inst + "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (rewrite "emptyset_is_empty?") (("2" (replace -6) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -5) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!2") (("2" (skosimp) (("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (rewrite "IUnion_0_def") (("1" (lemma "A_difference" ("a" "a!1" "b" "E!1(0)")) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (rewrite "IUnion_n_def") (("2" (rewrite "union_commutative" 1) (("2" (rewrite "difference_difference1" 1 :dir rl) (("2" (lemma "A_difference" ("a" "a!1" "b" "E!1(1+j!1)")) (("2" (expand "finite_disjoint_union?" -1) (("2" (skosimp) (("2" (case "forall (a,b,c:set[T]): difference(union(a,b),c)=union(difference(a,c),differ (("1" (case-replace "n!1=0") (("1" (assert) (("1" (case-replace "IUnion(E!2)=emptyset") (("1" (replace -5) (("1" (rewrite "difference_emptyset2") (("1" (hide-all-but 1) (("1" (expand "finite_disjoint_union?") (("1" (inst + "lambda (i:nat): emptyset" "0") (("1" (split) (("1" (grind) nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (expand "member") (("3" (expand "empty?") (("3" (expand "member") (("3" (expand "emptyset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -5)) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst - "i!1") (("2" (expand "empty?") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!1>0") (("1" (hide 1) (("1" (case-replace "IUnion(E!2)=IUnion(n!1-1,E!2)") (("1" (replace -5) (("1" (hide -1 -5) (("1" (case "forall (n:nat): finite_disjoint_union?(A) (difference(IUnion(n, E!2), IUnion(j!1, E!1)))") (("1" (inst - "n!1-1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (rewrite "IUnion_0_def") (("1" (inst -5 "E!2(0)" "E!1") (("1" (assert) (("1" (inst -4 "0") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "IUnion_n_def") (("2" (inst - "IUnion(j!2, E!2)" "E!2(1 + j!2)" "IUnion(j!1, E!1)") (("2" (replace -3) (("2" (inst -6 "E!2(1 + j!2)" "E!1") (("1" (hide -3 -5 -2) (("1" (name-replace "AA" "difference(IUnion(j!2, E!2), IUnion(j!1, E!1))") (("1" (name-replace "BB" "difference(E!2(1 + j!2), IUnion(j!1, E!1))") (("1" (case "disjoint?(AA,BB)") (("1" (expand "finite_disjoint_union?") (("1" (skosimp*) (("1" (inst + "lambda (i:nat): if i<n!2 then E!3(i) else E!4(i-n!2) endif" "n!2+n!3") (("1" (split) (("1" (expand "disjoint?" 1) (("1" (skosimp) (("1" (case-replace "i!1 < n!2") (("1" (case-replace "j!3 < n!2") (("1" (expand "disjoint?" -4) (("1" (inst - "i!1" "j!3") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "disjoint?" (-2 3)) (("2" (expand "intersection") (("2" (expand "empty?" (-2 3)) (("2" (skosimp) (("2" (expand "member") (("2" (flatten) (("2" (inst - "x!1") (("2" (replace -5) (("2" (split) (("1" (expand "IUnion" 1) (("1" (inst + "i!1") nil nil)) nil) ("2" (replace -9) (("2" (expand "IUnion") (("2" (inst + "j!3-n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "j!3 < n!2") (("1" (expand "disjoint?" (3 -2)) (("1" (expand "intersection") (("1" (expand "empty?" (3 -2)) (("1" (expand "member") (("1" (skosimp) (("1" (inst -4 "x!1") (("1" (split 3) (("1" (replace -5) (("1" (expand "IUnion") (("1" (inst + "j!3") nil nil)) nil)) nil) ("2" (replace -9) (("2" (expand "IUnion") (("2" (inst + "i!1-n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "disjoint?" -6) (("2" (inst -6 "i!1 - n!2" "j!3 - n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (expand "union") (("1" (expand "disjoint?" -1) (("1" (expand "intersection") (("1" (expand "empty?" -1) (("1" (expand "member") (("1" (inst - "x!1") (("1" (case-replace "AA(x!1)") (("1" (replace -3 -1) (("1" (expand "IUnion" (-1 1)) (("1" (skosimp) (("1" (inst -4 "i!1") (("1" (inst + "i!1") (("1" (case-replace "i!1 < n!2") (("1" (assert) (("1" (expand "empty?") (("1" (inst -4 "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "BB(x!1)") (("1" (replace -7) (("1" (expand "IUnion" (-1 2)) (("1" (skosimp) (("1" (inst + "n!2+i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 3) (("2" (replace -3) (("2" (replace -7) (("2" (expand "IUnion" (1 2 -1)) (("2" (skosimp) (("2" (case-replace "i!1 < n!2") (("1" (inst 2 "i!1") nil nil) ("2" (assert) (("2" (inst 2 "i!1-n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (expand "member") (("3" (assert) (("3" (case-replace "i!1 < n!2") (("1" (assert) (("1" (inst -5 "i!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -8 "i!1-n!2") (("2" (flatten) (("2" (assert) (("2" (case "i!1 - n!2 < n!3") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "disjoint?" 1) (("2" (expand "intersection") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (flatten) (("2" (expand "AA") (("2" (expand "BB") (("2" (expand "difference") (("2" (expand "member") (("2" (flatten) (("2" (hide 1 2) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!2") (("2" (skolem - "i!1") (("2" (replace -1) (("2" (hide -1) (("2" (expand "disjoint?") (("2" (inst - "i!1" "1+j!2") (("2" (assert) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("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)) nil)) nil)) nil)) nil) ("2" (inst -5 "1+j!2") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (rewrite "emptyset_is_empty?") (("2" (replace -5) (("2" (rewrite "A_empty") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1 -5)) (("2" (apply-extensionality :hide? t) (("2" (case-replace "IUnion(E!2)(x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst - "i!1") (("1" (flatten) (("1" (expand "image") (("1" (expand "Union") (("1" (inst + "E!2(i!1)") (("1" (inst + "i!1") (("1" (assert) (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!2") (("2" (skosimp) (("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (apply-extensionality :hide? t) (("2" (expand "difference") (("2" (expand "union") (("2" (expand "member") (("2" (case-replace "a!2(x!1)") (("1" (assert) (("1" (case-replace "c!1(x!1)") (("1" (assert) 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) ((IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (difference_difference1 formula-decl nil sets_lemmas nil) (union const-decl "set" sets nil) (j!2 skolem-const-decl "nat" ast_def nil) (n!2 skolem-const-decl "nat" ast_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (AA skolem-const-decl "set[T]" ast_def nil) (BB skolem-const-decl "set[T]" ast_def nil) (E!2 skolem-const-decl "sequence[set[T]]" ast_def nil) (n!1 skolem-const-decl "nat" ast_def nil) (i!1 skolem-const-decl "nat" ast_def nil) (/= const-decl "boolean" notequal nil) (finite_intersection2 application-judgement "finite_set[T]" countable_setofsets "sets_aux/") (difference_emptyset2 formula-decl nil sets_lemmas nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (union_commutative formula-decl nil sets_lemmas nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (A_difference formula-decl nil ast_def nil) (IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/") (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (> const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (A_empty formula-decl nil ast_def nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (< const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (n!1 skolem-const-decl "nat" ast_def nil) (E!1 skolem-const-decl "sequence[set[T]]" ast_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (a!1 skolem-const-decl "set[T]" ast_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (image const-decl "set[R]" function_image nil) (<= const-decl "bool" reals nil) (i!1 skolem-const-decl "nat" ast_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Union const-decl "set" sets nil) (member const-decl "bool" sets nil) (difference_emptyset1 formula-decl nil sets_lemmas nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (intersection const-decl "set" 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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/") (emptyset const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (T formal-type-decl nil ast_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (A formal-const-decl "(nonempty?[set[T]])" ast_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) (setof type-eq-decl nil defined_types nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (setofsets type-eq-decl nil sets nil) (finite_disjoint_union? const-decl "bool" subset_algebra_def nil) (difference const-decl "set" sets nil) (sequence type-eq-decl nil sequences nil) (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/")) shostak)) (measure_subadditive 0 (measure_subadditive-1 nil 3457882653 ("" (skosimp) (("" (typepred "mu!1") (("" (expand "measure?") (("" (flatten) (("" (lemma "disjoint_IUnion" ("A" "I!1")) (("" (skosimp) (("" (case "forall (n:nat): finite_disjoint_union?(A)(B!1(n))") (("1" (case "forall (n:nat): nonempty?({E: disjoint_indexed_measurable | B!1(n) = IUnion(E)})" (("1" (name "FDU" "lambda (n:nat): choose({E:disjoint_indexed_measurable | B!1(n) = IUnion(E)})") (("1" (case "forall (n:nat): IUnion(FDU(n)) = B!1(n)") (("1" (case "forall (j:nat): x_le(x_sum(mu!1 o FDU(j)),mu!1(I!1(j)))") (("1" (lemma "x_sum_le" ("S" "lambda (j:nat): x_sum(mu!1 o FDU(j))" "T" "mu!1 o I!1")) (("1" (split -1) (("1" (name "UU" "lambda (i,j:nat): FDU(i)(j)") (("1" (lemma "double_x_sum" ("U" "mu!1 o UU")) (("1" (expand "UU" -1 2) (("1" (expand "o" -1 2) (("1" (expand "o" -3 1) (("1" (name-replace "DRL1" "x_sum(LAMBDA (j: nat): x_sum(LAMBDA (x: nat): mu!1(FDU(j)(x))))") (("1" (case-replace "single_index(mu!1 o UU) = mu!1 o single_index(UU)") (("1" (hide -1) (("1" (expand "measure_countably_additive?") (("1" (inst -15 "single_index(UU)") (("1" (name-replace "DRL2" "x_sum(mu!1 o single_index(UU))") (("1" (name-replace "RHS" "x_sum(mu!1 o I!1)") (("1" (case-replace "IUnion(single_index(UU))=IUnion(I!1)") (("1" (assert) (("1" (name-replace "LHS" "mu!1(IUnion(I!1))") (("1" (hide-all-but (-2 -4 -16 1)) (("1" (expand "x_le") (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -13) (("2" (expand "UU") (("2" (hide-all-but (-5 -7 -8 -9 -10 -11 -12 1)) (("2" (apply-extensionality :hide? t) (("2" (case-replace "IUnion(B!1)(x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst -2 "i!1") (("1" (replace -2 -1 rl) (("1" (assert) (("1" (skosimp) (("1" (expand "single_index") (("1" (inst + "double_index_n(i!1,i!2)") (("1" (lemma "double_index_ij_n" ("i" "i!1" "j" "i!2")) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IUnion") (("2" (skolem - "n!1") (("2" (expand "single_index") (("2" (lemma "double_index_n_ij" ("n" "n!1")) (("2" (inst - "double_index_i(n!1)") (("2" (inst + "double_index_i(n!1)") (("2" (replace -3 1 rl) (("2" (assert) (("2" (inst + "double_index_j(n!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "disjoint_indexed_measurable?") (("2" (expand "disjoint?" 1) (("2" (skosimp) (("2" (expand "UU") (("2" (assert) (("2" (expand "single_index") (("2" (hide-all-but (-9 -5 1 2)) (("2" (case-replace "double_index_i(j!1)=double_index_i(i!1)") (("1" (inst - "double_index_i(i!1)") (("1" (typepred "FDU(double_index_i(i!1))") (("1" (expand "disjoint_indexed_measurable?") (("1" (expand "disjoint?" -1) (("1" (inst - "double_index_j(i!1)" "double_index_j(j!1)") (("1" (assert) (("1" (expand "/=" 1) (("1" (lemma "double_index_n_ij" ("n" "i!1")) (("1" (lemma "double_index_n_ij" ("n" "j!1")) (("1" (expand "double_index_n") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst-cp - "double_index_i(i!1)") (("2" (inst - "double_index_i(j!1)") (("2" (expand "disjoint?" -3) (("2" (inst - "double_index_i(i!1)" "double_index_i(j!1)") (("2" (assert) (("2" (replace -1 * rl) (("2" (replace -2 * rl) (("2" (hide -1 -2) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "x!1") (("2" (split) (("1" (expand "IUnion") (("1" (inst + "double_index_j(i!1)") nil nil)) nil) ("2" (expand "IUnion") (("2" (inst + "double_index_j(j!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (expand "o ") (("2" (expand "single_index") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (skolem + "n!1") (("3" (expand "single_index") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (expand "o" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "j!1") (("2" (inst -4 "j!1") (("2" (typepred "FDU(j!1)") (("2" (hide -2 -4 -5) (("2" (case "subset?(B!1(j!1),I!1(j!1))") (("1" (lemma "A_difference_union" ("a" "I!1(j!1)" "b" "B!1(j!1)")) (("1" (assert) (("1" (lemma "union_diff_subset" ("b" "I!1(j!1)" "a" "B!1(j!1)")) (("1" (assert) (("1" (lemma "difference_disjoint" ("a" "B!1(j!1)" "b" "I!1(j!1)")) (("1" (name-replace "DIFF" "difference(I!1(j!1), B!1(j!1))") (("1" (name-replace "BB" "B!1(j!1)") (("1" (name-replace "AA" "FDU(j!1)") (("1" (name-replace "II" "I!1(j!1)") (("1" (expand "finite_disjoint_union?") (("1" (skosimp) (("1" (expand "member") (("1" (name "XX" "lambda (i:nat): if i<n!1 then E!1(i) else AA(i-n!1) endif") (("1" (case "disjoint_indexed_measurable?(XX)") (("1" (expand "measure_countably_additive?") (("1" (inst -18 "XX") (("1" (case-replace "IUnion(XX)=II") (("1" (assert) (("1" (lemma "x_add_sum" ("S" "lambda (i:nat): if i<n!1 then mu!1(E!1(i)) else (TRUE,0) endif" "T" "lambda (i:nat): if i<n!1 then (TRUE,0) else mu!1(AA(i-n!1)) endif")) (("1" (lemma "x_sum_eq" ("S" "LAMBDA (i_1: nat): x_add((LAMBDA (i: nat): IF i < n!1 THEN mu!1(E!1(i)) ELSE (TRUE, 0) ENDIF) (i_1), (LAMBDA (i: nat): IF i < n!1 THEN (TRUE, 0) ELSE mu!1(AA(i - n!1)) ENDIF) (i_1))" "T" "mu!1 o XX")) (("1" (split -1) (("1" (name-replace "DRL1" "x_sum(LAMBDA (i_1: nat): x_add((LAMBDA (i: nat): IF i < n!1 THEN mu!1(E!1(i)) ELSE (TRUE, 0) ENDIF) (i_1), (LAMBDA (i: nat): IF i < n!1 THEN (TRUE, 0) ELSE mu!1(AA(i - n!1)) ENDIF) (i_1)))") (("1" (case "x_eq(x_sum(mu!1 o AA),x_sum(LAMBDA (i: nat): IF i < n!1 THEN (TRUE, 0) ELSE mu!1(AA(i - n!1)) ENDIF))") (("1" (name-replace "LHS" "x_sum(mu!1 o AA)") (("1" (name-replace "RHS" "mu!1(II)") (("1" (name-replace "DRL2" "x_sum(mu!1 o XX)") (("1" (name-replace "DRL3" "x_sum(LAMBDA (i: nat): IF i < n!1 THEN (TRUE, 0) ELSE mu!1(AA(i - n!1)) ENDIF)") (("1" (hide-all-but (-1 -2 -3 -22 1)) (("1" (expand "x_le") (("1" (flatten) (("1" (expand "x_eq") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "x_add") (("1" (assert) (("1" (lift-if) (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "x_sum") (("2" (expand "x_eq") (("2" (case-replace "FORALL (i:nat): (mu!1 o AA)(i)`1") (("1" (case-replace "FORALL (i_1: nat): IF i_1 < n!1 THEN TRUE ELSE mu!1(AA(i_1 - n!1))`1 ENDIF") (("1" (case-replace "convergence_sequences.convergent?(series(LAMBDA (i:nat): (mu!1 o AA)(i)`2))") (("1" (case-replace "convergence_sequences.convergent?(series(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0 ELSE mu!1(AA(i_1 - n!1))`2 ENDIF))") (("1" (case-replace "n!1=0") (("1" (case-replace "(LAMBDA (i_1: nat): IF i_1 < 0 THEN 0 ELSE mu!1(AA(i_1 - 0))`2 ENDIF)=(LAMBDA (i:nat): (mu!1 o AA)(i)`2)") (("1" (apply-extensionality :hide? t) (("1" (expand "o ") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "limit_series_shift" ("a" "(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0 ELSE mu!1(AA(i_1 - n!1))`2 ENDIF)" "pn" "n!1")) (("1" (replace -2) (("1" (replace -1) (("1" (expand "o ") (("1" (lemma "sigma_eq" ("F" "(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0 ELSE mu!1(AA(i_1 - n!1))`2 ENDIF)" "G" "lambda (i:nat): 0" "low" "0" "high" "n!1-1")) (("1" (split -1) (("1" (rewrite "sigma_zero") (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "conv_series_shift" ("a" "(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0 ELSE mu!1(AA(i_1 - n!1))`2 ENDIF)" "N" "n!1")) (("2" (expand "o ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) (("2" (prop) (("2" (expand "o ") (("2" (lemma "conv_series_shift" ("a" "(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0 ELSE mu!1(AA(i_1 - n!1))`2 ENDIF)" "N" "n!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (prop) (("2" (inst - "i!1-n!1") (("1" (expand "o ") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (case-replace "FORALL (i_1: nat): IF i_1 < n!1 THEN TRUE ELSE mu!1(AA(i_1 - n!1))`1 ENDIF") (("1" (hide 2) (("1" (skosimp) (("1" (expand "o ") (("1" (inst - "i!1+n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (lift-if 1) (("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (lift-if 1) (("3" (assert) (("3" (prop) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (expand "XX") (("2" (expand "o") (("2" (case-replace "i!1 < n!1") (("1" (expand "x_add") (("1" (expand "x_eq") (("1" (hide-all-but 1) (("1" (prop) (("1" (lift-if) (("1" (propax) nil nil)) nil) ("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but (1 2)) (("2" (expand "x_add") (("2" (expand "x_eq") (("2" (lift-if 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (lift-if 1) (("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (lift-if 1) (("4" (assert) (("4" (prop) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (inst -11 "i!2") (("5" (flatten) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -9 "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -4 1 rl) (("2" (replace -6) (("2" (replace -10 * rl) (("2" (hide-all-but (-7 1)) (("2" (apply-extensionality :hide? t) (("2" (expand "union") (("2" (expand "member") (("2" (case-replace "IUnion(E!1)(x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst + "i!1") (("1" (expand "XX") (("1" (inst - "i!1") (("1" (flatten) (("1" (assert) (("1" (case-replace "i!1 < n!1") (("1" (assert) (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "IUnion(AA)(x!1)") (("1" (hide 1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (expand "XX") (("1" (inst + "n!1+i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IUnion") (("2" (skosimp) (("2" (expand "XX") (("2" (case-replace "i!1<n!1") (("1" (inst 2 "i!1") nil nil) ("2" (assert) (("2" (inst 2 "i!1-n!1") 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 "disjoint_indexed_measurable?") (("2" (expand "disjoint?" 1) (("2" (skosimp) (("2" (expand "XX") (("2" (hide -1) (("2" (case-replace "i!1 < n!1") (("1" (case-replace "j!2 < n!1") (("1" (expand "disjoint?" -5) (("1" (inst -5 "i!1" "j!2") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (replace -5) (("2" (replace -9 -2 rl) (("2" (expand "disjoint?" (3 -2)) (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (inst -4 "x!1") (("2" (split 3) (("1" (expand "IUnion") (("1" (inst + "j!2-n!1") nil nil)) nil) ("2" (expand "IUnion") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "j!2 < n!1") (("1" (assert) (("1" (replace -5) (("1" (replace -9 -2 rl) (("1" (expand "disjoint?" (-2 3)) (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp) (("1" (inst - "x!1") (("1" (split 3) (("1" (expand "IUnion") (("1" (inst + "i!1-n!1") nil nil)) nil) ("2" (expand "IUnion") (("2" (inst + "j!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "disjoint?" -7) (("2" (inst -7 "i!1 - n!1" "j!2 - n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "XX") (("3" (case-replace "x1!1 < n!1") (("1" (inst -6 "x1!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (case-replace "j!1=0") (("1" (assert) nil nil) ("2" (inst -8 "j!1-1") (("1" (assert) (("1" (replace -8 -1) (("1" (expand "difference") (("1" (expand "member") (("1" (propax) 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" (skosimp) (("2" (inst - "n!1") (("2" (lemma "choose_member" ("a" "{E: disjoint_indexed_measurable | B!1(n!1) = IUnion(E)}")) (("2" (expand "nonempty?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (inst - "n!1") (("2" (expand "finite_disjoint_union?") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "E!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (assert) (("2" (skosimp) (("2" (inst - "x1!1") (("2" (flatten) (("2" (assert) (("2" (case-replace "E!1(x1!1)=emptyset") (("1" (rewrite "A_empty") nil nil) ("2" (apply-extensionality :hide? t) (("2" (inst - "x!1") (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -6 -7 -8 2) (("2" (lemma "NAT_induction" ("p" "lambda (n: nat): finite_disjoint_union?(A)(B!1(n))")) (("2" (split) (("1" (skosimp) (("1" (inst - "n!1") nil nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (case-replace "j!1=0") (("1" (replace -5) (("1" (hide-all-but 1) (("1" (expand "finite_disjoint_union?") (("1" (inst + "lambda (i:nat): if i=0 then I!1(0) else emptyset endif" "1") (("1" (split) (("1" (grind) nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (case-replace "I!1(0)(x!1)") (("1" (inst + "0") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "member") (("3" (rewrite "A_empty") (("3" (assert) (("3" (flatten) (("3" (assert) (("3" (expand "empty?") (("3" (skosimp) (("3" (expand "emptyset") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (hide 1) (("1" (inst -6 "j!1-1") (("1" (assert) (("1" (replace -6) (("1" (inst -4 "j!1-1") (("1" (case "forall (n:nat): n < j!1 => finite_disjoint_union?(A)(IUnion(n,B!1))") (("1" (inst - "j!1-1") (("1" (assert) (("1" (lemma "A_difference_union" ("a" "I!1(j!1)" "b" "IUnion(j!1 - 1, B!1)")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (flatten) (("1" (rewrite "IUnion_0_def") (("1" (replace -6) (("1" (hide-all-but 1) (("1" (expand "finite_disjoint_union?") (("1" (inst + "lambda (i:nat): if i=0 then I!1(0) else emptyset endif" "1") (("1" (expand "member") (("1" (rewrite "A_empty") (("1" (split) (("1" (grind) nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (case-replace "I!1(0)(x!1)") (("1" (inst + "0") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (split) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "empty?") (("2" (expand "emptyset") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (rewrite "IUnion_n_def" 1) (("2" (inst - "1+j!2") (("2" (assert) (("2" (name-replace "AA" "IUnion(j!2, B!1)") (("2" (name-replace "BB" "B!1(1 + j!2)") (("2" (hide-all-but (-1 -4 -5 1)) (("2" (expand "finite_disjoint_union?") (("2" (skosimp*) (("2" (inst + "lambda (i:nat): if i < n!1 then E!1(i) else E!2(i-n!1) endif" "n!1+n!2") (("1" (case "disjoint?(AA,BB)") (("1" (split) (("1" (expand "disjoint?" (1 -2 -5)) (("1" (skosimp) (("1" (case-replace "i!1 < n!1") (("1" (case-replace "j!3 < n!1") (("1" (inst - "i!1" "j!3") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (flatten) (("2" (inst - "x!1") (("2" (split) (("1" (replace -5) (("1" (expand "IUnion") (("1" (inst + "i!1") nil nil)) nil)) nil) ("2" (replace -8) (("2" (expand "IUnion") (("2" (inst + "j!3-n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "j!3 < n!1") (("1" (assert) (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp) (("1" (inst - "x!1") (("1" (split) (("1" (replace -5) (("1" (expand "IUnion") (("1" (inst + "j!3") nil nil)) nil)) nil) ("2" (replace -8) (("2" (expand "IUnion") (("2" (inst + "i!1-n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -5 "i!1-n!1" "j!3-n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (expand "union") (("1" (expand "member") (("1" (replace -3) (("1" (replace -6) (("1" (case-replace "IUnion(E!1)(x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst + "i!1") (("1" (inst -5 "i!1") (("1" (case-replace "i!1<n!1") (("1" (assert) (("1" (expand "empty?") (("1" (inst -5 "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (case-replace "IUnion(E!2)(x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (hide 1) (("1" (inst + "n!1+i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IUnion") (("2" (skosimp) (("2" (case-replace "i!1<n!1") (("1" (inst 2 "i!1") nil nil) ("2" (assert) (("2" (inst 2 "i!1-n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (case-replace "i!1 < n!1") (("1" (inst - "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst -7 "i!1-n!1") (("2" (flatten) (("2" (case-replace "i!1 < n!1 + n!2") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "BB") (("2" (expand "AA") (("2" (hide-all-but (-7 1)) (("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 - "i!2") (("2" (inst - "i!2" "1+j!2") (("2" (assert) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("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) ("2" (skosimp) (("2" (assert) 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) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measure_type nonempty-type-eq-decl nil generalized_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) (A formal-const-decl "(nonempty?[set[T]])" ast_def nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil ast_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (j!1 skolem-const-decl "nat" ast_def nil) (nat_induction formula-decl nil naturalnumbers nil) (IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (BB skolem-const-decl "set[T]" ast_def nil) (Union const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (AA skolem-const-decl "set[T]" ast_def nil) (n!1 skolem-const-decl "nat" ast_def nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/") (pred type-eq-decl nil defined_types nil) (NAT_induction formula-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) (= const-decl "[T, T -> boolean]" equalities nil) (IUnion const-decl "set[T]" indexed_sets nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (difference const-decl "set" sets nil) (XX skolem-const-decl "[nat -> set[T]]" ast_def nil) (union const-decl "set" sets nil) (x_sum_eq formula-decl nil extended_nnreal "extended_nnreal/") (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (limit_series_shift formula-decl nil series "series/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_eq formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (sigma_zero formula-decl nil sigma "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (conv_series_shift formula-decl nil series "series/") (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (i!1 skolem-const-decl "nat" ast_def nil) (n!1 skolem-const-decl "nat" ast_def nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (TRUE const-decl "bool" booleans nil) (x_add_sum formula-decl nil extended_nnreal "extended_nnreal/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (difference_disjoint formula-decl nil sets_lemmas nil) (union_diff_subset formula-decl nil sets_lemmas nil) (A_difference_union formula-decl nil ast_def nil) (j!1 skolem-const-decl "nat" ast_def nil) (int_plus_int_is_int application-judgement "int" integers nil) (x_sum_le formula-decl nil extended_nnreal "extended_nnreal/") (UU skolem-const-decl "[[nat, nat] -> (A)]" ast_def nil) (single_index const-decl "[nat -> T]" double_index "extended_nnreal/") (measure_countably_additive? const-decl "bool" generalized_measure_def nil) (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/") (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnrat_plus_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (/= const-decl "boolean" notequal 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (double_index_n_ij formula-decl nil code_product "extended_nnreal/") (double_index_j const-decl "nat" code_product "extended_nnreal/") (double_index_i const-decl "nat" code_product "extended_nnreal/") (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/") (double_index_ij_n formula-decl nil code_product "extended_nnreal/") (double_index_n const-decl "nat" code_product "extended_nnreal/") (double_x_sum formula-decl nil extended_nnreal "extended_nnreal/") (O const-decl "T3" function_props nil) (x_sum const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (choose_member formula-decl nil sets_lemmas nil) (choose const-decl "(p)" sets nil) (emptyset const-decl "set" sets 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) (A_empty formula-decl nil ast_def nil) (E!1 skolem-const-decl "sequence[set[T]]" ast_def nil) (finite_disjoint_union? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (disjoint_IUnion formula-decl nil nat_indexed_sets "sets_aux/") (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) (sequence type-eq-decl nil sequences nil)) shostak)) (generalized_monotonicity 0 (generalized_monotonicity-1 nil 3458063268 ("" (skosimp) (("" (lemma "A_difference_union" ("a" "Y!1" "b" "IUnion(n!1, I!1)")) (("" (assert) (("" (split) (("1" (expand "finite_disjoint_union?") (("1" (skosimp) (("1" (lemma "union_diff_subset" ("a" "IUnion(n!1, I!1)" "b" "Y!1")) (("1" (assert) (("1" (replace -3) (("1" (name "XX" "lambda (i:nat): if i<n!1 then I!1(i) else E!1(i-n!1) endif") (("1" (case "disjoint_indexed_measurable?(XX)") (("1" (typepred "mu!1") (("1" (expand "measure?") (("1" (expand "measure_countably_additive?") (("1" (flatten) (("1" (inst - "XX") (("1" (case-replace "IUnion(XX)=Y!1") (("1" (assert) (("1" (lemma "x_add_sum" ("S" "lambda (i:nat): if i<n!1 then mu!1(I!1(i)) else (TRUE,0) endif" "T" "lambda (i:nat): if i<n!1 then (TRUE,0) else mu!1(E!1(i-n!1)) endif")) (("1" (lemma "x_sum_eq" ("S" "LAMBDA (i_1: nat): x_add((LAMBDA (i: nat): IF i < n!1 THEN mu!1(I!1(i)) ELSE (TRUE, 0) ENDIF) (i_1), (LAMBDA (i: nat): IF i < n!1 THEN (TRUE, 0) ELSE mu!1(E!1(i - n!1)) ENDIF) (i_1))" "T" "mu!1 o XX")) (("1" (split -1) (("1" (name-replace "DRL1" "x_sum(LAMBDA (i_1: nat): x_add((LAMBDA (i: nat): IF i < n!1 THEN mu!1(I!1(i)) ELSE (TRUE, 0) ENDIF) (i_1), (LAMBDA (i: nat): IF i < n!1 THEN (TRUE, 0) ELSE mu!1(E!1(i - n!1)) ENDIF) (i_1)))") (("1" (case "x_eq(x_sum(mu!1 o I!1),x_sum(LAMBDA (i: nat): IF i < n!1 THEN mu!1(I!1(i)) ELSE (TRUE, 0) ENDIF))") (("1" (name-replace "LHS" "x_sum(mu!1 o I!1)") (("1" (name-replace "DRL2" "x_sum(LAMBDA (i: nat): IF i < n!1 THEN mu!1(I!1(i)) ELSE (TRUE, 0) ENDIF)") (("1" (hide-all-but (1 -1 -2 -3 -6)) (("1" (expand "x_eq") (("1" (expand "x_le") (("1" (expand "x_add") (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -2) (("2" (lemma "x_sum_eq" ("S" "mu!1 o I!1" "T" "LAMBDA (i: nat): IF i < n!1 THEN mu!1(I!1(i)) ELSE (TRUE, 0) ENDIF")) (("2" (assert) (("2" (hide 2) (("2" (skosimp) (("2" (expand "o ") (("2" (case-replace "i!1 < n!1") (("1" (expand "x_eq") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (inst -13 "i!1") (("2" (assert) (("2" (expand "measure_empty?") (("2" (case-replace "I!1(i!1)=emptyset") (("1" (replace -4) (("1" (expand "x_eq") (("1" (propax) nil nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "empty?") (("2" (inst -14 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (case-replace "i!1 < n!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (case-replace "i!1 < n!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (skosimp) (("2" (expand "o" 1) (("2" (expand "XX") (("2" (case-replace "i!1 < n!1") (("1" (hide-all-but 1) (("1" (expand "x_add") (("1" (expand "x_eq") (("1" (case-replace "mu!1(I!1(i!1))`1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but (1 2 -9)) (("2" (expand "x_add") (("2" (expand "x_eq") (("2" (inst - "i!1 - n!1") (("2" (flatten) (("2" (lift-if 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (lift-if 1) (("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (replace -1) (("3" (inst -11 "i!1-n!1") (("1" (flatten) (("1" (replace 2) (("1" (assert) (("1" (case-replace "E!1(i!1 - n!1)=emptyset") (("1" (rewrite "A_empty") nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "empty?") (("2" (inst -12 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil) ("5" (skosimp) (("5" (lift-if 1) (("5" (assert) (("5" (prop) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -9 "i!1-n!1") (("1" (flatten) (("1" (assert) (("1" (case-replace "E!1(i!1 - n!1)=emptyset") (("1" (rewrite "A_empty") nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "empty?") (("2" (inst -10 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (replace -5 1 rl) (("2" (expand "XX") (("2" (hide-all-but (1 -11 -8)) (("2" (expand "union") (("2" (expand "member") (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (case-replace "EXISTS (i_1: nat): IF i_1 < n!1 THEN I!1(i_1)(x!1) ELSE E!1(i_1 - n!1)(x!1) ENDIF") (("1" (skosimp) (("1" (case "i!1<n!1") (("1" (assert) (("1" (inst 1 "I!1(i!1)") (("1" (inst 1 "i!1") nil nil)) nil)) nil) ("2" (assert) (("2" (inst 3 "i!1-n!1") nil nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (split) (("1" (skosimp) (("1" (typepred "a!1") (("1" (skolem - "j!1") (("1" (typepred "j!1") (("1" (expand "<=" -1) (("1" (split) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil) ("2" (inst -5 "j!1") (("2" (assert) (("2" (expand "empty?") (("2" (inst -5 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst + "i!1+n!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" (hide -1 2) (("2" (expand "disjoint_indexed_measurable?") (("2" (expand "XX") (("2" (expand "disjoint?") (("2" (lemma "difference_disjoint" ("b" "Y!1" "a" "IUnion(n!1, I!1)")) (("2" (replace -4) (("2" (skosimp) (("2" (case-replace "i!1 < n!1") (("1" (case-replace "j!1 < n!1") (("1" (inst -8 "i!1" "j!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (inst -2 "x!1") (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (split 2) (("1" (inst + "I!1(i!1)") (("1" (inst + "i!1") nil nil)) nil) ("2" (inst + "j!1 - n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "j!1 < n!1") (("1" (assert) (("1" (expand "disjoint?" (-2 3)) (("1" (expand "intersection" (-2 3)) (("1" (expand "empty?" (-2 3)) (("1" (expand "member") (("1" (skosimp) (("1" (inst - "x!1") (("1" (expand "IUnion" 2) (("1" (expand "image") (("1" (expand "Union") (("1" (split) (("1" (inst + "I!1(j!1)") (("1" (inst + "j!1") nil nil)) nil) ("2" (inst + "i!1-n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -3 "i!1-n!1" "j!1-n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skolem + "i!1") (("3" (expand "XX") (("3" (case-replace "i!1<n!1") (("1" (assert) nil nil) ("2" (assert) (("2" (inst - "i!1-n!1") (("2" (flatten) (("2" (case-replace "i!1 - n!1 < n!2") (("2" (assert) (("2" (case-replace "E!1(i!1 - n!1)=emptyset") (("1" (rewrite "A_empty") nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "empty?") (("2" (inst -6 "x!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "finite_disjoint_union?") (("2" (inst + "I!1" "n!1") (("2" (split) (("1" (propax) nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (case-replace "EXISTS (i: nat): I!1(i)(x!1)") (("1" (skosimp) (("1" (inst - "i!1") (("1" (expand "image") (("1" (expand "Union") (("1" (case-replace "i!1 >= n!1") (("1" (expand "empty?") (("1" (inst -5 "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "I!1(i!1)") (("2" (inst + "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (skolem - "i!1") (("2" (inst + "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "member") (("3" (flatten) (("3" (inst - "i!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/") (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (A formal-const-decl "(nonempty?[set[T]])" ast_def nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil ast_def nil) (A_difference_union formula-decl nil ast_def nil) (member const-decl "bool" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (difference_disjoint formula-decl nil sets_lemmas nil) (j!1 skolem-const-decl "nat" ast_def nil) (disjoint? const-decl "bool" sets nil) (i!1 skolem-const-decl "nat" ast_def nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/") (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure_countably_additive? const-decl "bool" generalized_measure_def nil) (XX skolem-const-decl "[nat -> set[T]]" ast_def nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (image const-decl "set[R]" function_image nil) (<= const-decl "bool" reals nil) (I!1 skolem-const-decl "sequence[(A)]" ast_def nil) (i!1 skolem-const-decl "nat" ast_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (Union const-decl "set" sets nil) (union const-decl "set" sets nil) (i!1 skolem-const-decl "nat" ast_def nil) (x_sum_eq formula-decl nil extended_nnreal "extended_nnreal/") (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (O const-decl "T3" function_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (x_sum const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (measure_empty? const-decl "bool" generalized_measure_def nil) (empty? const-decl "bool" sets 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/") (emptyset const-decl "set" sets 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) (x_le 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_eq const-decl "bool" extended_nnreal "extended_nnreal/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (A_empty formula-decl nil ast_def nil) (n!1 skolem-const-decl "nat" ast_def nil) (i!1 skolem-const-decl "nat" ast_def nil) (TRUE const-decl "bool" booleans nil) (x_add_sum formula-decl nil extended_nnreal "extended_nnreal/") (IUnion const-decl "set[T]" indexed_sets nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (setof type-eq-decl nil defined_types nil) (union_diff_subset formula-decl nil sets_lemmas nil) (finite_disjoint_union? const-decl "bool" subset_algebra_def nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (i!1 skolem-const-decl "nat" ast_def nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil)) shostak)) (generalized_measure_monotone 0 (generalized_measure_monotone-1 nil 3458455064 ("" (skosimp) (("" (lemma "generalized_monotonicity" ("mu" "mu!1" "Y" "b!1" "n" "1" "I" "lambda (i:nat): if i=0 then a!1 else emptyset endif")) (("1" (split) (("1" (case "x_eq(x_sum(mu!1 o (LAMBDA (i: nat): IF i = 0 THEN a!1 ELSE emptyset ENDIF)), mu!1(a!1))") (("1" (expand "x_eq") (("1" (expand "x_le") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "x_eq") (("2" (expand "o") (("2" (typepred "mu!1") (("2" (expand "measure?") (("2" (flatten) (("2" (expand "measure_empty?") (("2" (replace -1) (("2" (expand "x_sum") (("2" (case-replace "FORALL i: IF i = 0 THEN mu!1(a!1)`1 ELSE TRUE ENDIF") (("1" (case-replace "convergence_sequences.convergent?(series(LAMBDA i: IF i = 0 THEN mu!1(a!1)`2 ELSE 0 ENDIF))") (("1" (hide -1) (("1" (inst - "0") (("1" (assert) (("1" (replace -1) (("1" (lemma "zero_tail_series_limit" ("n" "0" "a" "LAMBDA i: IF i = 0 THEN mu!1(a!1)`2 ELSE 0 ENDIF")) (("1" (split) (("1" (replace -1) (("1" (expand "series") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "zero_tail_series_conv" ("n" "0" "a" "LAMBDA i: IF i = 0 THEN mu!1(a!1)`2 ELSE 0 ENDIF")) (("2" (assert) (("2" (hide 2) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (skosimp) (("2" (assert) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (case-replace "IUnion(1, LAMBDA (i: nat): IF i = 0 THEN a!1 ELSE emptyset ENDIF)=a!1") (("3" (hide-all-but 1) (("3" (rewrite "IUnion_n_def") (("3" (rewrite "IUnion_0_def") (("3" (apply-extensionality :hide? t) (("3" (expand "union") (("3" (expand "member") (("3" (expand "emptyset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp) (("4" (assert) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "A_empty") nil nil)) nil)) nil)) nil) ((measure_type nonempty-type-eq-decl nil generalized_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) (setof type-eq-decl nil defined_types nil) (emptyset const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (A formal-const-decl "(nonempty?[set[T]])" ast_def nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil ast_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) (generalized_monotonicity formula-decl nil ast_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) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (union const-decl "set" sets nil) (IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (member const-decl "bool" sets nil) (/= const-decl "boolean" notequal nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (x_sum const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (O const-decl "T3" function_props nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (TRUE const-decl "bool" booleans nil) (zero_tail_series_conv formula-decl nil series_lems "series/") (zero_tail_series_limit formula-decl nil series_lems "series/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" sigma "reals/") (sigma_0_neg formula-decl nil sigma_nat "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (measure_empty? const-decl "bool" generalized_measure_def nil) (A_empty formula-decl nil ast_def nil)) shostak)) (ast_TCC1 0 (ast_TCC1-1 nil 3453349304 ("" (skosimp) (("" (typepred "mu!1") (("" (expand "outer_measure?") (("" (name "F" "LAMBDA X: x_inf({z | EXISTS I: x_eq (x_sum (o[nat, (A), extended_nnreal] (mu!1, I)), z) AND subset?[T](X, IUnion[nat, T](I))})") (("" (replace -1) (("" (case-replace "om_empty?(F)") (("1" (case-replace "om_increasing?(F)") (("1" (expand "om_countably_subadditive?") (("1" (skosimp) (("1" (hide -3) (("1" (case "forall (epsilon:posreal): x_lt(F(IUnion(X!1)), x_add((TRUE,epsilon),x_sum(F o X (("1" (expand "x_le") (("1" (flatten) (("1" (name-replace "LHS" "F(IUnion(X!1))") (("1" (name-replace "RHS" "x_sum(F o X!1)") (("1" (assert) (("1" (expand "x_add") (("1" (expand "x_lt") (("1" (inst-cp - "1") (("1" (flatten) (("1" (assert) (("1" (hide -3) (("1" (inst - "LHS`2-RHS`2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (case "x_lt(F(IUnion(X!1)), x_sum(LAMBDA (n: nat): x_add((TRUE, epsilon!1 / expt(2, n + 1)), F(X!1(n)))))") (("1" (case "x_eq(x_sum(lambda (n:nat): x_add((TRUE,epsilon!1/expt(2,n+1)),F(X!1(n)))),x_add(( (("1" (expand "x_eq") (("1" (expand "x_lt") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "x_add") (("2" (expand "x_sum") (("2" (expand "x_eq") (("2" (expand "o ") (("2" (lift-if) (("2" (case-replace "FORALL (i:nat): F(X!1(i))`1") (("1" (case "convergence(series(lambda (i:nat): epsilon!1 / expt(2, 1 + i)),epsilon!1)") (("1" (case-replace "convergence_sequences.convergent?(series(LAMBDA (i:nat): F(X!1(i))`2))") (("1" (lemma "convergence_sequences.limit_lemma" ("v" "series(LAMBDA (i: nat): F(X!1(i))`2)")) (("1" (hide -2) (("1" (lemma "cnv_seq_sum" ("s1" "series(LAMBDA (i: nat): F(X!1(i))`2)" "l1" "convergence_sequences.limit(series(LAMBDA (i:nat): F(X!1(i))`2))" "s2" "series(LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i))" "l2" "epsilon!1")) (("1" (assert) (("1" (case-replace "series(LAMBDA (i:nat): IF F(X!1(i))`1 THEN epsilon!1 / expt(2, 1 + i) + F(X!1(i))`2 ELSE 0 ENDIF)=series(LAMBDA (i: nat): F(X!1(i))`2) + series(LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i))") (("1" (hide -1) (("1" (name-replace "S1" "series(LAMBDA (i: nat): F(X!1(i))`2)") (("1" (name-replace "S2" "series(LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i))") (("1" (case-replace "convergence_sequences.convergent?(S1 + S2)") (("1" (rewrite "convergence_sequences.limit_def" -2 :dir rl) (("1" (assert) (("1" (replace -2 1 rl) (("1" (expand "limit") (("1" (expand "+ ") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "+ ") (("2" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergence_sequences.convergent?") (("2" (inst + "convergence_sequences.limit(S1) + epsilon!1") (("2" (expand "+ ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (expand "series") (("2" (apply-extensionality :hide? t) (("2" (expand "+") (("2" (rewrite "sigma_sum") (("2" (case-replace "(LAMBDA (i: nat): IF F(X!1(i))`1 THEN epsilon!1 / expt(2, 1 + i) + F(X!1(i))`2 ELSE 0 ENDIF) =LAMBDA (i_1: nat): epsilon!1 / expt(2, 1 + i_1) + F(X!1(i_1))`2") (("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (replace 1) (("2" (assert) (("2" (case-replace "convergence_sequences.convergent?(series(LAMBDA (i:nat): IF F(X!1(i))`1 THEN epsilon!1 / expt(2, 1 + i) + F(X!1(i))`2 ELSE 0 ENDIF))") (("1" (lemma "convergent_diff" ("s1" "series(LAMBDA (i: nat): IF F(X!1(i))`1 THEN epsilon!1 / expt(2, 1 + i) + F(X!1(i))`2 ELSE 0 ENDIF)" "s2" "series(LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i))")) (("1" (assert) (("1" (split) (("1" (expand "-" -1) (("1" (expand "series" (-1 1)) (("1" (case-replace "(LAMBDA (x: nat): sigma(0, x, LAMBDA (i: nat): IF F(X!1(i))`1 THEN epsilon!1 / expt(2, 1 + i) + F(X!1(i))`2 ELSE 0 ENDIF) - sigma(0, x, LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i)))=(LAMBDA (n: nat): sigma(0, n, LAMBDA (i: nat): F(X (("1" (apply-extensionality :hide? t) (("1" (hide-all-but (-4 1)) (("1" (rewrite "sigma_minus") (("1" (case-replace "(LAMBDA (i_1: nat): IF F(X!1(i_1))`1 THEN epsilon!1 / expt(2, 1 + i_1) + F(X!1(i_1))`2 ELSE 0 ENDIF - epsilon!1 / expt(2, 1 + i_1))=LAMBDA (i: nat): F(X!1(i))`2") (("1" (apply-extensionality :hide? t) (("1" (inst - "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergence_sequences.convergent?") (("2" (inst + "epsilon!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "geometric_series" ("x" "1/2")) (("2" (split) (("1" (expand "geometric") (("1" (expand "^") (("1" (case-replace "1 / (1 - 1 / 2)=2") (("1" (hide -1) (("1" (lemma "series_scal" ("a" "LAMBDA (n:nat): expt(1 / 2, n)" "c" "epsilon!1/2")) (("1" (case-replace "(LAMBDA (n_1: nat): epsilon!1 / 2 * (LAMBDA (n: nat): expt(1 / 2, n))(n_1))=(LAMBDA (i: nat): epsilon!1 / expt(2, 1 + (("1" (hide -1) (("1" (name-replace "S1" "series((LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i)))") (("1" (lemma "cnv_seq_scal" ("s1" "series(LAMBDA (n:nat): expt(1 / 2, n))" "l1" "2" "a" "epsilon!1/2")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (expand "expt" 1 2) (("2" (rewrite "expt_of_inv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "forall (x:(A)): x_le(F(x),mu!1(x))") (("1" (case "FORALL (n: nat): nonempty?({I | subset?(X!1(n), IUnion(I)) & x_lt(x_sum(mu!1 o I), x_add((TRUE, epsilon!1 / expt(2, n + 1)), F(X!1(n))))})") (("1" (name "II" "lambda (n:nat): choose({I | subset?(X!1(n), IUnion(I)) & x_lt(x_sum(mu!1 o I), x_add((TRUE, epsilon!1 / expt(2, n + 1)), F(X!1(n))))})") (("1" (hide -1) (("1" (lemma "x_sum_lt" ("S" "lambda (n:nat): x_sum(mu!1 o II(n))" "T" "LAMBDA (n: nat): x_add((TRUE, epsilon!1 / expt(2, n + 1)), F(X!1(n)))")) (("1" (split -1) (("1" (case "x_le(F(IUnion(X!1)),x_sum(LAMBDA (n: nat): x_sum(mu!1 o II(n))))") (("1" (name-replace "LHS" "F(IUnion(X!1))") (("1" (name-replace "RHS" "x_sum(LAMBDA (n: nat): x_add((TRUE, epsilon!1 / expt(2, n + 1)), F(X!1(n))))") (("1" (name-replace "DRL" "x_sum(LAMBDA (n: nat): x_sum(mu!1 o II(n)))") (("1" (hide-all-but (-1 -2 1)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (hide -1) (("2" (lemma "double_x_sum" ("U" "lambda (i,j:nat): mu!1(II(i)(j))")) (("2" (assert) (("2" (expand "o" 1) (("2" (name-replace "RHS" "x_sum(LAMBDA (n: nat): x_sum(LAMBDA (x: nat): mu!1(II(n)(x))))") (("2" (case "x_le(F(IUnion(X!1)),x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j)))))") (("1" (name-replace "DRL" "x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j))))") (("1" (name-replace "LHS" "F(IUnion(X!1))") (("1" (hide-all-but (-1 -2 1)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "x_le" 1) (("2" (expand "F" 1) (("2" (expand "x_inf") (("2" (flatten) (("2" (replace -1) (("2" (lift-if) (("2" (assert) (("2" (prop) (("1" (inst - "x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j))))") (("1" (expand "o") (("1" (expand "single_index") (("1" (inst + "lambda (n:nat): II(double_index_i(n))(double_index_j(n))") (("1" (split) (("1" (name-replace "SUM" "x_sum(LAMBDA (x: nat): mu!1(II(double_index_i(x))(double_index_j(x))))") (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "IUnion") (("2" (skosimp) (("2" (skosimp) (("2" (typepred "II(i!1)") (("2" (hide -2) (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (expand "member") (("2" (assert) (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst + "double_index_n(i!1,i!2)") (("2" (lemma "double_index_ij_n" ("i" "i!1" "j" "i!2")) (("2" (flatten) (("2" (replace -1) (("2" (replace -2) (("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) ("2" (skosimp) (("2" (typepred "glb({z_1: real | EXISTS (x:extended_nnreal): (EXISTS I: x_eq(x_sum(o[nat, (A), extended_nnreal](mu!1, I)), x) AND subset?[T](IUnion(X!1), IUnion[nat, T](I))) AND x`1 AND x`2 = z_1})") (("1" (name-replace "GLB" "glb({z_1: real | EXISTS (x:extended_nnreal): (EXISTS I: x_eq(x_sum(o[nat, (A), extended_nnreal](mu!1, I)), x) AND subset?[T](IUnion(X!1), IUnion[nat, T](I))) AND x`1 AND x`2 = z_1})") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (expand "lower_bound?") (("1" (inst - "x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j))))`2") (("1" (inst + "x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j))))") (("1" (replace -3) (("1" (hide -1 2) (("1" (expand "single_index") (("1" (inst + "LAMBDA (n:nat): II(double_index_i(n))(double_index_j(n))") (("1" (split) (("1" (expand "o") (("1" (name-replace "SUM" "x_sum(LAMBDA (x: nat): mu!1(II(double_index_i(x))(double_index_j(x))))") (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (hide-all-but 1) (("2" (expand "member") (("2" (expand "IUnion") (("2" (skosimp) (("2" (skosimp) (("2" (typepred "II(i!1)") (("2" (hide -2) (("2" (expand "subset?") (("2" (inst - "x!2") (("2" (expand "member") (("2" (assert) (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst + "double_index_n(i!1,i!2)") (("2" (lemma "double_index_ij_n" ("i" "i!1" "j" "i!2")) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (typepred "x!1") (("1" (skosimp) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst -3 "x!1`2") (("1" (expand "member") (("1" (inst + "x!1") (("1" (replace -3) (("1" (inst + "I!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("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) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "II(i!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (name "FX" "F(X!1(n!1))") (("2" (replace -1) (("2" (expand "F" -1) (("2" (expand "x_inf" -1) (("2" (lift-if -1) (("2" (assert) (("2" (case-replace "FORALL (x: ({z:extended_nnreal | EXISTS I: x_eq(x_sum(o[nat, (A), extended_nnreal](mu!1, I)), z) AND subset?[T](X!1(n!1), IUnion[nat, T](I))})): NOT x`1") (("1" (replace -2 -3 rl) (("1" (expand "x_add") (("1" (expand "x_lt") (("1" (inst -3 "lambda (n:nat): fullset[T]") (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (rewrite "A_fullset") nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (skosimp) (("2" (typepred "x!1") (("2" (skosimp) (("2" (replace -4 -5 rl) (("2" (hide -4) (("2" (expand "x_add") (("2" (expand "x_lt") (("2" (typepred "glb({z_1: real | EXISTS (x:extended_nnreal): (EXISTS I: x_eq(x_sum(o[nat, (A), extended_nnreal] (mu!1, I)), x) AND subset?[T](X!1(n!1), IUnion[nat, T](I))) AND x`1 AND x`2 = z_1})") (("1" (name-replace "GLB" "glb({z_1: real | EXISTS (x:extended_nnreal): (EXISTS I: x_eq(x_sum(o[nat, (A), extended_nnreal] (mu!1, I)), x) AND subset?[T](X!1(n!1), IUnion[nat, T](I))) AND x`1 AND x`2 = z_1})") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "epsilon!1" "py" "expt(2, 1 + n!1)")) (("1" (name-replace "R" "epsilon!1 / expt(2, 1 + n!1)") (("1" (inst -3 "GLB+R") (("1" (assert) (("1" (expand "lower_bound?") (("1" (skosimp) (("1" (case "s!1<GLB+R") (("1" (hide 1) (("1" (typepred "s!1") (("1" (skosimp) (("1" (skosimp) (("1" (inst -11 "I!2") (("1" (replace -2) (("1" (expand "x_eq" -1) (("1" (flatten) (("1" (replace -1) (("1" (replace -4) (("1" (replace -2) (("1" (replace -5) (("1" (propax) 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) ("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1`2") (("1" (expand "member") (("1" (inst + "x!1") (("1" (replace -3) (("1" (inst + "I!1") (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (assert) (("2" (typepred "s!1") (("2" (skosimp) (("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)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "F" 1) (("2" (expand "x_le") (("2" (flatten) (("2" (replace -1) (("2" (expand "x_inf") (("2" (lift-if) (("2" (assert) (("2" (prop) (("1" (inst - "mu!1(x!1)") (("1" (inst + "lambda (n:nat): if n=0 then x!1 else emptyset[T] endif") (("1" (split) (("1" (expand "o") (("1" (expand "measure?") (("1" (flatten) (("1" (expand "measure_empty?") (("1" (replace -4) (("1" (expand "x_eq") (("1" (expand "x_sum") (("1" (replace -1) (("1" (assert) (("1" (lift-if 1) (("1" (assert) (("1" (lemma "zero_tail_series_conv" ("n" "0" "a" "LAMBDA (i:nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF")) (("1" (lemma "zero_tail_series_limit" ("n" "0" "a" "LAMBDA (i:nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF")) (("1" (case-replace "FORALL (m:nat): 0 < m => (LAMBDA (i: nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF)(m) = 0") (("1" (replace -2) (("1" (replace -3) (("1" (expand "series") (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (expand "IUnion") (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "A_empty") nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "x!2") (("2" (skosimp) (("2" (typepred "glb({z_1: real | EXISTS (x:extended_nnreal): (EXISTS I: x_eq(x_sum(o[nat, (A), extended_nnreal](mu!1, I)), x) AND subset?[T](x!1, IUnion[nat, T](I))) AND x`1 AND x`2 = z_1})") (("1" (name-replace "LHS" "glb({z_1: real | EXISTS (x:extended_nnreal): (EXISTS I: x_eq(x_sum(o[nat, (A), extended_nnreal](mu!1, I)), x) AND subset?[T](x!1, IUnion[nat, T](I))) AND x`1 AND x`2 = z_1})") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (expand "lower_bound?") (("1" (inst - "mu!1(x!1)`2") (("1" (hide 2 -1) (("1" (inst + "mu!1(x!1)") (("1" (replace -4) (("1" (inst + "lambda (n:nat): if n=0 then x!1 else emptyset[T] endif") (("1" (split) (("1" (expand "o") (("1" (expand "measure?") (("1" (flatten) (("1" (expand "measure_empty?") (("1" (replace -7) (("1" (expand "x_eq" 1) (("1" (expand "x_sum" 1) (("1" (replace -4) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lemma "zero_tail_series_conv" ("a" "LAMBDA (i:nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF" "n" "0")) (("1" (lemma "zero_tail_series_limit" ("a" "LAMBDA (i:nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF" "n" "0")) (("1" (case-replace "FORALL (m:nat): 0 < m => (LAMBDA (i: nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF)(m) = 0") (("1" (replace -2) (("1" (replace -3) (("1" (expand "series") (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (expand "IUnion") (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "A_empty") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!2`2") (("1" (inst + "x!2") (("1" (replace -3) (("1" (inst + "I!1") (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("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)) nil)) nil) ("2" (hide 2) (("2" (expand "om_increasing?") (("2" (skosimp) (("2" (expand "x_le" 1) (("2" (flatten) (("2" (assert) (("2" (replace -2) (("2" (hide -4) (("2" (expand "F") (("2" (expand "o") (("2" (expand "x_inf") (("2" (case-replace "FORALL (x_1: ({z:extended_nnreal | EXISTS I: x_eq(x_sum(LAMBDA (x: nat): mu!1(I(x))), z) AND subset?[T](b!1, IUnion[nat, T](I))})): NOT x_1`1") (("2" (replace 1) (("2" (skosimp) (("2" (case-replace "FORALL (x_1: ({z:extended_nnreal | EXISTS I: x_eq(x_sum(LAMBDA (x: nat): mu!1(I(x))), z) AND subset?[T](a!1, IUnion[nat, T](I))})): NOT x_1`1") (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (skosimp) (("1" (inst + "I!1") (("1" (assert) (("1" (hide-all-but (-2 -4 1)) (("1" (expand "subset?") (("1" (skosimp) (("1" (inst - "x!2") (("1" (inst - "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (skosimp) (("2" (hide -4) (("2" (typepred "x!1") (("2" (skosimp) (("2" (typepred "x!2") (("2" (skosimp) (("2" (typepred "glb({z_1: real | EXISTS (x_1: extended_nnreal): (EXISTS I: x_eq(x_sum(LAMBDA (x: nat): mu!1(I(x))), x_1) AND subset?[T](b!1, IUnion[nat, T](I))) AND x_1`1 AND x_1`2 = z_1})") (("1" (name-replace "RHS" "glb({z_1: real | EXISTS (x_1: extended_nnreal): (EXISTS I: x_eq(x_sum(LAMBDA (x: nat): mu!1(I(x))), x_1) AND subset?[T](b!1, IUnion[nat, T](I))) AND x_1`1 AND x_1`2 = z_1})") (("1" (typepred "glb({z_1: real | EXISTS (x_1: extended_nnreal): (EXISTS I: x_eq(x_sum(LAMBDA (x: nat): mu!1(I(x))), x_1) AND subset?[T](a!1, IUnion[nat, T](I))) AND x_1`1 AND x_1`2 = z_1})") (("1" (name-replace "LHS" "glb({z_1: real | EXISTS (x_1: extended_nnreal): (EXISTS I: x_eq(x_sum(LAMBDA (x: nat): mu!1(I(x))), x_1) AND subset?[T](a!1, IUnion[nat, T](I))) AND x_1`1 AND x_1`2 = z_1})") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (hide -3 -2) (("1" (expand "lower_bound?") (("1" (inst -2 "LHS") (("1" (split -2) (("1" (propax) nil nil) ("2" (skosimp) (("2" (hide 2) (("2" (typepred "s!1") (("2" (skosimp) (("2" (skosimp) (("2" (inst -5 "s!1") (("2" (inst + "x!3") (("2" (replace -3) (("2" (replace -4) (("2" (inst + "I!3") (("2" (assert) (("2" (hide-all-but (-2 1 -11)) (("2" (expand "subset?") (("2" (skosimp) (("2" (inst - "x!4") (("2" (inst - "x!4") (("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) ("2" (hide-all-but (-2 -3 -6 1)) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!2`2") (("1" --> -------------------- --> maximum size reached --> --------------------
¤ 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.1.36Bemerkung: (vorverarbeitet am 2026-04-26) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26