Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: compatibility.pvs Sprache: Lisp

Original von: PVS^©

(rewrite_rules
(IMP_substitution_TCC1 0
  (IMP_substitution_TCC1-1 nil 3416209767
   ("" (lemma "var_countable") (("" (propax) nil nil)) nil)
   ((var_countable formula-decl nil rewrite_rules nil)) nil))
(ren_rewrite 0
  (ren_rewrite-1 nil 3402089498
   ("" (skeep)
    (("" (expand "rewrite_rule?")
      (("" (prop)
        (("1" (expand "ext")
          (("1" (lift-if) (("1" (prop) (("1" (assert) nil nil)) nil))
            nil))
          nil)
         ("2" (rewrite "rename_preserv_inclusion") nil nil))
        nil))
      nil))
    nil)
   ((rewrite_rule? const-decl "bool" rewrite_rules nil)
    (rename_preserv_inclusion formula-decl nil substitution nil)
    (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
    (V const-decl "set[term]" variables_term nil)
    (Sub? const-decl "bool" substitution nil)
    (Sub type-eq-decl nil substitution nil)
    (Ren? const-decl "bool" substitution nil)
    (Ren type-eq-decl nil substitution nil)
    (variable formal-nonempty-type-decl nil rewrite_rules nil)
    (symbol formal-nonempty-type-decl nil rewrite_rules 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)
    (arity formal-const-decl "[symbol -> nat]" rewrite_rules nil)
    (ext def-decl "term" substitution nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.