| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sigma_set/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 MB |
|
Quellcode-Bibliothek sigma_countable.prfSprache: Lisp |
|||||||||||||||
|
(sigma_countable (sigma_TCC1 0 (sigma_TCC1-1 nil 3322368543 ("" (skosimp) (("" (lemma "nonempty_card" ("S" "X!1")) (("1" (expand "nonempty?") (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ((T formal-type-decl nil sigma_countable nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nonempty_card formula-decl nil finite_sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty? const-decl "bool" sets nil)) shostak)) (sigma_TCC2 0 (sigma_TCC2-1 nil 3322368543 ("" (skosimp) (("" (lemma "nonempty_card" ("S" "X!1")) (("1" (expand "nonempty?") (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ((T formal-type-decl nil sigma_countable nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nonempty_card formula-decl nil finite_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty? const-decl "bool" sets nil)) shostak)) (sigma_TCC3 0 (sigma_TCC3-1 nil 3322368684 ("" (skosimp) (("" (skosimp) (("" (typepred "y!1") (("" (assert) nil nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil sigma_countable nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (below type-eq-decl nil nat_types nil)) shostak)) (sigma_TCC4 0 (sigma_TCC4-1 nil 3322368684 ("" (skosimp) (("" (rewrite "countably_infinite_def") nil nil)) nil) ((countably_infinite_def formula-decl nil countable_props "sets_aux/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (T formal-type-decl nil sigma_countable nil)) shostak)) (sigma_TCC5 0 (sigma_TCC5-1 nil 3405668249 ("" (skosimp) (("" (typepred "f!1") (("" (expand "convergent?") (("" (assert) (("" (expand "o") (("" (name-replace "FF" "LAMBDA (x: nat): f!1(denumerable_enumeration(X!1)(x))") (("1" (expand "absconvergent?") (("1" (hide 1 2) (("1" (lemma "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) ((convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (is_countably_infinite const-decl "bool" countability "sets_aux/") (countably_infinite_set type-eq-decl nil countability "sets_aux/") (denumerable_enumeration const-decl "[nat -> (X)]" denumerable_enumeration nil) (absconvergent_series nonempty-type-eq-decl nil absconv_series "series/") (sequence type-eq-decl nil sequences nil) (absconvergent_series_is_convergent judgement-tcc nil absconv_series "series/") (absconvergent? const-decl "bool" absconv_series "series/") (countably_infinite_def formula-decl nil countable_props "sets_aux/") (O const-decl "T3" function_props nil) (convergent? const-decl "bool" convergence_sequences "analysis/")) nil)) (sigma_empty_TCC1 0 (sigma_empty_TCC1-1 nil 3322640566 ("" (grind) nil nil) ((injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (T formal-type-decl nil sigma_countable nil) (denumerable_enumeration const-decl "[nat -> (X)]" denumerable_enumeration nil) (O const-decl "T3" function_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abs const-decl "sequence[real]" series "series/") (sigma def-decl "real" sigma "reals/") (series const-decl "sequence[real]" series "series/") (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (absconvergent? const-decl "bool" absconv_series "series/") (convergent? const-decl "bool" countable_convergence nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (sigma_empty 0 (sigma_empty-1 nil 3322641284 ("" (skosimp) (("" (expand "sigma") (("" (rewrite "emptyset_is_empty?") nil nil)) nil)) nil) ((finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable nil) (sigma const-decl "real" sigma_countable nil) (T formal-type-decl nil sigma_countable nil) (emptyset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil)) shostak)) (sigma_finite_TCC1 0 (sigma_finite_TCC1-2 nil 3508520761 ("" (skosimp) (("" (typepred "F!1") (("" (expand "convergent?") (("" (propax) nil nil)) nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (convergent? const-decl "bool" countable_convergence nil)) nil) (sigma_finite_TCC1-1 nil 3322640566 ("" (skosimp*) (("" (typepred "F!1") (("" (lemma "finite_countable" ("x" "F!1")) (("" (propax) nil nil)) nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (finite_countable judgement-tcc nil countable_props "sets_aux/")) shostak)) (sigma_finite_TCC2 0 (sigma_finite_TCC2-2 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) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (T formal-type-decl nil sigma_countable nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil)) nil) (sigma_finite_TCC2-1 nil 3322640566 ("" (skosimp) (("" (typepred "F!1") (("" (expand "convergent?") (("" (propax) nil nil)) nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (convergent? const-decl "bool" countable_convergence nil)) shostak)) (sigma_finite_TCC3 0 (sigma_finite_TCC3-1 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) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (T formal-type-decl nil sigma_countable nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil)) shostak)) (sigma_finite_TCC4 0 (sigma_finite_TCC4-2 nil 3508520831 ("" (skosimp*) (("" (replace -1) (("" (assert) nil nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil) (sigma_finite_TCC4-1 nil 3322640566 ("" (skosimp) (("" (typepred "F!1") (("" (rewrite "empty_card") (("" (assert) nil nil)) nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (empty_card formula-decl nil finite_sets nil)) shostak)) (sigma_finite_TCC5 0 (sigma_finite_TCC5-1 nil 3322640566 ("" (skosimp*) (("" (replace -1) (("" (assert) nil nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (sigma_finite 0 (sigma_finite-1 nil 3322641469 ("" (skosimp) (("" (assert) (("" (expand "sigma" 1 1) (("" (propax) nil nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (sigma const-decl "real" sigma_countable nil)) shostak)) (sigma_singleton_TCC1 0 (sigma_singleton_TCC1-1 nil 3351597966 ("" (grind) nil nil) ((injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (T formal-type-decl nil sigma_countable nil) (denumerable_enumeration const-decl "[nat -> (X)]" denumerable_enumeration nil) (O const-decl "T3" function_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abs const-decl "sequence[real]" series "series/") (sigma def-decl "real" sigma "reals/") (series const-decl "sequence[real]" series "series/") (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (absconvergent? const-decl "bool" absconv_series "series/") (convergent? const-decl "bool" countable_convergence nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" sigma_countable nil)) nil)) (sigma_singleton 0 (sigma_singleton-1 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 ") (("" (typepred "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) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil sigma_countable nil) (sigma_finite formula-decl nil sigma_countable nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" sigma_countable nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (O const-decl "T3" function_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (below type-eq-decl nil nat_types nil) (finite_enumeration const-decl "[below[card(X)] -> (X)]" finite_enumeration nil) (sigma def-decl "real" sigma "reals/") (card_singleton formula-decl nil finite_sets nil)) shostak)) (sigma_infinite_TCC1 0 (sigma_infinite_TCC1-1 nil 3322642826 ("" (skosimp) (("" (typepred "f!1") (("" (expand "convergent?") (("" (typepred "X!1") (("" (rewrite "countably_infinite_def") (("" (flatten) (("" (assert) (("" (lemma "absconvergent_series_is_convergent" ("x" "(o[nat, T, real] (f!1, denumerable_enumeration[T](X!1)))")) (("" (assert) (("" (expand "convergent?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((countably_infinite_set type-eq-decl nil countability "sets_aux/") (is_countably_infinite const-decl "bool" countability "sets_aux/") (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (denumerable_enumeration const-decl "[nat -> (X)]" denumerable_enumeration nil) (O const-decl "T3" function_props nil) (absconvergent_series nonempty-type-eq-decl nil absconv_series "series/") (absconvergent? const-decl "bool" absconv_series "series/") (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (absconvergent_series_is_convergent judgement-tcc nil absconv_series "series/") (countably_infinite_def formula-decl nil countable_props "sets_aux/") (convergent? const-decl "bool" convergence_sequences "analysis/")) shostak)) (sigma_infinite 0 (sigma_infinite-1 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" (lemma "bijective_inverse_exists[(X!1),nat]" ("f" "f!2")) (("1" (expand "exists1") (("1" (flatten) (("1" (skolem -1 ("gg")) (("1" (expand "empty?") (("1" (inst - "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) ((countably_infinite_set type-eq-decl nil countability "sets_aux/") (is_countably_infinite const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (infinite_countably_infinite judgement-tcc nil countable_props "sets_aux/") (empty? const-decl "bool" sets nil) (bijective? const-decl "bool" functions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (exists1 const-decl "bool" exists1 nil) (member const-decl "bool" sets nil) (bijective_inverse_exists formula-decl nil function_inverse_def nil) (sigma const-decl "real" sigma_countable nil)) shostak)) (nonempty_countable_is_countable 0 (nonempty_countable_is_countable-1 nil 3323139930 ("" (skosimp) (("" (typepred "x!1") (("" (expand "nonempty_countable?") (("" (flatten) nil nil)) nil)) nil)) nil) ((nonempty_countable type-eq-decl nil sigma_countable nil) (nonempty_countable? const-decl "bool" sigma_countable nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (nonempty_countable_is_nonempty 0 (nonempty_countable_is_nonempty-1 nil 3323139930 ("" (skosimp) (("" (typepred "x!1") (("" (expand "nonempty_countable?") (("" (flatten) nil nil)) nil)) nil)) nil) ((nonempty_countable type-eq-decl nil sigma_countable nil) (nonempty_countable? const-decl "bool" sigma_countable nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (sigma_disjoint_union_TCC1 0 (sigma_disjoint_union_TCC1-1 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) ((union const-decl "set" sets nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (convergent_subset formula-decl nil countable_convergence nil)) shostak)) (sigma_disjoint_union_TCC2 0 (sigma_disjoint_union_TCC2-1 nil 3323139931 ("" (skosimp) (("" (lemma "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) ((union const-decl "set" sets nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil sigma_countable nil) (sigma_disjoint_union_TCC1 subtype-tcc nil sigma_countable nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (intersection_commutative formula-decl nil sets_lemmas nil) (disjoint? const-decl "bool" sets nil) (countable_intersection1 application-judgement "countable_set[T]" sigma_countable nil) (union_commutative formula-decl nil sets_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (sigma_disjoint_union 0 (sigma_disjoint_union-1 nil 3351662957 ("" (case "FORALL (X:finite_set[T], Y:countably_infinite_set[T], f:(convergent?(union(X, disjoint?(X, Y) IMPLIES sigma(union(X, Y), f) = sigma(X, f) + sigma(Y, f)") (("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" (lemma "finite_union[T]") (("2" (inst - "X!1" "Y!1") (("2" (assert) (("2" (case-replace "empty?(union(X!1, Y!1))") (("1" (hide-all-but (1 2 -1)) (("1" (expand "union") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (inst - "x!1") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "card_disj_union" ("A" "X!1" "B" "Y!1")) (("2" (assert) (("2" (replace -1) (("2" (replace -4) (("2" (replace -5) (("2" (lemma "series_bijection") (("2" (name "PHI" "LAMBDA (n:[below[card(union(X!1,Y!1))]]): IF n < card(X!1) THEN finite_enumeration(X!1) (("1" (lemma "finite_enumeration_bij" ("X" "union(X!1,Y!1)")) (("1" (lemma "finite_enumeration_bij" ("X" "X!1")) (("1" (lemma "finite_enumeration_bij" ("X" "Y!1")) (("1" (name-replace "FX" "finite_enumeration(X!1)") (("1" (name-replace "FY" "finite_enumeration(Y!1)") (("1" (name-replace "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" (lemma "bijective_inverse_exists[below[card[T](union(X!1, Y!1))], (union(X!1, Y!1))]" ("f" "FXY")) (("1" (expand "exists1") (("1" (flatten) (("1" (skolem - ("CXY")) (("1" (hide -2) (("1" (expand "series") (("1" (hide -6 -7) (("1" (lemma "sigma_bijection[below[card(union(X!1, Y!1))]]" ("low" "0" "high" "NX+NY-1" "F" "f!1 o FXY")) (("1" (split -1) (("1" (lemma "bij_inv_is_bij_alt[below[card[T](union(X!1, Y!1))], (union(X!1, Y!1))]" ("f" "FXY" "g" "CXY")) (("1" (lemma "composition_bijective[below[card[T](union(X!1,Y!1))],(union(X!1,Y!1)),below[car ("f1" "PHI" "f2" "CXY")) (("1" (inst - "CXY o PHI") (("1" (case-replace "sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY)] (0, NX + NY - 1, f!1 o FXY o restrict [below[card[T](union[T](X!1, Y!1))], subrange_T[below[card[T](union[T](X!1, Y!1))]](0, NX - 1 + NY), below[card[T](union[T](X!1, Y!1))]] (CXY o PHI)) = sigma[below[card(union(X!1, Y!1))]](0, NX + NY - 1, f!1 o PHI)") (("1" (case-replace "sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY)] (0, NX + NY - 1, restrict [below[card(union(X!1, Y!1))], subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY), real] (f!1 o FXY)) = sigma[below[card(union(X!1, Y!1))]](0, NX + NY - 1, f!1 o FXY)") (("1" (replace -5 4) (("1" (hide-all-but (4 2 3 -14 -15 -11)) (("1" (lemma "nonempty_card" ("S" "X!1")) (("1" (lemma "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) = sigma[below[card(Y!1)]](0, n, f!1 o FY) + sigma[below[card(X!1)]](0, NX - 1, f!1 o FX)") (("1" (inst - "NY-1") (("1" (assert) nil nil)) nil) ("2" (hide 2 3 4) (("2" (induct "n") (("1" (assert) (("1" (expand "sigma" 1 2) (("1" (expand "sigma" 1 1) (("1" (expand "PHI" 1 1) (("1" (expand "FY" 1) (("1" (expand "o" 1 3) (("1" (expand "o" 1 1) (("1" (assert) (("1" (replace -5 1) (("1" (assert) (("1" (hide -1 -3 -4) (("1" (case "forall (n:nat): n<=NX-1 => sigma(0, n, f!1 o PHI) = sigma[below[card(X!1)]](0, n, f!1 o FX)") (("1" (inst - "NX-1") (("1" (assert) (("1" (expand "sigma" 1 2) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (expand "sigma") (("1" (expand "FX") (("1" (expand "PHI") (("1" (expand "o ") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "sigma" 1) (("2" (assert) (("2" (replace -1 1) (("2" (assert) (("2" (expand "o") (("2" (expand "PHI") (("2" (expand "FX") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "sigma" 1 2) (("2" (expand "sigma" 1 1) (("2" (assert) (("2" (replace -1 1) (("2" (assert) (("2" (expand "PHI" 1) (("2" (expand "o") (("2" (expand "FY") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (assert) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("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 (0, n, restrict [below[card(union(X!1, Y!1))], subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY), real] (f!1 o FXY)) = sigma[below[card(union(X!1, Y!1))]](0, n, f!1 o FXY)") (("1" (inst - "NX+NY-1") (("1" (assert) nil nil) ("2" (lemma "nonempty_card" ("S" "X!1")) (("2" (lemma "nonempty_card" ("S" "Y!1")) (("2" (expand "nonempty?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (induct "n") (("1" (expand "sigma") (("1" (expand "restrict") (("1" (expand "sigma" 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (expand "restrict") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("2" (hide 5 -3) (("2" (lemma "comp_inverse_right_alt[below[card[T](union(X!1, Y!1))], (union(X!1, Y!1))]" ("f" "FXY" "g" "CXY")) (("2" (hide -2 -3 -4 -5 -6 -7 -8) (("2" (lemma "nonempty_card" ("S" "X!1")) (("2" (lemma "nonempty_card" ("S" "Y!1")) (("2" (expand "nonempty?") (("2" (assert) (("2" (hide 2 3 4) (("2" (case "forall (n:nat): n <= NX-1+NY => sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY (0, n, f!1 o FXY o restrict [below[card[T](union[T](X!1, Y!1))], subrange_T[below[card[T](union[T](X!1, Y!1))]] (0, NX - 1 + NY), below[card[T](union[T](X!1, Y!1))]] (CXY o PHI)) = sigma[below[card(union(X!1, Y!1))]](0, n, f!1 o PHI)") (("1" (inst - "NX-1+NY") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "restrict") (("2" (expand "o ") (("2" (induct "n") (("1" (expand "sigma") (("1" (inst - "PHI(0)") (("1" (assert) (("1" (expand "sigma" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (assert) (("2" (replace -1 1) (("2" (assert) (("2" (hide -1) (("2" (inst - "PHI(1+j!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (expand "PHI") (("5" (case "x!1 < card(X!1)") (("1" (assert) (("1" (typepred "finite_enumeration(X!1)(x!1)") (("1" (expand "union") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "union") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("2" (split 1) (("1" (skosimp*) (("1" (expand "o") (("1" (typepred "CXY(PHI(x1!1))") (("1" (assert) nil nil) ("2" (hide 2 3 4 5 6) (("2" (expand "union") (("2" (expand "member") (("2" (flatten) (("2" (expand "PHI") (("2" (case-replace "x1!1 < card(X!1)") (("1" (expand "finite_enumeration") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -4 -5 -6 -7 5) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "o ") (("2" (split 1) (("1" (expand "restrict") (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (typepred "x2!1") (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (expand "restrict") (("2" (skosimp) (("2" (typepred "y!1") (("2" (inst - "y!1") (("2" (skosimp) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (lemma "nonempty_card" ("S" "X!1")) (("2" (lemma "nonempty_card" ("S" "Y!1")) (("2" (expand "nonempty?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "nonempty_card" ("S" "X!1")) (("2" (lemma "nonempty_card" ("S" "Y!1")) (("2" (expand "nonempty?") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (assert) (("3" (lemma "nonempty_card" ("S" "union(X!1, Y!1)")) (("3" (expand "nonempty?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (typepred "x!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but (3 4 1 -1 -2 -13 -11 -12)) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "PHI") (("2" (expand "FY") (("2" (expand "FX") (("2" (split) (("1" (expand "injective?") (("1" (skosimp*) (("1" (case-replace "x1!1 < card(X!1)") (("1" (case-replace "x2!1 < card(X!1)") (("1" (inst -6 "x1!1" "x2!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -9 "finite_enumeration(X!1)(x1!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "x2!1<card(X!1)") (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -9 "finite_enumeration(X!1)(x2!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -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" (skosimp*) (("2" (case "X!1(y!1)") (("1" (inst -5 "y!1") (("1" (skosimp) (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (typepred "y!1") (("2" (expand "union") (("2" (expand "member") (("2" (assert) (("2" (inst -3 "y!1") (("2" (skosimp) (("2" (inst + "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" (skosimp) (("3" (typepred "x1!1") (("3" (expand "PHI" 1) (("3" (expand "union" 1) (("3" (expand "member") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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" (lemma "convergent_subset" ("X" "X!1" "Y" "union(X!1,Y!1)" "g" "f!1")) (("2" (lemma "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" (lemma "infinite_union_right" ("S" "X!1" "Inf" "Y!1")) (("1" (lemma "infinite_nonempty" ("x" "X!1")) (("1" (lemma "infinite_nonempty" ("x" "Y!1")) (("1" (lemma "infinite_nonempty" ("x" "union(X!1,Y!1)")) (("1" (expand "nonempty?") (("1" (assert) (("1" (lemma "denumerable_enumeration_bij" ("X" "X!1")) (("1" (lemma "denumerable_enumeration_bij" ("X" "Y!1")) (("1" (lemma "denumerable_enumeration_bij" ("X" "union(X!1,Y!1)")) (("1" (name-replace "DXY" "denumerable_enumeration(union(X!1,Y!1))") (("1" (name-replace "DX" "denumerable_enumeration(X!1)") (("1" (name-replace "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" (name "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" (lemma "bijective_inverse_exists[nat, (union(X!1, Y!1))]" ("f" "DXY")) (("1" (expand "exists1") (("1" (flatten) (("1" (hide -2) (("1" (skolem - ("CXY")) (("1" (lemma "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" ("f" "DXY" "g" "CXY")) (("1" (lemma "comp_inverse_right_alt[nat, (union(X!1, Y!1))]" ("f" "DXY" "g" "CXY")) (("1" (lemma "composition_bijective[nat,(union(X!1, Y!1)),nat]" ("f1" "PHI" "f2" "CXY")) (("1" (lemma "abs_series_bij_limit" ("a" "f!1 o DXY" "phi" "CXY o PHI")) (("1" (split -1) (("1" (lemma "extensionality" ("f" "f!1 o DXY o (CXY o PHI)" "g" "f!1 o PHI")) (("1" (split -1) (("1" (replace -1) (("1" (replace -2) (("1" (case "forall (x:real): convergence(series(f!1 o DX),x) IFF convergence(series(LAMBDA (n:nat) (("1" (inst - "limit(series(f!1 o DX))") (("1" (rewrite "limit_equiv" -1) (("1" (lemma "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) (("1" (inst - "limit(series(f!1 o DY))") (("1" (rewrite "limit_equiv" -1) (("1" (lemma "absconvergent_series_is_convergent" ("x" "f!1 o DY")) (("1" (assert) (("1" (lemma "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)) ELSE 0 ENDIF)" "l2" "limit(series(f!1 o DY))")) (("1" (assert) (("1" (rewrite "series_sum" -1) (("1" (lemma "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)) ELSE 0 ENDIF)" "g" "f!1 o PHI")) (("1" (split -1) (("1" (replace -1) (("1" (rewrite "limit_equiv" -2) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "+") (("2" (expand "o") (("2" (expand "PHI") (("2" (skosimp) (("2" (case-replace "even?(x!1)") (("1" (lemma "even_iff_not_odd" ("x" "x!1")) (("1" (assert) nil nil)) nil) ("2" (lemma "even_iff_not_odd" ("x" "x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("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)) ELSE 0 ENDIF)") (("1" (case "FORALL (n: nat): even?(n) => sigma(0, n, (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): odd?(n) => sigma(0, n, (LAMBDA (n: nat): IF odd?(n) THEN f!1(DY((n - 1) / 2)) ELSE 0 ENDIF)) = sigma(0, (n-1)/ 2, f!1 o DY)") (("1" (expand "convergence") (("1" (split 1) (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + "2*n!1+1") (("1" (skosimp) (("1" (case "even?(i!1)") (("1" (inst -5 "i!1") (("1" (assert) (("1" (replace -5) (("1" (inst -2 "i!1/2-1") (("1" (assert) (("1" (hide-all-but (-1 -2 1)) (("1" (expand "even?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case-replace "i!1=0") (("1" (assert) nil nil) ("2" (expand "even?") (("2" (skosimp) (("2" (replace -1) (("2" (assert) (("2" (case-replace "2 * j!1 / 2 = j!1") (("1" (assert) nil nil) ("2" (lemma "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" 1) (("2" (inst -4 "i!1") (("2" (assert) (("2" (replace -4) (("2" (hide -5 -6 -4) (("2" (inst - "(i!1-1)/2") (("1" (split -2) (("1" (propax) nil nil) ("2" (assert) nil nil)) nil) ("2" (expand "odd?") (("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "epsilon!1") (("2" (skosimp) (("2" (inst + "2*n!1+1") (("2" (skosimp*) (("2" (inst -5 "i!1") (("2" (inst -1 "2*i!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "odd?" 1 1) (("2" (skosimp*) (("2" (replace -1) (("2" (assert) (("2" (inst - "j!1") (("1" (assert) nil nil) ("2" (assert) (("2" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "-1" "j!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skosimp*) (("3" (assert) (("3" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (assert) (("1" (expand "odd?") (("1" (skosimp) (("1" (replace -2) (("1" (assert) (("1" (flatten) (("1" (lemma "trichotomy" ("x" "j!1")) (("1" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (hide-all-but (-2 1)) (("4" (expand "odd?") (("4" (skosimp) (("4" (replace -1) (("4" (assert) (("4" (lemma "trichotomy" ("x" "j!1")) (("4" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (case "forall (i,j:int): i< j => i+1<=j") (("1" (inst - "j!1" "0") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (case-replace "n!1=0") (("1" (expand "sigma") (("1" (expand "odd?") (("1" (expand "sigma" 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "even?") (("2" (skosimp) (("2" (replace -1) (("2" (inst - "j!1-1") (("1" (expand "sigma" 2 1) (("1" (assert) (("1" (lemma "even_iff_not_odd" ("x" "2*j!1")) (("1" (expand "even?" -1) (("1" (flatten -1) (("1" (hide -2) (("1" (split -1) (("1" (assert) nil nil) ("2" (inst + "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" (skosimp*) (("3" (assert) (("3" (typepred "n!1") (("3" (replace -2) (("3" (assert) (("3" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "0" "j!1") (("1" (assert) (("1" (lemma "div_cancel2" ("x" "j!1" "n0z" "2")) (("1" (assert) (("1" (case-replace "2 * j!1 / 2 - 1 = j!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand "odd?") (("4" (skosimp*) (("4" (replace -2) (("4" (assert) (("4" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "-1" "j!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "o ") (("2" (induct "n") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "odd?") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (expand "sigma" 1 2) (("2" (replace -1 1 rl) (("2" (expand "odd?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "odd?") (("3" (skosimp*) (("3" (assert) (("3" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "-1" "j!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "odd?") (("3" (skosimp) (("3" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (skosimp) (("1" (inst - "-1" "j!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -14)) (("2" (skosimp*) (("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)) = sigma(0,n,f!1 o DX)") (("1" (case "FORALL (n: nat): even?(n) => sigma(0, n, (LAMBDA (n: nat): IF even?(n) THEN f!1(DX(n / 2)) ELSE 0 ENDIF)) = sigma(0, n/2, f!1 o DX)") (("1" (case "FORALL (n: nat): odd?(n) => sigma(0, n, (LAMBDA (n: nat): IF even?(n) THEN f!1(DX(n / 2)) ELSE 0 ENDIF)) = sigma(0, (n-1) / 2, f!1 o DX)") (("1" (expand "convergence") (("1" (split 1) (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + "2*n!1") (("1" (skosimp) (("1" (case "even?(i!1)") (("1" (expand "even?" -1) (("1" (skosimp) (("1" (inst - "j!1") (("1" (assert) (("1" (inst -5 "i!1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "even_or_odd" 1) (("2" (inst -4 "i!1") (("2" (assert) (("2" (replace -4 1) (("2" (inst -2 "(i!1-1)/2") (("1" (split -2) (("1" (propax) nil nil) ("2" (assert) (("2" (hide-all-but (-1 -2 1)) (("2" (expand "odd?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "odd?") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "epsilon!1") (("2" (skosimp) (("2" (case "even?(n!1)") (("1" (expand "even?" -1) (("1" (skosimp) (("1" (replace -1) (("1" (inst + "j!1") (("1" (skosimp) (("1" (inst - "2*i!1") (("1" (assert) (("1" (inst -5 "2*i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "even_or_odd" 1) (("2" (expand "odd?" -1) (("2" (skosimp) (("2" (replace -1) (("2" (inst + "j!1") (("1" (skosimp) (("1" (inst - "1+2*i!1") (("1" (assert) (("1" (inst -4 "1+2*i!1") (("1" (split -4) (("1" (assert) nil nil) ("2" (expand "odd?") (("2" (inst + "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" (hide-all-but (-2 1)) (("2" (expand "odd?") (("2" (skosimp*) (("2" (replace -1) (("2" (inst - "j!1") (("1" (assert) (("1" (expand "sigma" 1 1) (("1" (replace -2) (("1" (assert) (("1" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "-1" "j!1") (("1" (assert) (("1" (lift-if 1) (("1" (assert) (("1" (rewrite "even_or_odd" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "-1" "j!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "odd?") (("3" (skosimp*) (("3" (assert) (("3" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "-1" "j!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "even?") (("4" (skosimp*) (("4" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "-1" "j!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "even?" 1 1) (("2" (skosimp*) (("2" (inst - "j!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "even?") (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (expand "even?") (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "n") (("1" (expand "o") (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (expand "o") (("2" (assert) (("2" (expand "sigma" 1 1) (("2" (replace -1 1) (("2" (assert) (("2" (lift-if 1) (("2" (prop) (("1" (expand "even?") (("1" (propax) nil nil)) nil) ("2" (rewrite "even_or_odd" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "even?") (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (expand "even?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "even?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "o") (("2" (skosimp) (("2" (inst -3 "PHI(x!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "absconvergent?") (("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but (-2 -3 -5 -6 -12 1)) (("2" (expand "bijective?") (("2" (expand "PHI") (("2" (flatten) (("2" (split 1) (("1" (expand "injective?") (("1" (skosimp*) (("1" (case-replace "even?(x1!1)") (("1" (case-replace "even?(x2!1)") (("1" (inst -8 "x1!1/2" "x2!1/2") (("1" (assert) nil nil) ("2" (inst -5 "x2!1") (("2" (assert) nil nil)) nil) ("3" (inst -5 "x1!1") (("3" (assert) nil nil)) nil)) nil) ("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (assert) (("2" (inst -9 "DX(x1!1/2)") (("1" (assert) nil nil) ("2" (inst -4 "x1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "even?(x2!1)") (("1" (assert) (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -4 "x2!1") (("1" (assert) (("1" (typepred "DX(x2!1 / 2)") (("1" (inst -10 "DX(x2!1 / 2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst-cp - "x1!1") (("2" (inst - "x2!1") (("2" (assert) (("2" (flatten) (("2" (inst -7 "(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" (skosimp*) (("2" (typepred "y!1") (("2" (expand "union") (("2" (expand "member") (("2" (split -1) (("1" (inst -7 "y!1") (("1" (skosimp) (("1" (inst + "2*x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst -5 "y!1") (("2" (skosimp) (("2" (inst + "2*x!1+1") (("2" (assert) (("2" (lemma "div_cancel2" ("x" "x!1" "n0z" "2")) (("2" (lift-if 1) (("2" (assert) (("2" (prop) (("2" (expand "even?") (("2" (propax) 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" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp) (("3" (inst -3 "n!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (rewrite "even_or_odd") (("2" (expand "odd?") (("2" (skosimp) (("2" (replace -1) (("2" (assert) (("2" (case "forall (i,j:int):i<j=>i+1<=j") (("1" (inst - "-1" "j!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "even?") (("2" (skosimp*) (("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" (hide-all-but 1) (("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" (lemma "infinite_union_right" ("S" "X!1" "Inf" "Y!1")) (("2" (expand "convergent?") (("2" (assert) (("2" (expand "sigma") (("2" (assert) (("2" (lemma "infinite_nonempty[T]" ("x" "Y!1")) (("2" (lemma "infinite_nonempty[T]" ("x" "union(X!1,Y!1)")) (("2" (expand "nonempty?") (("2" (assert) (("2" (lemma "convergent_subset" ("X" "Y!1" "Y" "union(X!1,Y!1)" "g" "f!1")) (("2" (split -1) (("1" (expand "convergent?") (("1" (lemma "denumerable_enumeration_bij" ("X" "union(X!1,Y!1)")) (("1" (lemma "denumerable_enumeration_bij" ("X" "Y!1")) (("1" (lemma "finite_enumeration_bij" ("X" "X!1")) (("1" (name-replace "DX" "finite_enumeration(X!1)") (("1" (name-replace "DY" "denumerable_enumeration(Y!1)") (("1" (name-replace "DXY" "denumerable_enumeration(union(X!1,Y!1))") (("1" (lemma "nonempty_card" ("S" "X!1")) (("1" (expand "nonempty?") (("1" (hide 1 2) (("1" (name "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" (lemma "bijective_inverse_exists[nat, (union(X!1, Y!1))]" ("f" "DXY")) (("1" (expand "exists1") (("1" (flatten) (("1" (hide -2) (("1" (skolem - ("CXY")) (("1" (lemma "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]" ("f" "DXY" "g" "CXY")) (("1" (lemma "comp_inverse_right_alt[nat, (union(X!1, Y!1))]" ("f" "DXY" "g" "CXY")) (("1" (lemma "composition_bijective[nat,(union(X!1, Y!1)),nat]" ("f1" "PHI" "f2" "CXY")) (("1" (lemma "abs_series_bij_limit" ("a" "f!1 o DXY" "phi" "CXY o PHI")) (("1" (split -1) (("1" (lemma "extensionality" ("f" "f!1 o DXY o (CXY o PHI)" "g" "f!1 o PHI")) (("1" (split -1) (("1" (replace -1) (("1" (replace -2) (("1" (lemma "limit_series_shift" ("a" "f!1 o PHI" "pn" "card(X!1)")) (("1" (split -1) (("1" (replace -1) (("1" (expand "o" 4) (("1" (expand "PHI" 4) (("1" (hide-all-but (4 -17 -10)) (("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)) ELSE f!1(DY(x - card(X!1))) ENDIF) = sigma[below[card(X!1)]] (0, n, LAMBDA (x: below[card(X!1)]): f!1(DX(x)))") (("1" (inst - "card(X!1)-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (expand "sigma") (("1" (assert) (("1" (expand "sigma" 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) nil nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) nil nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "abs_series_bij_conv" ("a" "f!1 o DXY" "phi" "CXY o PHI")) (("2" (replace -2 -1) (("2" (expand "absconvergent?") (("2" (replace -15) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -3 "PHI(x!1)") (("1" (hide-all-but (-3 1)) (("1" (grind) nil nil)) nil) ("2" (expand "PHI") (("2" (assert) (("2" (expand "union") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "absconvergent?") (("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but (-2 -9 1 -3 -4 -10)) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "PHI") (("2" (split) (("1" (expand "injective?") (("1" (skosimp*) (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (case-replace "x1!1 < card(X!1)") (("1" (case-replace "x2!1 < card(X!1)") (("1" (inst -5 "x1!1" "x2!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst -9 "DX(x1!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case-replace "x2!1 < card(X!1)") (("1" (inst -9 "DX(x2!1)") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst -5 "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" (skosimp*) (("2" (typepred "y!1") (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "union") (("2" (expand "empty?") (("2" (expand "member") (("2" (split -1) (("1" (inst -4 "y!1") (("1" (skosimp) (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst -6 "y!1") (("2" (skosimp) (("2" (inst + "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" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (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" (lemma "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" (lemma "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) ((y!1 skolem-const-decl "(union(X!1, Y!1))" sigma_countable nil) (x!1 skolem-const-decl "nat" sigma_countable nil) (Y!1 skolem-const-decl "countably_infinite_set[T]" sigma_countable nil) (limit_series_shift formula-decl nil series "series/") (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (abs_series_bij_conv formula-decl nil series_lems "series/") (PHI skolem-const-decl "[nat -> T]" sigma_countable nil) (X!1 skolem-const-decl "finite_set[T]" sigma_countable nil) (infinite_union_left application-judgement "infinite_set[T]" sigma_countable nil) (countably_infinite_union1 application-judgement "countably_infinite_set[T]" sigma_countable nil) (intersection_commutative formula-decl nil sets_lemmas nil) (countable_intersection1 application-judgement "countable_set[T]" sigma_countable nil) (f!1 skolem-const-decl "(convergent?(union(X!1, Y!1)))" sigma_countable nil) (convergent_subset formula-decl nil countable_convergence nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (infinite_nonempty judgement-tcc nil infinite_sets_def nil) (denumerable_enumeration const-decl "[nat -> (X)]" denumerable_enumeration nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (j!1 skolem-const-decl "int" sigma_countable nil) (j!1 skolem-const-decl "int" sigma_countable nil) (j!1 skolem-const-decl "int" sigma_countable nil) (even_or_odd formula-decl nil naturalnumbers nil) (i!1 skolem-const-decl "nat" sigma_countable nil) (j!1 skolem-const-decl "int" sigma_countable nil) (j!1 skolem-const-decl "int" sigma_countable nil) (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (absconvergent_series_is_convergent judgement-tcc nil absconv_series "series/") (absconvergent? const-decl "bool" absconv_series "series/") (absconvergent_series nonempty-type-eq-decl nil absconv_series "series/") (odd? const-decl "bool" integers nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (even_iff_not_odd formula-decl nil naturalnumbers nil) (PHI skolem-const-decl "[nat -> T]" sigma_countable nil) (series_sum formula-decl nil series "series/") (cnv_seq_sum formula-decl nil convergence_ops "analysis/") (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (j!1 skolem-const-decl "int" sigma_countable nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (i!1 skolem-const-decl "nat" sigma_countable nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel2 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (j!1 skolem-const-decl "int" sigma_countable nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (trichotomy formula-decl nil real_axioms nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (limit_equiv formula-decl nil convergence_ops "analysis/") (convergence const-decl "bool" convergence_sequences "analysis/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (extensionality formula-decl nil functions nil) (sequence type-eq-decl nil sequences nil) (abs_series_bij_limit formula-decl nil series_lems "series/") (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (y!1 skolem-const-decl "(union(X!1, Y!1))" sigma_countable nil) (x1!1 skolem-const-decl "nat" sigma_countable nil) (x2!1 skolem-const-decl "nat" sigma_countable nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (even? const-decl "bool" integers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (denumerable_enumeration_bij formula-decl nil denumerable_enumeration nil) (infinite_set type-eq-decl nil infinite_sets_def nil) (infinite_union_right judgement-tcc nil infinite_sets_def nil) (subset? const-decl "bool" sets nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (emptyset const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (union_empty formula-decl nil sets_lemmas nil) (sigma_empty formula-decl nil sigma_countable nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (union_commutative formula-decl nil sets_lemmas nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (int_minus_int_is_int application-judgement "int" integers nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (card_disj_union formula-decl nil finite_sets nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (finite_enumeration const-decl "[below[card(X)] -> (X)]" finite_enumeration nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (intersection const-decl "set" sets nil) (y!1 skolem-const-decl "(union(X!1, Y!1))" sigma_countable nil) (bijective_inverse_exists formula-decl nil function_inverse_def nil) (composition_bijective judgement-tcc nil function_props nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (nonempty_card formula-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (FX skolem-const-decl "[below[card(X!1)] -> (X!1)]" sigma_countable nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (FY skolem-const-decl "[below[card(Y!1)] -> (Y!1)]" sigma_countable nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (comp_inverse_right_alt formula-decl nil function_inverse_def nil) (restrict const-decl "R" restrict nil) (PHI skolem-const-decl "[below[card(union(X!1, Y!1))] -> T]" sigma_countable nil) (CXY skolem-const-decl "[(union(X!1, Y!1)) -> below[card[T](union(X!1, Y!1))]]" sigma_countable nil) (subrange_T type-eq-decl nil sigma_bijection nil) (NY skolem-const-decl "{n: nat | n = Card(Y!1)}" sigma_countable nil) (NX skolem-const-decl "{n: nat | n = Card(X!1)}" sigma_countable nil) (Y!1 skolem-const-decl "countable_set[T]" sigma_countable nil) (X!1 skolem-const-decl "countable_set[T]" sigma_countable nil) (int_plus_int_is_int application-judgement "int" integers nil) (inverse? const-decl "bool" function_inverse_def nil) (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil) (integer nonempty-type-from-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (O const-decl "T3" function_props nil) (sigma_bijection formula-decl nil sigma_bijection nil) (series const-decl "sequence[real]" series "series/") (exists1 const-decl "bool" exists1 nil) (bijective? const-decl "bool" functions nil) (finite_enumeration_bij formula-decl nil finite_enumeration nil) (series_bijection formula-decl nil sigma_bijection_nat nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (finite_union judgement-tcc nil finite_sets nil) (countably_infinite_def formula-decl nil countable_props "sets_aux/") (NOT const-decl "[bool -> bool]" booleans nil) (infinite_union_right application-judgement "infinite_set[T]" sigma_countable nil) (countably_infinite_union2 application-judgement "countably_infinite_set[T]" sigma_countable nil) (real_plus_real_is_real application-judgement "real" reals nil) (T formal-type-decl nil sigma_countable nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_countably_infinite const-decl "bool" countability "sets_aux/") (countably_infinite_set type-eq-decl nil countability "sets_aux/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (convergent? const-decl "bool" countable_convergence nil) (union const-decl "set" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (disjoint? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma const-decl "real" sigma_countable nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (sigma_union_TCC1 0 (sigma_union_TCC1-1 nil 3351659919 ("" (skosimp) (("" (lemma "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) ((T formal-type-decl nil sigma_countable nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (union const-decl "set" sets nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (convergent_subset formula-decl nil countable_convergence nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil)) nil)) (sigma_union_TCC2 0 (sigma_union_TCC2-1 nil 3351659919 ("" (skosimp) (("" (typepred "f!1") (("" (lemma "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) ((union const-decl "set" sets nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (convergent_subset formula-decl nil countable_convergence nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil)) nil)) (sigma_union_TCC3 0 (sigma_union_TCC3-1 nil 3351659919 ("" (skosimp) (("" (typepred "f!1") (("" (lemma "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) ((union const-decl "set" sets nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (convergent_subset formula-decl nil countable_convergence nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (countable_intersection1 application-judgement "countable_set[T]" sigma_countable nil)) nil)) (sigma_union 0 (sigma_union-1 nil 3351661433 ("" (skosimp) (("" (rewrite "union_difference") (("" (case "union(difference(Y!1, X!1), intersection(X!1, Y!1)) = Y!1") (("1" (lemma "sigma_disjoint_union" ("X" "difference(Y!1, X!1)" "Y" "intersection(X!1, Y!1)" "f" "f!1")) (("1" (case-replace "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" (lemma "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" (lemma "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) ((union_difference formula-decl nil sets_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (T formal-type-decl nil sigma_countable nil) (countable_difference application-judgement "countable_set[T]" sigma_countable nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (sigma_disjoint_union formula-decl nil sigma_countable nil) (real_minus_real_is_real application-judgement "real" reals nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (disjoint? const-decl "bool" sets nil) (convergent_subset formula-decl nil countable_convergence nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (countable_intersection1 application-judgement "countable_set[T]" sigma_countable nil) (= const-decl "[T, T -> boolean]" equalities nil) (union const-decl "set" sets nil) (difference const-decl "set" sets nil) (intersection const-decl "set" sets nil)) shostak)) (sigma_intersection 0 (sigma_intersection-1 nil 3351660503 ("" (skosimp) (("" (lemma "sigma_union" ("f" "f!1" "X" "X!1" "Y" "Y!1")) (("" (assert) nil nil)) nil)) nil) ((union const-decl "set" sets nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil sigma_countable nil) (sigma_union formula-decl nil sigma_countable nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (countable_intersection1 application-judgement "countable_set[T]" sigma_countable nil)) shostak)) (sigma_difference_TCC1 0 (sigma_difference_TCC1-1 nil 3351659919 ("" (skosimp) (("" (typepred "f!1") (("" (lemma "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) ((union const-decl "set" sets nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (difference const-decl "set" sets nil) (convergent_subset formula-decl nil countable_convergence nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (countable_difference application-judgement "countable_set[T]" sigma_countable nil)) nil)) (sigma_difference_TCC2 0 (sigma_difference_TCC2-1 nil 3351659919 ("" (skosimp*) (("" (typepred "f!1") (("" (lemma "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) ((union const-decl "set" sets nil) (convergent? const-decl "bool" countable_convergence nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (T formal-type-decl nil sigma_countable nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (difference const-decl "set" sets nil) (convergent_subset formula-decl nil countable_convergence nil) (countable_union application-judgement "countable_set[T]" sigma_countable nil) (countable_difference application-judgement "countable_set[T]" sigma_countable nil)) nil)) (sigma_difference 0 (sigma_difference-1 nil 3351661074 ("" (case "forall (X,Y:set[T]): disjoint?(difference(X,Y),intersection(X,Y)) & union( (("1" (skosimp) (("1" (inst-cp - "X!1" "Y!1") (("1" (inst - "Y!1" "X!1") (("1" (rewrite "intersection_commutative" -1) (("1" (flatten) (("1" (lemma "convergent_subset" ("Y" "union(X!1,Y!1)" "g" "f!1")) --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.653Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26