| products/Sources/formale Sprachen/PVS/while/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: max_below.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(max_below
(max_TCC1 0 (max_TCC1-1 nil 3276608569 ("" (inst 1 "(LAMBDA S: N-1 - min({y: below[N] | S(N-1-y)}))") (("1" (skosimp*) (("1" (typepred "min[below[N]]({y: below[N] | S!1(N - 1 - y)})") (("1" (ground) (("1" (skosimp*) (("1" (inst - "N-1-x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (typepred "S!1") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand "member") (("2" (inst -2 "N-1-x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "S!1") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand "member") (("2" (inst - "N-1-x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (below type-eq-decl nil nat_types nil) (N formal-const-decl "nat" max_below nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (max_def 0 (max_def-1 nil 3276608569 ("" (skolem-typepred) (("" (typepred "max(S!1)") (("" (prop) (("1" (expand "maximum?") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "maximum?") (("2" (flatten) (("2" (inst -5 "a!1") (("2" (assert) (("2" (inst -2 "max(S!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((max const-decl "{a: below[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}" max_below nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (maximum? const-decl "bool" max_below nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_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) (below type-eq-decl nil nat_types nil) (N formal-const-decl "nat" max_below nil) (< const-decl "bool" reals 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (max_lem 0 (max_lem-1 nil 3276608569 ("" (skosimp*) (("" (expand "maximum?") (("" (assert) (("" (lemma "max_def") (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((maximum? const-decl "bool" max_below nil) (max_def formula-decl nil max_below nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{a: below[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}" max_below nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "nat" max_below nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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.4 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.Bot Zugriff |
