(real_lebesgue_scafnil 3396062613"" (skosimp*)"" (expand "convergent" )"" (expand "convergent?" )"" (expand "convergence" )"" (split)"1" (skosimp*)"1" (inst + "l!1" )"1" (rewrite "metric_convergence_def" *)"1" (expand "metric_converges_to" )"1" (skosimp)"1" (inst - "r!1" )"1" (skosimp)"1" (inst + "n!1" )"1" (skosimp)"1" "i!1" )"1" expand "ball" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "l!1" )"2" (skosimp)"2" (rewrite "metric_convergence_def" *)"2" (expand "metric_converges_to" )"2" (inst - "epsilon!1" )"2" (skosimp)"2" (inst + "n!1" )"2" (skosimp)"2" "i!1" )"2" expand "ball" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" topological_convergence "topology/" )"bool" convergence_sequences "analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" metric_space_def"metric_space/" )nil real_types nil )"bool" reals nil )"real" reals nil )"bool" sets nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"set[T]" metric_space_def "metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil sequences nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil metric_space"metric_space/" )"bool" convergence_sequences "analysis/" )"real" reals nil ))nil ))nil 3397030001"" (skosimp)"" (skolem + ("n!1" ))"" (typepred "I!1(n!1)" )"" (expand "bounded_open_interval?" )"" (expand "bounded_interval?" ) (("" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" real_topology "metric_space/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )set type-eq-decl nil sets nil )"bool" real_topology"metric_space/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil real_topology"metric_space/" )nil sequences nil ))nil ))nil 3407841244"" "L" "(LAMBDA A: AND subset?[real](A, IUnion[nat, real](I))}))") "1" (expand "outer_measure?" )"1" (case-replace "om_empty?(L)" )"1" (case-replace "om_increasing?(L)" )"1" (expand "om_countably_subadditive?" )"1" (skosimp)"1" (expand "x_le" )"1" (flatten)"1" (assert )"1" (case "forall (n:nat): L(X!1(n))`1" )"1" case "forall (n:nat,r:posreal): exists I: subset?[real](X!1(n),IUnion[nat,real](I)) & x_lt(x_sum(LAMBDA (n: nat):x_length(I(n))),x_add((TRUE,r/2^n),L(X!1(n))))" )"1" case "forall (r:posreal): EXISTS I: ") "1" (hide -2)"1" (inst-cp - "1" )"1" "1" expand "x_add" -3)"1" expand "x_lt" -3)"1" "1" assert )"1" case "x_sum(L o X!1)`2<L(IUnion(X!1))`2" )"1" "1" "L(IUnion(X!1))`2-x_sum(L o X!1)`2" )"1" "1" expand "x_add" )"1" expand "x_lt" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" case "EXISTS I: LAMBDA n: x_add((TRUE, (r!1/2) / 2 ^ n), L(X!1(n)))))") "1" "1" "I!1" )"1" "1" assert )"1" case "x_eq(x_sum(LAMBDA n: x_add((TRUE, (r!1 / 2) / 2 ^ n), L(X!1(n)))),x_add((TRUE, r!1), x_sum(L o X!1)))" )"1" "LHS" "L(IUnion(X!1))" )"1" "MID" "x_sum(LAMBDA n: x_add((TRUE, (r!1 / 2) / 2 ^ n), L(X!1(n))))" )"1" "RHS" "x_add((TRUE, r!1), x_sum(L o X!1))" )"1" "1" expand "x_lt" )"1" expand "x_eq" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_add" )"2" expand "x_eq" )"2" expand "o " )"2" "x_sum(LAMBDA n: IF L(X!1(n))`1 THEN (TRUE, (r!1 / 2) / 2 ^ n + L(X!1(n))`2)") "1" expand "x_sum" )"1" "1" replace -3)"1" replace "1" replace "1" replace "1" "const_geometric_series" "x" "1/2" "c" "r!1/2" ))"1" "r!1 / 2 / (1 - 1 / 2)=r!1" )"1" expand "abs" "1" "1" expand "convergent?" )"1" "1" "convergence_sequences.limit_def" "v" "series(LAMBDA (i:nat): IF L(X!1(i))`1 THEN (r!1 / 2) / 2 ^ i + L(X!1(i))`2" "l" "l!2" ))"1" assert )"1" replace "1" "1" "convergence_sequences.limit_def" "v" "series(LAMBDA (i:nat): " "l" "l!1" ))"1" assert )"1" replace "1" "1" "cnv_seq_sum" "s1" "series(LAMBDA (i:nat): L(X!1(i))`2)" "l1" "l!1" "s2" "series(r!1 / 2 * geometric(1 / 2))" "l2" "r!1" ))"1" assert )"1" rewrite "series_sum" )"1" expand "+" "1" "(LAMBDA (i:nat): IF L(X!1(i))`1LAMBDA (x: nat):") "1" "1" "convergence_sequences.unique_limit" "u" "series(LAMBDA (x: nat): " "l1" "l!2" "l2" "l!1+r!1" ))"1" assert )nil nil ))nil ))nil )"2" "2" "x!1" )"2" assert )"2" expand "geometric" )"2" expand "*" )"2" rewrite "inv_expt" )"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 )"2" "2" expand "x_sum" )"2" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil )"2" "geometric_conv" "x" "1/2" ))"2" expand "abs" )"2" "series_scal" "c" "r!1/2" "a" "geometric(1 / 2)" ))"2" "convergent_scal" "s1" "series(geometric(1 / 2))" "a" "r!1/2" ))"2" assert )"2" replace "2" "2" "convergent_sum" "s1" "series(LAMBDA n: r!1 / 2 * geometric(1 / 2)(n))" "s2" "series(LAMBDA n: L(X!1(n))`2)" ))"2" assert )"2" "2" rewrite "series_sum" )"2" expand "+" "2" "(LAMBDA (x: nat): LAMBDA n:IF L(X!1(n))`1") "2" "2" "x!1" )"2" assert )"2" expand "geometric" )"2" rewrite "inv_expt" "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" "2" "posreal_div_posreal_is_posreal" "px" "r!1" "py" "2" ))"2" "_" "r!1/2" )"2" "R" "r!1/2" )"2" "I_n" "lambda n: choose({I | subset?[real](X!1(n), IUnion[nat, real](I)) & LAMBDA (n: nat): x_length(I(n))),") "1" case "forall n: subset?[real](X!1(n), IUnion[nat, real](I_n(n))) & LAMBDA (m: nat): x_length(I_n(n)(m))),") "1" "double_index_n_ij" )"1" "double_index_ij_n" )"1" "NN" "double_index_n" )"1" "II" "double_index_i" )"1" "JJ" "double_index_j" )"1" "lambda (n:nat): I_n(II(n))(JJ(n))" )"1" "subset?[real] LAMBDA (n: nat): I_n(II(n))(JJ(n))))") "1" "1" case "x_lt(x_sum(LAMBDA n:x_sum(LAMBDA (m: nat): x_length(I_n(n)(m)))),x_sum(LAMBDA n: x_add((TRUE, R/2^n), L(X!1(n)))))" )"1" case "x_le(L(IUnion(X!1)),x_sum(LAMBDA n: x_sum(LAMBDA (m: nat): x_length(I_n(n)(m)))))" )"1" "LHS" "L(IUnion(X!1))" )"1" "RHS" "x_sum(LAMBDA n: x_add((TRUE, R / 2 ^ n), L(X!1(n))))" )"1" "MID" "x_sum(LAMBDA n: x_sum(LAMBDA (m: nat): x_length(I_n(n)(m))))" )"1" "1" expand "x_le" )"1" expand "x_lt" )"1" "1" assert )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "double_x_sum" "U" "lambda (i,j:nat): x_length(I_n(i)(j))" ))"2" case "x_le(L(IUnion(X!1)),x_sum(single_index(LAMBDA (i, j: nat): x_length(I_n(i)(j)))))" )"1" assert )"1" "LHS" "L(IUnion(X!1))" )"1" "RHS" "x_sum(LAMBDA n: x_sum(LAMBDA (m: nat): x_length(I_n(n)(m))))" )"1" "MID" "x_sum(single_index(LAMBDA (i, j: nat): x_length(I_n(i)(j))))" )"1" "1" expand "x_eq" )"1" expand "x_le" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall A,I: subset?(A,IUnion(I)) => x_le(L(A),x_sum(x_length o I))" )"1" expand "single_index" )"1" "IUnion(X!1)" "lambda n: I_n(II(n))(JJ(n))" )"1" replace "1" expand "o" "1" expand "JJ" )"1" expand "II" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "x_le" )"2" expand "o " )"2" expand "L" )"2" expand "o " )"2" "x_sum(LAMBDA (x: nat): x_length(I!1(x)))`1" )"1" "x_inf({z | LAMBDA (x: nat): x_length(I(x))), z) AND ") "1" expand "x_inf" )"1" "FORALL (x_1: LAMBDA (x: nat): x_length(I(x))), z)AND subset?[real](A!1, IUnion[nat, real](I))})):NOT x_1`1") "1" replace "1" "1" "1" "x!1" )"1" "1" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "GLB" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "1" "x_sum(LAMBDA (x: nat): x_length(I!1(x)))`2" )"1" "1" "x_sum(LAMBDA (x: nat): x_length(I!1(x)))" )"1" replace "1" "I!1" )"1" assert )"1" expand "x_le" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "I!1(x!2)" )"2" expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "I!1(x!2)" )"2" expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" 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!1`2" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" expand "lower_bound?" )"2" "2" "s!1" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "I!3(x!2)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_inf" )"2" "2" "x_sum(LAMBDA (x: nat): x_length(I!1(x)))" )"1" "I!1" )"1" assert )"1" expand "x_le" )"1" nil nil ))nil ))nil ))nil )"2" "2" "I!1(x!1)" )"2" expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "I!2(x!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" nil nil ))nil )"3" "3" "I!1(x!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "I!1(x1!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_sum" "2" expand "x_sum" "2" expand "x_lt" "2" "FORALL (i:nat): x_add((TRUE, R / 2 ^ i), L(X!1(i)))`1" )"1" "FORALL (i:nat): x_sum(LAMBDA (m: nat): x_length(I_n(i)(m)))`1" )"1" "1" replace "1" "convergence_sequences.convergent?(series(LAMBDA (i:nat): ") "1" "convergence_sequences.convergent?(series(LAMBDA (i:nat): LAMBDA ") "1" case "forall (nna,nnb:sequence[nnreal]): convergence_sequences.convergent?(series(nna))&convergence_sequences.convergent?(series(nnb))&(forall n: nna(n)<nnb(n)) => convergence_sequences.limit(series(nna))<convergence_sequences.limit(series(nnb))" )"1" "LAMBDA (i:nat): x_sum(LAMBDA (m: nat): x_length(I_n(i)(m)))`2" "LAMBDA (i:nat): x_add((TRUE, R / 2 ^ i), L(X!1(i)))`2" )"1" replace "1" replace "1" "1" nil nil )"2" "2" "2" "n!1" )"2" "n!1" )"2" "n!1" )"2" "2" expand "x_lt" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "I_n(i!1)(m!1)" )"2" expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "series_first" "2" rewrite "series_first" "2" case "forall (nna:sequence[nnreal]):series(nna, 1)=series(lambda n: if n=0 then 0 else nna(n) endif)" )"1" "nna!1" )"1" "nnb!1" )"1" replace "1" replace "1" "convergent_diff" "s1" "series(LAMBDA n: IF n = 0 THEN 0 ELSE nnb!1(n) ENDIF)" "s2" "series(LAMBDA n: IF n = 0 THEN 0 ELSE nna!1(n) ENDIF)" ))"1" "convergence_sequences.convergent?(series(LAMBDA n: IF n = 0 THEN 0 ELSE nnb!1(n) ENDIF))" )"1" "convergence_sequences.convergent?(series(LAMBDA n: IF n = 0 THEN 0 ELSE nna!1(n) ENDIF))" )"1" rewrite "series_diff" )"1" "limit_nonneg" "nna" "series((LAMBDA n: IF n = 0 THEN 0 ELSE nnb!1(n) ENDIF) - LAMBDA n: IF n = 0 THEN 0 ELSE nna!1(n) ENDIF))")) "1" replace "1" rewrite "series_diff" "1" rewrite "limit_diff" "1" "0" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" ))"2" expand "series" )"2" "sigma_ge_0" "low" "0" "high" "n!1" "F" "LAMBDA (x: nat): IF x = 0 THEN 0 ELSE nnb!1(x) ENDIF -IF x = 0 THEN 0 ELSE nna!1(x) ENDIF")) "2" "1" expand "-" )"1" nil nil ))nil )"2" "2" "2" "n!2" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "end_series_conv" "a" "nna!1" "m" "1" ))"2" assert )nil nil ))nil ))nil ))nil )"2" "end_series_conv" "a" "nnb!1" "m" "1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "series" )"2" "2" "sigma_first" "high" "x!1" "low" "0" "F" "LAMBDA n: IF n = 0 THEN 0 ELSE nna!2(n) ENDIF" ))"2" assert )"2" "sigma_eq" "low" "1" "high" "x!1" "F" "nna!2" "G" "LAMBDA n: IF n = 0 THEN 0 ELSE nna!2(n) ENDIF" ))"2" "1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comparison_test" "b" "LAMBDA (i: nat): " "a" "LAMBDA (i: nat): LAMBDA (m: nat): x_length(I_n(i)(m)))`2")) "2" replace "2" "1" nil nil )"2" "2" "2" expand "abs" "2" assert )"2" "2" assert )"2" "n!1" )"2" "n!1" )"2" "n!1" )"2" "2" expand "x_lt" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" )"2" "2" "i!1" )"2" expand "x_lt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "x_add" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "I_n(n!1)(m!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" "2" "2" expand "member" )"2" expand "IUnion" "2" "n!1" ))"2" "n!1" )"2" "2" expand "subset?" "2" "x!1" )"2" expand "member" )"2" assert )"2" expand "IUnion" "2" "2" "NN(n!1,i!1)" )"2" "n!1" "i!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 )"2" "2" "2" "n!1" )"2" "2" "2" expand "I_n" )"2" "choose_member" "a" "{I LAMBDA (n: nat): x_length(I(n))),")) "1" "1" "II" "choose({I | LAMBDA (n: nat): x_length(I(n))),") "1" expand "member" )"1" nil nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "I!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "empty?" )"2" expand "member" )"2" "I!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "I!2(n!2)" )"2" expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "I_n(n!1)(m!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!1" )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "I!1" )"2" assert )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 "x_lt" )"2" expand "x_add" )"2" "n!1" )"2" replace -1)"2" expand "L" (-1 1))"2" expand "x_inf" )"2" "2" replace 1 2)"2" "2" expand "o " )"2" case "nonempty?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x) AND AND x`1 AND x`2 = z_1})") "1" case "bounded_below?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x) AND AND x`1 AND x`2 = z_1})") "1" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))),AND AND x`1 AND x`2 = z_1})") "1" "LIMIT" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))),AND AND x`1 AND x`2 = z_1})") "1" "1" expand "greatest_lower_bound?" )"1" "1" "posreal_div_posreal_is_posreal" "px" "r!1" "py" "2^n!1" ))"1" "r!1 / 2 ^ n!1 + LIMIT" )"1" expand "lower_bound?" )"1" assert )"1" "1" case "s!1<r!1 / 2 ^ n!1 + LIMIT" )"1" "1" "s!1" )"1" "1" "1" "I!1" )"1" assert )"1" expand "x_le" )"1" "1" assert )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" assert )nil nil ))nil )"2" "2" expand "bounded_below?" )"2" "0" )"2" expand "lower_bound?" )"2" "2" "s!1" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "x!1`2" )"2" "x!1" )"2" assert )"2" "x!1" )"2" "2" expand "o" )"2" "I!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "I!1(x1!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (skosimp)"3" (typepred "I!1(n1!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "o " )"2" (expand "x_sum" ) (("2" (prop) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "om_increasing?" )"2" (skosimp)"2" (expand "x_le" )"2" (case-replace "L(a!1)`1" )"1" (expand "L" )"1" (expand "o" )"1" (expand "x_inf" )"1" "FORALL (x_1: LAMBDA (x: nat): x_length(I(x))), z)AND subset?[real](a!1, IUnion[nat, real](I))})):NOT x_1`1") "1" (replace 1)"1" "AAX" ))"1" "1" replace 1)"1" "BBX" ))"1" "1" case "nonempty?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" case "bounded_below?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "GLBA" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "1" case "nonempty?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" case "bounded_below?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "GLBB" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "1" expand "greatest_lower_bound?" )"1" expand "lower_bound?" )"1" "1" "GLBA" )"1" assert )"1" "1" case "GLBB<GLBA" )"1" "1" "s!1" )"1" "1" "1" "s!1" )"1" "x!1" )"1" assert )"1" "I!1" )"1" assert )"1" "1" expand "subset?" )"1" "1" "x!2" )"1" "x!2" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "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 )"3" nil nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "BBX`2" )"2" "BBX" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "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 )"3" (propax) nil nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "AAX`2" )"2" "AAX" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "I!1(x!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1)"2" (hide -3)"2" (expand "L" )"2" (expand "o" )"2" (expand "x_inf" )"2" "2" "2" "x!1" )"2" "2" "x!1" )"2" "I!1" )"2" assert )"2" "2" expand "subset?" )"2" expand "member" )"2" "2" "x!2" )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "om_empty?" )"2" (expand "L" )"2" (expand "o" )"2" (expand "x_inf" )"2" (lift-if 1)"2" (assert )"2" (prop)"1" (inst - "(TRUE,0)" )"1" (inst + "lambda n: emptyset[real]" )"1" (split)"1" "x_length(emptyset[real]) = (TRUE,0)" )"1" "1" expand "x_le" )"1" expand "x_sum" )"1" rewrite "zero_series_conv" )"1" rewrite "zero_series_limit" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_length" )"2" "length(emptyset[real])=0" )"1" "1" assert )"1" "1" "1" expand "bounded_interval?" )"1" "1" expand "emptyset" )"1" expand "interval?" )"1" nil nil ))nil ))nil )"2" expand "bounded?" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "length_empty_rew" )nil nil )"3" "3" expand "bounded_interval?" )"3" "1" expand "emptyset" )"1" expand "interval?" )"1" (grind) nil nil ))nil ))nil )"2" expand "bounded?" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" expand "subset?" )"2" expand "emptyset" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" "1" (grind) nil nil )"2" expand "bounded?" )"2" "2" "2" (grind) nil nil ))nil ))nil ))nil )"3" "metric_open_def" "S" "emptyset[real]" ))"3" assert )"3" "3" "metric_induced_topology" )"3" expand "open?" )"3" expand "member" )"3" expand "hausdorff_space?" )"3" expand "topology?" )"3" "3" expand "topology_empty?" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" case "nonempty?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" case "bounded_below?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "GLB" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})") "1" "1" expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "0" )"1" "1" "0" )"1" (assert ) nil nil )"2" "2" "(TRUE,0)" )"2" "lambda n: emptyset[real]" )"1" "x_length(emptyset[real])=(TRUE,0)" )"1" "1" "1" expand "x_le" )"1" expand "x_sum" )"1" rewrite "zero_series_conv" )"1" rewrite "zero_series_limit" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" expand "emptyset" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "x_length" )"2" "2" "2" assert )"2" rewrite "length_empty_rew" )"2" "2" expand "bounded_interval?" )"2" "1" nil nil )"2" expand "bounded?" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil )"2" expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" "1" nil nil )"2" expand "bounded?" )"2" "2" "2" nil nil ))nil ))nil ))nil )"3" "metric_induced_topology" )"3" rewrite "metric_open_def" "3" expand "open?" )"3" expand "hausdorff_space?" )"3" expand "topology?" )"3" "3" expand "topology_empty?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "s!1" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" expand "bounded_below?" )"2" "0" )"2" expand "lower_bound?" )"2" "2" "s!1" )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide 2)"2" expand "nonempty?" )"2" expand "empty?" )"2" "x!1`2" )"2" expand "member" )"2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" "I!1(x!2)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (skosimp)"2" (typepred "I!1(x1!1)" )"2" (expand "bounded_open_interval?" )"2" (expand "bounded_interval?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" outer_measure_def"measure_integration/" )"set" sets nil )"hausdorff[real]" "metric_space/" )"(hausdorff?)" "metric_space/" )"second_countable" real_topology "metric_space/" )nil defined_types nil )nil sets nil )"bool" topology_prelim "topology/" )"setofsets[T]" metric_space_def"metric_space/" )"bool" topology_prelim "topology/" )"bool" topology_def "topology/" )"bool" topology_prelim "topology/" )"bool" topology_prelim "topology/" )"bool" topology "topology/" )"[numfield -> numfield]" number_fields nil )nil metric_space "metric_space/" )"nnreal" real_intervals_aux nil )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )nil real_intervals_aux nil )nil series "series/" )nil series "series/" )"finite_set" finite_sets nil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"bool" outer_measure_def"measure_integration/" )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(partial_order?[set[T]])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"bool" sets nil )"(p)" sets nil )nil sets_lemmas nil )nil code_product"extended_nnreal/" )"nat" code_product "extended_nnreal/" )"nat" code_product "extended_nnreal/" )"[nat -> T]" double_index"extended_nnreal/" )"[nat -> nat]" real_lebesgue_scaf nil )"[nat -> nat]" real_lebesgue_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"sequence[bounded_open_interval]" nil )"set[real]" real_lebesgue_scaf nil )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"[set[real] -> extended_nnreal]" nil )nil extended_nnreal "extended_nnreal/" )"(total_order?[real])" nil )nil series "series/" )"sequence[real]" series "series/" )nil series "series/" )nil series "series/" )nil integers nil )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )nil sigma "reals/" )nil convergence_ops "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil series_aux "series/" )nil convergence_ops "analysis/" )"real" sigma "reals/" )"nnreal" sigma_nat "reals/" )nil sigma "reals/" )nil sigma "reals/" )"[nat -> set[real]]" real_lebesgue_scaf nil )"posreal" real_lebesgue_scaf nil )"[n: nat -> LAMBDA (n: nat): x_length(I(n)))," nil )"real" convergence_sequences "analysis/" )nil series "series/" )"nat" code_product "extended_nnreal/" )nil code_product"extended_nnreal/" )nil real_types nil )"bool" extended_nnreal "extended_nnreal/" )nil convergence_ops "analysis/" )nil convergence_ops "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil series "series/" )nil series "series/" )"posrat" nil )nil series "series/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" convergence_sequences "analysis/" )nil convergence_sequences "analysis/" )"sequence[real]" series "series/" )nil convergence_ops "analysis/" )"[T -> real]" real_fun_ops "reals/" )"sequence[real]" series "series/" )nil series "series/" )nil convergence_sequences "analysis/" )nil reals nil )nil exponentiation nil )"posreal" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"nzreal" nil )"rat" rationals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" booleans nil )"[bool, bool -> bool]" booleans nil )"posint" exponentiation nil )"posreal" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" booleans nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"bool" outer_measure_def"measure_integration/" )"({z | LAMBDA (x: nat): x_length(I(x))), z) AND " real_lebesgue_scaf nil )"({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x_1`1 AND x_1`2 = z_1})" real_lebesgue_scaf nil) "set[real]" real_lebesgue_scaf nil )"set[real]" real_lebesgue_scaf nil )"bool" outer_measure_def"measure_integration/" )"set[T]" indexed_sets nil )"bool" sets nil )"extended_nnreal" real_lebesgue_scaf nil )"T3" function_props nil )nil real_topology "metric_space/" )"bool" real_topology "metric_space/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil sequences nil )nil real_topology"metric_space/" )"bool" real_topology"metric_space/" )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"[T, T -> boolean]" equalities nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3408170906"" (skosimp)"" (expand "x_eq" )"" (expand "lebesgue_outer_measure" )"" "ZZ" "{z | AND ") "1" (replace -1)"1" (expand "x_inf" )"1" (hide -1)"1" (case "forall (r:posreal): ZZ(TRUE,r)" )"1" (case-replace "FORALL (x: (ZZ)): NOT x`1" )"1" (inst -2 "1" )"1" (inst - "(TRUE, 1)" ) nil nil )) nil )"2" (replace 1 2)"2" (hide 1)"2" case "nonempty?({x | EXISTS z: ZZ(z) AND z`1 AND z`2 = x})" )"1" case "bounded_below?({x | EXISTS z: ZZ(z) AND z`1 AND z`2 = x})" )"1" "glb({x | EXISTS z: ZZ(z) AND z`1 AND z`2 = x})" )"1" "GLB" "glb({x | EXISTS z: ZZ(z) AND z`1 AND z`2 = x})" )"1" "1" expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" expand "<=" -2 2)"1" "0" )"1" assert )"1" "1" "1" "GLB/2" )"1" "GLB/2" )"1" assert )nil nil )"2" "(TRUE, GLB / 2)" )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" "s!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2)"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 )"3" (propax) nil nil ))nil )"2" (hide 2)"2" (expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "1" )"2" "1" )"2" "(TRUE, 1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "ZZ" )"2" "lambda n: if n=0 then {x | x!1-r!1/2<x&x<x!1+r!1/2} else emptyset[real] endif" )"1" (split)"1" (expand "o" )"1" "x_length(emptyset[real])=(TRUE,0)" )"1" "1" "x_length({x ") "1" "1" expand "x_le" )"1" expand "x_sum" )"1" "FORALL (i:nat): IF i = 0 THEN TRUE ELSE TRUE ENDIF" )"1" "zero_tail_series_conv" "a" "LAMBDA (i:nat): IF i = 0 THEN r!1 ELSE 0 ENDIF" "n" "0" ))"1" "zero_tail_series_limit" "a" "LAMBDA (i:nat): IF i = 0 THEN r!1 ELSE 0 ENDIF" "n" "0" ))"1" "FORALL (m:nat): LAMBDA (i: nat): IF i = 0 THEN r!1 ELSE 0 ENDIF)(m) = 0") "1" replace -3)"1" replace -2)"1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_length" )"2" "2" assert )"2" "1" "1" expand "length" )"1" "1" assert )"1" "1" expand "empty?" )"1" "x!1" )"1" nil nil ))nil ))nil )"2" "sup({x | x!1 - r!1 / 2 < x & x < r!1 / 2 + x!1}) " )"1" "SUP" "sup({x | x!1 - r!1 / 2 < x & x < r!1 / 2 + x!1})" )"1" "SUP=x!1+r!1/2" )"1" "1" "1" "inf({x | x!1 - r!1 / 2 < x & x < r!1 / 2 + x!1})" )"1" "inf({x | x!1 - r!1 / 2 < x & x < r!1 / 2 + x!1})=x!1-r!1/2" )"1" assert )nil nil )"2" "2" "INF" "inf({x | x!1 - r!1 / 2 < x & x < r!1 / 2 + x!1})" )"2" expand "greatest_lower_bound" )"2" expand "lower_bound" )"2" "2" "x!1 - r!1 / 2" )"2" expand "<=" "2" replace "2" "1" "1" case "exists x: x<=x!1 & x<INF & x!1 - r!1 / 2 < x" )"1" "1" "x!2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "EPS" "INF+r!1/2-x!1" )"2" case "EPS>0" )"1" "min(x!1,INF-EPS/2)" )"1" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" assert )"2" expand "below_bounded" )"2" "x!1 - r!1 / 2" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "least_upper_bound" )"2" "2" expand "upper_bound" )"2" "x!1+r!1/2" )"2" expand "<=" "2" replace "2" case "EXISTS x: x > SUP & x < r!1 / 2 + x!1 & x!1 <= x" )"1" "1" "x!2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "2" "EPS" "x!1+r!1/2-SUP" )"2" case "EPS>0" )"1" "max(x!1,SUP+EPS/2)" )"1" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" assert )"2" expand "above_bounded" )"2" "x!1+r!1/2" )"2" expand "upper_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_interval?" )"2" expand "bounded?" )"2" expand "nonempty?" )"2" "1" nil nil )"2" "2" assert )"2" "1" expand "above_bounded" )"1" "x!1+r!1/2" )"1" expand "upper_bound" )"1" nil nil ))nil ))nil ))nil )"2" expand "below_bounded" )"2" "x!1-r!1/2" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil )"2" "2" expand "x_length" )"2" expand "bounded_interval?" )"2" "2" assert )"2" expand "length" )"2" "empty?[real](emptyset[real])" )"1" "1" (grind) nil nil )"2" "2" nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil )"2" (expand "emptyset" )"2" expand "IUnion" )"2" expand "singleton" )"2" expand "subset?" )"2" expand "member" )"2" "2" replace -1)"2" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (expand "bounded_open_interval?" )"2" rewrite "metric_open_def" )"2" rewrite "emptyset_is_open" )"2" expand "bounded_interval?" )"2" "1" expand "interval?" )"1" (grind) nil nil ))nil )"2" expand "bounded?" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (expand "bounded_open_interval?" )"3" "1" expand "bounded_interval?" )"1" "1" (grind) nil nil )"2" expand "bounded?" )"2" "2" expand "nonempty?" )"2" replace 1 2)"2" "1" expand "above_bounded" )"1" "x!1+r!1/2" )"1" expand "upper_bound" )"1" nil nil ))nil ))nil ))nil )"2" expand "below_bounded" )"2" "x!1-r!1/2" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "metric_open_ball" "x" "x!1" "r" "r!1/2" ))"2" expand "ball" )"2" "{y: real | abs(x!1 - y) < r!1 / 2}={x | x!1 - r!1 / 2 < x & x < r!1 / 2 + x!1}" )"2" "2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (skosimp)"2" (typepred "I!1(x1!1)" )"2" (expand "bounded_open_interval?" )"2" (expand "bounded_interval?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" extended_nnreal "extended_nnreal/" )"set[T]" indexed_sets nil )"(singleton?)" sets nil )"bool" sets nil )"bool" sets nil )"extended_nnreal" real_lebesgue_scaf nil )"T3" function_props nil )nil real_topology "metric_space/" )"bool" real_topology "metric_space/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil sequences nil )nil real_topology"metric_space/" )"bool" real_topology"metric_space/" )set type-eq-decl nil sets nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities 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 )nil booleans nil )nil booleans nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" booleans nil )"bool" sets nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"{x_1 | AND z`1 AND z`2 = x})}" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )"bool" sets nil )"[extended_nnreal -> boolean]" nil )NOT const-decl "[bool -> bool]" booleans nil )"posreal" nil )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"outer_negligible[real, lebesgue_outer_measure]" nil )"(induced_sigma_algebra)" nil )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set" finite_sets nil )"real" reals nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" real_lebesgue_scaf nil )"posreal" real_lebesgue_scaf nil )"[numfield, numfield -> numfield]" number_fields nil )"set" sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"nnreal" real_intervals_aux nil )nil defined_types nil )"bool" bound_defs "reals/" )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" bound_defs "reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" real_lebesgue_scaf nil )"real" real_lebesgue_scaf nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" bound_defs "reals/" )"real" real_lebesgue_scaf nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"odd_int" integers nil )"bool" real_topology "metric_space/" )"bool" real_topology "metric_space/" )nil series_aux "series/" )"real" sigma "reals/" )"int" integers nil )"sequence[real]" series "series/" )nil series_aux "series/" )"setofsets[T]" metric_space_def"metric_space/" )nil sets nil )nil topology "topology/" )nil metric_space "metric_space/" )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil metric_space "metric_space/" )"real" reals nil )"set[T]" metric_space_def "metric_space/" )"outer_measure" nil ))nil 3475908490"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" ))nil ))nil 3475908490"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"real" real_lebesgue_scaf nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )nil bounded_reals "reals/" )nil defined_types nil )"bounded_interval" real_lebesgue_scaf nil )"bool" real_topology "metric_space/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" real_topology "metric_space/" )"(total_order?[real])" nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" ))nil ))nil 3475908490"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"bounded_interval" real_lebesgue_scaf nil )"real" real_lebesgue_scaf nil )"bool" real_topology "metric_space/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" real_topology "metric_space/" )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" ))nil ))nil 3408180824"" (skosimp)"" (typepred "lebesgue_outer_measure" )"" (typepred "b!1" )"" (expand "bounded_interval?" )"" (flatten)"" (expand "bounded?" )"" (assert )"" (split -2)"1" (expand "nonempty?" ) (("1" (propax) nil nil ))nil )"2" (flatten)"2" "x_le_antisymmetric" "x" "lebesgue_outer_measure({x | inf(b!1) <= x AND x <= sup(b!1)})" "y" "lebesgue_outer_measure({x | inf(b!1) < x AND x < sup(b!1)})" ))"1" (assert )"1" (hide 2)"1" (split)"1" "pairwise_subadditive" "y" "{x | inf(b!1) <= x AND x <= sup(b!1)}" "x" "union[real](singleton[real](inf(b!1)),singleton[real](sup(b!1)))" ))"1" "intersection AND x <= sup(b!1)},AND x < sup(b!1)}") "1" "1" "LHS" "lebesgue_outer_measure({x | inf(b!1) <= x AND x <= sup(b!1)})" )"1" "RHS" "lebesgue_outer_measure({x | inf(b!1) < x AND x < sup(b!1)})" )"1" "intersection AND x <= sup(b!1)},") "1" "1" "lebesgue_outer_measure_singleton" "x" "inf(b!1)" ))"1" "lebesgue_outer_measure_singleton" "x" "sup(b!1)" ))"1" "outer_negligible_union" "n1" "singleton[real](inf(b!1))" "n2" "singleton[real](sup(b!1))" ))"1" expand "outer_negligible?" )"1" replace -1)"1" "1" expand "x_add" )"1" expand "x_le" )"1" "1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "outer_negligible?" )"2" "2" expand "x_eq" )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "outer_negligible?" )"3" expand "x_eq" )"3" "3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "intersection" )"2" expand "member" )"2" "union[real] ") "1" expand "singleton" )"1" expand "union" )"1" expand "member" )"1" "1" assert )"1" "sup(b!1)" )"1" expand "least_upper_bound" )"1" expand "upper_bound" )"1" "1" expand "nonempty?" )"1" expand "empty?" )"1" "1" expand "member" )"1" "x!2" )"1" "inf(b!1)" )"1" expand "greatest_lower_bound" )"1" "1" expand "lower_bound" )"1" "x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "nonempty?" )"2" expand "empty?" )"2" "2" expand "member" )"2" "inf(b!1)" )"2" expand "greatest_lower_bound" )"2" expand "lower_bound" )"2" "2" "x!2" )"2" "sup(b!1)" )"2" expand "least_upper_bound" )"2" "2" expand "upper_bound" )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "singleton" )"2" expand "union" )"2" expand "complement" )"2" expand "intersection" )"2" expand "member" )"2" assert )"2" "inf(b!1) < x!1 AND x!1 < sup(b!1)" )"1" "1" assert )nil nil ))nil )"2" replace 1 2)"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "outer_measure?" )"2" "2" assert )"2" expand "om_increasing?" )"2" "{x | inf(b!1) < x AND x < sup(b!1)}" "{x | inf(b!1) <= x AND x <= sup(b!1)}" )"2" assert )"2" "2" expand "subset?" )"2" "2" expand "member" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) nil nil ) ("3" (skosimp) nil nil )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"outer_measure" nil )nil outer_measure_def"measure_integration/" )"bool" outer_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil ) (set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" reals nil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" bound_defs "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" bound_defs "reals/" )nil defined_types nil )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil extended_nnreal"extended_nnreal/" )"[bool, bool -> bool]" booleans nil )"bool" sets nil )"(partial_order?[set[T]])" nil )"bool" outer_measure_def"measure_integration/" )"(singleton?)" sets nil )"bool" sets nil )"set" sets nil )nil outer_measure_props"measure_integration/" )"(strict_total_order?[real])" real_props nil )"bool" bound_defs "reals/" )"bounded_interval" real_lebesgue_scaf nil )"real" real_lebesgue_scaf nil )"bool" bound_defs "reals/" )"bool" sets nil )"(total_order?[real])" nil )"real" real_lebesgue_scaf nil )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )"bool" booleans nil )"bool" extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )nil outer_measure_props"measure_integration/" )"bool" outer_measure_props"measure_integration/" )nil outer_measure_props"measure_integration/" )"compact[real, metric_induced_topology]" real_intervals nil )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"non_empty_finite_set[T]" bounded_nats "orders/" )nil nil )"(LAMBDA (S: set[T]): " "orders/" )"finite_set[T]" "orders/" )"non_empty_finite_set[T]" bounded_nats "orders/" )"(nonempty?)" bounded_nats"orders/" )"closed[real, metric_induced_topology]" real_intervals nil )"compact[real, metric_induced_topology]" real_intervals nil )"open[real, metric_induced_topology]" real_intervals nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"set" sets nil )nil real_topology"metric_space/" )"bool" real_topology"metric_space/" ))nil 3408257030"" (skosimp)"" (typepred "b!1" )"" (expand "<=" -1)"" (split)"1" "lebesgue_outer_measure_closed_open" "b" "{x | a!1 <= x AND x <= b!1}" ))"1" "nonempty?[real]({x | a!1 <= x AND x <= b!1})" )"1" case "above_bounded[real]({x | a!1 <= x AND x <= b!1})" )"1" case "below_bounded[real]({x | a!1 <= x AND x <= b!1})" )"1" "inf({x | a!1 <= x AND x <= b!1})=a!1" )"1" "sup({x | a!1 <= x AND x <= b!1})=b!1" )"1" (hide-all-but (-3 -4 -6 1))"1" "sup({x | a!1 <= x AND x <= b!1})" )"1" (expand "least_upper_bound" )"1" (flatten)"1" "b!1" )"1" "SUP" "sup({x | a!1 <= x AND x <= b!1})" )"1" "1" expand "<=" -1)"1" "1" expand "upper_bound" )"1" "b!1" )"1" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (propax) nil nil )"3" expand "upper_bound" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide-all-but (-1 -3 -5 1))"2" "inf({x | a!1 <= x AND x <= b!1})" )"1" "INF" "inf({x | a!1 <= x AND x <= b!1})" )"1" (expand "greatest_lower_bound" )"1" (flatten)"1" expand "lower_bound" )"1" "a!1" )"1" "a!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" (assert ) nil nil ))nil )"2" (expand "below_bounded" )"2" (inst + "a!1" )"2" (expand "lower_bound" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (expand "above_bounded" )"2" (inst + " b!1" )"2" (expand "upper_bound" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "a!1" )"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "bounded_interval?" )"2" (split)"1" (expand "interval?" ) (("1" (grind) nil nil ))nil )"2" (expand "bounded?" )"2" (expand "nonempty?" )"2" (flatten)"2" (assert )"2" (split)"1" (expand "above_bounded" )"1" "b!1" )"1" expand "upper_bound" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "below_bounded" )"2" "a!1" )"2" expand "lower_bound" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "{x | a!1 < x AND x < b!1}=emptyset[real]" )"1" "{x | a!1 <= x AND x <= b!1}=singleton[real](b!1)" )"1" "lebesgue_outer_measure_singleton" ("x" "b!1" ))"1" (hide -2 -3)"1" "LHS" "lebesgue_outer_measure(singleton[real](b!1))" )"1" (typepred "lebesgue_outer_measure" )"1" (expand "outer_measure?" )"1" (flatten)"1" "lebesgue_outer_measure(emptyset[real])=(TRUE, 0)" )"1" (hide 2 -4)"1" "1" expand "lebesgue_outer_measure" )"1" expand "x_inf" )"1" "1" assert )"1" "FORALL (x: AND NOT x`1") "1" "(TRUE,0)" )"1" "lambda (n:nat): emptyset[real]" )"1" "1" expand "o" )"1" "x_length(emptyset[real])=(TRUE, 0)" )"1" "1" expand "x_sum" )"1" expand "x_le" )"1" rewrite "zero_series_limit" )"1" rewrite "zero_series_conv" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_length" )"2" "2" rewrite "length_empty_rew" )"2" assert )"2" "2" expand "bounded_interval?" )"2" "1" nil nil )"2" expand "bounded?" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil )"2" expand "subset?" )"2" expand "emptyset" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" "1" nil nil )"2" expand "bounded?" )"2" "2" "2" nil nil ))nil ))nil ))nil )"3" "metric_induced_topology" )"3" expand "metric_induced_topology" )"3" rewrite "metric_open_def" )"3" expand "open?" )"3" expand "hausdorff_space?" )"3" expand "topology?" )"3" "3" expand "topology_empty?" )"3" expand "member" )"3" rewrite "metric_open_def" )"3" expand "open?" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "2" case "nonempty?({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" case "below_bounded({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" "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" "1" expand "greatest_lower_bound?" )"1" "1" "0" )"1" "1" expand "lower_bound?" )"1" "0" )"1" assert )nil nil )"2" "(TRUE,0)" )"2" "lambda (n:nat): emptyset[real]" )"1" assert )"1" "1" expand "o" "1" "1" "x_length(emptyset[real])=(TRUE, 0)" )"1" "1" expand "x_sum" )"1" expand "x_le" )"1" rewrite "zero_series_conv" )"1" rewrite "zero_series_limit" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "x_length" )"2" "2" "2" assert )"2" rewrite "length_empty_rew" )"2" "2" expand "bounded_interval?" )"2" "1" nil nil )"2" expand "bounded?" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "emptyset" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_open_interval?" )"2" expand "bounded_interval?" )"2" "1" nil nil )"2" expand "bounded?" )"2" "2" "2" nil nil ))nil ))nil ))nil )"3" "metric_induced_topology" )"3" expand "metric_induced_topology" )"3" expand "hausdorff_space?" )"3" expand "topology?" )"3" "3" expand "topology_empty?" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "lower_bound?" )"2" "2" "s!1" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "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 )"2" "2" expand "below_bounded" )"2" "0" )"2" expand "lower_bound" )"2" "2" "z!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "x!1" )"2" "2" "x!1`2" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "I!1(x1!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" 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 1))"2" (apply-extensionality :hide? t)"2" (expand "singleton" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (expand "emptyset" )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"bool" real_topology "metric_space/" )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" bound_defs "reals/" )nil bounded_reals "reals/" )"bool" bound_defs "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" bound_defs "reals/" )nil defined_types nil )nil bounded_reals "reals/" )"[T, T -> boolean]" equalities nil )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" sets nil )"bool" sets nil )nil nil )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )AND const-decl "[bool, bool -> bool]" booleans nil )"(singleton?)" sets nil )"bool" sets nil )"compact[real, metric_induced_topology]" real_intervals nil )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"non_empty_finite_set[T]" bounded_nats "orders/" )"set[T]" indexed_sets nil )"bool" sets nil )"extended_nnreal" real_lebesgue_scaf nil )"T3" function_props nil )nil real_topology "metric_space/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )nil sequences nil )nil real_topology"metric_space/" )"bool" real_topology"metric_space/" )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_intervals_aux nil )nil series "series/" )nil series "series/" )"hausdorff[real]" "metric_space/" )"(hausdorff?)" "metric_space/" )"second_countable" real_topology "metric_space/" )nil sets nil )"bool" topology_prelim "topology/" )nil real_types nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"bool" topology_prelim "topology/" )"bool" topology_def "topology/" )nil metric_space "metric_space/" )"bool" topology_prelim "topology/" )"bool" topology_prelim "topology/" )"bool" topology "topology/" )"(partial_order?[set[T]])" nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" booleans nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def"measure_integration/" )nil outer_measure_def"measure_integration/" )"outer_measure" nil )nil nil )"finite_set" finite_sets nil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" bounded_nats"orders/" )"(induced_sigma_algebra)" nil )"outer_negligible[real, lebesgue_outer_measure]" nil )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"bool" reals nil )"set" sets nil ))nil 3408182751"" (skosimp)"" (typepred "b!1" )"" (expand "bounded_interval?" )"" (expand "bounded?" )"" (assert )"" (flatten)"" (split)"1" (expand "nonempty?" ) (("1" (propax) nil nil ))nil )"2" (flatten)"2" "lebesgue_outer_measure_closed_open" "b" "b!1" ))"2" (assert )"2" (typepred "lebesgue_outer_measure" )"2" (expand "outer_measure?" )"2" (flatten)"2" (hide -1 -3)"2" expand "om_increasing?" )"2" "{x | inf(b!1) < x AND x < sup(b!1)}" "b!1" )"2" "b!1" "{x | inf(b!1) <= x AND x <= sup(b!1)}" )"2" "OPEN" "lebesgue_outer_measure({x | inf(b!1) < x AND x < sup(b!1)})" )"2" "CLOSED" "lebesgue_outer_measure({x | inf(b!1) <= x AND x <= sup(b!1)})" )"2" "INTERVAL" "lebesgue_outer_measure(b!1)" )"2" "1" "1" "1" (grind) nil nil ))nil )"2" "2" expand "subset?" )"2" expand "member" )"2" "2" "sup(b!1)" )"2" expand "least_upper_bound" )"2" expand "upper_bound" )"2" "2" "x!1" )"2" assert )"2" "2" "z!1" )"2" case "x!1<z!1" )"1" "1" "inf(b!1)" )"1" expand "greatest_lower_bound" )"1" expand "lower_bound" )"1" "1" "x!1" )"1" assert )"1" "1" "z!2" )"1" case "z!2<x!1" )"1" "1" expand "interval?" )"1" "z!2" "z!1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "member" )"2" "2" "sup(b!1)" )"2" "inf(b!1)" )"2" expand "least_upper_bound" )"2" expand "greatest_lower_bound" )"2" expand "lower_bound" )"2" expand "upper_bound" )"2" "2" "x!1" )"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 ))nil )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" real_topology "metric_space/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"bool" bound_defs "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"real" real_lebesgue_scaf nil )"bounded_interval" real_lebesgue_scaf nil )"real" reals nil )"(total_order?[real])" nil )"bool" extended_nnreal "extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"bool" real_topology "metric_space/" )"bool" bound_defs "reals/" )"bool" bound_defs "reals/" )"bool" sets nil )"bool" outer_measure_def"measure_integration/" )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def"measure_integration/" )nil outer_measure_def"measure_integration/" )"outer_measure" nil )nil nil )"bool" sets nil ))nil 3408184157"" (skosimp)"" (lemma "lebesgue_outer_measure_closed" ("b" "b!1" ))"" (lemma "lebesgue_outer_measure_closed_open" ("b" "b!1" ))"" (assert )"" (typepred "b!1" )"" (expand "bounded_interval?" )"" (expand "bounded?" )"" (flatten)"" (split)"1" (expand "nonempty?" ) (("1" (propax) nil nil ))nil )"2" (flatten)"2" "OPEN" "lebesgue_outer_measure({x | inf(b!1) < x AND x < sup(b!1)})" )"1" "CLOSED" "lebesgue_outer_measure({x | inf(b!1) <= x AND x <= sup(b!1)})" )"1" "INTERVAL" "lebesgue_outer_measure(b!1)" )"1" (expand "x_eq" )"1" "1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) nil nil ))nil )"2" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_lebesgue_scafnil )"bool" extended_nnreal "extended_nnreal/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" bound_defs "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"outer_measure" nil )nil outer_measure_def"measure_integration/" )"bool" outer_measure_def"measure_integration/" )"[T, T -> boolean]" equalities nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"bool" sets nil )"bool" real_topology "metric_space/" )NOT const-decl "[bool -> bool]" booleans nil )nil nil ))nil 3408184601"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"(total_order?[real])" nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" real_topology "metric_space/" )"bool" real_topology "metric_space/" ))nil ))nil 3408184601"" (skosimp)"" (case "nonempty?[real](b!1)" )"1" (lemma "lebesgue_outer_measure_open" ("b" "b!1" ))"1" (assert )"1" (lemma "length_open" ("b" "b!1" ))"1" (assert )"1" (typepred "b!1" )"1" (expand "bounded_interval?" )"1" (expand "bounded?" )"1" (flatten)"1" (split)"1" (expand "nonempty?" )"1" (propax) nil nil )) nil )"2" (flatten)"2" (typepred "inf(b!1)" )"1" (name-replace "AA" "inf(b!1)" )"1" "sup(b!1)" )"1" "BB" "sup(b!1)" )"1" case "x_le(lebesgue_outer_measure({x | AA < x AND x < BB}), x_length({x | AA < x AND x < BB}))" )"1" "LHS" "lebesgue_outer_measure(b!1)" )"1" "LHS1" "lebesgue_outer_measure({x | AA < x AND x < BB})" )"1" expand "x_length" )"1" replace -7 * rl)"1" "bounded_interval?({x | AA < x AND x < BB})" )"1" "1" expand "x_le" )"1" expand "x_eq" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_interval?" )"2" "1" expand "interval?" )"1" "1" "x!1" )"1" "y!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "bounded?" )"2" "2" expand "nonempty?" )"2" assert )"2" "1" expand "above_bounded" )"1" "BB" )"1" expand "upper_bound" )"1" nil nil ))nil ))nil ))nil )"2" expand "below_bounded" )"2" "AA" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_length" )"2" "bounded_interval?({x | AA < x AND x < BB})" )"1" expand "x_le" )"1" expand "lebesgue_outer_measure" )"1" expand "o " )"1" expand "x_inf" )"1" "1" "(TRUE,length({x | AA < x AND x < BB}))" )"1" "lambda (i:nat): if i=0 then {x | AA < x AND x < BB} else emptyset[real] endif" )"1" "1" expand "x_le" )"1" expand "x_sum" )"1" expand "x_length" "1" replace "1" "bounded_interval?(emptyset[real])" )"1" "length(emptyset[real])=0" )"1" "FORALL (i:nat): IF i = 0 THEN TRUE ELSE TRUE ENDIF" )"1" "1" "zero_tail_series_conv" "a" "LAMBDA (i:nat): IF i = 0 THEN length({x | AA < x AND x < BB})" "n" "0" ))"1" "zero_tail_series_limit" "a" "LAMBDA (i:nat): IF i = 0 THEN length({x | AA < x AND x < BB})" "n" "0" ))"1" "(FORALL (m:nat): LAMBDA (i: nat):IF i = 0 THEN length({x | AA < x AND x < BB}) ELSE 0 ENDIF)") "1" replace "1" replace "1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" "3" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil )"2" expand "length" )"2" "2" "empty?[real](emptyset[real])" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" expand "member" )"2" "2" expand "IUnion" )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_open_interval?" )"2" rewrite "metric_open_def" )"2" rewrite "emptyset_is_open" )"2" expand "bounded_interval?" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" expand "bounded_open_interval?" )"3" case "AA<BB" )"1" "metric_open_ball" "x" "(BB+AA)/2" "r" "(BB-AA)/2" ))"1" "ball((BB + AA) / 2, (BB - AA) / 2)={x | AA < x AND x < BB}" )"1" "1" "1" expand "ball" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" "{x | AA < x AND x < BB}=emptyset[real]" )"1" rewrite "metric_open_def" )"1" rewrite "emptyset_is_open" )nil nil ))nil )"2" "2" "2" expand "emptyset" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "FORALL (x_1: LAMBDA (x: nat): x_length(I(x))), z)AND AND x < BB}, IUnion(I))})):NOT x_1`1") "1" assert )nil nil )"2" replace 1 2)"2" "2" case "nonempty?({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x < BB}, IUnion(I)))AND x_1`1 AND x_1`2 = z_1})") "1" case "bounded_below?({z_1: real | LAMBDA (x: nat): x_length(I(x))),AND AND x < BB},AND x_1`1 AND x_1`2 = z_1})") "1" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x < BB}, IUnion(I)))AND x_1`1 AND x_1`2 = z_1})") "1" "GLB" "glb({z_1: real | LAMBDA (x: nat): x_length(I(x))), x_1) AND AND x < BB}, IUnion(I)))AND x_1`1 AND x_1`2 = z_1})") "1" "1" expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "length({x | AA < x AND x < BB})" )"1" "(TRUE,length({x | AA < x AND x < BB}))" )"1" "1" "lambda (i:nat): if i=0 then {x | AA < x AND x < BB} else emptyset[real] endif" )"1" "1" expand "x_sum" )"1" expand "x_le" )"1" "x_length(emptyset[real])=(TRUE,0)" )"1" assert )"1" "1" expand "x_length" "1" replace "1" replace "1" "FORALL (i:nat): IF i = 0 THEN TRUE ELSE TRUE ENDIF" )"1" "zero_tail_series_conv" "a" "LAMBDA (i:nat): IF i = 0 THEN length(b!1) ELSE 0 ENDIF" "n" "0" ))"1" "zero_tail_series_limit" "a" "LAMBDA (i:nat): IF i = 0 THEN length(b!1) ELSE 0 ENDIF" "n" "0" ))"1" "FORALL (m:nat): LAMBDA (i: nat): IF i = 0 THEN length(b!1) ELSE 0 ENDIF)(m) = 0") "1" replace "1" replace "1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_length" )"2" "2" "1" expand "length" )"1" "empty?[real](emptyset[real])" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "member" )"2" expand "IUnion" )"2" "2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_open_interval?" )"2" rewrite "metric_open_def" )"2" rewrite "emptyset_is_open" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "bounded_open_interval?" )"3" assert )"3" "3" case "AA<BB" )"1" "metric_open_ball" "x" "(AA+BB)/2" "r" "(BB-AA)/2" ))"1" "ball((AA + BB) / 2, (BB - AA) / 2)={x | AA < x AND x < BB}" )"1" "1" expand "ball" )"1" "1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" "{x | AA < x AND x < BB}=emptyset[real]" )"1" "1" rewrite "metric_open_def" )"1" rewrite "emptyset_is_open" )nil nil ))nil ))nil )"2" "2" "2" expand "emptyset" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "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 )"3" nil nil ))nil )"2" expand "nonempty?" "2" expand "empty?" "2" expand "member" )"2" "x!1`2" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" "I!1(x!2)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_interval?" )"2" "1" expand "interval?" )"1" "1" assert )nil nil ))nil ))nil )"2" expand "bounded?" )"2" "2" expand "nonempty?" )"2" assert )"2" "1" expand "above_bounded" )"1" "BB" )"1" expand "upper_bound" )"1" nil nil ))nil ))nil ))nil )"2" expand "below_bounded" )"2" "AA" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "interval?" )"3" "3" "z!1" )"3" "x!1" )"3" "x!1" "y!1" "z!1" )"1" (assert ) nil nil )"2" "y!1" )"2" assert )nil nil ))nil )"3" assert )
Messung V0.5 in Prozent C=100 H=98 G=98
¤ Dauer der Verarbeitung: 0.943 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
