| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 6 kB |
|
Quelle min_posnat.prf Sprache: Lisp |
|||||||||
|
(min_posnat
(min_TCC1 0 (min_TCC1-1 nil 3507028515 ("" (inst + "lambda S : choose({a : posnat | S(a) AND (FORALL (x : posnat) : S(x) IMPLIES a <= x)})" (("" (skosimp*) (("" (typepred "S!1") (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (skosimp*) (("" (lemma "wf_nat") (("" (expand "well_founded?") (("" (inst - "S!1") (("" (split -1) (("1" (assert) (("1" (skosimp*) (("1" (typepred "y!1") (("1" (expand "extend") (("1" (inst -4 "y!1") (("1" (ground) (("1" (skosimp*) (("1" (inst - "x!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (propax) nil))))))))) ("2" (ground) nil))))))))))) ("2" (inst?) (("2" (assert) (("2" (grind) nil)))))))))))))))))))))))))) nil) ((member const-decl "bool" sets nil) (wf_nat formula-decl nil naturalnumbers nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (S!1 skolem-const-decl "(nonempty?[posnat])" min_posnat nil) (y!1 skolem-const-decl "(extend[nat, posnat, bool, FALSE](S!1))" min_posnat nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!2 skolem-const-decl "posnat" min_posnat nil) (nonempty_extend application-judgement "(nonempty?[T])" extend_set_props nil) (well_founded? const-decl "bool" orders nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (choose const-decl "(p)" sets nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (min_def 0 (min_def-1 nil 3507028515 ("" (skolem-typepred) (("" (typepred "min(S!1)") (("" (prop) (("1" (expand "minimum?") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil))))))))) ("2" (expand "minimum?") (("2" (flatten) (("2" (inst -5 "a!1") (("2" (assert) (("2" (inst -2 "min(S!1)") (("2" (assert) nil)))))))))))))))) nil) ((min const-decl "{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_posnat nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (minimum? const-decl "bool" min_posnat nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (min_lem 0 (min_lem-1 nil 3507028515 ("" (skosimp*) (("" (lemma "min_def") (("" (inst?) (("" (assert) nil)))))) nil) ((min_def formula-decl nil min_posnat nil) (min const-decl "{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_posnat nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil))) ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28