Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: real_finite_sequences.pvs Sprache: Lisp

Original von: PVS^©

(outer_measure_def
(outer_measure_TCC1 0
  (outer_measure_TCC1-1 nil 3396582266
   ("" (expand "zero_outer_measure")
    (("" (expand "outer_measure?")
      (("" (split)
        (("1" (expand "om_empty?") (("1" (propax) nil nil)) nil)
         ("2" (expand "om_increasing?")
          (("2" (skosimp)
            (("2" (expand "x_le") (("2" (assert) nil nil)) nil)) nil))
          nil)
         ("3" (expand "om_countably_subadditive?")
          (("3" (skosimp)
            (("3" (expand "o ")
              (("3" (expand "x_sum")
                (("3" (expand "x_le")
                  (("3" (rewrite "zero_series_conv")
                    (("3" (rewrite "zero_series_limit")
                      (("3" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((outer_measure? const-decl "bool" outer_measure_def nil)
    (om_countably_subadditive? const-decl "bool" outer_measure_def nil)
    (O const-decl "T3" function_props nil)
    (zero_series_limit formula-decl nil series "series/")
    (zero_series_conv formula-decl nil series "series/")
    (x_sum const-decl "extended_nnreal" extended_nnreal
     "extended_nnreal/")
    (om_increasing? const-decl "bool" outer_measure_def nil)
    (x_le const-decl "bool" extended_nnreal "extended_nnreal/")
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (om_empty? const-decl "bool" outer_measure_def nil)
    (zero_outer_measure const-decl "extended_nnreal" outer_measure_def
     nil))
   nil)))

¤ Dauer der Verarbeitung: 0.2 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.