Quelle scott_composition_continuity.prf Sprache: Lisp

(scott_composition_continuity
(IMP_composition_continuity_TCC1 0
  (IMP_composition_continuity_TCC1-1 nil 3353641502 3353641645
   ("" (assert) nil nil) proved nil 4548 280 t nil))
(IMP_composition_continuity_TCC2 0
  (IMP_composition_continuity_TCC2-1 nil 3353641502 3353641655
   ("" (assert) nil nil) proved nil 3733 290 t nil))
(IMP_composition_continuity_TCC3 0
  (IMP_composition_continuity_TCC3-1 nil 3353641502 3353641664
   ("" (assert) nil nil) proved nil 4352 280 t nil))
(composition_scott_continuous 0
  (composition_scott_continuous-1 nil 3353641502 3353641627
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (typepred "g!1")
        (("" (rewrite "scott_continuous_def" -1 :dir rl)
          (("" (rewrite "scott_continuous_def" -2 :dir rl)
            (("" (rewrite "scott_continuous_def" 1 :dir rl)
              ((""
                (lemma "composition_continuous" ("f" "f!1" "g" "g!1"))
                (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((scott_continuous? const-decl "bool" scott_continuity nil)
    (le3 formal-const-decl "(directed_complete_partial_order?[T3])"
     scott_composition_continuity nil)
    (le2 formal-const-decl "(directed_complete_partial_order?[T2])"
     scott_composition_continuity nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     nil)
    (pred type-eq-decl nil defined_types nil)
    (T3 formal-type-decl nil scott_composition_continuity nil)
    (T2 formal-type-decl nil scott_composition_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (scott_continuous_def formula-decl nil scott_continuity nil)
    (O const-decl "T3" function_props nil)
    (composition_continuous formula-decl nil composition_continuity
     "topology/")
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (scott_open_sets const-decl "setofsets[T]" scott nil)
    (T1 formal-type-decl nil scott_composition_continuity nil)
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_composition_continuity nil))
   120165 2310 t nil)))

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.