products/sources/formale Sprachen/PVS/ints image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: abstract_max.prf   Sprache: Lisp

Original 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") (("" (assertnil))))))))))))))))
    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" (assertnil)))))))
             ("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" (assertnil)))))))))
                               ("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?) (("" (assertnil))))))))))
    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)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff