| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 20 kB |
|
Quelle pigeonhole.prf Sprache: Lisp |
|||||||||
|
(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))) ¤ 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.22Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28