| products/sources/formale Sprachen/PVS/ints/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: abstract_max.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(abstract_max
(prep0 0 (prep0-1 nil 3507028518 ("" (lemma "T_ne") (("" (expand "nonempty?") (("" (expand "empty?") (("" (skosimp*) (("" (expand "member") (("" (expand "is_one") (("" (inst -2 "f(t!1)") (("" (inst 1 "t!1") (("" (assert) nil)))))))))))))))) nil) ((nonempty? const-decl "bool" sets nil) (is_one const-decl "bool" abstract_max nil) (f formal-const-decl "[T -> upto[N]]" abstract_max nil) (T formal-type-decl nil abstract_max nil) (upto nonempty-type-eq-decl nil nat_types nil) (N formal-const-decl "nat" abstract_max 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) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (T_ne formula-decl nil abstract_max nil)) nil)) (max_f_TCC1 0 (max_f_TCC1-1 nil 3507028518 ("" (lemma "prep0") (("" (propax) nil)) nil) ((prep0 formula-decl nil abstract_max nil)) nil)) (prep1 0 (prep1-1 nil 3507028518 ("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (expand "max_f") (("" (typepred "max({n: upto[N] | is_one(n)})") (("1" (expand "is_one") (("1" (skosimp*) (("1" (inst -5 "S!1") (("1" (assert) nil))))))) ("2" (rewrite "prep0") nil)))))))))) nil) ((empty? const-decl "bool" sets nil) (max_f const-decl "upto[N]" abstract_max nil) (prep0 formula-decl nil abstract_max nil) (T formal-type-decl nil abstract_max nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans 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) (<= const-decl "bool" 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) (N formal-const-decl "nat" abstract_max nil) (upto nonempty-type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{a: upto[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}" max_upto nil) (is_one const-decl "bool" abstract_max nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil)) nil)) (max_TCC1 0 (max_TCC1-1 nil 3507028518 ("" (lemma "prep1") (("" (expand "nonempty?") (("" (expand "empty?") (("" (skosimp*) (("" (expand "member") (("" (inst?) (("" (expand "maximal?") (("" (flatten) (("" (assert) (("" (skosimp*) (("" (expand "max_f") (("" (replace -2) (("" (hide -2) (("" (typepred "max({n: upto[N] | is_one(n)})") (("1" (inst -3 "f(SS!1)") (("1" (assert) (("1" (expand "is_one") (("1" (inst?) (("1" (assert) nil))))))))) ("2" (lemma "prep0") (("2" (propax) nil)))))))))))))))))))))))))))))) nil) ((nonempty? const-decl "bool" sets nil) (T formal-type-decl nil abstract_max nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (maximal? const-decl "bool" abstract_max nil) (x!1 skolem-const-decl "T" abstract_max nil) (is_one const-decl "bool" abstract_max nil) (max const-decl "{a: upto[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}" max_upto nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (upto nonempty-type-eq-decl nil nat_types nil) (N formal-const-decl "nat" abstract_max 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) (<= const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (f formal-const-decl "[T -> upto[N]]" abstract_max nil) (prep0 formula-decl nil abstract_max nil) (max_f const-decl "upto[N]" abstract_max nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (prep1 formula-decl nil abstract_max nil)) nil)) (max_def 0 (max_def-1 nil 3507028518 ("" (typepred "max") (("" (propax) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil abstract_max nil) (maximal? const-decl "bool" abstract_max nil) (max const-decl "{S: T | maximal?(S)}" abstract_max nil)) nil)) (max_in 0 (max_in-1 nil 3507028518 ("" (typepred "max") (("" (expand "maximal?") (("" (flatten) (("" (propax) nil)))))) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil abstract_max nil) (maximal? const-decl "bool" abstract_max nil) (max const-decl "{S: T | maximal?(S)}" abstract_max nil)) nil)) (max_is_max 0 (max_is_max-1 nil 3507028518 ("" (skosimp*) (("" (typepred "max") (("" (expand "maximal?") (("" (flatten) (("" (inst?) (("" (assert) nil)))))))))) nil) ((max const-decl "{S: T | maximal?(S)}" abstract_max nil) (maximal? const-decl "bool" abstract_max nil) (T formal-type-decl nil abstract_max nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil))) ¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
