Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: direct.prf Sprache: Lisp

Original von: PVS^©

(direct
(SS_TCC1 0
  (SS_TCC1-1 nil 3353075465 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil direct nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(SS_TCC2 0
  (SS_TCC2-1 nil 3353075465 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil direct nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(SS_TCC3 0
  (SS_TCC3-1 nil 3353075465 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil direct nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(SS_TCC4 0
  (SS_TCC4-1 nil 3353075465 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil direct nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(SS_TCC5 0
  (SS_TCC5-1 nil 3353075465 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil direct nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(SS_TCC6 0
  (SS_TCC6-1 nil 3353077513
   ("" (skosimp)
    (("" (expand "increasing?")
      (("" (skosimp)
        (("" (expand "sq_le")
          (("" (expand "conditional")
            (("" (skosimp*)
              (("" (case-replace "B(b!1)(s1!1)")
                (("1" (expand "o")
                  (("1" (case-replace "v!1(S1!1)(s1!1) = bottom")
                    (("1" (assert) nil nil)
                     ("2" (assert)
                      (("2" (inst - "down(v!1(S1!1)(s1!1))" "s2!1")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((increasing? const-decl "bool" fun_preds_partial "scott/")
    (sq_le const-decl "bool" Cont nil)
    (O const-decl "LiftPartialFunction[X, Z]"
     PartialFunctionComposition nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil)
    (strict_well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (Stm type-decl nil Stm nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (lift type-decl nil lift_adt nil)
    (B def-decl "[State -> bool]" BExp nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (State nonempty-type-eq-decl nil State 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)
    (BExp type-decl nil BExp nil)
    (V formal-nonempty-type-decl nil direct nil)
    (conditional const-decl "Cont" Cont nil))
   nil)))

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.