Quellcode-Bibliothek countable_convergence.prf
Interaktion und
(countable_convergencenil 3322366680"" (skosimp)"" (typepred "X!1" )"" (lemma "countably_infinite_def" ("S" "X!1" ))"" (assert ) nil nil )) nil ))nil ))nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil countable_convergence nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil countable_props"sets_aux/" ))nil 3323142075"" (skosimp)"" (typepred "X!1" )"" (expand "convergent?" )"" (flatten)"" (expand "o" )"" (expand "absconvergent?" )"" (expand "abs" )"" (expand "abs" )"" (rewrite "zero_series_conv" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil countable_convergence nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" absconv_series "series/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil series "series/" )"sequence[real]" series "series/" )"T3" function_props nil )"bool" countable_convergence nil ))nil 3351595333"" (skosimp)"" (typepred "X!1" )"" (expand "convergent?" )"" (flatten)"" (assert )"" (expand "absconvergent?" )"" (name-replace "DX" "denumerable_enumeration(X!1)" )"" "sum_absconvergent" "aa" "f!1 o DX" "bb" "g!1 o DX" ))"1" (expand "absconvergent?" )"1" (expand "o " )"1" (expand "+" ) (("1" (propax) nil nil )) nil ))nil ))nil )"2" (expand "o" )"2" (expand "absconvergent?" )"2" (propax) nil nil )) nil ))nil )"3" (expand "o" )"3" (expand "absconvergent?" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil countable_convergence nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" absconv_series "series/" )nil absconv_series "series/" )nil sequences nil )nil absconv_series"series/" )"T3" function_props nil )"[T -> real]" real_fun_ops "reals/" )"[nat -> (X)]" nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )"[T, T -> boolean]" equalities 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 )"bool" countable_convergence nil ))nil 3351595652"" (skosimp)"" (expand "convergent?" )"" (flatten)"" (assert )"" (name-replace "DX" "denumerable_enumeration(X!1)" )"" "scal_absconvergent" ("aa" "f!1 o DX" "x" "a!1" ))"1" (expand "o" )"1" (expand "*" ) (("1" (propax) nil nil )) nil )) nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countable_convergence nil )"T3" function_props nil )nil absconv_series"series/" )"bool" absconv_series "series/" )nil sequences nil )nil absconv_series "series/" )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[nat -> (X)]" nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )"[T, T -> boolean]" equalities nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil countable_convergence 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 3351596230"" (skosimp)"" (lemma "convergent_scal" ("X" "X!1" "f" "f!1" "a" "-1" ))"" (expand "-" ) (("" (expand "*" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_convergence nil )nil countable_convergence nil )"odd_int" integers nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"real" reals nil ))nil 3351596280"" (skosimp)"" (lemma "convergent_opp" ("X" "X!1" "f" "g!1" ))"" (assert )"" (lemma "convergent_plus" ("X" "X!1" "f" "f!1" "g" "-g!1" ))"" (assert )"" (expand "-" )"" (expand "+" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_convergence nil )nil countable_convergence nil )"[T -> real]" real_fun_ops "reals/" )nil countable_convergence nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" ))nil 3351599438"" (expand "convergent?" )"" (skosimp*)"" (assert )"" (expand "absconvergent?" )"" (name-replace "DX" "denumerable_enumeration(X!1)" )"" "comparison_test" "b" "abs(f!1 o DX)" "a" "abs(g!1 o DX)" ))"" (split -1)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (hide-all-but (-1 1))"3" (skosimp)"3" (inst - "DX(n!1)" ) (("3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" absconv_series "series/" )nil series "series/" )nil sequences nil )"sequence[real]" series "series/" )"T3" function_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[nat -> (X)]" nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )"[T, T -> boolean]" equalities nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil countable_convergence 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 )"bool" countable_convergence nil ))nil 3406442125"" (skosimp)"" (typepred "X!1" )"" (expand "convergent?" )"" (flatten)"" (expand "absconvergent?" )"" (lemma "zero_series_conv" )"" (expand "o " )"" (lemma "countably_infinite_def" ("S" "X!1" ))"" (assert )"" "abs(LAMBDA (x: nat): lambda (x:nat): 0") "" (hide-all-but (1 -4 -1))"" (apply-extensionality :hide? t)"" (expand "abs" )"" "denumerable_enumeration(X!1)(x!1)" )"" replace -2)"" expand "abs" )"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil countable_convergence nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil series "series/" )nil countable_props"sets_aux/" )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 )"[T, T -> boolean]" equalities nil )nil sequences nil )"sequence[real]" series "series/" )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"[nat -> (X)]" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"T3" function_props nil )"bool" absconv_series "series/" )"bool" countable_convergence nil ))nil 3351591225"" (skosimp)"" (expand "convergent?" ) (("" (propax) nil nil )) nil )) nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" nil )"bool" countable_convergence nil ))nil 3351591618"" (skosimp*)"" (expand "convergent?" ) (("" (propax) nil nil )) nil )) nil )"non_empty_finite_set[T]" countable_convergence nil )"bool" countable_convergence nil ))nil 3323142263"" (skosimp)"" (expand "convergent?" )"" (flatten)"" (case-replace "is_finite(Y!1)" )"1" (lemma "finite_subset" ("s" "X!1" "A" "Y!1" ))"1" (assert ) nil nil ) ("2" (propax) nil nil )) nil )"2" (assert )"2" (typepred "X!1" )"2" (typepred "Y!1" )"2" (rewrite "countable_props.countable_card" -1)"2" (rewrite "countable_props.countable_card" -2)"2" (hide 1 2)"2" "denumerable_enumeration_bij" "X" "X!1" ))"2" "denumerable_enumeration_bij" "X" "Y!1" ))"2" "PHI_X" "denumerable_enumeration(X!1)" )"2" "PHI_Y" "denumerable_enumeration(Y!1)" )"2" expand "o" )"2" "bijective_inverse_exists[nat, (X!1)]" "f" "PHI_X" ))"1" "bijective_inverse_exists[nat, (Y!1)]" "f" "PHI_Y" ))"1" expand "exists1" )"1" "1" "PSI_Y" ))"1" "PSI_X" ))"1" "bij_inv_is_bij_alt[nat,(X!1)]" "f" "PHI_X" "g" "PSI_X" ))"1" "bij_inv_is_bij_alt[nat,(Y!1)]" "f" "PHI_Y" "g" "PSI_Y" ))"1" case "FORALL (a:sequence[real],inj:(injective?[nat,nat])):absconvergent?(a) => absconvergent?(a o inj)" )"1" case "injective?[nat,nat](PSI_Y o PHI_X)" )"1" "g!1 o PHI_Y" "PSI_Y o PHI_X" )"1" "1" expand "o" )"1" "comp_inverse_right_surj_alt[nat,(Y!1)]" "f" "PHI_Y" "g" "PSI_Y" ))"1" "extensionality" "f" "LAMBDA (x_1: nat): g!1(PHI_Y(PSI_Y(PHI_X(x_1))))" "g" "LAMBDA (x: nat): g!1(PHI_X(x))" ))"1" "1" replace "1" nil nil ))nil )"2" "2" "PHI_X(x!1)" )"2" "2" expand "subset?" )"2" "PHI_X(x!1)" )"2" expand "member" )"2" "PHI_X(x!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bijective?" )"2" nil nil ))nil ))nil ))nil )"2" expand "o " )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "bijective?" )"2" "2" expand "injective?" )"2" "2" expand "o" )"2" "x1!1" "x2!1" )"2" expand "subset?" )"2" expand "member" )"2" "PHI_X(x1!1)" )"2" "PHI_X(x2!1)" )"2" assert )"2" "2" "PHI_X(x1!1)" "PHI_X(x2!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "subset?" )"3" "PHI_X(x1!1)" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "absconvergent?" )"2" "abs_series_inj_conv" "aa" "abs(a!1)" "inj" "inj!1" ))"1" "extensionality" "f" "abs(a!1) o inj!1" "g" "abs(a!1 o inj!1)" ))"1" "1" replace "1" nil nil ))nil )"2" "2" "2" expand "abs" )"2" expand "o" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "absconvergent?" )"2" "2" "extensionality" "f" "abs(a!1)" "g" "abs(abs(a!1))" ))"2" "1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countable_convergence nil )nil countable_convergence nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"(partial_order?[set[T]])" nil )nil finite_sets nil )nil finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil countable_props "sets_aux/" )nil function_inverse_defnil )"bool" functions nil )"bool" exists1 nil )nil function_inverse_def nil )"bool" function_inverse_def nil )nil sequences nil )"bool" functions nil )"[bool, bool -> bool]" booleans nil )"bool" absconv_series "series/" )"countable_set[T]" countable_convergencenil )"[(Y!1) -> nat]" countable_convergencenil )"countable_set[T]" countable_convergencenil )"[nat -> (X!1)]" countable_convergencenil )nil functions nil )"bool" sets nil )"bool" sets nil )"bool" functions nil )nil function_inverse_defnil )nil absconv_series_aux nil )nil absconv_series"series/" )"sequence[real]" series "series/" )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"T3" function_props nil )"[nat -> (X)]" nil )"[T, T -> boolean]" equalities 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 )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil nil ))nil 3351591237"" (skosimp)"" (split)"1" "convergent_subset" "X" "intersection(X!1, Y!1)" "Y" "X!1" "g" "g!1" ))"1" (assert )"1" (hide-all-but 1) (("1" (grind) nil nil )) nil )) nil ))nil )"2" "convergent_subset" "X" "intersection(X!1, Y!1)" "Y" "Y!1" "g" "g!1" ))"2" (split)"1" (propax) nil nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )"countable_set[T]" nil )nil countable_convergence nil )nil countable_convergence nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3351593239"" (skosimp)"" "convergent_subset" "X" "difference(X!1, Y!1)" "Y" "X!1" "g" "g!1" ))"" (assert ) (("" (hide-all-but 1) (("" (grind) nil nil )) nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_convergence nil )nil countable_convergence nil )"countable_set[T]" nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil 3462016397"" case "FORALL (X:finite_set[T], Y: countable_set[T], g: [T -> real]): AND convergent?(X)(g) AND convergent?(Y)(g) IMPLIES") "1" (skosimp)"1" (expand "convergent?" )"1" (case-replace "is_finite(X!1)" )"1" (inst - "X!1" "Y!1" "g!1" )"1" (replace -4) (("1" (assert ) nil nil )) nil )) nil )"2" (assert )"2" (case-replace "is_finite(Y!1)" )"1" (inst - "Y!1" "X!1" "g!1" )"1" (assert )"1" (split -2)"1" (rewrite "union_commutative" )"1" (assert ) nil nil )) nil )"2" (rewrite "union_commutative" )"2" (assert ) nil nil )) nil )"3" (hide-all-but (-2 1))"3" (expand "disjoint?" )"3" (rewrite "intersection_commutative" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide -1)"2" (expand "absconvergent?" )"2" "denumerable_enumeration_bij" "X" "X!1" ))"2" "denumerable_enumeration_bij" "X" "Y!1" ))"2" "denumerable_enumeration_bij" "X" "union(X!1,Y!1)" ))"2" "DX" "denumerable_enumeration(X!1)" )"2" "DY" "denumerable_enumeration(Y!1)" )"2" "DXY" "denumerable_enumeration(union(X!1,Y!1))" )"2" "bijective_inverse_exists[nat, (union(X!1, Y!1))]" "f" "DXY" ))"1" expand "exists1" )"1" "1" "CXY" ))"1" "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" "f" "DXY" "g" "CXY" ))"1" "PHI" "LAMBDA (n:nat): IF even?(n) THEN DX(n/2) ELSE DY((n-1)/2) ENDIF" )"1" case "bijective?[nat, (union(X!1, Y!1))](PHI)" )"1" "1" case "forall (a:sequence[real]): convergent?(series(a)) => convergent?(series(LAMBDA (n:nat): IF even?(n) THEN a(n/2) ELSE 0 ENDIF))" )"1" case "FORALL (a: sequence[real]): LAMBDA (n: nat):IF odd?(n) THEN a((n-1)/2) ELSE 0 ENDIF))") "1" "abs(g!1 o DY)" )"1" "abs(g!1 o DX)" )"1" assert )"1" "series_sum_conv" "a" "(LAMBDA (n: nat): IF even?(n) THEN abs(g!1 o DX)(n / 2)" "b" "(LAMBDA (n: nat): IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)")) "1" assert )"1" "1" "extensionality" "f" "((LAMBDA (n: nat): IF even?(n) THEN abs(g!1 o DX)(n / 2)LAMBDA (n: nat):IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)" "g" "abs(g!1 o PHI)" ))"1" "1" replace "1" "1" "bijective_inverse_exists[nat, (union(X!1, Y!1))]" "f" "PHI" ))"1" expand "exists1" )"1" "1" "PSI" ))"1" "1" "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" "f" "PHI" "g" "PSI" ))"1" "composition_bijective[nat,(union(X!1, Y!1)),nat]" "f2" "PSI" "f1" "DXY" ))"1" "comp_inverse_right_alt[nat, (union(X!1, Y!1))]" "f" "PHI" "g" "PSI" ))"1" "1" "abs_series_bij_conv_abs" "phi" "PSI o DXY" "aa" "abs(g!1 o PHI)" ))"1" assert )"1" "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)" )"1" "1" "1" expand "o" )"1" expand "abs" )"1" "DXY(x!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" expand "absconvergent?" )"3" "3" "abs(abs(o[nat, T, real](g!1, PHI))) = abs(g!1 o PHI)" )"3" "3" "3" expand "abs" )"3" expand "o " )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "+" )"2" expand "PHI" )"2" expand "abs" )"2" expand "o" )"2" "even?(x!1)" )"1" "even_or_odd" "x" "x!1" ))"1" assert )nil nil ))nil )"2" "even_or_odd" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "even?" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "odd?" )"2" "2" assert )"2" replace "2" assert )"2" case "forall (i,j:int):i<j=>i+1<=j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "even?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "convergent?" )"2" "2" "l!1" )"2" expand "convergence" )"2" "2" "epsilon!1" )"2" "2" case "FORALL (m: nat): LAMBDA (n: nat):IF odd?(n) THEN a!1((n - 1) / 2) ELSE 0 ENDIF)") "1" "2*n!1+1" )"1" "1" case "even?(i!1)" )"1" expand "even?" )"1" "1" expand "series" )"1" replace "1" "j!1=0" )"1" assert )nil nil )"2" "j!1-1" )"1" "j!1-1" )"1" assert )"1" replace "1" expand "sigma" "1" expand "odd?" "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" "2" expand "odd?" "2" "2" replace "2" "j!1" )"1" assert )"1" "j!1" )"1" expand "series" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "m" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "odd?" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" expand "sigma" "2" replace "2" "2" assert )"2" expand "odd?" )"2" "div_cancel2" "x" "1+j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "odd?" )"3" "3" replace "3" assert )"3" case "forall (i,j:int):i<j=>i+1<=j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "odd?" )"3" "3" assert )"3" assert )"3" case "forall (i,j:int):i<j=>i+1<=j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "odd?" )"3" "3" replace "3" assert )"3" "n!1" )"3" case "forall (i,j:int): i<j => i+1<=j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "convergent?" )"2" "2" "l!1" )"2" expand "convergence" )"2" "2" "epsilon!1" )"2" "2" "2*n!1" )"2" "2" case "even?(i!1)" )"1" expand "even?" "1" "1" replace "1" "j!1" )"1" assert )"1" expand "series" )"1" case "forall (m:nat): sigma(0, m, a!1) = sigma(0, 2*m, LAMBDA (n: nat):IF even?(n) THEN a!1(n / 2) ELSE 0 ENDIF)") "1" "j!1" )"1" assert )nil nil ))nil )"2" "2" "m" )"1" expand "sigma" )"1" assert )nil nil ))nil )"2" "2" expand "sigma" "2" expand "sigma" "2" "div_cancel2" "x" "1+j!1" "n0z" "2" ))"2" assert )"2" expand "even?" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" "div_cancel2" "x" "j!2" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" "2" expand "odd?" )"2" "2" replace "2" "j!1" )"1" assert )"1" expand "series" )"1" case "forall (m:nat): sigma(0,m,a!1) = sigma(0,1+2*m,LAMBDA (n:nat): IF even?(n) THEN a!1(n/2) ELSE 0 ENDIF)" )"1" "j!1" )"1" assert )nil nil ))nil )"2" "2" "m" )"1" expand "sigma" )"1" expand "sigma" )"1" assert )"1" expand "even?" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" expand "sigma" "2" replace "2" assert )"2" "2" expand "even?" )"2" "div_cancel2" "x" "1+j!2" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" "div_cancel2" "x" "j!2" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" "div_cancel2" "x" "j!2" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "3" expand "even?" )"3" "3" "div_cancel2" "x" "j!1" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bijective?" )"2" "2" expand "PHI" )"2" "1" expand "injective?" )"1" "1" "even?(x1!1)" )"1" "even?(x2!1)" )"1" "x1!1/2" "x2!1/2" )"1" assert )nil nil )"2" "2" expand "even?" )"2" "2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "even?" )"3" "3" "div_cancel2" "x" "j!1" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "DX(x1!1 / 2)" )"1" assert )nil nil )"2" expand "even?" )"2" "2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "even?(x2!1)" )"1" assert )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "DX(x2!1 / 2)" )"1" assert )nil nil )"2" expand "even?" )"2" "2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "(x1!1 - 1) / 2" "(x2!1 - 1) / 2" )"1" assert )nil nil )"2" "2" rewrite "even_or_odd" )"2" expand "odd?" )"2" "2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "even_or_odd" )"3" expand "odd?" )"3" "3" "div_cancel2" "x" "j!1" "n0z" "2" ))"3" assert )"3" replace "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "union" )"2" expand "member" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "1" "y!1" )"1" "1" "2*x!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "y!1" )"2" "2" "2*x!1+1" )"2" assert )"2" "div_cancel2" "x" "x!1" "n0z" "2" ))"2" replace "2" assert )"2" replace "2" "2" "2" expand "even?" )"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 ))nil ))nil )"3" "3" expand "union" )"3" expand "member" )"3" expand "PHI" )"3" "3" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "even_or_odd" )"2" expand "odd?" )"2" "2" replace -1)"2" assert )"2" assert )"2" "div_cancel1" "x" "j!1" "n0z" "2" ))"2" assert )"2" "n!1" )"2" case "0 <= j!1" )"1" assert )nil nil )"2" "trich_lt" "x" "j!1" "y" "-1" ))"2" "1" assert )nil nil )"2" assert )nil nil )"3" assert )"3" case "forall (i,j:int): i < j IFF i + 1 <= j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" "2" "1" "1" assert )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 ))nil ))nil )"3" "3" "3" expand "even?" )"3" "3" replace -1)"3" "div_cancel1" "x" "j!1" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "convergent?" )"2" (typepred "X!1" )"2" (hide -3)"2" (flatten)"2" (split -3)"1" (lemma "finite_union" ("A" "X!1" "B" "Y!1" ))"1" (propax) nil nil ) ("2" (propax) nil nil ))nil )"2" "denumerable_enumeration_bij" ("X" "Y!1" ))"2" "denumerable_enumeration_bij" "X" "union(X!1,Y!1)" ))"2" "infinite_union" ("S" "X!1" "R" "Y!1" ))"2" (assert )"2" "DXY" "denumerable_enumeration(union(X!1, Y!1))" )"2" "DY" "denumerable_enumeration(Y!1)" )"2" expand "absconvergent?" )"2" "bijective_inverse_exists[nat, (union(X!1, Y!1))]" "f" "DXY" ))"1" expand "exists1" )"1" "1" "CXY" ))"1" "1" "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" "f" "DXY" "g" "CXY" ))"1" "N" "card(X!1)" )"1" "card_bij_inv" "S" "X!1" "N" "N" ))"1" assert )"1" "DX" ))"1" "PHI" "LAMBDA (n:nat): IF n < N THEN DX(n) ELSE DY(n-N) ENDIF" )"1" case "bijective?[nat, (union(X!1, Y!1))](PHI)" )"1" "composition_bijective[nat,(union(X!1, Y!1)),nat]" "f1" "PHI" "f2" "CXY" ))"1" case "absconvergent?(g!1 o PHI)" )"1" "bijective_inverse_exists[nat,(union(X!1,Y!1))]" "f" "PHI" ))"1" expand "exists1" )"1" "1" "PSI" ))"1" "bij_inv_is_bij_alt[nat,(union(X!1,Y!1))]" "f" "PHI" "g" "PSI" ))"1" "composition_bijective[nat,(union(X!1,Y!1)),nat]" "f1" "DXY" "f2" "PSI" ))"1" "abs_series_bij_conv_abs" "aa" "abs(g!1 o PHI)" "phi" "PSI o DXY" ))"1" expand "absconvergent?" "1" assert )"1" "comp_inverse_right_alt[nat, (union(X!1, Y!1))]" "f" "PHI" "g" "PSI" ))"1" "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)" )"1" "1" "1" expand "o " )"1" expand "abs" )"1" "DXY(x!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" expand "absconvergent?" )"3" expand "o " )"3" "abs(abs(LAMBDA (x: nat): g!1(PHI(x)))) = abs(LAMBDA (x: nat): g!1(PHI(x)))" )"3" "3" "3" expand "abs" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "absconvergent?" )"2" "conv_series_shift" "N" "N" ))"2" "abs(g!1 o PHI)" )"2" replace "2" "(LAMBDA n: abs(g!1 o PHI)(n + N)) = abs(g!1 o DY)" )"2" "2" "2" expand "abs" )"2" expand "o " )"2" expand "abs" )"2" expand "PHI" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "bijective?" )"2" "2" "1" expand "injective?" )"1" "1" expand "PHI" )"1" "x1!1<N" )"1" "x2!1 < N" )"1" "x1!1" "x2!1" )"1" assert )nil nil ))nil )"2" assert )"2" "DX(x1!1)" )"2" "DY(x2!1-N)" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "DX(x1!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x2!1<N" )"1" assert )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "DX(x2!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x1!1-N" "x2!1-N" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "union" )"2" expand "member" )"2" "1" "y!1" )"1" "1" "x!1" )"1" expand "PHI" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "y!1" )"2" "2" "N+x!1" )"2" expand "PHI" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "PHI" )"3" expand "union" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp) (("3" (rewrite "countable_union" ) nil nil )) nil ))nil )"4" (skosimp)"4" (assert )"4" (typepred "X!1" )"4" (lemma "finite_countable" ("x" "X!1" ))"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil finite_sets nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil nat_types nil )"finite_set[T]" countable_convergence nil )"countable_set[T]" countable_convergencenil )"(union(X!1, Y!1))" countable_convergencenil )"nonneg_int" nil )"[nat -> T]" countable_convergence nil )nil series "series/" )nil finite_sets nil )nil infinite_sets_def nil )"countable_set[T]" countable_convergencenil )nil sets_lemmas nil )"countable_set[T]" nil )nil sets_lemmas nil )"countable_set[T]" countable_convergencenil )"bool" absconv_series "series/" )"[nat -> (X)]" nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" exists1 nil )"nonneg_rat" nil )"rat" rationals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" integers nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"nat" countable_convergence nil )"nat" countable_convergence nil )"bool" sets nil )"bool" sets nil )"set" sets nil )"bool" functions nil )"(union(X!1, Y!1))" countable_convergencenil )"nonneg_rat" nil )"bool" functions nil )"int" countable_convergence nil )"rat" rationals nil )"int" countable_convergence nil )"bool" integers nil )nil series "series/" )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil function_inverse_def nil )nil absconv_series "series/" )nil absconv_series"series/" )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil function_props nil )"[nat -> T]" countable_convergence nil )nil naturalnumbers nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil functions nil )"odd_int" integers nil )"even_int" integersnil )"(total_order?[real])" nil )"odd_int" integers nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil ) (< const-decl "bool" reals nil )"int" integers nil )"sequence[real]" series "series/" )"T3" function_props nil )"real" reals nil )"bool" convergence_sequences "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"posint" nil )"odd_int" integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"int" countable_convergence nil )"posint" nil )"odd_int" integersnil )"int" countable_convergence nil )nil defined_types nil )nil naturalnumbers nil )nil sigma_nat "reals/" )"even_int" integersnil )"posrat" nil )nil real_props nil )nil reals nil )"posrat" nil )"sequence[real]" series "series/" )"bool" convergence_sequences "analysis/" )nil sequences nil )"[bool, bool -> bool]" booleans nil )"even_int" integersnil )nil real_props nil )nil real_props nil )"bool" function_inverse_def nil )nil function_inverse_def nil )"bool" functions nil )nil function_inverse_defnil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil nil )"countable_set[T]" nil )nil countable_convergence nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )"bool" countable_convergence nil )"set" sets nil ))nil )nil 3351593524"" case "FORALL (X:finite_set[T], Y: countable_set[T], g: [T -> real]): AND convergent?(X)(g) AND convergent?(Y)(g) IMPLIES") "1" (skosimp)"1" (expand "convergent?" )"1" (case-replace "is_finite(X!1)" )"1" (inst - "X!1" "Y!1" "g!1" )"1" (replace -4) (("1" (assert ) nil nil )) nil )) nil )"2" (assert )"2" (case-replace "is_finite(Y!1)" )"1" (inst - "Y!1" "X!1" "g!1" )"1" (assert )"1" (split -2)"1" (rewrite "union_commutative" )"1" (assert ) nil nil )) nil )"2" (rewrite "union_commutative" )"2" (assert ) nil nil )) nil )"3" (hide-all-but (-2 1))"3" (expand "disjoint?" )"3" (rewrite "intersection_commutative" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide -1)"2" (expand "absconvergent?" )"2" "denumerable_enumeration_bij" "X" "X!1" ))"2" "denumerable_enumeration_bij" "X" "Y!1" ))"2" "denumerable_enumeration_bij" "X" "union(X!1,Y!1)" ))"2" "DX" "denumerable_enumeration(X!1)" )"2" "DY" "denumerable_enumeration(Y!1)" )"2" "DXY" "denumerable_enumeration(union(X!1,Y!1))" )"2" "bijective_inverse_exists[nat, (union(X!1, Y!1))]" "f" "DXY" ))"1" expand "exists1" )"1" "1" "CXY" ))"1" "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" "f" "DXY" "g" "CXY" ))"1" "PHI" "LAMBDA (n:nat): IF even?(n) THEN DX(n/2) ELSE DY((n-1)/2) ENDIF" )"1" case "bijective?[nat, (union(X!1, Y!1))](PHI)" )"1" "1" case "forall (a:sequence[real]): convergent(series(a)) => convergent(series(LAMBDA (n:nat): IF even?(n) THEN a(n/2) ELSE 0 ENDIF))" )"1" case "FORALL (a: sequence[real]): LAMBDA (n: nat):IF odd?(n) THEN a((n-1)/2) ELSE 0 ENDIF))") "1" "abs(g!1 o DY)" )"1" "abs(g!1 o DX)" )"1" assert )"1" "series_sum_conv" "a" "(LAMBDA (n: nat): IF even?(n) THEN abs(g!1 o DX)(n / 2)" "b" "(LAMBDA (n: nat): IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)")) "1" assert )"1" "1" "extensionality" "f" "((LAMBDA (n: nat): IF even?(n) THEN abs(g!1 o DX)(n / 2)LAMBDA (n: nat):IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)" "g" "abs(g!1 o PHI)" ))"1" "1" replace "1" "1" "bijective_inverse_exists[nat, (union(X!1, Y!1))]" "f" "PHI" ))"1" expand "exists1" )"1" "1" "PSI" ))"1" "1" "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" "f" "PHI" "g" "PSI" ))"1" "composition_bijective[nat,(union(X!1, Y!1)),nat]" "f2" "PSI" "f1" "DXY" ))"1" "comp_inverse_right_alt[nat, (union(X!1, Y!1))]" "f" "PHI" "g" "PSI" ))"1" "1" "abs_series_bij_conv_abs" "phi" "PSI o DXY" "aa" "abs(g!1 o PHI)" ))"1" assert )"1" "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)" )"1" "1" "1" expand "o" )"1" expand "abs" )"1" "DXY(x!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" expand "absconvergent?" )"3" "3" "abs(abs(o[nat, T, real](g!1, PHI))) = abs(g!1 o PHI)" )"3" "3" "3" expand "abs" )"3" expand "o " )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "+" )"2" expand "PHI" )"2" expand "abs" )"2" expand "o" )"2" "even?(x!1)" )"1" "even_or_odd" "x" "x!1" ))"1" assert )nil nil ))nil )"2" "even_or_odd" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "even?" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "odd?" )"2" "2" assert )"2" replace "2" assert )"2" case "forall (i,j:int):i<j=>i+1<=j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "even?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "convergent" )"2" "2" "l!1" )"2" expand "convergence" )"2" "2" "epsilon!1" )"2" "2" case "FORALL (m: nat): LAMBDA (n: nat):IF odd?(n) THEN a!1((n - 1) / 2) ELSE 0 ENDIF)") "1" "2*n!1+1" )"1" "1" case "even?(i!1)" )"1" expand "even?" )"1" "1" expand "series" )"1" replace "1" "j!1=0" )"1" assert )nil nil )"2" "j!1-1" )"1" "j!1-1" )"1" assert )"1" replace "1" expand "sigma" "1" expand "odd?" "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" "2" expand "odd?" "2" "2" replace "2" "j!1" )"1" assert )"1" "j!1" )"1" expand "series" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "m" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "odd?" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" expand "sigma" "2" replace "2" "2" assert )"2" expand "odd?" )"2" "div_cancel2" "x" "1+j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "odd?" )"3" "3" replace "3" assert )"3" case "forall (i,j:int):i<j=>i+1<=j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "odd?" )"3" "3" assert )"3" assert )"3" case "forall (i,j:int):i<j=>i+1<=j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "odd?" )"3" "3" replace "3" assert )"3" "n!1" )"3" case "forall (i,j:int): i<j => i+1<=j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "convergent" )"2" "2" "l!1" )"2" expand "convergence" )"2" "2" "epsilon!1" )"2" "2" "2*n!1" )"2" "2" case "even?(i!1)" )"1" expand "even?" "1" "1" replace "1" "j!1" )"1" assert )"1" expand "series" )"1" case "forall (m:nat): sigma(0, m, a!1) = sigma(0, 2*m, LAMBDA (n: nat):IF even?(n) THEN a!1(n / 2) ELSE 0 ENDIF)") "1" "j!1" )"1" assert )nil nil ))nil )"2" "2" "m" )"1" expand "sigma" )"1" assert )nil nil ))nil )"2" "2" expand "sigma" "2" expand "sigma" "2" "div_cancel2" "x" "1+j!1" "n0z" "2" ))"2" assert )"2" expand "even?" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" "div_cancel2" "x" "j!2" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" "2" expand "odd?" )"2" "2" replace "2" "j!1" )"1" assert )"1" expand "series" )"1" case "forall (m:nat): sigma(0,m,a!1) = sigma(0,1+2*m,LAMBDA (n:nat): IF even?(n) THEN a!1(n/2) ELSE 0 ENDIF)" )"1" "j!1" )"1" assert )nil nil ))nil )"2" "2" "m" )"1" expand "sigma" )"1" expand "sigma" )"1" assert )"1" expand "even?" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" expand "sigma" "2" replace "2" assert )"2" "2" expand "even?" )"2" "div_cancel2" "x" "1+j!2" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" "div_cancel2" "x" "j!2" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" "div_cancel2" "x" "j!2" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "3" expand "even?" )"3" "3" "div_cancel2" "x" "j!1" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bijective?" )"2" "2" expand "PHI" )"2" "1" expand "injective?" )"1" "1" "even?(x1!1)" )"1" "even?(x2!1)" )"1" "x1!1/2" "x2!1/2" )"1" assert )nil nil )"2" "2" expand "even?" )"2" "2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "even?" )"3" "3" "div_cancel2" "x" "j!1" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "DX(x1!1 / 2)" )"1" assert )nil nil )"2" expand "even?" )"2" "2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "even?(x2!1)" )"1" assert )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "DX(x2!1 / 2)" )"1" assert )nil nil )"2" expand "even?" )"2" "2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "(x1!1 - 1) / 2" "(x2!1 - 1) / 2" )"1" assert )nil nil )"2" "2" rewrite "even_or_odd" )"2" expand "odd?" )"2" "2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "even_or_odd" )"3" expand "odd?" )"3" "3" "div_cancel2" "x" "j!1" "n0z" "2" ))"3" assert )"3" replace "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "union" )"2" expand "member" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "1" "y!1" )"1" "1" "2*x!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "y!1" )"2" "2" "2*x!1+1" )"2" assert )"2" "div_cancel2" "x" "x!1" "n0z" "2" ))"2" replace "2" assert )"2" replace "2" "2" "2" expand "even?" )"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 ))nil ))nil )"3" "3" expand "union" )"3" expand "member" )"3" expand "PHI" )"3" "3" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "even_or_odd" )"2" expand "odd?" )"2" "2" replace -1)"2" assert )"2" assert )"2" "div_cancel1" "x" "j!1" "n0z" "2" ))"2" assert )"2" "n!1" )"2" case "0 <= j!1" )"1" assert )nil nil )"2" "trich_lt" "x" "j!1" "y" "-1" ))"2" "1" assert )nil nil )"2" assert )nil nil )"3" assert )"3" case "forall (i,j:int): i < j IFF i + 1 <= j" )"1" "-1" "j!1" )"1" assert )nil nil ))nil )"2" "2" "2" "1" "1" assert )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 ))nil ))nil )"3" "3" "3" expand "even?" )"3" "3" replace -1)"3" "div_cancel1" "x" "j!1" "n0z" "2" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "convergent?" )"2" (typepred "X!1" )"2" (hide -3)"2" (flatten)"2" (split -3)"1" (lemma "finite_union" ("A" "X!1" "B" "Y!1" ))"1" (propax) nil nil ) ("2" (propax) nil nil ))nil )"2" "denumerable_enumeration_bij" ("X" "Y!1" ))"2" "denumerable_enumeration_bij" "X" "union(X!1,Y!1)" ))"2" "infinite_union" ("S" "X!1" "R" "Y!1" ))"2" (assert )"2" "DXY" "denumerable_enumeration(union(X!1, Y!1))" )"2" "DY" "denumerable_enumeration(Y!1)" )"2" expand "absconvergent?" )"2" "bijective_inverse_exists[nat, (union(X!1, Y!1))]" "f" "DXY" ))"1" expand "exists1" )"1" "1" "CXY" ))"1" "1" "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" "f" "DXY" "g" "CXY" ))"1" "N" "card(X!1)" )"1" "card_bij_inv" "S" "X!1" "N" "N" ))"1" assert )"1" "DX" ))"1" "PHI" "LAMBDA (n:nat): IF n < N THEN DX(n) ELSE DY(n-N) ENDIF" )"1" case "bijective?[nat, (union(X!1, Y!1))](PHI)" )"1" "composition_bijective[nat,(union(X!1, Y!1)),nat]" "f1" "PHI" "f2" "CXY" ))"1" case "absconvergent?(g!1 o PHI)" )"1" "bijective_inverse_exists[nat,(union(X!1,Y!1))]" "f" "PHI" ))"1" expand "exists1" )"1" "1" "PSI" ))"1" "bij_inv_is_bij_alt[nat,(union(X!1,Y!1))]" "f" "PHI" "g" "PSI" ))"1" "composition_bijective[nat,(union(X!1,Y!1)),nat]" "f1" "DXY" "f2" "PSI" ))"1" "abs_series_bij_conv_abs" "aa" "abs(g!1 o PHI)" "phi" "PSI o DXY" ))"1" expand "absconvergent?" "1" assert )"1" "comp_inverse_right_alt[nat, (union(X!1, Y!1))]" "f" "PHI" "g" "PSI" ))"1" "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)" )"1" "1" "1" expand "o " )"1" expand "abs" )"1" "DXY(x!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" expand "absconvergent?" )"3" expand "o " )"3" "abs(abs(LAMBDA (x: nat): g!1(PHI(x)))) = abs(LAMBDA (x: nat): g!1(PHI(x)))" )"3" "3" "3" expand "abs" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "absconvergent?" )"2" "conv_series_shift" "N" "N" ))"2" "abs(g!1 o PHI)" )"2" replace "2" "(LAMBDA n: abs(g!1 o PHI)(n + N)) = abs(g!1 o DY)" )"2" "2" "2" expand "abs" )"2" expand "o " )"2" expand "abs" )"2" expand "PHI" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "bijective?" )"2" "2" "1" expand "injective?" )"1" "1" expand "PHI" )"1" "x1!1<N" )"1" "x2!1 < N" )"1" "x1!1" "x2!1" )"1" assert )nil nil ))nil )"2" assert )"2" "DX(x1!1)" )"2" "DY(x2!1-N)" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "DX(x1!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x2!1<N" )"1" assert )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "DX(x2!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x1!1-N" "x2!1-N" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "union" )"2" expand "member" )"2" "1" "y!1" )"1" "1" "x!1" )"1" expand "PHI" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "y!1" )"2" "2" "N+x!1" )"2" expand "PHI" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "PHI" )"3" expand "union" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp) (("3" (rewrite "countable_union" ) nil nil )) nil ))nil )"4" (skosimp)"4" (assert )"4" (typepred "X!1" )"4" (lemma "finite_countable" ("x" "X!1" ))"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil finite_sets nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil series "series/" )nil finite_sets nil )nil infinite_sets_def nil )"bool" absconv_series "series/" )"[nat -> (X)]" nil )"bool" sets nil )"bool" sets nil )"set" sets nil )nil series "series/" )nil absconv_series "series/" )nil absconv_series"series/" )"[T -> real]" real_fun_ops "reals/" )"sequence[real]" series "series/" )"bool" convergence_sequences "analysis/" )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil sigma_nat "reals/" )nil nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )"set" sets nil ))nil 3351591647"" (skosimp*)"" (rewrite "union_difference" )"" "convergent_difference" ("X" "Y!1" "Y" "X!1" "g" "g!1" ))"" (assert )"" "convergent_disjoint_union" "X" "X!1" "Y" "difference(Y!1,X!1)" "g" "g!1" ))"" (assert )"" (hide-all-but 1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )nil countable_convergence nil )"countable_set[T]" nil )"countable_set[T]" nil )"countable_set[T]" nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"set" sets nil )nil countable_convergencenil )nil countable_convergence nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3351591509"" (skosimp)"" (lemma "add_as_union" ("x" "t!1" "a" "X!1" ))"" "convergent_union" "X" "X!1" "Y" "singleton(t!1)" "g" "g!1" ))"1" (rewrite "convergent_singleton" ) (("1" (assert ) nil nil ))nil )"2" (lemma "finite_countable" ("x" "singleton[T](t!1)" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil )nil countable_convergence nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sets_lemmas nil )nil countable_convergence nil )"countable_set[T]" nil )"(nonempty?)" sets nil )"countable_set[T]" nil )"non_empty_finite_set[T]" countable_convergence nil )nil countable_convergence nil )"bool" sets nil )"(singleton?)" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3351595861"" (skosimp)"" "convergent_subset" "X" "remove(t!1,X!1)" "Y" "X!1" "g" "g!1" ))"" (split -1)"1" (propax) nil nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil )"3" (propax) nil nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_convergence nil )nil countable_convergence nil )"countable_set[T]" nil )"bool" sets nil )"bool" sets nil )"boolean" notequal nil )"(partial_order?[set[T]])" nil ))nil 3395767351"" (skosimp)"" (expand "convergent?" )"" (case-replace "is_finite(X!1)" )"1" (assert ) nil nil )"2" (assert )"2" (name-replace "D" "denumerable_enumeration(X!1)" )"2" (expand "absconvergent?" )"2" (expand "o " )"2" (expand "abs" )"2" "(LAMBDA (n: nat): abs(abs(g!1(D(n)))))=(LAMBDA (n: nat): abs(g!1(D(n))))" )"1" (assert ) nil nil )"2" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil ))nil )"2" (skosimp)"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countable_convergence nil )"bool" absconv_series "series/" )"[T -> nonneg_real]" real_fun_ops "reals/" )"sequence[real]" series "series/" )"[nat -> (X!1)]" countable_convergence nil )"countable_set[T]" countable_convergencenil )"[T -> real]" countable_convergence nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"T3" function_props nil )"[nat -> (X)]" nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )"[T, T -> boolean]" equalities 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 )nil countability "sets_aux/" )"bool" countability "sets_aux/" )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_convergence nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.623Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
