Impressum ast_def.prf
Sprache: Lisp
(ast_defnil 3457694307 ("" (postpone) nil nil ) nil shostak))nil 3458454898"" (rewrite "A_empty" ) nil nil )nil ast_def nil )) nil ))nil 3457883471"" case "forall (a:(A),E:disjoint_indexed_measurable,n:nat): finite_disjoint_union?(A)(difference(a, IUnion(n,E)))" )"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" "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" "1" expand "emptyset" )"1" "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" "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" "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" "i!1" )"1" expand "image" )"1" expand "Union" )"1" "E!1(i!1)" )"1" "1" "i!1 < n!1" )"1" "i!1" )"1" (assert ) nil nil ))nil )"2" assert )"2" rewrite "emptyset_is_empty?" )"2" replace -6)"2" expand "emptyset" )"2" 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" "2" "a!2" )"2" "2" "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" "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),difference(b,c))" )"1" (case-replace "n!1=0" )"1" (assert )"1" "IUnion(E!2)=emptyset" )"1" replace -5)"1" rewrite "difference_emptyset2" )"1" "1" expand "finite_disjoint_union?" )"1" "lambda (i:nat): emptyset" "0" )"1" "1" (grind) nil nil )"2" "2" expand "emptyset" )"2" expand "IUnion" )"2" nil nil ))nil ))nil ))nil )"3" expand "member" )"3" expand "empty?" )"3" expand "member" )"3" expand "emptyset" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "emptyset" )"2" expand "IUnion" )"2" "2" "i!1" )"2" expand "empty?" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "n!1>0" )"1" "1" "IUnion(E!2)=IUnion(n!1-1,E!2)" )"1" replace -5)"1" "1" case "forall (n:nat): finite_disjoint_union?(A) ") "1" "n!1-1" )"1" (assert ) nil nil ))nil )"2" "2" "n" )"1" rewrite "IUnion_0_def" )"1" "E!2(0)" "E!1" )"1" assert )"1" "0" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "IUnion_n_def" )"2" "IUnion(j!2, E!2)" "E!2(1 + j!2)" "IUnion(j!1, E!1)" )"2" replace -3)"2" "E!2(1 + j!2)" "E!1" )"1" "1" "AA" "difference(IUnion(j!2, E!2), ") "1" "BB" "difference(E!2(1 + j!2), IUnion(j!1, E!1))" )"1" case "disjoint?(AA,BB)" )"1" expand "finite_disjoint_union?" )"1" "1" "lambda (i:nat): if i<n!2 then E!3(i) else E!4(i-n!2) endif" "n!2+n!3" )"1" "1" expand "disjoint?" "1" "1" "i!1 < n!2" )"1" "j!3 < n!2" )"1" expand "disjoint?" "1" "i!1" "j!3" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" expand "disjoint?" "2" expand "intersection" )"2" expand "empty?" "2" "2" expand "member" )"2" "2" "x!1" )"2" replace "2" "1" expand "IUnion" "1" "i!1" )nil nil ))nil )"2" replace "2" expand "IUnion" )"2" "j!3-n!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "j!3 < n!2" )"1" expand "disjoint?" "1" expand "intersection" )"1" expand "empty?" "1" expand "member" )"1" "1" "x!1" )"1" "1" replace "1" expand "IUnion" )"1" "j!3" )nil nil ))nil ))nil )"2" replace "2" expand "IUnion" )"2" "i!1-n!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "disjoint?" "2" "i!1 - n!2" "j!3 - n!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "union" )"1" expand "disjoint?" "1" expand "intersection" )"1" expand "empty?" "1" expand "member" )"1" "x!1" )"1" "AA(x!1)" )"1" replace "1" expand "IUnion" "1" "1" "i!1" )"1" "i!1" )"1" "i!1 < n!2" )"1" assert )"1" expand "empty?" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "BB(x!1)" )"1" replace "1" expand "IUnion" "1" "1" "n!2+i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace "2" replace "2" expand "IUnion" "2" "2" "i!1 < n!2" )"1" "i!1" )nil nil )"2" assert )"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" "2" assert )nil nil ))nil ))nil )"3" "3" expand "member" )"3" assert )"3" "i!1 < n!2" )"1" assert )"1" "i!1" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "i!1-n!2" )"2" "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" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint?" "2" expand "intersection" )"2" expand "empty?" )"2" "2" expand "member" )"2" "2" expand "AA" )"2" expand "BB" )"2" expand "difference" )"2" expand "member" )"2" "2" "2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "2" "a!2" )"2" "i!1" )"2" replace "2" "2" expand "disjoint?" )"2" "i!1" "1+j!2" )"2" assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "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" "1+j!2" )"2" assert )"2" "2" assert )"2" rewrite "emptyset_is_empty?" )"2" replace "2" rewrite "A_empty" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "IUnion(E!2)(x!1)" )"1" expand "IUnion" )"1" "1" "i!1" )"1" "1" expand "image" )"1" expand "Union" )"1" "E!2(i!1)" )"1" "i!1" )"1" assert )"1" expand "empty?" )"1" "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" "2" "a!2" )"2" "2" "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" "2" expand "difference" )"2" expand "union" )"2" expand "member" )"2" "a!2(x!1)" )"1" assert )"1" "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 )nil nat_indexed_sets "sets_aux/" )"posint" nil )nil sets_lemmas nil )"set" sets nil )"nat" ast_def nil )"nat" ast_def nil )"[bool, bool -> bool]" booleans nil )"nonneg_int" nil )"set[T]" ast_def nil )"set[T]" ast_def nil )"sequence[set[T]]" ast_def nil )"nat" ast_def nil )"nat" ast_def nil )"boolean" notequal nil )"finite_set[T]" "sets_aux/" )nil sets_lemmas nil )"posint" nil )nil sets_lemmas nil )"[numfield, numfield -> numfield]" number_fields nil )nil ast_def nil )nil nat_indexed_sets "sets_aux/" )nil naturalnumbers nil )nil defined_types nil )"bool" reals nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil ast_def nil )nil sets_lemmas nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"nat" ast_def nil )"sequence[set[T]]" ast_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set[T]" ast_def nil )NOT const-decl "[bool -> bool]" booleans nil )"set[R]" function_image nil )"bool" reals nil )"nat" ast_def nil )"(total_order?[real])" nil )"set" sets nil )"bool" sets nil )nil sets_lemmas nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" indexed_sets_aux "sets_aux/" )"set[T]" indexed_sets nil )"(strict_total_order?[real])" real_props nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"set" sets nil )"[T, T -> boolean]" equalities nil )nil ast_def nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"(nonempty?[set[T]])" ast_def nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil defined_types nil )"bool" nil )nil nil )nil sets nil )"bool" subset_algebra_def nil )"set" sets nil )nil sequences nil )"set[T]" nat_indexed_sets "sets_aux/" ))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" "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" "x_sum_le" "S" "lambda (j:nat): x_sum(mu!1 o FDU(j))" "T" "mu!1 o I!1" ))"1" (split -1)"1" "UU" "lambda (i,j:nat): FDU(i)(j)" )"1" "double_x_sum" "U" "mu!1 o UU" ))"1" expand "UU" -1 2)"1" expand "o" -1 2)"1" expand "o" -3 1)"1" "DRL1" "x_sum(LAMBDA (j: nat): x_sum(LAMBDA (x: nat): mu!1(FDU(j)(x))))" )"1" "single_index(mu!1 o UU) = mu!1 o single_index(UU)" )"1" "1" expand "measure_countably_additive?" )"1" "single_index(UU)" )"1" "DRL2" "x_sum(mu!1 o single_index(UU))" )"1" "RHS" "x_sum(mu!1 o I!1)" )"1" "IUnion(single_index(UU))=IUnion(I!1)" )"1" assert )"1" "LHS" "mu!1(IUnion(I!1))" )"1" "1" expand "x_le" )"1" expand "x_eq" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -13)"2" expand "UU" )"2" "2" "2" "IUnion(B!1)(x!1)" )"1" expand "IUnion" )"1" "1" "i!1" )"1" replace "1" assert )"1" "1" expand "single_index" )"1" "double_index_n(i!1,i!2)" )"1" "double_index_ij_n" "i" "i!1" "j" "i!2" ))"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" "n!1" )"2" expand "single_index" )"2" "double_index_n_ij" "n" "n!1" ))"2" "double_index_i(n!1)" )"2" "double_index_i(n!1)" )"2" replace "2" assert )"2" "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" "2" expand "disjoint_indexed_measurable?" )"2" expand "disjoint?" "2" "2" expand "UU" )"2" assert )"2" expand "single_index" )"2" "2" "double_index_i(j!1)=double_index_i(i!1)" )"1" "double_index_i(i!1)" )"1" "FDU(double_index_i(i!1))" )"1" expand "disjoint_indexed_measurable?" )"1" expand "disjoint?" "1" "double_index_j(i!1)" "double_index_j(j!1)" )"1" assert )"1" expand "/=" "1" "double_index_n_ij" "n" "i!1" ))"1" "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" "double_index_i(i!1)" )"2" "double_index_i(j!1)" )"2" expand "disjoint?" "2" "double_index_i(i!1)" "double_index_i(j!1)" )"2" assert )"2" replace "2" replace "2" "2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" "x!1" )"2" "1" expand "IUnion" )"1" "double_index_j(i!1)" )nil nil ))nil )"2" expand "IUnion" )"2" "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" "2" "2" expand "o " )"2" expand "single_index" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "n!1" )"3" expand "single_index" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" "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" "j!1" )"2" "FDU(j!1)" )"2" "2" case "subset?(B!1(j!1),I!1(j!1))" )"1" "A_difference_union" "a" "I!1(j!1)" "b" "B!1(j!1)" ))"1" assert )"1" "union_diff_subset" "b" "I!1(j!1)" "a" "B!1(j!1)" ))"1" assert )"1" "difference_disjoint" "a" "B!1(j!1)" "b" "I!1(j!1)" ))"1" "DIFF" "difference(I!1(j!1), B!1(j!1))" )"1" "BB" "B!1(j!1)" )"1" "AA" "FDU(j!1)" )"1" "II" "I!1(j!1)" )"1" expand "finite_disjoint_union?" )"1" "1" expand "member" )"1" "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" "XX" )"1" "IUnion(XX)=II" )"1" assert )"1" "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" "x_sum_eq" "S" "LAMBDA (i_1: nat): LAMBDA (i: nat):IF i < n!1 THEN mu!1(E!1(i))LAMBDA (i: nat):IF i < n!1 THEN (TRUE, 0)" "T" "mu!1 o XX" ))"1" "1" "DRL1" "x_sum(LAMBDA (i_1: nat): LAMBDA (i: nat):IF i < n!1 THEN mu!1(E!1(i))LAMBDA (i: nat):IF i < n!1 THEN (TRUE, 0)") "1" case "x_eq(x_sum(mu!1 o AA),x_sum(LAMBDA (i: nat): IF i < n!1 THEN (TRUE, 0)") "1" "LHS" "x_sum(mu!1 o AA)" )"1" "RHS" "mu!1(II)" )"1" "DRL2" "x_sum(mu!1 o XX)" )"1" "DRL3" "x_sum(LAMBDA (i: nat): IF i < n!1 THEN (TRUE, 0) ELSE mu!1(AA(i - n!1)) ENDIF)") "1" "1" expand "x_le" )"1" "1" expand "x_eq" )"1" assert )"1" "1" assert )"1" expand "x_add" )"1" assert )"1" "1" "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" "2" expand "x_sum" )"2" expand "x_eq" )"2" "FORALL (i:nat): (mu!1 o AA)(i)`1" )"1" "FORALL (i_1: nat): IF i_1 < n!1 THEN TRUE ELSE mu!1(AA(i_1 - n!1))`1 ENDIF") "1" "convergence_sequences.convergent?(series(LAMBDA (i:nat): (mu!1 o AA)(i)`2))" )"1" "convergence_sequences.convergent?(series(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0") "1" "n!1=0" )"1" "(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" "1" expand "o " )"1" nil nil ))nil ))nil ))nil )"2" "limit_series_shift" "a" "(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0" "pn" "n!1" ))"1" replace "1" replace "1" expand "o " )"1" "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" "1" rewrite "sigma_zero" )"1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" "conv_series_shift" "a" "(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0" "N" "n!1" ))"2" expand "o " )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" expand "o " )"2" "conv_series_shift" "a" "(LAMBDA (i_1: nat): IF i_1 < n!1 THEN 0" "N" "n!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1-n!1" )"1" expand "o " )"1" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "FORALL (i_1: nat): IF i_1 < n!1 THEN TRUE ELSE mu!1(AA(i_1 - n!1))`1 ENDIF") "1" "1" "1" expand "o " )"1" "i!1+n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "XX" )"2" expand "o" )"2" "i!1 < n!1" )"1" expand "x_add" )"1" expand "x_eq" )"1" "1" "1" "1" nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "x_add" )"2" expand "x_eq" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" "4" assert )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil )"5" "5" "i!2" )"5" "5" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" "2" "2" expand "union" )"2" expand "member" )"2" "IUnion(E!1)(x!1)" )"1" expand "IUnion" )"1" "1" "i!1" )"1" expand "XX" )"1" "i!1" )"1" "1" assert )"1" "i!1 < n!1" )"1" assert )"1" expand "empty?" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "IUnion(AA)(x!1)" )"1" "1" expand "IUnion" )"1" "1" expand "XX" )"1" "n!1+i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" "2" expand "XX" )"2" "i!1<n!1" )"1" "i!1" )nil nil )"2" assert )"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" "2" expand "disjoint_indexed_measurable?" )"2" expand "disjoint?" "2" "2" expand "XX" )"2" "2" "i!1 < n!1" )"1" "j!2 < n!1" )"1" expand "disjoint?" "1" "i!1" "j!2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" replace "2" replace "2" expand "disjoint?" "2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" "x!1" )"2" "1" expand "IUnion" )"1" "j!2-n!1" )nil nil ))nil )"2" expand "IUnion" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "j!2 < n!1" )"1" assert )"1" replace "1" replace "1" expand "disjoint?" "1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "1" "x!1" )"1" "1" expand "IUnion" )"1" "i!1-n!1" )nil nil ))nil )"2" expand "IUnion" )"2" "j!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "disjoint?" "2" "i!1 - n!1" "j!2 - n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "XX" )"3" "x1!1 < n!1" )"1" "x1!1" )"1" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" "2" expand "member" )"2" "j!1=0" )"1" (assert ) nil nil )"2" "j!1-1" )"1" assert )"1" replace -8 -1)"1" expand "difference" )"1" expand "member" )"1" 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" "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" "E!1" )"2" expand "disjoint_indexed_measurable?" )"2" assert )"2" "2" "x1!1" )"2" "2" assert )"2" "E!1(x1!1)=emptyset" )"1" rewrite "A_empty" )nil nil )"2" "2" "x!1" )"2" expand "emptyset" )"2" 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" "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" "1" expand "finite_disjoint_union?" )"1" "lambda (i:nat): if i=0 then I!1(0) else emptyset endif" "1" )"1" "1" (grind) nil nil )"2" "2" expand "IUnion" )"2" expand "emptyset" )"2" "I!1(0)(x!1)" )"1" "0" )nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "member" )"3" rewrite "A_empty" )"3" assert )"3" "3" assert )"3" expand "empty?" )"3" "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" "1" "j!1-1" )"1" assert )"1" replace -6)"1" "j!1-1" )"1" case "forall (n:nat): n < j!1 => finite_disjoint_union?(A)(IUnion(n,B!1))" )"1" "j!1-1" )"1" assert )"1" "A_difference_union" "a" "I!1(j!1)" "b" "IUnion(j!1 - 1, B!1)" ))"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "n" )"1" "1" rewrite "IUnion_0_def" )"1" replace -6)"1" "1" expand "finite_disjoint_union?" )"1" "lambda (i:nat): if i=0 then I!1(0) else emptyset endif" "1" )"1" expand "member" )"1" rewrite "A_empty" )"1" "1" nil nil )"2" "2" expand "IUnion" )"2" expand "emptyset" )"2" "I!1(0)(x!1)" )"1" "0" )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" expand "empty?" )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" rewrite "IUnion_n_def" "2" "1+j!2" )"2" assert )"2" "AA" "IUnion(j!2, B!1)" )"2" "BB" "B!1(1 + j!2)" )"2" "2" expand "finite_disjoint_union?" )"2" "2" "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" "1" expand "disjoint?" "1" "1" "i!1 < n!1" )"1" "j!3 < n!1" )"1" "i!1" "j!3" )"1" assert )nil nil ))nil )"2" assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" "2" expand "member" )"2" "2" "x!1" )"2" "1" replace "1" expand "IUnion" )"1" "i!1" )nil nil ))nil ))nil )"2" replace "2" expand "IUnion" )"2" "j!3-n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "j!3 < n!1" )"1" assert )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "1" "x!1" )"1" "1" replace "1" expand "IUnion" )"1" "j!3" )nil nil ))nil ))nil )"2" replace "2" expand "IUnion" )"2" "i!1-n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "i!1-n!1" "j!3-n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "union" )"1" expand "member" )"1" replace "1" replace "1" "IUnion(E!1)(x!1)" )"1" expand "IUnion" )"1" "1" "i!1" )"1" "i!1" )"1" "i!1<n!1" )"1" assert )"1" expand "empty?" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "IUnion(E!2)(x!1)" )"1" expand "IUnion" )"1" "1" "1" "n!1+i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" "2" "i!1<n!1" )"1" "i!1" )nil nil )"2" assert )"2" "i!1-n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"3" "3" "i!1 < n!1" )"1" "i!1" )"1" assert )nil nil ))nil )"2" assert )"2" "i!1-n!1" )"2" "2" "i!1 < n!1 + n!2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "BB" )"2" expand "AA" )"2" "2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "2" "a!1" )"2" "i!2" )"2" "i!2" "1+j!2" )"2" assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "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" "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 )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"(nonempty?[set[T]])" ast_def nil )"bool" sets nil )set type-eq-decl nil sets nil )nil defined_types nil )nil ast_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nat" ast_def nil )nil naturalnumbers nil )nil nat_indexed_sets "sets_aux/" )"posint" nil )"set[T]" ast_def nil )"set" sets nil )"set[R]" function_image nil )"set[T]" ast_def nil )"nat" ast_def nil )"odd_int" integers nil )"odd_int" integersnil )"even_int" integersnil )"even_int" integersnil )"posint" nil )nil nat_indexed_sets "sets_aux/" )nil defined_types nil )nil naturalnumbers nil )"bool" nil )nil nil )"[T, T -> boolean]" equalities nil )"set[T]" indexed_sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil )"set" sets nil )"[nat -> set[T]]" ast_def nil )"set" sets nil )nil extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil series "series/" )nil integers nil )"bool" reals nil )nil integers nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil series "series/" )"bool" convergence_sequences "analysis/" )"sequence[real]" series "series/" )"(total_order?[real])" nil )"nat" ast_def nil )"nat" ast_def nil )"nnreal" nil )"bool" booleans nil )nil extended_nnreal "extended_nnreal/" )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"int" integers nil )nil sets_lemmas nil )nil sets_lemmas nil )nil ast_def nil )"nat" ast_def nil )"int" integers nil )nil extended_nnreal "extended_nnreal/" )"[[nat, nat] -> (A)]" ast_def nil )"[nat -> T]" double_index"extended_nnreal/" )"bool" nil )"bool" indexed_sets_aux "sets_aux/" )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_int" nil )"nonneg_rat" nil )"nonneg_rat" nil )"boolean" notequal nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"(total_order?[real])" nil )"bool" extended_nnreal "extended_nnreal/" )nil code_product"extended_nnreal/" )"nat" code_product "extended_nnreal/" )"nat" code_product "extended_nnreal/" )"set[T]" nat_indexed_sets "sets_aux/" )nil code_product"extended_nnreal/" )"nat" code_product "extended_nnreal/" )nil extended_nnreal "extended_nnreal/" )"T3" function_props nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )nil sets_lemmas nil )"(p)" sets nil )"set" sets nil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )nil ast_def nil )"sequence[set[T]]" ast_def nil )"bool" subset_algebra_def nil )nil sets nil )nil nat_indexed_sets "sets_aux/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil sequences nil ))nil 3458063268"" (skosimp)"" "A_difference_union" ("a" "Y!1" "b" "IUnion(n!1, I!1)" ))"" (assert )"" (split)"1" (expand "finite_disjoint_union?" )"1" (skosimp)"1" "union_diff_subset" "a" "IUnion(n!1, I!1)" "b" "Y!1" ))"1" (assert )"1" (replace -3)"1" "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" "1" "XX" )"1" "IUnion(XX)=Y!1" )"1" assert )"1" "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" "x_sum_eq" "S" "LAMBDA (i_1: nat): LAMBDA (i: nat):IF i < n!1 THEN mu!1(I!1(i))LAMBDA (i: nat):IF i < n!1 THEN (TRUE, 0)" "T" "mu!1 o XX" ))"1" "1" "DRL1" "x_sum(LAMBDA (i_1: nat): LAMBDA (i: nat):IF i < n!1 THEN mu!1(I!1(i))LAMBDA (i: nat):IF i < n!1 THEN (TRUE, 0)") "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))") "1" "LHS" "x_sum(mu!1 o I!1)" )"1" "DRL2" "x_sum(LAMBDA (i: nat): IF i < n!1 THEN mu!1(I!1(i)) ELSE (TRUE, 0) ENDIF)") "1" "1" expand "x_eq" )"1" expand "x_le" )"1" expand "x_add" )"1" "1" assert )"1" assert )"1" "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" "2" "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" "2" "2" expand "o " )"2" "i!1 < n!1" )"1" expand "x_eq" )"1" nil nil ))nil )"2" assert )"2" "i!1" )"2" assert )"2" expand "measure_empty?" )"2" "I!1(i!1)=emptyset" )"1" replace "1" expand "x_eq" )"1" nil nil ))nil ))nil )"2" "2" expand "emptyset" )"2" expand "empty?" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1 < n!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"3" "3" "i!1 < n!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "o" 1)"2" expand "XX" )"2" "i!1 < n!1" )"1" "1" expand "x_add" )"1" expand "x_eq" )"1" "mu!1(I!1(i!1))`1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "x_add" )"2" expand "x_eq" )"2" "i!1 - n!1" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" replace -1)"3" "i!1-n!1" )"1" "1" replace 2)"1" assert )"1" "E!1(i!1 - n!1)=emptyset" )"1" rewrite "A_empty" )nil nil )"2" "2" expand "emptyset" )"2" expand "empty?" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" "5" "5" assert )"5" "5" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1-n!1" )"1" "1" assert )"1" "E!1(i!1 - n!1)=emptyset" )"1" rewrite "A_empty" )nil nil )"2" "2" expand "emptyset" )"2" expand "empty?" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace -5 1 rl)"2" expand "XX" )"2" "2" expand "union" )"2" expand "member" )"2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "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" "1" case "i!1<n!1" )"1" assert )"1" "I!1(i!1)" )"1" "i!1" )nil nil ))nil ))nil )"2" assert )"2" "i!1-n!1" )nil nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "1" "1" "a!1" )"1" "j!1" )"1" "j!1" )"1" expand "<=" "1" "1" "j!1" )"1" assert )nil nil ))nil )"2" "j!1" )"2" assert )"2" expand "empty?" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "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" "difference_disjoint" "b" "Y!1" "a" "IUnion(n!1, I!1)" ))"2" replace -4)"2" "2" "i!1 < n!1" )"1" "j!1 < n!1" )"1" "i!1" "j!1" )"1" (assert ) nil nil ))nil )"2" assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" "x!1" )"2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "1" "I!1(i!1)" )"1" "i!1" )nil nil ))nil )"2" "j!1 - n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "j!1 < n!1" )"1" assert )"1" expand "disjoint?" "1" expand "intersection" "1" expand "empty?" "1" expand "member" )"1" "1" "x!1" )"1" expand "IUnion" "1" expand "image" )"1" expand "Union" )"1" "1" "I!1(j!1)" )"1" "j!1" )nil nil ))nil )"2" "i!1-n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "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" "i!1<n!1" )"1" (assert ) nil nil )"2" assert )"2" "i!1-n!1" )"2" "2" "i!1 - n!1 < n!2" )"2" assert )"2" "E!1(i!1 - n!1)=emptyset" )"1" rewrite "A_empty" )nil nil )"2" "2" expand "emptyset" )"2" expand "empty?" )"2" "x!1" )"2" expand "member" )"2" 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" "EXISTS (i: nat): I!1(i)(x!1)" )"1" (skosimp)"1" (inst - "i!1" )"1" (expand "image" )"1" expand "Union" )"1" "i!1 >= n!1" )"1" expand "empty?" )"1" "x!1" )"1" (assert ) nil nil ))nil ))nil )"2" "I!1(i!1)" )"2" "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" "2" "a!1" )"2" "i!1" )"2" "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 )"set[T]" nat_indexed_sets "sets_aux/" )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"(nonempty?[set[T]])" ast_def nil )"bool" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil ast_def nil )nil ast_def nil )"bool" sets nil )"int" integers nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil sets_lemmas nil )"nat" ast_def nil )"bool" sets nil )"nat" ast_def nil )"set" sets nil )"bool" indexed_sets_aux "sets_aux/" )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"bool" nil )"[nat -> set[T]]" ast_def nil )nil nil )"set[R]" function_image nil )"bool" reals nil )"sequence[(A)]" ast_def nil )"nat" ast_def nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"set" sets nil ) (union const-decl "set" sets nil )"nat" ast_def nil )nil extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"T3" function_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )"bool" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"set" sets nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" extended_nnreal "extended_nnreal/" )"nnreal" nil )"(total_order?[real])" nil )"bool" extended_nnreal "extended_nnreal/" )"odd_int" integers nil )nil ast_def nil )"nat" ast_def nil )"nat" ast_def nil )"bool" booleans nil )nil extended_nnreal "extended_nnreal/" )"set[T]" indexed_sets nil )"bool" nil )nil defined_types nil )nil sets_lemmas nil )"bool" subset_algebra_def nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"nat" ast_def nil )"(partial_order?[set[T]])" nil ))nil 3458455064"" (skosimp)"" "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)),") "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" "FORALL i: IF i = 0 THEN mu!1(a!1)`1 ELSE TRUE ENDIF" )"1" "convergence_sequences.convergent?(series(LAMBDA i: IF i = 0 THEN mu!1(a!1)`2 ELSE 0 ENDIF))") "1" "1" "0" )"1" assert )"1" replace -1)"1" "zero_tail_series_limit" "n" "0" "a" "LAMBDA i: IF i = 0 THEN mu!1(a!1)`2 ELSE 0 ENDIF" ))"1" "1" replace -1)"1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "zero_tail_series_conv" "n" "0" "a" "LAMBDA i: IF i = 0 THEN mu!1(a!1)`2 ELSE 0 ENDIF" ))"2" assert )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" "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" "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 )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )nil defined_types nil )"set" sets nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sequences nil )"(nonempty?[set[T]])" ast_def nil )"bool" sets nil )set type-eq-decl nil sets nil )nil ast_def nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ast_def nil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"set[T]" nat_indexed_sets "sets_aux/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil nat_indexed_sets "sets_aux/" )"even_int" integersnil )"odd_int" integers nil )"set" sets nil )nil nat_indexed_sets "sets_aux/" )"(total_order?[real])" nil )"bool" indexed_sets_aux "sets_aux/" )"bool" sets nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"boolean" notequal nil )"bool" extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"T3" function_props nil )"bool" extended_nnreal "extended_nnreal/" )"(total_order?[real])" nil )"(partial_order?[set[T]])" nil )"bool" booleans nil )nil series_lems "series/" )nil series_lems "series/" )"(strict_total_order?[real])" real_props nil )"real" sigma "reals/" )nil sigma_nat "reals/" )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )"bool" convergence_sequences "analysis/" )"sequence[real]" series "series/" )"bool" generalized_measure_def nil )nil ast_def nil ))nil 3453349304"" (skosimp)"" (typepred "mu!1" )"" (expand "outer_measure?" )"" "F" "LAMBDA X: AND ") "" (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)))" )"1" (expand "x_le" )"1" (flatten)"1" (name-replace "LHS" "F(IUnion(X!1))" )"1" "RHS" "x_sum(F o X!1)" )"1" assert )"1" expand "x_add" )"1" expand "x_lt" )"1" "1" )"1" "1" assert )"1" "1" "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)), LAMBDA (n: nat):") "1" case "x_eq(x_sum(lambda (n:nat): x_add((TRUE,epsilon!1/expt(2,n+1)),F(X!1(n)))),x_add((TRUE, epsilon!1), x_sum(F o X!1)))" )"1" expand "x_eq" )"1" expand "x_lt" )"1" "1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_add" )"2" expand "x_sum" )"2" expand "x_eq" )"2" expand "o " )"2" "2" "FORALL (i:nat): F(X!1(i))`1" )"1" case "convergence(series(lambda (i:nat): epsilon!1 / expt(2, 1 + i)),epsilon!1)" )"1" "convergence_sequences.convergent?(series(LAMBDA (i:nat): F(X!1(i))`2))" )"1" "convergence_sequences.limit_lemma" "v" "series(LAMBDA (i: nat): F(X!1(i))`2)" ))"1" "1" "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" "series(LAMBDA (i:nat): IF F(X!1(i))`1LAMBDA (i: nat): F(X!1(i))`2) +LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i))") "1" "1" "S1" "series(LAMBDA (i: nat): F(X!1(i))`2)" )"1" "S2" "series(LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i))" )"1" "convergence_sequences.convergent?(S1 + S2)" )"1" rewrite "convergence_sequences.limit_def" "1" assert )"1" replace "1" expand "limit" )"1" expand "+ " )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "+ " )"2" nil nil ))nil ))nil )"2" "2" expand "convergence_sequences.convergent?" )"2" "convergence_sequences.limit(S1) + epsilon!1" )"2" expand "+ " )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" "2" expand "+" )"2" rewrite "sigma_sum" )"2" "(LAMBDA (i: nat): IF F(X!1(i))`1 THEN epsilon!1 / expt(2, 1 + i) + F(X!1(i))`2LAMBDA (i_1: nat):") "2" "2" "2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" replace 1)"2" assert )"2" "convergence_sequences.convergent?(series(LAMBDA (i:nat): IF F(X!1(i))`1") "1" "convergent_diff" "s1" "series(LAMBDA (i: nat): IF F(X!1(i))`1" "s2" "series(LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i))" ))"1" assert )"1" "1" expand "-" "1" expand "series" "1" "(LAMBDA (x: nat): LAMBDA (i: nat):IF F(X!1(i))`1LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i)))=(LAMBDA (n: nat): sigma(0, n, LAMBDA (i: nat): F(X!1(i))`2))") "1" "1" "1" rewrite "sigma_minus" )"1" "(LAMBDA (i_1: nat): IF F(X!1(i_1))`1LAMBDA (i: nat): F(X!1(i))`2") "1" "1" "x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergence_sequences.convergent?" )"2" "epsilon!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "geometric_series" "x" "1/2" ))"2" "1" expand "geometric" )"1" expand "^" )"1" "1 / (1 - 1 / 2)=2" )"1" "1" "series_scal" "a" "LAMBDA (n:nat): expt(1 / 2, n)" "c" "epsilon!1/2" ))"1" "(LAMBDA (n_1: nat): LAMBDA (n: nat): expt(1 / 2, n))(n_1))=(LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i))") "1" "1" "S1" "series((LAMBDA (i: nat): epsilon!1 / expt(2, 1 + i)))" )"1" "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" "2" "2" expand "expt" "2" rewrite "expt_of_inv" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (x:(A)): x_le(F(x),mu!1(x))" )"1" case "FORALL (n: nat): ") "1" "II" "lambda (n:nat): choose({I | ") "1" "1" "x_sum_lt" "S" "lambda (n:nat): x_sum(mu!1 o II(n))" "T" "LAMBDA (n: nat): ")) "1" "1" case "x_le(F(IUnion(X!1)),x_sum(LAMBDA (n: nat): x_sum(mu!1 o II(n))))" )"1" "LHS" "F(IUnion(X!1))" )"1" "RHS" "x_sum(LAMBDA (n: nat): ") "1" "DRL" "x_sum(LAMBDA (n: nat): x_sum(mu!1 o II(n)))" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "double_x_sum" "U" "lambda (i,j:nat): mu!1(II(i)(j))" ))"2" assert )"2" expand "o" 1)"2" "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" "DRL" "x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j))))" )"1" "LHS" "F(IUnion(X!1))" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" expand "x_le" "2" expand "F" "2" expand "x_inf" )"2" "2" replace "2" "2" assert )"2" "1" "x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j))))" )"1" expand "o" )"1" expand "single_index" )"1" "lambda (n:nat): II(double_index_i(n))(double_index_j(n))" )"1" "1" "SUM" "x_sum(LAMBDA (x: nat): ") "1" "1" nil nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "member" )"2" expand "IUnion" )"2" "2" "2" "II(i!1)" )"2" "2" expand "subset?" )"2" "x!1" )"2" expand "member" )"2" assert )"2" expand "IUnion" )"2" "2" "double_index_n(i!1,i!2)" )"2" "double_index_ij_n" "i" "i!1" "j" "i!2" ))"2" "2" replace "2" replace "2" 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" "2" "glb({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" "GLB" "glb({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j))))`2" )"1" "x_sum(single_index(LAMBDA (i, j: nat): mu!1(II(i)(j))))" )"1" replace "1" "1" expand "single_index" )"1" "LAMBDA (n:nat): II(double_index_i(n))(double_index_j(n))" )"1" "1" expand "o" )"1" "SUM" "x_sum(LAMBDA (x: nat): ") "1" "1" nil nil ))nil ))nil ))nil )"2" expand "subset?" )"2" "2" expand "member" )"2" expand "IUnion" )"2" "2" "2" "II(i!1)" )"2" "2" expand "subset?" )"2" "x!2" )"2" expand "member" )"2" assert )"2" expand "IUnion" )"2" "2" "double_index_n(i!1,i!2)" )"2" "double_index_ij_n" "i" "i!1" "j" "i!2" ))"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 ))nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" "1" expand "nonempty?" )"1" expand "empty?" )"1" "x!1`2" )"1" expand "member" )"1" "x!1" )"1" replace "1" "I!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" expand "lower_bound?" )"2" "2" "s!1" )"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 ))nil ))nil ))nil )"2" "2" "2" "II(i!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "FX" "F(X!1(n!1))" )"2" replace -1)"2" expand "F" -1)"2" expand "x_inf" "2" "2" assert )"2" "FORALL (x: AND subset?[T](X!1(n!1), IUnion[nat, T](I))})):NOT x`1") "1" replace "1" expand "x_add" )"1" expand "x_lt" )"1" "lambda (n:nat): fullset[T]" )"1" "1" nil nil ))nil )"2" rewrite "A_fullset" )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "x!1" )"2" "2" replace "2" "2" expand "x_add" )"2" expand "x_lt" )"2" "glb({z_1: real | AND subset?[T](X!1(n!1), IUnion[nat, T](I)))AND x`1 AND x`2 = z_1})") "1" "GLB" "glb({z_1: real | 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" "1" "posreal_div_posreal_is_posreal" "px" "epsilon!1" "py" "expt(2, 1 + n!1)" ))"1" "R" "epsilon!1 / expt(2, 1 + n!1)" )"1" "GLB+R" )"1" assert )"1" expand "lower_bound?" )"1" "1" case "s!1<GLB+R" )"1" "1" "s!1" )"1" "1" "1" "I!2" )"1" replace "1" expand "x_eq" "1" "1" replace "1" replace "1" replace "1" replace "1" 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" "1" expand "nonempty?" )"1" expand "empty?" )"1" "x!1`2" )"1" expand "member" )"1" "x!1" )"1" replace "1" "I!1" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" expand "lower_bound?" )"2" "2" assert )"2" "s!1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "F" 1)"2" expand "x_le" )"2" "2" replace -1)"2" expand "x_inf" )"2" "2" assert )"2" "1" "mu!1(x!1)" )"1" "lambda (n:nat): if n=0 then x!1 else emptyset[T] endif" )"1" "1" expand "o" )"1" expand "measure?" )"1" "1" expand "measure_empty?" )"1" replace "1" expand "x_eq" )"1" expand "x_sum" )"1" replace "1" assert )"1" "1" assert )"1" "zero_tail_series_conv" "n" "0" "a" "LAMBDA (i:nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF")) "1" "zero_tail_series_limit" "n" "0" "a" "LAMBDA (i:nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF")) "1" "FORALL (m:nat): LAMBDA (i: nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF)(m) = 0") "1" replace "1" replace "1" expand "series" )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "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" "2" expand "IUnion" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "A_empty" )nil nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" "2" "glb({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" "LHS" "glb({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "mu!1(x!1)`2" )"1" "1" "mu!1(x!1)" )"1" replace "1" "lambda (n:nat): if n=0 then x!1 else emptyset[T] endif" )"1" "1" expand "o" )"1" expand "measure?" )"1" "1" expand "measure_empty?" )"1" replace "1" expand "x_eq" "1" expand "x_sum" "1" replace "1" assert )"1" "1" assert )"1" "zero_tail_series_conv" "a" "LAMBDA (i:nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF" "n" "0" ))"1" "zero_tail_series_limit" "a" "LAMBDA (i:nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF" "n" "0" ))"1" "FORALL (m:nat): LAMBDA (i: nat): IF i = 0 THEN mu!1(x!1)`2 ELSE 0 ENDIF)(m) = 0") "1" replace "1" replace "1" expand "series" )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "member" )"2" "2" expand "IUnion" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "A_empty" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "x!2`2" )"1" "x!2" )"1" replace "1" "I!1" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" expand "lower_bound?" )"2" "2" "s!1" )"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 ))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" "2" expand "F" )"2" expand "o" )"2" expand "x_inf" )"2" "FORALL (x_1: LAMBDA (x: nat): mu!1(I(x))), z) AND NOT x_1`1") "2" replace 1)"2" "2" "FORALL (x_1: LAMBDA (x: nat): mu!1(I(x))), z) AND NOT x_1`1") "1" "x!1" )"1" "x!1" )"1" "1" "I!1" )"1" assert )"1" "1" expand "subset?" )"1" "1" "x!2" )"1" "x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "2" "2" "x!1" )"2" "2" "x!2" )"2" "2" "glb({z_1: real | LAMBDA (x: nat): mu!1(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "RHS" "glb({z_1: real | LAMBDA (x: nat): mu!1(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "glb({z_1: real | LAMBDA (x: nat): mu!1(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "LHS" "glb({z_1: real | LAMBDA (x: nat): mu!1(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" expand "greatest_lower_bound?" )"1" "1" "1" expand "lower_bound?" )"1" "LHS" )"1" "1" nil nil )"2" "2" "2" "s!1" )"2" "2" "2" "s!1" )"2" "x!3" )"2" replace "2" replace "2" "I!3" )"2" assert )"2" "2" expand "subset?" )"2" "2" "x!4" )"2" "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" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" "x!2`2" )"1"
Messung V0.5 in Prozent C=100 H=99 G=99
¤ 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.938Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
