Quelle sigma_countable.prf
Sprache: Lisp
(sigma_countablenil 3322368543"" (skosimp)"" (lemma "nonempty_card" ("S" "X!1" ))"1" (expand "nonempty?" ) (("1" (assert ) nil nil )) nil )"2" (propax) nil nil ))nil ))nil )nil sigma_countable nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_sets nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil ))nil 3322368543"" (skosimp)"" (lemma "nonempty_card" ("S" "X!1" ))"1" (expand "nonempty?" ) (("1" (assert ) nil nil )) nil )"2" (propax) nil nil ))nil ))nil )nil sigma_countable nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_sets nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil ))nil 3322368684"" (skosimp)"" (skosimp) (("" (typepred "y!1" ) (("" (assert ) nil nil )) nil ))nil ))nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props 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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sigma_countable nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )nil nat_types nil ))nil 3322368684"" (skosimp) (("" (rewrite "countably_infinite_def" ) nil nil )) nil )nil countable_props"sets_aux/" )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )nil sigma_countable nil ))nil 3405668249"" (skosimp)"" (typepred "f!1" )"" (expand "convergent?" )"" (assert )"" (expand "o" )"" "FF" "LAMBDA (x: nat): f!1(denumerable_enumeration(X!1)(x))" )"1" (expand "absconvergent?" )"1" (hide 1 2)"1" "absconvergent_series_is_convergent" "x" "FF" ))"1" (expand "convergent?" )"1" (propax) nil nil )) nil )"2" (expand "absconvergent?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (assert )"2" (typepred "X!1" )"2" (rewrite "countably_infinite_def" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countable_convergence 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 sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans 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 )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"[nat -> (X)]" nil )nil absconv_series"series/" )nil sequences nil )nil "series/" )"bool" absconv_series "series/" )nil countable_props"sets_aux/" )"T3" function_props nil )"bool" convergence_sequences "analysis/" ))nil ))nil 3322640566 ("" (grind) nil nil )"bool" functions nil )"bool" functions nil )"bool" functions nil )nil sigma_countable nil )"[nat -> (X)]" nil )"T3" function_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"sequence[real]" series "series/" )"real" sigma "reals/" )"sequence[real]" series "series/" )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"bool" absconv_series "series/" )"bool" countable_convergence nil )"int" integers nil )"real" reals nil )"finite_set[T]" sigma_countablenil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil 3322641284"" (skosimp)"" (expand "sigma" ) (("" (rewrite "emptyset_is_empty?" ) nil nil ))nil ))nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" sigma_countablenil )"real" sigma_countable nil )nil sigma_countable nil )"set" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sets_lemmas nil ))nil 3508520761"" (skosimp)"" (typepred "F!1" )"" (expand "convergent?" ) (("" (propax) nil nil )) nil )) nil ))nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" countable_convergence nil ))nil )nil 3322640566"" (skosimp*)"" (typepred "F!1" )"" (lemma "finite_countable" ("x" "F!1" ))"" (propax) nil nil )) nil ))nil ))nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil countable_props "sets_aux/" ))nil 3508521550"" (skosimp)"" (assert )"" (typepred "n!1" )"" (replace -2)"" (assert )"" (typepred "F!1" )"" (lemma "nonempty_card" ("S" "F!1" ))"" (expand "nonempty?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil sigma_countable nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"int" integers 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil ))nil )nil 3322640566"" (skosimp)"" (typepred "F!1" )"" (expand "convergent?" ) (("" (propax) nil nil )) nil )) nil ))nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )"bool" countable_convergence nil ))nil 3322640566"" (skosimp)"" (assert )"" (typepred "n!1" )"" (replace -2)"" (assert )"" (typepred "F!1" )"" (lemma "nonempty_card" ("S" "F!1" ))"" (expand "nonempty?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil sigma_countable nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil ))nil 3508520831"" (skosimp*) (("" (replace -1) (("" (assert ) nil nil )) nil )) nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil )nil 3322640566"" (skosimp)"" (typepred "F!1" )"" (rewrite "empty_card" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil finite_sets nil ))nil 3322640566"" (skosimp*) (("" (replace -1) (("" (assert ) nil nil )) nil )) nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil 3322641469"" (skosimp)"" (assert )"" (expand "sigma" 1 1) (("" (propax) nil nil )) nil )) nil ))nil )"int" integers nil )"real" sigma_countable nil ))nil 3351597966 ("" (grind) nil nil )"bool" functions nil )"bool" functions nil )"bool" functions nil )nil sigma_countable nil )"[nat -> (X)]" nil )"T3" function_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"sequence[real]" series "series/" )"real" sigma "reals/" )"sequence[real]" series "series/" )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"bool" absconv_series "series/" )"bool" countable_convergence nil )"int" integers nil )"real" reals nil )"non_empty_finite_set[T]" sigma_countable nil ))nil ))nil 3351597967"" (skosimp)"" (lemma "sigma_finite" ("F" "singleton(t!1)" "g" "g!1" ))"" (rewrite "card_singleton" )"" (assert )"" (replace -1)"" (hide -1)"" (expand "sigma" )"" (expand "o " )"" "finite_enumeration(singleton(t!1))(0)" )"" (expand "singleton" )"" (assert )"" (replace -1)"" (expand "sigma" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))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 )"(singleton?)" sets nil )"bool" sets nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_countable nil )nil sigma_countable nil )"non_empty_finite_set[T]" sigma_countable nil )"even_int" integersnil )"T3" function_props nil )"real" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil nat_types nil )"[below[card(X)] -> (X)]" nil )"real" sigma "reals/" )nil finite_sets nil ))nil 3322642826"" (skosimp)"" (typepred "f!1" )"" (expand "convergent?" )"" (typepred "X!1" )"" (rewrite "countably_infinite_def" )"" (flatten)"" (assert )"" "absconvergent_series_is_convergent" "x" "(o[nat, T, real] ")) "" (assert )"" (expand "convergent?" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )"bool" countable_convergence 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 sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[nat -> (X)]" nil )"T3" function_props nil )nil absconv_series"series/" )"bool" absconv_series "series/" )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil "series/" )nil countable_props"sets_aux/" )"bool" convergence_sequences "analysis/" ))nil 3322642960"" (skosimp)"" (typepred "X!1" )"" (expand "sigma" 1 1)"" (lemma "infinite_countably_infinite" )"" (inst - "X!1" )"" (assert )"" (lift-if 2)"" (case-replace "empty?(X!1)" )"1" (hide 2)"1" (expand "is_countably_infinite" )"1" (skosimp)"1" (typepred "f!2" )"1" "bijective_inverse_exists[(X!1),nat]" "f" "f!2" ))"1" (expand "exists1" )"1" "1" "gg" ))"1" expand "empty?" )"1" "gg(0)" )"1" expand "member" )"1" (propax) 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 countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil countable_props"sets_aux/" )"bool" sets nil )"bool" functions 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" exists1 nil )"bool" sets nil )nil function_inverse_defnil )"real" sigma_countable nil ))nil 3323139930"" (skosimp)"" (typepred "x!1" )"" (expand "nonempty_countable?" ) (("" (flatten) nil nil ))nil ))nil ))nil )nil sigma_countable nil )"bool" sigma_countable nil )set type-eq-decl nil sets nil )nil sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3323139930"" (skosimp)"" (typepred "x!1" )"" (expand "nonempty_countable?" ) (("" (flatten) nil nil ))nil ))nil ))nil )nil sigma_countable nil )"bool" sigma_countable nil )set type-eq-decl nil sets nil )nil sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3323139931"" (skosimp*)"" (typepred "f!1" )"" (lemma "convergent_subset" )"" (inst - "X!1" "union(X!1, Y!1)" "f!1" )"" (split)"1" (propax) nil nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" countable_convergence 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 sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"countable_set[T]" nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil )nil countable_convergence nil ))nil 3323139931"" (skosimp)"" "sigma_disjoint_union_TCC1" "X" "Y!1" "Y" "X!1" "f" "f!1" ))"1" (assert )"1" (hide 2)"1" (expand "disjoint?" )"1" (rewrite "intersection_commutative" ) nil nil )) nil ))nil ))nil )"2" (typepred "f!1" )"2" (hide -2 2) (("2" (rewrite "union_commutative" ) nil nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" countable_convergence 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 sigma_countable nil )nil sigma_countable nil )"countable_set[T]" nil )nil sets_lemmas nil )"bool" sets nil )"countable_set[T]" nil )nil sets_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3351662957"" case "FORALL (X:finite_set[T], Y:countably_infinite_set[T], f:(convergent?(union(X, Y)))): ") "1" (skosimp)"1" (typepred "X!1" )"1" (typepred "Y!1" )"1" (case "is_finite(X!1)" )"1" (case "is_finite(Y!1)" )"1" (hide -5 -3 -4)"1" (name "NX" "card(X!1)" )"1" (name "NY" "card(Y!1)" )"1" (case-replace "X!1=emptyset[T]" )"1" (rewrite "union_commutative" 1)"1" (rewrite "union_empty" )"1" (rewrite "sigma_empty" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (case-replace "Y!1=emptyset[T]" )"1" (rewrite "sigma_empty" )"1" (rewrite "union_empty" )"1" (assert ) nil nil )) nil ))nil )"2" (rewrite "emptyset_is_empty?" 1 :dir rl)"2" rewrite "emptyset_is_empty?" 2 :dir rl)"2" (typepred "f!1" )"2" expand "sigma" )"2" assert )"2" "finite_union[T]" )"2" "X!1" "Y!1" )"2" assert )"2" "empty?(union(X!1, Y!1))" )"1" "1" expand "union" )"1" expand "empty?" )"1" "1" expand "member" )"1" "x!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "card_disj_union" "A" "X!1" "B" "Y!1" ))"2" assert )"2" replace -1)"2" replace -4)"2" replace -5)"2" "series_bijection" )"2" "PHI" "LAMBDA (n:[below[card(union(X!1,Y!1))]]): IF n < card(X!1) THEN finite_enumeration(X!1)(n) ELSE finite_enumeration(Y!1)(n-card(X!1)) ENDIF" )"1" "finite_enumeration_bij" "X" "union(X!1,Y!1)" ))"1" "finite_enumeration_bij" "X" "X!1" ))"1" "finite_enumeration_bij" "X" "Y!1" ))"1" "FX" "finite_enumeration(X!1)" )"1" "FY" "finite_enumeration(Y!1)" )"1" "FXY" "finite_enumeration(union(X!1,Y!1))" )"1" case "bijective?[below[card[T](union(X!1,Y!1))],(union(X!1,Y!1))](PHI)" )"1" "bijective_inverse_exists[below[card[T](union(X!1, Y!1))], (union(X!1, Y!1))]" "f" "FXY" ))"1" expand "exists1" )"1" "1" "CXY" ))"1" "1" expand "series" )"1" "1" "sigma_bijection[below[card(union(X!1, Y!1))]]" "low" "0" "high" "NX+NY-1" "F" "f!1 o FXY" ))"1" "1" "bij_inv_is_bij_alt[below[card[T](union(X!1, Y!1))], (union(X!1, Y!1))]" "f" "FXY" "g" "CXY" ))"1" "composition_bijective[below[card[T](union(X!1,Y!1))],(union(X!1,Y!1)),below[card[T](union(X!1, Y!1))]]" "f1" "PHI" "f2" "CXY" ))"1" "CXY o PHI" )"1" "sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY)] ") "1" "sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY)] ") "1" replace "1" "1" "nonempty_card" "S" "X!1" ))"1" "nonempty_card" "S" "Y!1" ))"1" expand "nonempty?" )"1" assert )"1" case "forall (n:nat): n <= NY-1 => sigma[below[card(union(X!1, Y!1))]](0, NX + n, f!1 o PHI) = ") "1" "NY-1" )"1" assert )nil nil ))nil )"2" "2" "n" )"1" assert )"1" expand "sigma" "1" expand "sigma" "1" expand "PHI" "1" expand "FY" "1" expand "o" "1" expand "o" "1" assert )"1" replace "1" assert )"1" "1" case "forall (n:nat): n<=NX-1 => sigma(0, n, f!1 o PHI) = ") "1" "NX-1" )"1" assert )"1" expand "sigma" "1" nil nil ))nil ))nil ))nil )"2" "2" "n" )"1" expand "sigma" )"1" expand "FX" )"1" expand "PHI" )"1" expand "o " )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "sigma" "2" assert )"2" replace "2" assert )"2" expand "o" )"2" expand "PHI" )"2" expand "FX" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "sigma" "2" expand "sigma" "2" assert )"2" replace "2" assert )"2" expand "PHI" "2" expand "o" )"2" expand "FY" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )"4" "4" assert )nil nil ))nil ))nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil )"7" "7" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil )"7" "7" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "forall (n:nat): n <= NX + NY - 1 => sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY)] ") "1" "NX+NY-1" )"1" assert )nil nil )"2" "nonempty_card" "S" "X!1" ))"2" "nonempty_card" "S" "Y!1" ))"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "n" )"1" expand "sigma" )"1" expand "restrict" )"1" expand "sigma" "1" nil nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" expand "restrict" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"2" "2" "comp_inverse_right_alt[below[card[T](union(X!1, Y!1))], (union(X!1, Y!1))]" "f" "FXY" "g" "CXY" ))"2" "2" "nonempty_card" "S" "X!1" ))"2" "nonempty_card" "S" "Y!1" ))"2" expand "nonempty?" )"2" assert )"2" "2" case "forall (n:nat): n <= NX-1+NY => sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY)] ") "1" "NX-1+NY" )"1" assert )nil nil ))nil )"2" "2" expand "restrict" )"2" expand "o " )"2" "n" )"1" expand "sigma" )"1" "PHI(0)" )"1" assert )"1" expand "sigma" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" assert )"2" replace "2" assert )"2" "2" "PHI(1+j!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" expand "PHI" )"5" case "x!1 < card(X!1)" )"1" assert )"1" "finite_enumeration(X!1)(x!1)" )"1" expand "union" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "union" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" "6" assert )nil nil ))nil )"7" "7" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"2" "1" "1" expand "o" )"1" "CXY(PHI(x1!1))" )"1" assert )nil nil )"2" "2" expand "union" )"2" expand "member" )"2" "2" expand "PHI" )"2" "x1!1 < card(X!1)" )"1" expand "finite_enumeration" )"1" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bijective?" )"2" "2" expand "o " )"2" "1" expand "restrict" )"1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" "x1!1" "x2!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" expand "restrict" )"2" "2" "y!1" )"2" "y!1" )"2" "2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil ))nil )"2" "nonempty_card" "S" "X!1" ))"2" "nonempty_card" "S" "Y!1" ))"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "nonempty_card" "S" "X!1" ))"2" "nonempty_card" "S" "Y!1" ))"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil )"3" assert )"3" assert )"3" "nonempty_card" "S" "union(X!1, Y!1)" ))"3" expand "nonempty?" )"3" nil nil ))nil ))nil ))nil ))nil )"4" "4" "x!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "bijective?" )"2" "2" expand "PHI" )"2" expand "FY" )"2" expand "FX" )"2" "1" expand "injective?" )"1" "1" "x1!1 < card(X!1)" )"1" "x2!1 < card(X!1)" )"1" "x1!1" "x2!1" )"1" assert )nil nil ))nil )"2" assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "finite_enumeration(X!1)(x1!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x2!1<card(X!1)" )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "finite_enumeration(X!1)(x2!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x1!1-card(X!1)" "x2!1-card(X!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" case "X!1(y!1)" )"1" "y!1" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "disjoint?" )"2" expand "intersection" )"2" "y!1" )"2" expand "union" )"2" expand "member" )"2" assert )"2" "y!1" )"2" "2" "x!1+card(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 )"3" "3" "x1!1" )"3" expand "PHI" "3" expand "union" "3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (inst - "X!1" "Y!1" "f!1" )"1" (assert ) nil nil )"2" (rewrite "countably_infinite_def" ) nil nil ))nil ))nil )"2" (case "is_finite(Y!1)" )"1" (inst - "Y!1" "X!1" "f!1" )"1" (rewrite "union_commutative" -4)"1" (assert )"1" (hide-all-but (-4 2))"1" (expand "disjoint?" )"1" (rewrite "intersection_commutative" ) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "union_commutative" )"2" (typepred "f!1" ) (("2" (propax) nil nil )) nil ))nil )"3" (rewrite "countably_infinite_def" ) nil nil ))nil )"2" (assert )"2" (hide -3)"2" (typepred "f!1" )"2" "convergent_subset" "X" "X!1" "Y" "union(X!1,Y!1)" "g" "f!1" ))"2" "convergent_subset" "X" "Y!1" "Y" "union(X!1,Y!1)" "g" "f!1" ))"2" (assert )"2" (split -1)"1" (split -2)"1" expand "sigma" )"1" expand "convergent?" )"1" "infinite_union_right" "S" "X!1" "Inf" "Y!1" ))"1" "infinite_nonempty" "x" "X!1" ))"1" "infinite_nonempty" "x" "Y!1" ))"1" "infinite_nonempty" "x" "union(X!1,Y!1)" ))"1" expand "nonempty?" )"1" assert )"1" "denumerable_enumeration_bij" "X" "X!1" ))"1" "denumerable_enumeration_bij" "X" "Y!1" ))"1" "denumerable_enumeration_bij" "X" "union(X!1,Y!1)" ))"1" "DXY" "denumerable_enumeration(union(X!1,Y!1))" )"1" "DX" "denumerable_enumeration(X!1)" )"1" "DY" "denumerable_enumeration(Y!1)" )"1" case "forall (n:nat): even?(n) IMPLIES integer_pred(n / 2) & n/2 >= 0" )"1" case "forall (n:nat): NOT even?(n) IMPLIES integer_pred((n-1) / 2) & (n-1)/2 >= 0" )"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" "bijective_inverse_exists[nat, (union(X!1, Y!1))]" "f" "DXY" ))"1" expand "exists1" )"1" "1" "1" "CXY" ))"1" "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" "f" "DXY" "g" "CXY" ))"1" "comp_inverse_right_alt[nat, (union(X!1, Y!1))]" "f" "DXY" "g" "CXY" ))"1" "composition_bijective[nat,(union(X!1, Y!1)),nat]" "f1" "PHI" "f2" "CXY" ))"1" "abs_series_bij_limit" "a" "f!1 o DXY" "phi" "CXY o PHI" ))"1" "1" "extensionality" "f" "f!1 o DXY o (CXY o PHI)" "g" "f!1 o PHI" ))"1" "1" replace "1" replace "1" case "forall (x:real): convergence(series(f!1 o DX),x) IFF convergence(series(LAMBDA (n:nat): if even?(n) then f!1(DX(n/2)) else 0 endif),x)" )"1" "limit(series(f!1 o DX))" )"1" rewrite "limit_equiv" "1" "absconvergent_series_is_convergent" "x" "f!1 o DX" ))"1" assert )"1" case "forall (x:real): convergence(series(f!1 o DY),x) IFF convergence(series(LAMBDA (n:nat):IF odd?(n) THEN f!1(DY((n-1)/2)) ELSE 0 ENDIF),x)" )"1" "limit(series(f!1 o DY))" )"1" rewrite "limit_equiv" "1" "absconvergent_series_is_convergent" "x" "f!1 o DY" ))"1" assert )"1" "cnv_seq_sum" "s1" "series(LAMBDA (n: nat): IF even?(n) THEN f!1(DX(n / 2)) ELSE 0 ENDIF)" "l1" "limit(series(f!1 o DX))" "s2" "series(LAMBDA (n: nat): IF odd?(n) THEN f!1(DY((n - 1) / 2))" "l2" "limit(series(f!1 o DY))" ))"1" assert )"1" rewrite "series_sum" "1" "extensionality" "f" "(LAMBDA (n: nat): IF even?(n) THEN f!1(DX(n / 2)) ELSE 0 ENDIF)LAMBDA (n: nat):IF odd?(n) THEN f!1(DY((n - 1) / 2))" "g" "f!1 o PHI" ))"1" "1" replace "1" rewrite "limit_equiv" nil nil ))nil )"2" "2" expand "+" )"2" expand "o" )"2" expand "PHI" )"2" "2" "even?(x!1)" )"1" "even_iff_not_odd" "x" "x!1" ))"1" assert )nil nil ))nil )"2" "even_iff_not_odd" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "series" )"2" case "forall (n:nat): sigma(0, n, f!1 o DY) = sigma(0,2*n+1 , LAMBDA (n: nat):IF odd?(n) THEN f!1(DY((n - 1) / 2))") "1" case "FORALL (n: nat): LAMBDA (n: nat):IF odd?(n) THEN f!1(DY((n - 1) / 2)) ELSE 0 ENDIF))IF n = 0 THEN 0 ELSE sigma(0, n / 2-1, f!1 o DY) ENDIF") "1" case "FORALL (n: nat): LAMBDA (n: nat):IF odd?(n) THEN f!1(DY((n - 1) / 2)) ELSE 0 ENDIF))") "1" expand "convergence" )"1" "1" "1" "epsilon!1" )"1" "1" "2*n!1+1" )"1" "1" case "even?(i!1)" )"1" "i!1" )"1" assert )"1" replace "1" "i!1/2-1" )"1" assert )"1" "1" expand "even?" )"1" nil nil ))nil ))nil ))nil )"2" "i!1=0" )"1" assert )nil nil )"2" expand "even?" )"2" "2" replace "2" assert )"2" "2 * j!1 / 2 = j!1" )"1" assert )nil nil )"2" "div_cancel2" "x" "j!1" "n0z" "2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "even_iff_not_odd" "2" "i!1" )"2" assert )"2" replace "2" "2" "(i!1-1)/2" )"1" "1" nil nil )"2" assert )nil nil ))nil )"2" expand "odd?" )"2" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "epsilon!1" )"2" "2" "2*n!1+1" )"2" "2" "i!1" )"2" "2*i!1+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "odd?" "2" "2" replace "2" assert )"2" "j!1" )"1" assert )nil nil )"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 ))nil )"3" "3" "3" assert )"3" case "forall (i,j:int):i<j=>i+1<=j" )"1" assert )"1" expand "odd?" )"1" "1" replace "1" assert )"1" "1" "trichotomy" "x" "j!1" ))"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" expand "odd?" )"4" "4" replace "4" assert )"4" "trichotomy" "x" "j!1" ))"4" "1" assert )nil nil )"2" assert )nil nil )"3" case "forall (i,j:int): i< j => i+1<=j" )"1" "j!1" "0" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!1=0" )"1" expand "sigma" )"1" expand "odd?" )"1" expand "sigma" "1" nil nil ))nil ))nil ))nil )"2" assert )"2" expand "even?" )"2" "2" replace "2" "j!1-1" )"1" expand "sigma" "1" assert )"1" "even_iff_not_odd" "x" "2*j!1" ))"1" expand "even?" "1" "1" "1" "1" assert )nil nil )"2" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" assert )"3" "n!1" )"3" replace "3" assert )"3" case "forall (i,j:int):i<j=>i+1<=j" )"1" "0" "j!1" )"1" assert )"1" "div_cancel2" "x" "j!1" "n0z" "2" ))"1" assert )"1" "2 * j!1 / 2 - 1 = j!1-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "odd?" )"4" "4" replace "4" assert )"4" 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 )"2" "2" expand "o " )"2" "n" )"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" expand "odd?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "odd?" )"3" "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 )"3" expand "odd?" )"3" "3" case "forall (i,j:int):i<j=>i+1<=j" )"1" "1" "-1" "j!1" )"1" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" "2" "2" expand "series" )"2" case "FORALL (n:nat):sigma(0,2*n,(LAMBDA (n: nat): IF even?(n) THEN f!1(DX(n / 2)) ELSE 0 ENDIF))") "1" case "FORALL (n: nat): even?(n) => LAMBDA (n: nat):IF even?(n) THEN f!1(DX(n / 2)) ELSE 0 ENDIF))") "1" case "FORALL (n: nat): LAMBDA (n: nat):IF even?(n) THEN f!1(DX(n / 2)) ELSE 0 ENDIF))") "1" expand "convergence" )"1" "1" "1" "epsilon!1" )"1" "1" "2*n!1" )"1" "1" case "even?(i!1)" )"1" expand "even?" "1" "1" "j!1" )"1" assert )"1" "i!1" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" "2" "i!1" )"2" assert )"2" replace "2" "(i!1-1)/2" )"1" "1" nil nil )"2" assert )"2" "2" expand "odd?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "odd?" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "epsilon!1" )"2" "2" case "even?(n!1)" )"1" expand "even?" "1" "1" replace "1" "j!1" )"1" "1" "2*i!1" )"1" assert )"1" "2*i!1" )"1" assert )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" "1" "1+2*i!1" )"1" assert )"1" "1+2*i!1" )"1" "1" assert )nil nil )"2" expand "odd?" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "odd?" )"2" "2" replace "2" "j!1" )"1" assert )"1" expand "sigma" "1" replace "1" assert )"1" case "forall (i,j:int):i<j=>i+1<=j" )"1" "-1" "j!1" )"1" assert )"1" "1" assert )"1" rewrite "even_or_odd" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"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 )"3" expand "odd?" )"3" "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 )"4" expand "even?" )"4" "4" 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 )"2" "2" expand "even?" "2" "2" "j!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" assert )nil nil ))nil ))nil )"4" expand "even?" )"4" "4" assert )nil nil ))nil ))nil ))nil )"2" "2" "n" )"1" expand "o" )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "sigma" "2" expand "o" )"2" assert )"2" expand "sigma" "2" replace "2" assert )"2" "2" "1" expand "even?" )"1" nil nil ))nil )"2" rewrite "even_or_odd" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" expand "even?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "even?" )"3" nil nil ))nil ))nil ))nil ))nil )"2" expand "o" )"2" "2" "PHI(x!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "absconvergent?" )"2" nil nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "bijective?" )"2" expand "PHI" )"2" "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" "x2!1" )"2" assert )nil nil ))nil )"3" "x1!1" )"3" assert )nil nil ))nil ))nil )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" assert )"2" "DX(x1!1/2)" )"1" assert )nil nil )"2" "x1!1" )"2" assert )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" "x2!1" )"1" assert )"1" "DX(x2!1 / 2)" )"1" "DX(x2!1 / 2)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x1!1" )"2" "x2!1" )"2" assert )"2" "2" "(x1!1 - 1) / 2" "(x2!1 - 1) / 2" )"1" assert )nil nil )"2" assert )nil nil )"3" assert )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" "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" "2" assert )"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 )"3" expand "PHI" )"3" expand "union" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" "n!1" )"3" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" rewrite "even_or_odd" )"2" expand "odd?" )"2" "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 ))nil ))nil )"2" "2" expand "even?" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "X!1" )"2" (typepred "Y!1" )"2" (typepred "f!1" )"2" (case-replace "X!1=emptyset[T]" )"1" (rewrite "sigma_empty" 1)"1" (rewrite "union_commutative" 1)"1" (rewrite "union_empty" 1)"1" (assert ) nil nil )) nil ))nil ))nil )"2" (rewrite "emptyset_is_empty?" 1 :dir rl)"2" (rewrite "countably_infinite_def" )"2" (flatten)"2" "infinite_union_right" "S" "X!1" "Inf" "Y!1" ))"2" (expand "convergent?" )"2" (assert )"2" (expand "sigma" )"2" assert )"2" "infinite_nonempty[T]" "x" "Y!1" ))"2" "infinite_nonempty[T]" "x" "union(X!1,Y!1)" ))"2" expand "nonempty?" )"2" assert )"2" "convergent_subset" "X" "Y!1" "Y" "union(X!1,Y!1)" "g" "f!1" ))"2" "1" expand "convergent?" )"1" "denumerable_enumeration_bij" "X" "union(X!1,Y!1)" ))"1" "denumerable_enumeration_bij" "X" "Y!1" ))"1" "finite_enumeration_bij" "X" "X!1" ))"1" "DX" "finite_enumeration(X!1)" )"1" "DY" "denumerable_enumeration(Y!1)" )"1" "DXY" "denumerable_enumeration(union(X!1,Y!1))" )"1" "nonempty_card" "S" "X!1" ))"1" expand "nonempty?" )"1" "1" "PHI" "LAMBDA (n:nat): IF n<card(X!1) THEN DX(n) ELSE DY(n-card(X!1)) ENDIF" )"1" case "bijective?[nat, (union(X!1, Y!1))](PHI)" )"1" "bijective_inverse_exists[nat, (union(X!1, Y!1))]" "f" "DXY" ))"1" expand "exists1" )"1" "1" "1" "CXY" ))"1" "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" "f" "DXY" "g" "CXY" ))"1" "comp_inverse_right_alt[nat, (union(X!1, Y!1))]" "f" "DXY" "g" "CXY" ))"1" "composition_bijective[nat,(union(X!1, Y!1)),nat]" "f1" "PHI" "f2" "CXY" ))"1" "abs_series_bij_limit" "a" "f!1 o DXY" "phi" "CXY o PHI" ))"1" "1" "extensionality" "f" "f!1 o DXY o (CXY o PHI)" "g" "f!1 o PHI" ))"1" "1" replace "1" replace "1" "limit_series_shift" "a" "f!1 o PHI" "pn" "card(X!1)" ))"1" "1" replace "1" expand "o" "1" expand "PHI" "1" "1" case "forall (n:nat): n < card(X!1) => sigma(0,n, LAMBDA (x: nat):IF x < card(X!1) THEN f!1(DX(x))LAMBDA (x: below[card(X!1)]): f!1(DX(x)))") "1" "card(X!1)-1" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "2" "n" )"1" expand "sigma" )"1" assert )"1" expand "sigma" "1" nil nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" nil nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" nil nil )"5" "5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "abs_series_bij_conv" "a" "f!1 o DXY" "phi" "CXY o PHI" ))"2" replace "2" expand "absconvergent?" )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" "2" "PHI(x!1)" )"1" "1" nil nil ))nil )"2" expand "PHI" )"2" assert )"2" expand "union" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "absconvergent?" )"2" nil nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "bijective?" )"2" "2" expand "PHI" )"2" "1" expand "injective?" )"1" "1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "x1!1 < card(X!1)" )"1" "x2!1 < card(X!1)" )"1" "x1!1" "x2!1" )"1" assert )nil nil ))nil )"2" assert )"2" "DX(x1!1)" )"2" assert )nil nil ))nil ))nil ))nil )"2" "x2!1 < card(X!1)" )"1" "DX(x2!1)" )"1" assert )nil nil ))nil )"2" assert )"2" "x1!1 - card(X!1)" "x2!1 - card(X!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "union" )"2" expand "empty?" )"2" expand "member" )"2" "1" "y!1" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "y!1" )"2" "2" "x!1+card(X!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PHI" )"3" expand "union" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" expand "convergent?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp)"3" (typepred "f!1" )"3" "convergent_subset" "g" "f!1" "X" "Y!1" "Y" "union(X!1,Y!1)" ))"3" (assert )"3" (hide-all-but 1) (("3" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (skosimp)"4" (typepred "f!1" )"4" "convergent_subset" "g" "f!1" "X" "X!1" "Y" "union(X!1,Y!1)" ))"4" (assert )"4" (hide-all-but 1)"4" (typepred "Y!1" )"4" (rewrite "countably_infinite_def" )"4" (expand "subset?" )"4" (expand "union" )"4" (expand "member" ) (("4" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(union(X!1, Y!1))" sigma_countable nil )"nat" sigma_countable nil )"countably_infinite_set[T]" sigma_countablenil )nil series "series/" )nil integers nil )nil integers nil )nil series_lems "series/" )"[nat -> T]" sigma_countable nil )"finite_set[T]" sigma_countable nil )"infinite_set[T]" nil )"countably_infinite_set[T]" sigma_countable nil )nil sets_lemmas nil )"countable_set[T]" nil )"(convergent?(union(X!1, Y!1)))" nil )nil countable_convergence nil )"(partial_order?[set[T]])" nil )nil infinite_sets_def nil )"[nat -> (X)]" nil )"rat" rationals nil )"int" sigma_countable nil )"int" sigma_countable nil )"int" sigma_countable nil )nil naturalnumbers nil )"nat" sigma_countable nil )"int" sigma_countable nil )"int" sigma_countable nil )"real" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil "series/" )"bool" absconv_series "series/" )nil absconv_series"series/" )"bool" integers nil )"[T -> real]" real_fun_ops "reals/" )nil naturalnumbers nil )"[nat -> T]" sigma_countable nil )nil series "series/" )nil convergence_ops "analysis/" )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"odd_int" integersnil )"int" sigma_countable nil )nil real_types nil )"bool" reals nil )nil real_types nil )"odd_int" integers nil )"nat" sigma_countable nil )"rat" rationals nil )nil reals nil )nil real_props nil )"odd_int" integers nil )"even_int" integersnil )"real" reals nil )"int" sigma_countable nil )"[numfield -> numfield]" number_fields nil )nil sigma_nat "reals/" )nil real_axioms nil )"rat" rationals nil )"posrat" nil )"even_int" integersnil )nil convergence_ops "analysis/" )"bool" convergence_sequences "analysis/" )"[bool, bool -> bool]" booleans nil )nil functions nil )nil sequences nil )nil series_lems "series/" )"nonneg_rat" nil )"(union(X!1, Y!1))" sigma_countable nil )"nat" sigma_countable nil )"nat" sigma_countable nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" integers nil )"nonneg_rat" nil )nil nil )nil infinite_sets_def nil )nil infinite_sets_def nil )"bool" sets nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"set" sets nil )"finite_set[T]" sigma_countablenil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )nil sets_lemmas nil )nil sigma_countable nil )"countable_set[T]" nil )nil sets_lemmas nil )nil sets_lemmas nil )"int" integers nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )"bool" reals nil )nil nat_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[below[card(X)] -> (X)]" nil )"[numfield, numfield -> numfield]" number_fields nil )"set" sets nil )"(union(X!1, Y!1))" sigma_countable nil )nil function_inverse_defnil )nil function_props nil )"bool" functions nil )"bool" functions nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" sets nil )"(total_order?[real])" nil )nil defined_types nil )nil naturalnumbers nil )"[below[card(X!1)] -> (X!1)]" sigma_countablenil )"posint" nil )"posint" nil )"[below[card(Y!1)] -> (Y!1)]" sigma_countablenil )"(strict_total_order?[real])" real_props nil )nil function_inverse_def nil )"R" restrict nil )"[below[card(union(X!1, Y!1))] -> T]" nil )"[(union(X!1, Y!1)) -> below[card[T](union(X!1, Y!1))]]" nil )nil sigma_bijection nil )"{n: nat | n = Card(Y!1)}" sigma_countablenil )"{n: nat | n = Card(X!1)}" sigma_countablenil )"countable_set[T]" sigma_countable nil )"countable_set[T]" sigma_countable nil )"int" integers nil )"bool" function_inverse_def nil )nil function_inverse_def nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"T3" function_props nil )nil sigma_bijection nil )"sequence[real]" series "series/" )"bool" exists1 nil )"bool" functions nil )nil finite_enumeration nil )nil sigma_bijection_nat nil )"nonneg_int" nil )nil finite_sets nil )nil countable_props"sets_aux/" )NOT const-decl "[bool -> bool]" booleans nil )"infinite_set[T]" nil )"countably_infinite_set[T]" sigma_countable nil )"real" reals nil )nil sigma_countable 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" countability "sets_aux/" )nil countability "sets_aux/" )"bool" countable_convergence nil )"set" sets nil )"[bool, bool -> bool]" booleans nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"real" sigma_countable nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3351659919"" (skosimp)"" "convergent_subset" "X" "X!1" "Y" "union(X!1,Y!1)" "g" "f!1" ))"" (split)"1" (propax) nil nil )"2" (hide 2) (("2" (grind) nil nil )) nil )"3" (typepred "f!1" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )nil sigma_countable nil )"bool" countable_convergence 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 )"countable_set[T]" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil ))nil 3351659919"" (skosimp)"" (typepred "f!1" )"" "convergent_subset" "X" "Y!1" "Y" "union(X!1,Y!1)" "g" "f!1" ))"" (assert )"" (hide-all-but 1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"set" sets nil )"bool" countable_convergence 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 sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )nil countable_convergence nil )"countable_set[T]" nil ))nil ))nil 3351659919"" (skosimp)"" (typepred "f!1" )"" "convergent_subset" "X" "intersection(X!1,Y!1)" "Y" "union(X!1,Y!1)" "g" "f!1" ))"" (assert )"" (hide-all-but 1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"set" sets nil )"bool" countable_convergence 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 sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )"set" sets nil )nil countable_convergence nil )"countable_set[T]" nil )"countable_set[T]" nil ))nil ))nil 3351661433"" (skosimp)"" (rewrite "union_difference" )"" case "union(difference(Y!1, X!1), intersection(X!1, Y!1)) = Y!1" )"1" "sigma_disjoint_union" "X" "difference(Y!1, X!1)" "Y" "intersection(X!1, Y!1)" "f" "f!1" ))"1" "disjoint?(difference(Y!1, X!1), intersection(X!1, Y!1))" )"1" (replace -3 -2)"1" (replace -2 1)"1" (assert )"1" (hide-all-but 1)"1" "sigma_disjoint_union" "X" "X!1" "Y" "difference(Y!1, X!1)" "f" "f!1" ))"1" (assert )"1" (hide-all-but 1) (("1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil )"2" (replace -1)"2" "convergent_subset" "X" "Y!1" "Y" "union(X!1,Y!1)" "g" "f!1" ))"2" (typepred "f!1" )"2" (assert )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t) (("2" (grind) 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 sigma_countable nil )"countable_set[T]" nil )"countable_set[T]" nil )"bool" countable_convergence nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil sigma_countable nil )"real" reals nil )"bool" sets nil )"bool" sets nil )"odd_int" integers nil )"real" reals nil )"bool" sets nil )nil countable_convergence nil )"(partial_order?[set[T]])" nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"countable_set[T]" nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"set" sets nil )"set" sets nil ))nil 3351660503"" (skosimp)"" (lemma "sigma_union" ("f" "f!1" "X" "X!1" "Y" "Y!1" ))"" (assert ) nil nil )) nil ))nil )"set" sets nil )"bool" countable_convergence 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 sigma_countable nil )nil sigma_countable nil )"countable_set[T]" nil )"real" reals nil )"real" reals nil )"countable_set[T]" nil ))nil 3351659919"" (skosimp)"" (typepred "f!1" )"" "convergent_subset" "X" "difference(X!1,Y!1)" "Y" "union(X!1,Y!1)" "g" "f!1" ))"" (assert )"" (hide-all-but 1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"set" sets nil )"bool" countable_convergence 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 sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )"set" sets nil )nil countable_convergence nil )"countable_set[T]" nil )"countable_set[T]" nil ))nil ))nil 3351659919"" (skosimp*)"" (typepred "f!1" )"" "convergent_subset" "X" "difference(Y!1,X!1)" "Y" "union(X!1,Y!1)" "g" "f!1" ))"" (assert )"" (hide-all-but 1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"set" sets nil )"bool" countable_convergence 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 sigma_countable nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )"set" sets nil )nil countable_convergence nil )"countable_set[T]" nil )"countable_set[T]" nil ))nil ))nil 3351661074"" case "forall (X,Y:set[T]): disjoint?(difference(X,Y),intersection(X,Y)) & union(difference(X,Y),intersection(X,Y)) = X" )"1" (skosimp)"1" (inst-cp - "X!1" "Y!1" )"1" (inst - "Y!1" "X!1" )"1" (rewrite "intersection_commutative" -1)"1" (flatten)"1" "convergent_subset" "Y" "union(X!1,Y!1)" "g" "f!1" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.660 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
