|
(infinite_nat_def
(infinite_def 0
(infinite_def-1 nil 3313932679
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (name "HH" "lambda (Y:infinite_set[T]): rest[T](Y)")
(("1" (name "GG" "lambda (n:nat): iterate(HH,n)(X!1)")
(("1" (name "FF" "lambda (n:nat): choose(GG(n))")
(("1" (case "forall (n:nat): GG(n+1)=rest(GG(n))")
(("1" (case "GG(0)=X!1")
(("1"
(case "forall (n:nat): add(FF(n),GG(n+1)) = GG(n) & not member(FF(n),GG(n+1))")
(("1"
(case "forall (n:nat): strict_subset?(GG(n+1),GG(n))")
(("1" (case "forall (n:nat): subset?(GG(n),X!1)")
(("1" (case "injective?[nat, (X!1)](FF)")
(("1" (inst + "FF") nil nil)
("2" (hide 3)
(("2" (expand "injective?")
(("2"
(case
"forall (i,j:nat): i < j => FF(i) /= FF(j)")
(("1"
(skosimp)
(("1"
(lemma
"trich_lt"
("x" "x1!1" "y" "x2!1"))
(("1"
(split)
(("1"
(inst - "x1!1" "x2!1")
(("1"
(assert)
(("1"
(expand "FF")
(("1"
(expand "/=" -2)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3"
(inst - "x2!1" "x1!1")
(("3"
(expand "/=")
(("3"
(replace -3)
(("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(inst-cp -5 "i!1")
(("2"
(inst -5 "j!1")
(("2"
(flatten)
(("2"
(hide -6 1)
(("2"
(case
"member(FF(j!1), GG(i!1 + 1))")
(("1"
(expand "member")
(("1"
(assert)
nil
nil))
nil)
("2"
(case
"forall (n:nat): subset?(GG(i!1 + 1+n),GG(i!1+1))")
(("1"
(inst
-
"j!1-(i!1+1)")
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1"
(inst
-
"FF(j!1)")
(("1"
(split -1)
(("1"
(propax)
nil
nil)
("2"
(expand
"FF")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(hide-all-but (1 -4))
(("2"
(induct "n")
(("1"
(expand
"subset?")
(("1"
(expand
"member")
(("1"
(skosimp)
nil
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand
"strict_subset?")
(("2"
(expand
"subset?")
(("2"
(expand
"member")
(("2"
(skosimp)
(("2"
(inst
-
"x!1")
(("2"
(inst
-3
"1+i!1+j!2")
(("2"
(flatten)
(("2"
(inst
-
"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))
nil))
nil))
nil)
("3" (skolem + "n!1")
(("3" (expand "FF")
(("3"
(inst - "n!1")
(("3"
(lemma
"choose_member[T]"
("a" "GG(n!1)"))
(("3"
(split -1)
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1"
(inst - "choose(GG(n!1))")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma
"infinite_nonempty[T]"
("x" "GG(n!1)"))
(("2"
(expand "nonempty?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (induct "n")
(("1" (expand "subset?")
(("1"
(expand "GG")
(("1"
(expand "iterate")
(("1" (skosimp) nil nil))
nil))
nil))
nil)
("2" (skosimp)
(("2"
(inst - "j!1")
(("2"
(hide-all-but (-1 -2 1))
(("2"
(expand "strict_subset?")
(("2"
(expand "subset?")
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2"
(inst - "x!1")
(("2"
(expand "member")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (skosimp)
(("2" (inst -3 "n!1")
(("2" (replace -3)
(("2"
(expand "strict_subset?")
(("2"
(rewrite "rest_subset")
(("2"
(assert)
(("2"
(inst - "n!1")
(("2"
(flatten -1)
(("2"
(lemma
"rest_not_equal"
("a" "GG(n!1)"))
(("2"
(split -1)
(("1" (propax) nil nil)
("2"
(typepred "GG(n!1)")
(("2"
(lemma
"infinite_nonempty[T]")
(("2"
(inst - "GG(n!1)")
(("2"
(expand
"nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 3)
(("2" (skosimp)
(("2" (expand "FF")
(("2" (inst -2 "n!1")
(("2" (replace -2)
(("2"
(lemma
"choose_rest[T]"
("a" "GG(n!1)"))
(("2"
(lemma
"choose_not_member[T]"
("a" "GG(n!1)"))
(("2"
(case-replace "empty?[T](GG(n!1))")
(("1"
(typepred "GG(n!1)")
(("1"
(lemma "infinite_nonempty[T]")
(("1"
(inst - "GG(n!1)")
(("1"
(expand "nonempty?")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "GG")
(("2" (expand "iterate") (("2" (propax) nil nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (expand "GG" 1)
(("2" (expand "iterate" 1 1)
(("2" (expand "HH" 1 1) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "is_finite")
(("2" (skolem - "f!2")
(("2" (typepred "f!2")
(("2" (skosimp)
(("2"
(lemma
"composition_injective[below[N!1 + 1], (X!1), below[N!1]]")
(("2" (inst - "lambda (n:below[N!1+1]): f!2(n)" "_")
(("1" (inst - "f!1")
(("1"
(lemma "injection_n_to_m"
("n" "N!1+1" "m" "N!1"))
(("1" (assert)
(("1" (expand "o ") (("1" (inst?) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "injective?")
(("2" (skosimp)
(("2" (inst -2 "x1!1" "x2!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rest const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities 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 infinite_nat_def nil)
(infinite_rest application-judgement "infinite_set"
infinite_sets_def nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(HH skolem-const-decl "[infinite_set[T] -> infinite_set[T]]"
infinite_nat_def nil)
(choose_not_member formula-decl nil sets_lemmas nil)
(empty? const-decl "bool" sets nil)
(choose_rest formula-decl nil sets_lemmas nil)
(strict_subset? const-decl "bool" sets nil)
(injective? const-decl "bool" functions nil)
(FF skolem-const-decl "[n: nat -> (GG(n))]" infinite_nat_def nil)
(GG skolem-const-decl "[nat -> infinite_set[T]]" infinite_nat_def
nil)
(X!1 skolem-const-decl "set[T]" infinite_nat_def nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(i!1 skolem-const-decl "nat" infinite_nat_def nil)
(j!1 skolem-const-decl "nat" infinite_nat_def nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(trich_lt formula-decl nil real_props nil)
(/= const-decl "boolean" notequal nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(choose_member formula-decl nil sets_lemmas nil)
(infinite_nonempty judgement-tcc nil infinite_sets_def nil)
(subset? const-decl "bool" sets nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(rest_subset formula-decl nil sets_lemmas nil)
(rest_not_equal formula-decl nil sets_lemmas nil)
(member const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(infinite_add application-judgement "infinite_set"
infinite_sets_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(iterate def-decl "T" function_iterate nil)
(below type-eq-decl nil nat_types nil)
(composition_injective judgement-tcc nil function_props nil)
(f!1 skolem-const-decl "[(X!1) -> below[N!1]]" infinite_nat_def
nil)
(below type-eq-decl nil naturalnumbers nil)
(O const-decl "T3" function_props nil)
(injection_n_to_m formula-decl nil nat_fun_props nil)
(f!2 skolem-const-decl "(injective?[nat, (X!1)])" infinite_nat_def
nil)
(N!1 skolem-const-decl "nat" infinite_nat_def nil))
shostak))
(infinite_def2 0
(infinite_def2-1 nil 3454896480
("" (skosimp)
(("" (rewrite "infinite_def" 1)
(("" (split)
(("1" (skosimp*)
(("1" (typepred "f!1")
(("1" (lemma "surj_inv[nat, (S!1)]" ("f" "f!1"))
(("1" (split)
(("1" (inst + "inverse[nat, (S!1)](f!1)") nil nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (typepred "f!1")
(("2" (case "nonempty?(S!1)")
(("1" (lemma "inj_inv[(S!1), nat]" ("f" "f!1"))
(("1" (split)
(("1" (inst + "inverse[(S!1), nat](f!1)")
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (skosimp)
(("1" (expand "member")
(("1" (inst + "x!1") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (hide 2 -2)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (skosimp)
(("2" (inst + "x!1")
(("2" (assert)
(("2" (expand "member")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (hide 1)
(("2" (expand "surjective?")
(("2" (inst - "0")
(("2" (skosimp)
(("2" (expand "empty?")
(("2" (inst - "x!1")
(("2" (expand "member")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((infinite_def formula-decl nil infinite_nat_def nil)
(T formal-type-decl nil infinite_nat_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(x!1 skolem-const-decl "T" infinite_nat_def nil)
(x!1 skolem-const-decl "T" infinite_nat_def nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(S!1 skolem-const-decl "set[T]" infinite_nat_def nil)
(inv_surj_is_inj application-judgement "(injective?[R, D])"
function_inverse nil)
(TRUE const-decl "bool" booleans nil)
(inj_inv formula-decl nil function_inverse nil)
(surj_inv formula-decl nil function_inverse nil)
(inv_inj_is_surj application-judgement "(surjective?[R, D])"
function_inverse nil)
(inverse const-decl "D" function_inverse nil)
(surjective? const-decl "bool" functions 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(injective? const-decl "bool" functions nil))
shostak)))
¤ Dauer der Verarbeitung: 0.21 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.
|
