|
(pigeonhole
(pigeonhole_principle_nat 0
(pigeonhole_principle_nat-1 nil 3540897992
(""
(case "FORALL (n: nat, f: [below(n+1) -> below(n+1)]):
bijective?(f) IFF (injective?(f) OR surjective?(f))")
(("1" (skeep)
(("1" (case "n = 0")
(("1" (hide -2)
(("1" (expand "bijective?")
(("1" (expand "injective?")
(("1" (expand "surjective?")
(("1" (assert)
(("1" (ground)
(("1" (skosimp*) nil nil) ("2" (skosimp*) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) (("2" (inst - "n-1" "f") nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2"
(case "NOT FORALL (n: nat, f: [below(n + 1) -> below(n + 1)]):
bijective?(f) IFF (injective?(f))")
(("1" (hide 2)
(("1" (induct "n")
(("1" (grind) nil nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (split)
(("1" (flatten)
(("1" (expand "bijective?")
(("1" (ground) nil nil)) nil))
nil)
("2" (flatten)
(("2" (case "f(1+n) = 1+n")
(("1" (inst - "LAMBDA (i:below(1+n)): f(i)")
(("1" (ground)
(("1" (expand "bijective?")
(("1"
(expand "surjective?")
(("1"
(skosimp*)
(("1"
(typepred "y!1")
(("1"
(case "y!1 = 1+n")
(("1"
(inst + "1+n")
(("1" (assert) nil nil))
nil)
("2"
(inst - "y!1")
(("1"
(skosimp*)
(("1"
(inst + "x!1")
nil
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "injective?")
(("2"
(skosimp*)
(("2"
(inst - "x1!1" "x2!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "injective?")
(("2"
(inst - "i!1" "1+n")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(inst -
"LAMBDA (i:below(1+n)): IF f(i) < f(1+n) THEN f(i) ELSE f(i)-1 ENDIF")
(("1" (ground)
(("1" (expand "bijective?")
(("1"
(expand "surjective?")
(("1"
(skosimp*)
(("1"
(case "y!1 = 1+n")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(inst - "n")
(("1"
(skosimp*)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(replace
-1
3
:dir
rl)
(("1"
(inst + "x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "y!1 < f(1+n)")
(("1"
(inst - "y!1")
(("1"
(skosimp*)
(("1"
(inst + "x!1")
(("1"
(ground)
(("1"
(lift-if)
(("1"
(assert)
(("1"
(ground)
(("1"
(case
"NOT f(x!1) = f(1+n)")
(("1"
(assert)
nil
nil)
("2"
(expand
"injective?"
-5)
(("2"
(inst
-
"x!1"
"1+n")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2"
(case "y!1 = f(1+n)")
(("1"
(inst + "1+n")
(("1" (assert) nil nil))
nil)
("2"
(inst - "y!1-1")
(("1"
(skosimp*)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(inst + "x!1")
nil
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "injective?")
(("2"
(skosimp*)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(assert)
(("2"
(ground)
(("1"
(inst - "x1!1" "x2!1")
(("1" (assert) nil nil))
nil)
("2"
(inst - "1+n" "x2!1")
(("2" (assert) nil nil))
nil)
("3"
(inst - "1+n" "x1!1")
(("3" (assert) nil nil))
nil)
("4"
(inst - "x1!1" "x2!1")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2"
(case "i!1 = 1+n")
(("1" (assert) nil nil)
("2"
(expand "injective?")
(("2"
(inst - "i!1" "1+n")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*) (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "NOT FORALL (n: nat, f: [below(n + 1) -> below(n + 1)]):
bijective?(f) IFF surjective?(f)")
(("1" (hide 2)
(("1" (induct "n")
(("1" (hide -) (("1" (grind) nil nil)) nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (expand "bijective?" +)
(("2" (ground)
(("2"
(case "EXISTS (g:[below(2+n)->below(2+n)]): FORALL (i:below(2+n)): f(g(i)) = i")
(("1" (skeep -1)
(("1" (case "injective?(g)")
(("1"
(inst -5 "n+1" "g")
(("1"
(assert)
(("1"
(expand "injective?" +)
(("1"
(skeep)
(("1"
(copy -6)
(("1"
(expand "bijective?" -1)
(("1"
(expand "surjective?" -1)
(("1"
(inst-cp - "x1")
(("1"
(inst - "x2")
(("1"
(skolem -1 "y2")
(("1"
(skolem -2 "y1")
(("1"
(inst-cp - "y2")
(("1"
(inst - "y1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "injective?" +)
(("2"
(skosimp*)
(("2"
(inst-cp - "x1!1")
(("2"
(inst - "x2!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst +
"LAMBDA (ii:below(2+n)): choose({jj:below(2+n)|f(jj) = ii})")
(("1" (skeep) (("1" (assert) nil nil)) nil)
("2" (skeep)
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "surjective?" -2)
(("2"
(inst -2 "ii")
(("2"
(skosimp*)
(("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))
nil))
nil))
nil)
("2" (skeep)
(("2" (inst - "n" "f")
(("2" (inst - "n" "f") (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(f skolem-const-decl "[below(2 + n) -> below(2 + n)]" pigeonhole
nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(n skolem-const-decl "nat" pigeonhole nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(y!1 skolem-const-decl "below(2 + n)" pigeonhole nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(n skolem-const-decl "nat" pigeonhole nil)
(f skolem-const-decl "[below(2 + n) -> below(2 + n)]" pigeonhole
nil)
(y!1 skolem-const-decl "below(2 + n)" pigeonhole nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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 "[T, T -> boolean]" equalities nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(bijective? const-decl "bool" functions nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(injective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil))
shostak)))
¤ Dauer der Verarbeitung: 0.12 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.
|
