Quelle  outer_measure.prf

(outer_measure
 (IMP_ast_def_TCC1 0
  (IMP_ast_def_TCC1-1 nil 3458456184
   ("" (typepred "A")
    (("" (expand "subset_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?")
          (("" (expand "nonempty?")
            (("" (expand "member")
              (("" (expand "empty?")
                (("" (inst - "emptyset[T]")
                  (("" (expand "member") (("" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (subset_algebra_emptyset name-judgement "(S)" outer_measure nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil outer_measure nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (A formal-const-decl "subset_algebra" outer_measure nil))
   nil))
 (IMP_ast_def_TCC2 0
  (IMP_ast_def_TCC2-1 nil 3458456184
   ("" (typepred "A")
    (("" (expand "subset_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?")
          (("" (assert)
            (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (subset_algebra_emptyset name-judgement "(S)" outer_measure nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil outer_measure nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (A formal-const-decl "subset_algebra" outer_measure nil))
   nil))
 (IMP_ast_def_TCC3 0
  (IMP_ast_def_TCC3-1 nil 3458456184
   ("" (lemma "subset_algebra_fullset") (("" (propax) nil nil)) nil)
   ((subset_algebra_fullset judgement-tcc nil subset_algebra nil)
    (T formal-type-decl nil outer_measure nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (A formal-const-decl "subset_algebra" outer_measure nil))
   nil))
 (IMP_ast_def_TCC4 0
  (IMP_ast_def_TCC4-1 nil 3458456184
   ("" (skosimp)
    (("" (lemma "subset_algebra_intersection")
      (("" (inst - "a!1" "b!1") nil nil)) nil))
    nil)
   ((A formal-const-decl "subset_algebra" outer_measure nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil outer_measure nil)
    (subset_algebra_intersection judgement-tcc nil subset_algebra nil)
    (set type-eq-decl nil sets nil))
   nil))
 (IMP_ast_def_TCC5 0
  (IMP_ast_def_TCC5-1 nil 3458456184
   ("" (skosimp)
    (("" (lemma "subset_algebra_difference" ("x" "a!1" "y" "b!1"))
      (("" (expand "finite_disjoint_union?")
        ((""
          (inst +
           "lambda (i:nat): if i=0 then difference[T](a!1, b!1) else emptyset endif"
           "1")
          (("" (split)
            (("1" (grind) nil nil)
             ("2" (apply-extensionality :hide? t)
              (("2" (expand "IUnion")
                (("2" (expand "emptyset")
                  (("2" (case-replace "difference[T](a!1, b!1)(x!1)")
                    (("1" (inst + "0") nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("3" (skosimp)
              (("3" (case-replace "i!1=0")
                (("1" (expand "member") (("1" (propax) nil nil)) nil)
                 ("2" (assert) (("2" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((A formal-const-decl "subset_algebra" outer_measure nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil outer_measure nil)
    (set type-eq-decl nil sets nil)
    (subset_algebra_difference judgement-tcc nil subset_algebra nil)
    (subset_algebra_difference application-judgement "(A)"
     outer_measure nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (difference const-decl "set" sets nil)
    (emptyset const-decl "set" sets nil)
    (subset_algebra_emptyset name-judgement "(S)" outer_measure nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (subset_algebra_intersection application-judgement "(S)"
     outer_measure nil)
    (/= const-decl "boolean" notequal nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_disjoint_union? const-decl "bool" subset_algebra_def nil))
   nil)))