Impressum countable_props.prf
Interaktion und
(countable_propsnil 3316998965"" (skosimp)"" (typepred "x!1" )"" (expand "is_countably_infinite" )"" (skosimp)"" (typepred "f!1" )"" (lemma "infinite_def2" ("S" "x!1" ))"" (replace -3)"" (assert ) (("" (inst + "f!1" ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countability nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil infinite_nat_def nil )"bool" functions nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil ))nil ))nil 3316998965"" (skolem-typepred)"" (case "member(t!1, CountInf!1)" )"1" (forward-chain "member_add[T]" ) (("1" (assert ) nil nil ))nil )"2" (expand * "is_countably_infinite" "member" )"2" (skolem-typepred)"2" "LAMBDA (x: (add(t!1, CountInf!1))): IF x = t!1 THEN 0 ELSE f!1(x) + 1 ENDIF" )"1" (grind :if-match nil )"1" (case "y!1 = 0" )"1" (inst + "t!1" ) (("1" (assert ) nil nil )) nil )"2" (assert )"2" (inst - "y!1 - 1" )"2" (skolem!)"2" (inst + "x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "x1!1" "x2!1" ) (("2" (assert ) nil nil ))nil ))nil )"2" (skosimp :preds? t)"2" (expand * "add" "member" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"infinite_set[T]" nil )nil sets_lemmas nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )"bool" functions nil )"bool" functions nil )"int" integers nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"(bijective?[(CountInf!1), nat])" nil )"[bool, bool -> bool]" booleans nil )"countably_infinite_set" nil )"T" countable_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"(nonempty?)" sets nil )"bool" sets nil )"posint" nil )"posint" nil )nil countability nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3316998965"" (skolem-typepred)"" (case "member[T](t!1,Count!1)" )"1" (lemma "member_add[T]" ("x" "t!1" "a" "Count!1" ))"1" (assert ) nil nil )) nil )"2" (expand "is_countable" )"2" (skosimp)"2" (typepred "f!1" )"2" "lambda (x:(add[T](t!1, Count!1))): if x = t!1 then 0 else f!1(x)+1 endif" )"1" (expand "injective?" )"1" (skosimp)"1" (typepred "x1!1" )"1" (typepred "x2!1" )"1" (expand "add" )"1" (split)"1" (expand "member" )"1" (assert ) nil nil )) nil )"2" (assert )"2" (expand "member" )"2" assert )"2" "1" (assert ) nil nil )"2" "x1!1" "x2!1" )"2" "x1!1 = t!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "x!1" )"2" (expand "add" )"2" (assert )"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil sets_lemmas nil )"posint" nil )"posint" nil )"bool" sets nil )"(nonempty?)" sets nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"T" countable_props nil )"countable_set[T]" countable_props nil )"[bool, bool -> bool]" booleans nil )"(injective?[(Count!1), nat])" nil )"(add[T](t!1, Count!1))" countable_propsnil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil countability nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3316998965"" (skolem-typepred)"" (case "member(t!1, CountInf!1)" )"1" (expand "is_countably_infinite" )"1" (skolem-typepred)"1" "LAMBDA (x: (remove(t!1, CountInf!1))): IF f!1(x) <= f!1(t!1) THEN f!1(x) ELSE f!1(x) - 1 ENDIF" )"1" (grind :if-match nil )"1" (case "y!1 < f!1(t!1)" )"1" (inst - "y!1" )"1" (skolem!)"1" (assert )"1" (inst + "x!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (inst - "1 + y!1" )"2" (skolem!)"2" (assert )"2" (inst + "x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "x1!1" "x2!1" ) (("2" (assert ) nil nil ))nil )"3" (inst - "x1!1" "t!1" ) (("3" (assert ) nil nil )) nil )"4" (inst - "t!1" "x2!1" ) (("4" (assert ) nil nil )) nil )"5" (inst - "x1!1" "x2!1" ) (("5" (assert ) nil nil ))nil ))nil )"2" (skosimp :preds? t)"2" (expand * "remove" "member" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp :preds? t)"3" (expand * "remove" "member" )"3" (flatten) nil nil )) nil ))nil )"4" (skosimp :preds? t)"4" (expand * "remove" "member" )"4" (flatten) nil nil )) nil ))nil )"5" (skolem-typepred)"5" (expand * "remove" "member" ) nil nil )) nil )"6" (skolem-typepred)"6" (expand * "remove" "member" )"6" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (forward-chain "member_remove[T]" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"bool" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )"bool" functions nil )"bool" functions nil )"boolean" notequal nil )"infinite_set[T]" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"(bijective?[(CountInf!1), nat])" nil )"countably_infinite_set" nil )"T" countable_props nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"set" sets nil )"int" integers nil )nil sets_lemmas nil )nil countability nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3316998965"" (skosimp)"" (typepred "Count!1" )"" (lemma "member_remove" ("x" "t!1" "a" "Count!1" ))"" (case-replace "member(t!1, Count!1)" )"1" (expand "is_countable" )"1" (skosimp)"1" (typepred "f!1" )"1" "lambda (x:(remove[T](t!1, Count!1))): f!1(x)" )"1" (expand "injective?" )"1" (skosimp)"1" (inst - "x1!1" "x2!1" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp)"2" (typepred "x!1" )"2" (expand "remove" )"2" (flatten)"2" (assert )"2" (expand "member" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil countability nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"set" sets nil )"T" countable_props nil )"countable_set[T]" countable_props nil )"(injective?[(Count!1), nat])" nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil sets_lemmas nil ))nil ))nil 3316998965"" (expand "rest" ) (("" (propax) nil nil )) nil )"set" sets nil )"countably_infinite_set[T]" countable_props nil )"countable_set[T]" nil ))nil ))nil 3316998965"" (expand "rest" ) (("" (propax) nil nil )) nil )"set" sets nil )"countable_set[T]" nil ))nil ))nil 3316998965"" (skolem-typepred)"" (expand "is_countable" )"" (skolem-typepred)"" "LAMBDA (x: (intersection(Count!1, S!1))): f!1(x)" )"1" (expand "injective?" )"1" (skosimp :preds? t)"1" (expand * "intersection" "member" )"1" (flatten)"1" (inst - "x1!1" "x2!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil )"set" sets nil )"countable_set[T]" countable_props nil )"set[T]" countable_props nil )"(injective?[(Count!1), nat])" nil )"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 )nil countability nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3316998965"" (skolem!)"" (rewrite "intersection_commutative[T]" )"" (assert ) nil nil )) nil ))nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability nil )nil countability nil )nil countable_props nil )"countable_set[T]" nil ))nil ))nil 3316998965"" case "forall (n:nat,CountInf, Fin):card(Fin) <= n => ") "1" (skosimp)"1" (inst - "card(Fin!1)" "CountInf!1" "Fin!1" )"1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skosimp)"1" (expand "<=" )"1" (split)"1" (assert ) nil nil )"2" (lemma "card_is_0[T]" ("S" "Fin!1" ))"2" (replace -2)"2" (replace -1)"2" (rewrite "difference_emptyset1[T]" )"2" (typepred "CountInf!1" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "<=" -2)"2" (split -2)"1" (inst - "CountInf!1" "Fin!1" )"1" (assert ) nil nil )) nil )"2" (lemma "nonempty_card[T]" ("S" "Fin!1" ))"2" (assert )"2" (lemma "card_rest[T]" ("S" "Fin!1" ))"2" (split -1)"1" (replace -3)"1" (assert )"1" "remove(choose[T](Fin!1),CountInf!1)" "rest(Fin!1)" )"1" (assert )"1" "(difference[T](remove(choose[T](Fin!1), CountInf!1), rest(Fin!1)))=(difference[T](CountInf!1, Fin!1))" )"1" "1" "1" expand "difference" )"1" expand "rest" )"1" expand "nonempty?" )"1" assert )"1" expand "member" )"1" expand "remove" )"1" expand "member" )"1" "CountInf!1(x!1)" )"1" assert )"1" "Fin!1(x!1)" )"1" assert )"1" nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"finite_set[T]" countable_propsnil )"bool" sets nil )"finite_set[T]" nil )"set" sets nil )"bool" sets nil )"(p)" sets nil ) (rest const-decl "set" sets nil )"countable_set[T]" nil )"countably_infinite_set[T]" countable_props nil )nil finite_sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )nil sets_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"infinite_set[T]" nil )nil numbers nil )nil booleans 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 booleans nil )"bool" reals nil )nil naturalnumbers nil )nil countable_props nil )set type-eq-decl nil sets nil )"bool" countability nil )nil countability nil )"bool" finite_sets nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"set" sets nil ))nil ))nil 3316998965"" (grind :if-match nil )"" (inst + "LAMBDA (x: (difference[T](Count!1, S!1))): f!1(x)" )"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil )"set" sets nil )"countable_set[T]" countable_props nil )"set[T]" countable_props nil )"(injective?[(Count!1), nat])" nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"bool" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil countability nil )"bool" countability nil )nil countable_props nil ))nil ))nil 3316998965 ("" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets 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 )nil naturalnumbers nil )"finite_set[T]" countable_props nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"nat" countable_props nil )"[(x!1) -> below[N!1]]" countable_props nil )"bool" reals nil )nil nat_types nil )"(total_order?[real])" nil )nil countable_props nil )"bool" countability nil )"bool" functions nil ))nil ))nil 3316998965 ("" (judgement-tcc) nil nil )nil countable_props nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability nil )NOT const-decl "[bool -> bool]" booleans nil )nil countability 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 )nil naturalnumbers nil )"uncountable_set[T]" countable_props nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"nat" countable_props nil )"[(x!1) -> below[N!1]]" countable_props nil )nil nat_types nil )"bool" reals nil )"(total_order?[real])" nil )"bool" finite_sets nil )"bool" functions nil ))nil ))nil 3317000413"" (skolem + "X!1" )"" (typepred "X!1" )"" (lemma "infinite_def" ("X" "X!1" ))"" (replace 1)"" (flatten)"" (skosimp)"" (typepred "f!1" )"" "bijective_image[nat, (X!1)]" ("inj" "f!1" ))"" "bij_inv_is_bij[nat, ((image(f!1, fullset[nat])))]" "f" "f!1" ))"" (assert )"" "image[nat,(X!1)](f!1, fullset[nat])" )"1" (expand "subset?" )"1" (expand "member" )"1" (expand "extend" )"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (expand "is_countably_infinite" )"2" "inverse[nat, ((image[nat, (X!1)](f!1, fullset[nat])))](f!1)" )"2" "1" "1" "1" (assert ) nil nil ))nil ))nil )"2" "2" expand "bijective?" )"2" "2" "1" expand "injective?" )"1" "1" "x1!1" "x2!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" "2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil infinite_sets_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_props nil )nil function_image_aux nil )"D" function_inverse nil )"bool" functions nil )IF const-decl "[boolean, T, T -> T]" if_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"bool" functions nil )"bool" sets nil )"bool" sets nil )nil countability nil )"bool" countability nil )"infinite_set[T]" countable_props nil )"bool" booleans nil )"R" extend nil )"(injective?[nat, (X!1)])" countable_propsnil )nil function_inverse nil )"set[R]" function_image nil )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil infinite_nat_def nil ))nil 3317000591"" (skolem!)"" (use "countably_infinite_subset_exists" )"" (skolem-typepred)"" (use "infinite_nonempty[T]" )"" (expand * "nonempty?" "empty?" "member" )"" (skolem!)"" (inst + "remove(x!1, CountInf!1)" )"1" (expand * "strict_subset?" "subset?" "member" )"1" (split)"1" (expand * "remove" "member" )"1" (skosimp)"1" (inst - "x!2" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (decompose-equality)"2" (expand * "remove" "member" )"2" (inst - "x!1" )"2" (inst - "x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "countably_infinite_subset[T]" "CountInf" "CountInf!1" "Inf" "remove(x!1, CountInf!1)" ))"2" (assert )"2" (expand * "subset?" "remove" "member" )"2" (skosimp) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countable_propsnil )nil infinite_sets_def nil )"bool" finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_props nil )nil infinite_sets_def nil )"bool" sets nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"countable_set[T]" nil )"countably_infinite_set[T]" countable_props nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" countability nil )nil countability nil ))nil 3317002096"" (skosimp)"" (split)"1" (flatten)"1" (expand "is_countable" )"1" (skosimp)"1" (typepred "f!1" )"1" (expand "is_countably_infinite" )"1" case "is_finite[nat](image(f!1, fullset[(S!1)]))" )"1" (assert )"1" (hide 2 3)"1" (expand "fullset" )"1" (expand "is_finite" )"1" (skosimp)"1" (inst + "N!1" "f!2 o f!1" )"1" expand "injective?" )"1" expand "o " )"1" "1" "x1!1" )"1" "x2!1" )"1" "x1!1" "x2!1" )"1" assert )"1" "f!1(x1!1)" "f!1(x2!1)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "image" )"2" "x1!1" )"2" (inst + "x1!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "nonempty?(S!1)" )"1" "bijective_image[(S!1), nat]" "inj" "f!1" ))"1" case "exists (phi:(bijective?[nat,(image(f!1, fullset[(S!1)]))])):TRUE" )"1" (skosimp)"1" (typepred "phi!1" )"1" "bijective_inverse_exists[nat, (image(f!1, fullset[(S!1)]))]" "f" "phi!1" ))"1" expand "exists1" )"1" "1" "psi!1" )"1" "1" "bij_inv_is_bij_alt[nat, (image(f!1, fullset[(S!1)]))]" "f" "phi!1" "g" "psi!1" ))"1" "psi!1 o f!1" )"1" "1" expand "bijective?" )"1" "1" "1" expand "o" )"1" expand "injective?" )"1" "1" "x1!1" "x2!1" )"1" assert )"1" "f!1(x1!1)" "f!1(x2!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "o" )"2" expand "surjective?" )"2" "2" "y!1" )"2" "2" "x!1" )"2" "x!1" )"2" "2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 4)"2" "REMOVE_MIN" "lambda (X:infinite_set[nat]): remove(min(X),X)" )"2" case "forall (X: infinite_set[nat]): strict_subset?(REMOVE_MIN(X),X)" )"1" "GG" "lambda (n:nat): iterate(REMOVE_MIN,n)(image[(S!1), nat](f!1, fullset[(S!1)]))" )"1" case "FORALL (X: infinite_set[nat]): min[nat](X)<min[nat](REMOVE_MIN(X))" )"1" "FF" "lambda (n:nat): min[nat](GG(n))" )"1" case "forall (n:nat): subset?(GG(n),image(f!1, fullset[(S!1)]))" )"1" case "forall (n:nat): image(f!1, fullset[(S!1)])(FF(n))" )"1" case "forall (i,j:nat): i<j => FF(i)<FF(j)" )"1" case "forall (n:nat): n <= FF(n)" )"1" case "forall (n:(image(f!1, fullset[(S!1)]))): exists (k:nat): FF(k)=n" )"1" "FF" )"1" "1" nil nil )"2" expand "bijective?" )"2" "1" expand "injective?" )"1" "i!1" "j!1" ))"1" "1" "trich_lt" "x" "i!1" "y" "j!1" ))"1" "1" "i!1" "j!1" )"1" assert )nil nil ))nil )"2" nil nil )"3" "j!1" "i!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (i,n,k:nat): image(f!1, fullset[(S!1)])(k) & FF(i)<=k & k<=FF(i+n) => exists (j:nat): FF(j) = k" )"1" "1" "n!1" )"1" "0" "FF(n!1)" "n!1" )"1" assert )"1" "1" nil nil )"2" "2" expand "FF" )"2" expand "GG" )"2" expand "REMOVE_MIN" )"2" expand "iterate" )"2" "n!1" )"2" "min[nat](image[(S!1), nat](f!1, fullset[(S!1)]))" )"2" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "<=" "3" "1" "n!1" "FF(n!1)" )"1" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" "1" "i!1" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "<=" "2" "1" "i!1+1" "k!1" )"1" assert )"1" "1" nil nil )"2" "2" case "k!1<FF(1 + i!1)" )"1" "1" expand "FF" )"1" "1" "min[nat](GG(1 + i!1))" )"1" "k!1" )"1" "1" assert )nil nil )"2" case "forall (n:nat): min[nat](GG(n)) < k!1 => GG(n+1)(k!1)" )"1" "i!1" )"1" assert )nil nil ))nil )"2" "2" "n" )"1" "1" "0" "1" )"1" assert )"1" expand "GG" )"1" expand "iterate" )"1" expand "REMOVE_MIN" )"1" expand "iterate" )"1" expand "remove" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "j!2" "1+j!2" )"2" assert )"2" assert )"2" expand "GG" )"2" expand "iterate" "2" expand "REMOVE_MIN" "2" expand "remove" "2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" (assert ) nil nil )"2" "2" "j!1" "j!1+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (i,n:nat): FF(i)< FF(i+1+n)" )"1" "1" "i!1" "j!1-i!1-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "2" "n" )"1" "1" expand "FF" )"1" expand "GG" )"1" expand "iterate" "1" "iterate(REMOVE_MIN, i!1) ") nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" )"2" "LHS" "FF(i!1)" )"2" expand "FF" )"2" expand "GG" )"2" expand "iterate" "2" "iterate(REMOVE_MIN, 1 + i!1 + j!1) ") "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "FF" )"2" "min[nat](GG(n!1))" )"2" "n!1" )"2" expand "subset?" )"2" "min[nat](GG(n!1))" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" expand "GG" )"1" expand "iterate" )"1" expand "subset?" )"1" nil nil ))nil ))nil ))nil )"2" "2" expand "strict_subset?" )"2" expand "GG" )"2" expand "iterate" 1)"2" "iterate(REMOVE_MIN, j!1) ") "2" "2" "2" expand "subset?" )"2" "2" "x!1" )"2" "x!1" )"2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "min[nat](X!1)" )"2" expand "REMOVE_MIN" )"2" "min[nat](remove(min(X!1), X!1))" )"2" expand "remove" -1 1)"2" "2" expand "member" )"2" "min[nat](remove(min(X!1), X!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" "2" "2" expand "REMOVE_MIN" )"2" expand "strict_subset?" )"2" "min(X!1)" )"2" expand "remove" )"2" expand "member" )"2" "1" expand "subset?" )"1" "n!1" ))"1" expand "member" )"1" "n!1" )"1" assert )"1" "min(X!1)=n!1" )"1" assert )nil nil )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "/=" 1)"2" replace -1 -2 rl)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (lemma "infinite_nonempty[T]" )"2" (inst - "S!1" )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (split)"1" (expand "is_countable" )"1" (expand "is_finite" )"1" (skosimp)"1" (inst + "f!1" )"1" (expand "injective?" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "is_countably_infinite" )"2" (expand "is_countable" )"2" (skosimp)"2" (typepred "f!1" ) (("2" (inst + "f!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countability 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 )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"set[R]" function_image nil )"bool" finite_sets nil )"set[T]" countable_props nil )"(injective?[(S!1), nat])" countable_propsnil )"bool" booleans nil )"T3" function_props nil )nil nat_types nil )"bool" reals nil )nil infinite_sets_def nil )nil function_image_aux nil )"bool" sets nil )"bool" sets nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"[n: nat -> {a | GG(n)(a) AND (FORALL (x: nat): GG(n)(x) IMPLIES a <= x)}]" nil )"[nat -> infinite_set[nat]]" countable_propsnil )"nonneg_int" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"[infinite_set[nat] -> infinite_set[nat]]" countable_props nil )"posint" nil )nil defined_types nil )nil naturalnumbers nil )"posint" nil )"odd_int" integers nil )"bool" sets nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" countable_props nil )"nat" countable_props nil )"int" integers nil )"even_int" integersnil )"T" function_iterate nil )"boolean" notequal nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set" sets nil )"[T, T -> boolean]" equalities nil )nil infinite_sets_def nil )"infinite_set[nat]" nil )nil function_inverse_defnil )"[(image(f!1, fullset[(S!1)])) -> nat]" nil )"bool" functions nil )"bool" function_inverse_def nil )nil function_inverse_def nil )"bool" exists1 nil )"bool" functions nil )"bool" sets nil )"bool" countability nil )"[(S!1) -> below[N!1]]" countable_props nil )"nat" countable_props nil ))nil 3316998965"" (skolem + ("X!1" "Y!1" ))"" (typepred "X!1" )"" (typepred "Y!1" )"" (name "DD" "difference(X!1,Y!1)" )"" (lemma "countable_difference" ("Count" "X!1" "S" "Y!1" ))"" (replace -2)"" (lemma "union_difference" ("a" "Y!1" "b" "X!1" ))"" (replace -1)"" (replace -3)"" "difference_disjoint" "a" "Y!1" "b" "X!1" ))"" (replace -4)"" (hide -2 -4 -6)"" (rewrite "countable_card" )"" (split)"1" "N" "card(DD)" )"1" "card_bij[T]" "N" "N" "S" "DD" ))"1" assert )"1" "1" expand "is_countably_infinite" )"1" "1" "f!2" )"1" "lambda (x:(union(Y!1, DD))): if DD(x) then f!1(x) else N+f!2(x) endif" )"1" expand "bijective?" )"1" "1" "1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "union" )"1" expand "member" )"1" "1" "1" assert )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "x1!1" )"1" "x2!1" )"1" assert )"1" assert )"1" "x1!1" "x2!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "x1!1" )"2" "x2!1" )"2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "x1!1" )"1" "x2!1" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x1!1" "x2!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "surjective?" )"2" "2" case "y!1>=N" )"1" "y!1-N" )"1" "1" "x!1" )"1" "x!1" )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "x!1" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "union" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "y!1" )"1" "1" "x!1" )"1" assert )nil nil )"2" expand "union" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "union" )"2" expand "member" )"2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" expand "is_countably_infinite" )"2" "2" "f!1" )"2" "f!2" )"2" "lambda (x:(union(Y!1, DD))): if DD(x) then 2*f!1(x) else 2*f!2(x)+1 endif" )"1" expand "bijective?" )"1" "1" "1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "union" )"1" expand "member" )"1" "1" "1" "x1!1" "x2!1" )"1" assert )"1" "x1!1" )"1" "x2!1" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x2!1" )"2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "1" "x1!1" )"1" assert )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "x1!1" "x2!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "surjective?" )"2" "2" case "even?(y!1)" )"1" expand "even?" )"1" "1" replace "1" "j!1" )"1" "1" "x!1" )"1" assert )nil nil )"2" expand "union" )"2" expand "member" )"2" 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" "x!1" )"1" "x!1" )"1" assert )"1" assert )nil nil ))nil ))nil )"2" expand "union" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "union" )"2" expand "member" )"2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countability nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"[T, T -> boolean]" equalities nil )"countable_set[T]" nil )nil sets_lemmas nil )nil finite_sets nil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )nil integers nil )"set" sets nil )"countably_infinite_set" countable_propsnil )"countable_set[T]" countable_props nil )"[bool, bool -> bool]" booleans nil )"(bijective?[(Y!1), nat])" countable_propsnil )"[(DD) -> below[N]]" countable_props nil )"{n: nat | n = Card(DD)}" countable_props nil )"(strict_total_order?[real])" real_props nil )"(DD)" countable_props nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" countable_props nil )"(Y!1)" countable_props nil )"bool" functions nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"set" sets nil )"bool" functions nil )"bool" functions nil )"infinite_set[T]" nil )nil numbers nil )"bool" finite_sets nil )nil finite_sets nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"(union(Y!1, DD))" countable_props nil )"(union(Y!1, DD))" countable_props nil )"posint" nil )"odd_int" integers nil )"bool" integers nil )"int" countable_props nil )"(DD)" countable_props nil )"bool" integers nil )"(Y!1)" countable_props nil )"int" countable_props nil )nil naturalnumbers nil )"(bijective?[(Y!1), nat])" countable_propsnil )"(bijective?[(DD), nat])" countable_propsnil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" nil )"odd_int" integers nil )nil countable_props nil )nil sets_lemmas nil )nil countable_props nil )"bool" countability nil )nil countability nil ))nil ))nil 3316998965"" (skolem!)"" (rewrite "union_commutative[T]" ) (("" (assert ) nil nil )) nil ))nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability nil )nil countability nil )"bool" countability nil )nil countability nil )nil countable_props nil )"countably_infinite_set[T]" countable_props nil ))nil ))nil 3316998965"" (skolem-typepred)"" (auto-rewrite "countable_card" )"" (smash)"1" (use "finite_union[T]" ) nil nil )"2" (use "countably_infinite_union2" ) nil nil )"3" (use "countably_infinite_union1" ) nil nil )"4" (use "countably_infinite_union1" ) nil nil ))nil ))nil ))nil )nil countable_props nil )"bool" countability nil )nil countability nil )nil countable_props nil )"bool" finite_sets nil )nil finite_sets nil )nil finite_sets nil )nil countable_props nil )nil countability nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3454922909"" (skosimp)"" (split)"1" (flatten)"1" (lemma "countable_card" ("S" "S!1" ))"1" (replace -1 1)"1" (hide -1)"1" (case-replace "is_finite(S!1)" )"1" (lemma "infinite_countably_infinite" )"1" (inst - "S!1" ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "countable_card" ("S" "S!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_props nil )nil countable_props nil )nil countable_props nil )"set[T]" countable_props nil )"bool" countability nil )nil countability nil )"bool" finite_sets nil ))nil 3454937862"" (lemma "finite_countable" ) (("" (inst - "emptyset[T]" ) nil nil ))nil )"finite_set" finite_sets nil )"finite_set" countable_props nil )nil countable_props nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set" sets nil )nil countable_props nil ))nil 3454937897"" (skosimp)"" (lemma "finite_countable" )"" (inst - "singleton(t!1)" ) nil nil )) nil ))nil )nil countable_props nil )"(singleton?)" sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_props nil )"non_empty_finite_set" countable_props nil ))nil 3462010233"" (grind :if-match nil )"" (inst + "N!1" "f!2 o f!1" )"" (expand "o" )"" (skosimp)"" (inst - "f!1(x1!1)" "f!1(x2!1)" )"" (inst - "x1!1" "x2!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"T3" function_props nil )nil nat_types nil )"bool" reals nil )"(total_order?[real])" 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 )nil naturalnumbers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil finite_sets nil )"bool" finite_sets nil )"bool" card_comp_set nil )nil countable_props nil )"bool" functions nil ))nil ))nil 3462010266"" (grind :if-match nil )"" (inst + "N!1" "f!2 o f!1" )"" (skosimp)"" (expand "o" )"" (inst - "x1!1" "x2!1" )"" (inst - "f!1(x1!1)" "f!1(x2!1)" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil nat_types nil )"T3" function_props nil )"(total_order?[real])" 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 )nil naturalnumbers nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil infinite_sets_def nil )"bool" finite_sets nil )"bool" card_comp_set nil )nil countable_props nil )"bool" functions nil ))nil ))nil 3462010285"" (skosimp :preds? t)"" (expand * "is_countably_infinite" "card_eq" )"" (skosimp* t)"" (use "composition_bijective[(S!1), (CountInf!1), nat]" )"" (inst + "f!1 o f!2" ) nil nil )) nil ))nil ))nil ))nil )"bool" card_comp_set nil )nil function_props nil )"[(S!1) -> (CountInf!1)]" countable_propsnil )"countably_infinite_set" nil )"set[T]" countable_props nil )"(bijective?[(CountInf!1), nat])" nil )"T3" function_props nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil countable_props nil )set type-eq-decl nil sets nil )"bool" countability nil )nil countability nil ))nil ))nil 3462010304"" (skosimp* t)"" (expand * "is_countable" "card_le" )"" (skosimp* t)"" (use "composition_injective[(S!1), (Count!1), nat]" )"" (inst + "f!1 o f!2" ) nil nil )) nil ))nil ))nil ))nil )"bool" card_comp_set nil )nil function_props nil )"[(S!1) -> (Count!1)]" countable_props nil )"countable_set[T]" countable_props nil )"set[T]" countable_props nil )"(injective?[(Count!1), nat])" nil )"T3" function_props nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil countable_props nil )set type-eq-decl nil sets nil )"bool" countability nil )nil countability nil ))nil ))nil 3462010326"" (skosimp* t)"" (expand * "card_ge" "is_countable" )"" (skosimp* t)"" (use "composition_injective[(Uncount!1), (S!1), nat]" )"" (inst + "f!2 o f!1" ) nil nil )) nil ))nil ))nil ))nil )"bool" card_comp_set nil )nil function_props nil )"[(Uncount!1) -> (S!1)]" countable_propsnil )"set[T]" countable_props nil )"uncountable_set[T]" countable_propsnil )"(injective?[(S!1), nat])" countable_propsnil )"T3" function_props nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil countable_props nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability nil )NOT const-decl "[bool -> bool]" booleans nil )nil countability nil ))nil ))nil 3462010351"" (expand * "is_countably_infinite" "card_eq" )"" (skosimp* t)"" (use "bijective_inverse_exists[(Q!1), nat]" )"" (use "bijective_inverse_exists[(R!1), nat]" )"" (expand "exists1" )"" (skosimp*)"" (assert )"" "bij_left_right[(Q!1), nat]" "f" "f!2" "g" "x!2" ))"" (use "bij_inv_is_bij_alt[(Q!1), nat]" )"" "bij_left_right[(R!1), nat]" "f" "f!1" "g" "x!1" ))"" (use "bij_inv_is_bij_alt[(R!1), nat]" )"" (flatten)"" (delete -7 -8 -9 -10)"" "LAMBDA (p: (S!1)): IF Q!1(p) THEN IF odd?(f!2(p)) THEN x!1((f!2(p) - 1) / 2) ELSE x!2(f!2(p) / 2) ENDIF ELSE p ENDIF" )"1" expand "bijective?" )"1" "1" expand "injective?" )"1" "1" "1" "(f!2(x1!1) - 1) / 2" "(f!2(x2!1) - 1) / 2" )"1" assert )"1" "x1!1" "x2!1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" "odd_div2" )"2" assert )"2" expand "odd?" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "odd_div2" )"3" assert )"3" expand "odd?" )"3" nil nil ))nil ))nil ))nil ))nil )"2" expand *"subset?" "disjoint?" "empty?" "intersection" "member" )"2" "x!1((f!2(x1!1) - 1) / 2)" )"1" "x!1((f!2(x1!1) - 1) / 2)" )"1" (assert ) nil nil )"2" "odd_div2" )"2" assert )"2" expand "odd?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "odd_div2" )"2" assert )"2" expand "odd?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "x2!1" )"3" expand *"disjoint?" "empty?" "intersection" "member" )"3" "x2!1" )"3" (assert ) nil nil ))nil ))nil ))nil )"4" expand *"subset?" "disjoint?" "empty?" "intersection" "member" )"4" "x!2(f!2(x1!1) / 2)" )"1" "x!2(f!2(x1!1) / 2)" )"1" (assert ) nil nil )"2" "2" rewrite "odd_iff_not_even" )"2" "even_div2" )nil nil ))nil ))nil ))nil )"2" rewrite "odd_iff_not_even" )"2" "even_div2" )nil nil ))nil ))nil ))nil )"5" "f!2(x1!1) / 2" "f!2(x2!1) / 2" )"1" assert )"1" "x1!1" "x2!1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" rewrite "odd_iff_not_even" )"2" "even_div2" )nil nil ))nil ))nil )"3" rewrite "odd_iff_not_even" )"3" "even_div2" )nil nil ))nil ))nil )"6" expand *"disjoint?" "empty?" "intersection" "member" )"6" "x1!1" )"6" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" expand * "union" "member" )"2" "1" case "Q!1(y!1)" )"1" assert )"1" "x!2(f!2(y!1) * 2)" )"1" "1" expand "right_inverse?" "1" "2 * f!2(y!1)" )"1" replace -10)"1" rewrite "odd_iff_not_even" )nil nil ))nil ))nil ))nil )"2" expand "right_inverse?" "2" "2 * f!2(y!1)" )"2" replace -9)"2" expand "left_inverse?" "2" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand *"subset?" "member" )"2" "x!2(2 * f!2(y!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "y!1" )"2" (assert ) nil nil ))nil ))nil )"2" "x!2(f!1(y!1) * 2 + 1)" )"1" assert )"1" expand "right_inverse?" "1" "1 + 2 * f!1(y!1)" )"1" replace -8)"1" expand "left_inverse?" "1" "y!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand *"subset?" "member" )"2" "x!2(1 + 2 * f!1(y!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "union" "member" ) nil nil )"3" expand * "subset?" "union" "member" )"3" "3" "x!2(f!2(p!1) / 2)" )"1" (assert ) nil nil )"2" rewrite "odd_iff_not_even" )"2" "even_div2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" rewrite "odd_iff_not_even" )"4" "even_div2" )"4" (assert ) nil nil ))nil ))nil ))nil )"5" (expand * "union" "member" ) nil nil )"6" "6" "odd_div2" )"6" assert )"6" expand "odd?" )"6" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )set type-eq-decl nil sets nil )nil countable_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil function_inverse_def nil )"bool" function_inverse_def nil )"int" integers nil )"nonneg_rat" nil )"rat" rationals nil )"set[T]" countable_props nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" integers nil )"set[T]" countable_props nil )"(bijective?[(Q!1), nat])" countable_propsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[nat -> (R!1)]" countable_props nil )"set[T]" countable_props nil )"set" sets nil )"[nat -> (Q!1)]" countable_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )nil naturalnumbers nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"(total_order?[real])" nil )"(S!1)" countable_props nil )"(S!1)" countable_props nil )nil naturalnumbers nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" functions nil )"bool" function_inverse_def nil )"bool" function_inverse_def nil )"(union(S!1, R!1))" countable_props nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"even_int" integersnil )"odd_int" integers nil )"posint" nil )"even_int" integersnil )"(bijective?[(R!1), nat])" countable_propsnil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"odd_int" integers nil )"bool" functions nil )"(S!1)" countable_props nil )nil function_inverse_def nil )"(partial_order?[set[T]])" nil )"bool" exists1 nil )nil function_inverse_defnil )"bool" countability nil )"bool" card_comp_set nil ))nil ))nil 3462010371"" (skosimp)"" (assert )"" (lemma "bij_exists[T]" ("S" "R!1" ))"" (expand * "is_countably_infinite" "card_eq" )"" (skosimp* :preds? t)"" (use "bijective_inverse_exists[(Q!1), nat]" )"" (assert )"" "bijective_inverse_exists[(R!1), below(card(R!1))]" "f" "f!1" ))"" (expand "exists1" )"" (skosimp*)"" (assert )"" "bij_left_right[(Q!1), nat]" "f" "f!2" "g" "x!2" ))"" "bij_left_right[(R!1), below(card(R!1))]" "f" "f!1" "g" "x!1" ))"" "bij_inv_is_bij_alt[(R!1), below(card(R!1))]" "f" "f!1" "g" "x!1" ))"" "bij_inv_is_bij_alt[(Q!1), nat]" "f" "f!2" "g" "x!2" ))"" "" "" "LAMBDA (p: (S!1)): IF Q!1(p) THEN IF f!2(p) < card(R!1) THEN x!1(f!2(p)) ELSE x!2(f!2(p) - card(R!1)) ENDIF ELSE p ENDIF" )"1" expand "bijective?" )"1" "1" expand "injective?" )"1" "1" "1" "f!2(x1!1)" "f!2(x2!1)" )"1" "x1!1" "x2!1" )"1" assert )nil nil ))nil ))nil )"2" expand *"subset?" "disjoint?" "empty?" "intersection" "member" )"2" "x!1(f!2(x1!1))" )"2" "x!1(f!2(x1!1))" )"2" assert )nil nil ))nil ))nil ))nil )"3" "x2!1" )"3" expand *"disjoint?" "empty?" "intersection" "member" )"3" "x2!1" )"3" assert )nil nil ))nil ))nil ))nil )"4" expand *"subset?" "disjoint?" "empty?" "intersection" "member" )"4" "x!2(f!2(x1!1) - card(R!1))" )"4" "x!2(f!2(x1!1) - card(R!1))" )"4" assert )nil nil ))nil ))nil ))nil )"5" "f!2(x1!1) - card(R!1)" "f!2(x2!1) - card(R!1)" )"5" "x1!1" "x2!1" )"5" assert )nil nil ))nil ))nil )"6" expand *"disjoint?" "empty?" "intersection" "member" )"6" "x1!1" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" expand *"union" "member" )"2" "1" case "Q!1(y!1)" )"1" assert )"1" "x!2(f!2(y!1) + card(R!1))" )"1" "1" expand "right_inverse?" "1" "card(R!1) + f!2(y!1)" )"1" assert )nil nil ))nil ))nil )"2" expand "right_inverse?" "2" "card(R!1) + f!2(y!1)" )"2" assert )"2" expand "left_inverse?" "2" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand *"subset?" "member" )"2" "x!2(card(R!1) + f!2(y!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "y!1" )"2" assert )nil nil ))nil ))nil )"2" "x!2(f!1(y!1))" )"1" assert )"1" expand "right_inverse?" "1" "f!1(y!1)" )"1" replace "1" expand "left_inverse?" "1" "y!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand *"subset?" "member" )"2" "x!2(f!1(y!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand * "union" "member" )nil nil )"3" expand *"subset?" "union" "member" )"3" "3" assert )"3" "x!2(f!2(p!1) - card(R!1))" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" expand * "union" "member" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(partial_order?[set[T]])" nil )"bool" card_comp_set nil )"bool" countability nil )nil function_inverse_defnil )nil naturalnumbers nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil function_inverse_def nil )"bool" function_inverse_def nil )nil function_inverse_def nil )"int" integers nil )"set[T]" countable_props nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set[T]" countable_props nil )"(bijective?[(Q!1), nat])" countable_propsnil )"set[T]" countable_props nil )"set" sets nil )"[below(card(R!1)) -> (R!1)]" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[nat -> (Q!1)]" countable_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(total_order?[real])" nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"bool" function_inverse_def nil )"bool" function_inverse_def nil )"(union(S!1, R!1))" countable_props nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"odd_int" integers nil )"[(R!1) -> below(card(R!1))]" nil )"bool" functions nil )"bool" exists1 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 )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil finite_sets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )nil countable_props nil ))nil ))nil 3462010390"" (skolem-typepred)"" (use "union_difference[T]" )"" (use "difference_disjoint[T]" )"" (assert )"" (use "countably_infinite_subset_exists" )"" (skolem-typepred)"" (rewrite "countable_card" )"" (split)"1" "countable_finite_subset_union" "Q" "CountInf!1" "R" "difference(Count!1, Inf!1)" "S" "Inf!1" ))"1" (assert )"1" (use "finite_difference[T]" ) nil nil ))nil ))nil )"2" (use "countable_difference" )"2" (rewrite "countable_card" )"2" (split)"1" "countable_finite_subset_union" "Q" "CountInf!1" "R" "difference(Count!1, Inf!1)" "S" "Inf!1" ))"1" (assert ) nil nil )) nil )"2" "countably_infinite_subset_union" "Q" "CountInf!1" "R" "difference(Count!1, Inf!1)" "S" "Inf!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sets_lemmas nil )"infinite_set[T]" nil )"countable_set[T]" nil )nil countability nil )"bool" countability nil )"(partial_order?[set[T]])" nil )nil finite_sets nil )nil finite_sets nil )"set" sets nil )nil countable_propsnil )nil countable_propsnil )nil countable_props nil )nil countable_props nil )nil countable_propsnil )nil sets_lemmas nil )nil countability nil )"bool" countability nil )nil infinite_sets_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countable_props nil ))nil ))nil 3462010407"" (skosimp :preds? t)"" "countable_intersection2" ("S" "S!1" "Count" "Count!1" ))"" case "S!1 = union(difference(S!1, Count!1), intersection(S!1, Count!1))" )"1" (lemma "infinite_countable_union" )"1" "difference(S!1, Count!1)" "intersection(S!1, Count!1)" )"1" (replace -2 -1 :dir rl)"1" (rewrite "card_eq_symmetric" ) nil nil )) nil ))nil ))nil )"2" (hide -1 -2 2 3) (("2" (grind-with-ext) nil nil )) nil ))nil ))nil ))nil )nil countable_props nil )"bool" sets nil )nil countable_props nil )nil card_comp_set_props nil )nil infinite_sets_def nil )"countable_set[T]" countable_props nil )"set[T]" countable_props nil )"bool" finite_sets nil )"countable_set[T]" nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"set" sets nil )"set" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil countable_props nil )set type-eq-decl nil sets nil )"bool" countability nil )nil countability nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.203Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
