Quelle  outer_measure_def.prf   Sprache: unbekannt

(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)))

quality84%

[ zur Elbe Produktseite wechseln0.19Quellennavigators  Analyse erneut starten  ]