|
(countable_props
(infinite_countably_infinite 0
(infinite_countably_infinite-1 nil 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)
((countably_infinite_set type-eq-decl nil countability nil)
(is_countably_infinite const-decl "bool" countability nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil countable_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(infinite_def2 formula-decl nil infinite_nat_def nil)
(surjective? const-decl "bool" functions 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil))
nil))
(countably_infinite_add 0
(countably_infinite_add-1 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"
(inst +
"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)
((member const-decl "bool" sets nil)
(infinite_add application-judgement "infinite_set[T]"
countable_props nil)
(member_add formula-decl nil sets_lemmas 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(f!1 skolem-const-decl "(bijective?[(CountInf!1), nat])"
countable_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(CountInf!1 skolem-const-decl "countably_infinite_set"
countable_props nil)
(t!1 skolem-const-decl "T" countable_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(countably_infinite_set type-eq-decl nil countability nil)
(is_countably_infinite const-decl "bool" countability nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil countable_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(countable_add 0
(countable_add-1 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"
(inst +
"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"
(split)
(("1" (assert) nil nil)
("2"
(inst - "x1!1" "x2!1")
(("2"
(case-replace "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)
((member const-decl "bool" sets nil)
(member_add formula-decl nil sets_lemmas nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nonempty? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(t!1 skolem-const-decl "T" countable_props nil)
(Count!1 skolem-const-decl "countable_set[T]" countable_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(f!1 skolem-const-decl "(injective?[(Count!1), nat])"
countable_props nil)
(x1!1 skolem-const-decl "(add[T](t!1, Count!1))" countable_props
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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(injective? const-decl "bool" functions nil)
(countable_set nonempty-type-eq-decl nil countability nil)
(is_countable const-decl "bool" countability nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil countable_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(countably_infinite_remove 0
(countably_infinite_remove-1 nil 3316998965
("" (skolem-typepred)
(("" (case "member(t!1, CountInf!1)")
(("1" (expand "is_countably_infinite")
(("1" (skolem-typepred)
(("1"
(inst +
"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)
((member const-decl "bool" sets 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(/= const-decl "boolean" notequal nil)
(infinite_remove application-judgement "infinite_set[T]"
countable_props 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(f!1 skolem-const-decl "(bijective?[(CountInf!1), nat])"
countable_props nil)
(CountInf!1 skolem-const-decl "countably_infinite_set"
countable_props nil)
(t!1 skolem-const-decl "T" countable_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(remove const-decl "set" sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(member_remove formula-decl nil sets_lemmas nil)
(countably_infinite_set type-eq-decl nil countability nil)
(is_countably_infinite const-decl "bool" countability nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil countable_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(countable_remove 0
(countable_remove-1 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"
(inst +
"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)
((countable_set nonempty-type-eq-decl nil countability nil)
(is_countable const-decl "bool" countability nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil countable_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil)
(t!1 skolem-const-decl "T" countable_props nil)
(Count!1 skolem-const-decl "countable_set[T]" countable_props nil)
(f!1 skolem-const-decl "(injective?[(Count!1), nat])"
countable_props 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(injective? const-decl "bool" functions nil)
(member_remove formula-decl nil sets_lemmas nil))
nil))
(countably_infinite_rest 0
(countably_infinite_rest-1 nil 3316998965
("" (expand "rest") (("" (propax) nil nil)) nil)
((rest const-decl "set" sets nil)
(countably_infinite_remove application-judgement
"countably_infinite_set[T]" countable_props nil)
(countable_remove application-judgement "countable_set[T]"
countable_props nil))
nil))
(countable_rest 0
(countable_rest-1 nil 3316998965
("" (expand "rest") (("" (propax) nil nil)) nil)
((rest const-decl "set" sets nil)
(countable_remove application-judgement "countable_set[T]"
countable_props nil))
nil))
(countable_intersection1 0
(countable_intersection1-1 nil 3316998965
("" (skolem-typepred)
(("" (expand "is_countable")
(("" (skolem-typepred)
((""
(inst + "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)
((intersection const-decl "set" sets nil)
(Count!1 skolem-const-decl "countable_set[T]" countable_props nil)
(S!1 skolem-const-decl "set[T]" countable_props nil)
(f!1 skolem-const-decl "(injective?[(Count!1), nat])"
countable_props nil)
(member const-decl "bool" sets nil)
(injective? 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)
(countable_set nonempty-type-eq-decl nil countability nil)
(is_countable const-decl "bool" countability nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil countable_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(countable_intersection2 0
(countable_intersection2-1 nil 3316998965
("" (skolem!)
(("" (rewrite "intersection_commutative[T]")
(("" (assert) nil nil)) nil))
nil)
((intersection_commutative 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 nil)
(countable_set nonempty-type-eq-decl nil countability nil)
(T formal-type-decl nil countable_props nil)
(countable_intersection1 application-judgement "countable_set[T]"
countable_props nil))
nil))
(countably_infinite_difference 0
(countably_infinite_difference-1 nil 3316998965
(""
(case "forall (n:nat,CountInf, Fin):card(Fin) <= n =>
is_countably_infinite[T](difference[T](CountInf, Fin))")
(("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"
(inst -
"remove(choose[T](Fin!1),CountInf!1)"
"rest(Fin!1)")
(("1" (assert)
(("1"
(case-replace
"(difference[T](remove(choose[T](Fin!1), CountInf!1), rest(Fin!1)))=(difference[T](CountInf!1, Fin!1))")
(("1"
(hide -1 -3 -4 2)
(("1"
(apply-extensionality :hide? t)
(("1"
(expand "difference")
(("1"
(expand "rest")
(("1"
(expand "nonempty?")
(("1"
(assert)
(("1"
(expand "member")
(("1"
(expand "remove")
(("1"
(expand "member")
(("1"
(case-replace
"CountInf!1(x!1)")
(("1"
(assert)
(("1"
(case-replace
"Fin!1(x!1)")
(("1"
(assert)
(("1"
(flatten)
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_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(finite_rest application-judgement "finite_set[T]" countable_props
nil)
(member const-decl "bool" sets nil)
(finite_remove application-judgement "finite_set[T]"
countable_props nil)
(remove const-decl "set" sets nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil) (rest const-decl "set" sets nil)
(countable_remove application-judgement "countable_set[T]"
countable_props nil)
(countably_infinite_remove application-judgement
"countably_infinite_set[T]" countable_props nil)
(card_rest formula-decl nil finite_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)
(difference_emptyset1 formula-decl nil sets_lemmas nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(card_is_0 formula-decl nil finite_sets nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(infinite_difference application-judgement "infinite_set[T]"
countable_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil countable_props nil)
(set type-eq-decl nil sets nil)
(is_countably_infinite const-decl "bool" countability nil)
(countably_infinite_set type-eq-decl nil countability nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(difference const-decl "set" sets nil))
nil))
(countable_difference 0
(countable_difference-1 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)
((difference const-decl "set" sets nil)
(Count!1 skolem-const-decl "countable_set[T]" countable_props nil)
(S!1 skolem-const-decl "set[T]" countable_props nil)
(f!1 skolem-const-decl "(injective?[(Count!1), nat])"
countable_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(member const-decl "bool" sets 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(injective? const-decl "bool" functions nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(countable_set nonempty-type-eq-decl nil countability nil)
(is_countable const-decl "bool" countability nil)
(T formal-type-decl nil countable_props nil))
nil))
(finite_countable 0
(finite_countable-1 nil 3316998965 ("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" 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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(x!1 skolem-const-decl "finite_set[T]" countable_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(N!1 skolem-const-decl "nat" countable_props nil)
(f!1 skolem-const-decl "[(x!1) -> below[N!1]]" countable_props nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T formal-type-decl nil countable_props nil)
(is_countable const-decl "bool" countability nil)
(injective? const-decl "bool" functions nil))
nil))
(infinite_uncountable 0
(infinite_uncountable-1 nil 3316998965 ("" (judgement-tcc) nil nil)
((T formal-type-decl nil countable_props 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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(uncountable_set type-eq-decl nil countability 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(x!1 skolem-const-decl "uncountable_set[T]" countable_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(N!1 skolem-const-decl "nat" countable_props nil)
(f!1 skolem-const-decl "[(x!1) -> below[N!1]]" countable_props nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(is_finite const-decl "bool" finite_sets nil)
(injective? const-decl "bool" functions nil))
nil))
(countably_infinite_subset_exists 0
(countably_infinite_subset_exists-1 nil 3317000413
("" (skolem + "X!1")
(("" (typepred "X!1")
(("" (lemma "infinite_def" ("X" "X!1"))
(("" (replace 1)
(("" (flatten)
(("" (skosimp)
(("" (typepred "f!1")
((""
(lemma "bijective_image[nat, (X!1)]" ("inj" "f!1"))
((""
(lemma
"bij_inv_is_bij[nat, ((image(f!1, fullset[nat])))]"
("f" "f!1"))
(("" (assert)
((""
(inst + "image[nat,(X!1)](f!1, fullset[nat])")
(("1" (expand "subset?")
(("1" (expand "member")
(("1" (expand "extend")
(("1"
(hide-all-but 2)
(("1"
(skosimp)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "extend")
(("2" (expand "is_countably_infinite")
(("2"
(inst +
"inverse[nat, ((image[nat, (X!1)](f!1, fullset[nat])))](f!1)")
(("2"
(split)
(("1"
(skosimp)
(("1"
(lift-if 1)
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2"
(expand "bijective?")
(("2"
(flatten)
(("2"
(split)
(("1"
(expand "injective?")
(("1"
(skosimp)
(("1"
(inst -2 "x1!1" "x2!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(expand "surjective?")
(("2"
(skosimp)
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((infinite_set type-eq-decl nil infinite_sets_def nil)
(NOT const-decl "[bool -> bool]" booleans 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 countable_props nil)
(bijective_image formula-decl nil function_image_aux nil)
(inverse const-decl "D" function_inverse nil)
(bijective? const-decl "bool" functions nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(surjective? const-decl "bool" functions nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(countably_infinite_set type-eq-decl nil countability nil)
(is_countably_infinite const-decl "bool" countability nil)
(X!1 skolem-const-decl "infinite_set[T]" countable_props nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(f!1 skolem-const-decl "(injective?[nat, (X!1)])" countable_props
nil)
(bij_inv_is_bij formula-decl nil function_inverse nil)
(image const-decl "set[R]" function_image nil)
(fullset const-decl "set" sets 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(injective? const-decl "bool" functions nil)
(infinite_def formula-decl nil infinite_nat_def nil))
shostak))
(countably_infinite_strict_subset_exists 0
(countably_infinite_strict_subset_exists-1 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"
(lemma "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)
((countably_infinite_subset_exists formula-decl nil countable_props
nil)
(infinite_set type-eq-decl nil infinite_sets_def nil)
(is_finite const-decl "bool" finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans 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 countable_props nil)
(infinite_nonempty judgement-tcc nil infinite_sets_def nil)
(subset? const-decl "bool" sets nil)
(strict_subset? const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(remove const-decl "set" sets nil)
(countable_remove application-judgement "countable_set[T]"
countable_props nil)
(countably_infinite_remove application-judgement
"countably_infinite_set[T]" countable_props nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(is_countably_infinite const-decl "bool" countability nil)
(countably_infinite_set type-eq-decl nil countability nil))
shostak))
(countable_card 0
(countable_card-1 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"
(skosimp)
(("1"
(typepred "x1!1")
(("1"
(typepred "x2!1")
(("1"
(inst -4 "x1!1" "x2!1")
(("1"
(assert)
(("1"
(inst
-
"f!1(x1!1)"
"f!1(x2!1)")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand "image")
(("2"
(typepred "x1!1")
(("2" (inst + "x1!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "nonempty?(S!1)")
(("1"
(lemma "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"
(lemma
"bijective_inverse_exists[nat, (image(f!1, fullset[(S!1)]))]"
("f" "phi!1"))
(("1"
(expand "exists1")
(("1"
(flatten)
(("1"
(skolem - "psi!1")
(("1"
(hide -2)
(("1"
(lemma
"bij_inv_is_bij_alt[nat, (image(f!1, fullset[(S!1)]))]"
("f" "phi!1" "g" "psi!1"))
(("1"
(inst + "psi!1 o f!1")
(("1"
(hide-all-but (-1 -4 1))
(("1"
(expand "bijective?")
(("1"
(flatten)
(("1"
(split)
(("1"
(expand "o")
(("1"
(expand
"injective?")
(("1"
(skosimp)
(("1"
(inst
-4
"x1!1"
"x2!1")
(("1"
(assert)
(("1"
(inst
-
"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"
(skosimp)
(("2"
(inst
-2
"y!1")
(("2"
(skosimp)
(("2"
(typepred
"x!1")
(("2"
(inst
-
"x!1")
(("2"
(skosimp)
(("2"
(inst
+
"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"
(name "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"
(name
"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))
(("1"
(name
"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 FF(i))
(("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"
(inst + "FF")
(("1"
(split)
(("1"
(propax)
nil
nil)
("2"
(expand
"bijective?")
(("2"
(split)
(("1"
(expand
"injective?")
(("1"
(skolem
+
("i!1"
"j!1"))
(("1"
(flatten)
(("1"
(lemma
"trich_lt"
("x"
"i!1"
"y"
"j!1"))
(("1"
(split)
(("1"
(inst
-5
"i!1"
"j!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(propax)
nil
nil)
("3"
(inst
-5
"j!1"
"i!1")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"surjective?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 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"
(skosimp)
(("1"
(inst-cp
-2
"n!1")
(("1"
(inst
-
"0"
"FF(n!1)"
"n!1")
(("1"
(assert)
(("1"
(split -1)
(("1"
(propax)
nil
nil)
("2"
(hide-all-but
(1 3))
(("2"
(expand
"FF")
(("2"
(expand
"GG")
(("2"
(expand
"REMOVE_MIN")
(("2"
(expand
"iterate")
(("2"
(typepred
"n!1")
(("2"
(typepred
"min[nat](image[(S!1), nat](f!1, fullset[(S!1)]))")
(("2"
(inst
-
"n!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(expand
"<="
-2)
(("3"
(split)
(("1"
(inst
-3
"n!1"
"FF(n!1)")
(("1"
(assert)
nil
nil))
nil)
("2"
(replace
-1
*
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.47 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
