Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: isf.pvs Sprache: Unknown

Original von: PVS^©

(isf
(nonzero_measurable 0
  (nonzero_measurable-1 nil 3390787726
   ("" (skosimp)
    (("" (typepred "g!1")
      (("" (expand "measurable_function?")
        (("" (lemma "singleton_is_borel" ("x" "0"))
          (("" (lemma "fullset_is_borel[real,metric_induced_topology]")
            ((""
              (lemma
               "difference_is_borel[real,metric_induced_topology]"
               ("a" "fullset[real]" "b" "singleton[real](0)"))
              (("1"
                (inst -
                 "difference[real](fullset[real], singleton[real](0))")
                (("1" (expand "measurable_set?")
                  (("1"
                    (case-replace "inverse_image(g!1,
                      difference[real](fullset[real], singleton[real](0))) = nonzero_set?(g!1)")
                    (("1" (hide-all-but 1)
                      (("1" (apply-extensionality :hide? t)
                        (("1" (expand "nonzero_set?")
                          (("1" (expand "singleton")
                            (("1" (expand "fullset")
                              (("1"
                                (expand "difference")
                                (("1"
                                  (expand "member")
                                  (("1"
                                    (expand "inverse_image")
                                    (("1"
                                      (expand "member")
                                      (("1"
                                        (expand "/=")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (S formal-const-decl "sigma_algebra" isf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types 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)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     "metric_space/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (singleton_is_borel formula-decl nil hausdorff_borel nil)
    (real_is_complete name-judgement "metric_complete" real_topology
     "metric_space/")
    (fullset_is_clopen name-judgement
     "clopen[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[real]" measure_space nil)
    (singleton_is_compact application-judgement
     "compact[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (singleton_is_closed application-judgement
     "closed[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[nat]" countability "sets_aux/")
    (difference_is_borel formula-decl nil borel nil)
    (borel? const-decl "sigma_algebra" borel nil)
    (borel nonempty-type-eq-decl nil borel nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (member const-decl "bool" sets nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (nonzero_set? const-decl "set[T]" isf nil)
    (difference const-decl "set" sets nil)
    (open_diff_closed_is_open application-judgement
     "open[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (fullset_is_borel formula-decl nil borel nil))
   shostak))
(nonzero_set_phi 0
  (nonzero_set_phi-1 nil 3390785835
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (apply-extensionality 1 :hide? t)
        (("" (expand "nonzero_set?")
          (("" (expand "phi")
            (("" (expand "member")
              (("" (case-replace "X!1(x!1)")
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "sigma_algebra" isf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (phi_is_simple application-judgement "simple" isf 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)
    (set type-eq-decl nil sets nil)
    (nonzero_set? const-decl "set[T]" isf 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)
    (phi const-decl "nat" measure_space nil))
   shostak))
(isf?_TCC1 0
  (isf?_TCC1-1 nil 3390785367
   ("" (skosimp*)
    (("" (expand "simple?")
      (("" (flatten)
        (("" (lemma "nonzero_measurable" ("g" "f!1"))
          (("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((simple? const-decl "bool" measure_space nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (S formal-const-decl "sigma_algebra" isf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_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)
    (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)
    (T formal-type-decl nil isf nil)
    (nonzero_measurable formula-decl nil isf nil))
   nil))
(isf_zero 0
  (isf_zero-1 nil 3395229959
   ("" (expand "isf?")
    (("" (lemma "simple_const" ("c" "0"))
      (("" (replace -1)
        (("" (hide -1)
          (("" (expand "nonzero_set?")
            (("" (expand "mu_fin?")
              (("" (lemma "m_emptyset")
                (("" (expand "emptyset")
                  (("" (replace -1) (("" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "sigma_algebra" isf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_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 isf 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)
    (number nonempty-type-decl nil numbers nil)
    (simple_const formula-decl nil measure_space nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (emptyset const-decl "set" sets nil)
    (m_emptyset formula-decl nil measure_props nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (m formal-const-decl "measure_type" isf nil)
    (nonzero_set? const-decl "set[T]" isf nil)
    (isf? const-decl "bool" isf nil))
   shostak))
(isf_TCC1 0
  (isf_TCC1-1 nil 3390785367
   ("" (expand "isf?")
    (("" (split)
      (("1" (expand "simple?")
        (("1" (split)
          (("1" (expand "measurable_function?")
            (("1" (skosimp)
              (("1" (case "B!1(0)")
                (("1"
                  (case-replace
                   "inverse_image(LAMBDA (x: T): 0, B!1)=fullset[T]")
                  (("1" (expand "measurable_set?")
                    (("1" (propax) nil nil)) nil)
                   ("2" (hide 2)
                    (("2" (apply-extensionality 1 :hide? t)
                      (("2" (expand "fullset")
                        (("2" (expand "inverse_image")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2"
                  (case-replace
                   "inverse_image(LAMBDA (x: T): 0, B!1)=emptyset[T]")
                  (("1" (expand "measurable_set?")
                    (("1" (propax) nil nil)) nil)
                   ("2" (hide 3)
                    (("2" (apply-extensionality :hide? t)
                      (("2" (expand "emptyset")
                        (("2" (expand "inverse_image")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (case "empty?(fullset[T])")
            (("1"
              (case-replace
               "image(LAMBDA (x: T): 0, fullset[T]) = emptyset[real]")
              (("1" (assert) nil nil)
               ("2" (apply-extensionality :hide? t)
                (("2" (expand "emptyset")
                  (("2" (expand "fullset")
                    (("2" (hide 1)
                      (("2" (expand "image")
                        (("2" (skolem - ("TT"))
                          (("2" (expand "empty?")
                            (("2" (inst - "TT")
                              (("2"
                                (expand "member")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2"
              (case-replace
               "image[T,real](LAMBDA (x: T): 0, fullset[T]) = singleton[real](0)")
              (("1" (assert) nil nil)
               ("2" (hide 3)
                (("2" (expand "singleton")
                  (("2" (apply-extensionality :hide? t)
                    (("2" (case-replace "x!1=0")
                      (("1" (expand "fullset")
                        (("1" (expand "image")
                          (("1" (expand "empty?")
                            (("1" (skosimp)
                              (("1" (inst + "x!2") nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert)
                        (("2" (expand "fullset")
                          (("2" (expand "image")
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "nonzero_set?")
        (("2" (typepred "m")
          (("2" (expand "measure?")
            (("2" (flatten)
              (("2" (expand "mu_fin?")
                (("2" (assert)
                  (("2" (expand "measure_empty?")
                    (("2" (expand "emptyset")
                      (("2" (replace -1) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((emptyset const-decl "set" sets nil)
    (subset_algebra_emptyset name-judgement "(S)" isf nil)
    (null_emptyset name-judgement "null_set" isf nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (measurable_fullset name-judgement "measurable_set[T, S]" isf nil)
    (subset_algebra_fullset name-judgement "(S)" isf nil)
    (T formal-type-decl nil isf nil) (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (fullset const-decl "set" sets nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (member const-decl "bool" sets nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     "metric_space/")
    (borel? const-decl "sigma_algebra" borel nil)
    (borel nonempty-type-eq-decl nil borel nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[real]" measure_space nil)
    (singleton_is_compact application-judgement
     "compact[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (singleton_is_closed application-judgement
     "closed[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[nat]" countability "sets_aux/")
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (image const-decl "set[R]" function_image nil)
    (emptyset_is_compact name-judgement
     "compact[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (emptyset_is_clopen name-judgement
     "clopen[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (finite_emptyset name-judgement "finite_set[real]" measure_space
     nil)
    (TRUE const-decl "bool" booleans nil)
    (empty? const-decl "bool" sets nil)
    (simple? const-decl "bool" measure_space nil)
    (m formal-const-decl "measure_type" isf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (S formal-const-decl "sigma_algebra" isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (measure_empty? const-decl "bool" generalized_measure_def nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (nonzero_set? const-decl "set[T]" isf nil)
    (isf? const-decl "bool" isf nil))
   nil))
(isf_is_simple 0
  (isf_is_simple-1 nil 3390790021
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "isf?") (("" (flatten) nil nil)) nil)) nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf 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)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(isf_add 0
  (isf_add-1 nil 3390785367
   ("" (skosimp)
    (("" (typepred "i1!1")
      (("" (typepred "i2!1")
        (("" (expand "isf?")
          (("" (flatten)
            (("" (lemma "simple_add" ("h1" "i1!1" "h2" "i2!1"))
              (("" (assert)
                (("" (expand "+")
                  (("" (expand "simple?")
                    (("" (flatten)
                      (("" (hide-all-but (-5 -8 1))
                        ((""
                          (lemma "union_difference"
                           ("a" "nonzero_set?(i1!1)" "b"
                            "nonzero_set?(i2!1)"))
                          ((""
                            (lemma "difference_disjoint"
                             ("a" "nonzero_set?(i1!1)" "b"
                              "nonzero_set?(i2!1)"))
                            ((""
                              (lemma "m_disjoint_union"
                               ("a"
                                "nonzero_set?(i1!1)"
                                "b"
                                "difference(nonzero_set?(i2!1), nonzero_set?(i1!1))"))
                              (("1"
                                (replace -2 -1)
                                (("1"
                                  (replace -3 -1 rl)
                                  (("1"
                                    (expand "mu_fin?")
                                    (("1"
                                      (expand "x_eq")
                                      (("1"
                                        (expand "x_add")
                                        (("1"
                                          (replace -5)
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (hide -2)
                                              (("1"
                                                (lemma
                                                 "m_monotone"
                                                 ("a"
                                                  "difference(nonzero_set?(i2!1), nonzero_set?(i1!1))"
                                                  "b"
                                                  "nonzero_set?(i2!1)"))
                                                (("1"
                                                  (split -1)
                                                  (("1"
                                                    (expand "x_le")
                                                    (("1"
                                                      (replace -5)
                                                      (("1"
                                                        (flatten)
                                                        (("1"
                                                          (replace -1)
                                                          (("1"
                                                            (hide -2)
                                                            (("1"
                                                              (hide-all-but
                                                               (-2 1))
                                                              (("1"
                                                                (lemma
                                                                 "m_monotone"
                                                                 ("a"
                                                                  "nonzero_set?(LAMBDA (x: T): i1!1(x) + i2!1(x))"
                                                                  "b"
                                                                  "union(nonzero_set?(i1!1), nonzero_set?(i2!1))"))
                                                                (("1"
                                                                  (split
                                                                   -1)
                                                                  (("1"
                                                                    (expand
                                                                     "x_le")
                                                                    (("1"
                                                                      (replace
                                                                       -2)
                                                                      (("1"
                                                                        (flatten)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide-all-but
                                                                     1)
                                                                    (("2"
                                                                      (expand
                                                                       "nonzero_set?")
                                                                      (("2"
                                                                        (expand
                                                                         "union")
                                                                        (("2"
                                                                          (expand
                                                                           "subset?")
                                                                          (("2"
                                                                            (expand
                                                                             "member")
                                                                            (("2"
                                                                              (skosimp*)
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide-all-but
                                                                   1)
                                                                  (("2"
                                                                    (lemma
                                                                     "nonzero_measurable"
                                                                     ("g"
                                                                      "i1!1"))
                                                                    (("2"
                                                                      (lemma
                                                                       "nonzero_measurable"
                                                                       ("g"
                                                                        "i2!1"))
                                                                      (("2"
                                                                        (expand
                                                                         "measurable_set?")
                                                                        (("2"
                                                                          (lemma
                                                                           "sigma_algebra_union"
                                                                           ("x"
                                                                            "nonzero_set?(i1!1)"
                                                                            "y"
                                                                            "nonzero_set?(i2!1)"))
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (propax)
                                                                            nil
                                                                            nil)
                                                                           ("3"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("3"
                                                                  (hide-all-but
                                                                   1)
                                                                  (("3"
                                                                    (lemma
                                                                     "nonzero_measurable"
                                                                     ("g"
                                                                      "LAMBDA (x: T): i1!1(x) + i2!1(x)"))
                                                                    (("1"
                                                                      (propax)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2)
                                                                      (("2"
                                                                        (lemma
                                                                         "sum_measurable"
                                                                         ("g1"
                                                                          "i1!1"
                                                                          "g2"
                                                                          "i2!1"))
                                                                        (("2"
                                                                          (expand
                                                                           "+")
                                                                          (("2"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide-all-but 1)
                                                    (("2"
                                                      (expand
                                                       "nonzero_set?")
                                                      (("2"
                                                        (expand
                                                         "difference")
                                                        (("2"
                                                          (expand
                                                           "subset?")
                                                          (("2"
                                                            (expand
                                                             "member")
                                                            (("2"
                                                              (skosimp*)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (lemma
                                                   "nonzero_measurable"
                                                   ("g" "i2!1"))
                                                  (("2"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (lemma
                                 "sigma_algebra_difference"
                                 ("x"
                                  "nonzero_set?(i2!1)"
                                  "y"
                                  "nonzero_set?(i1!1)"))
                                (("1"
                                  (expand "measurable_set?")
                                  (("1"
                                    (expand "member")
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (lemma
                                   "nonzero_measurable"
                                   ("g" "i1!1"))
                                  (("2"
                                    (expand "measurable_set?")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (lemma
                                   "nonzero_measurable"
                                   ("g" "i2!1"))
                                  (("3"
                                    (expand "measurable_set?")
                                    (("3" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf 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)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (sum_measurable application-judgement "measurable_function[T, S]"
     isf nil)
    (simple_add application-judgement "simple" isf nil)
    (S formal-const-decl "sigma_algebra" isf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (simple nonempty-type-eq-decl nil measure_space nil)
    (simple? const-decl "bool" measure_space nil)
    (simple_add judgement-tcc nil measure_space nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (union_difference formula-decl nil sets_lemmas nil)
    (set type-eq-decl nil sets nil)
    (nonzero_set? const-decl "set[T]" isf nil)
    (m formal-const-decl "measure_type" isf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (difference const-decl "set" sets nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (m_disjoint_union formula-decl nil measure_props nil)
    (x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
    (sum_measurable judgement-tcc nil measure_space_def nil)
    (sigma_algebra_union formula-decl nil sigma_algebra nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (nonzero_measurable formula-decl nil isf nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (x_le const-decl "bool" extended_nnreal "extended_nnreal/")
    (m_monotone formula-decl nil measure_props nil)
    (x_add const-decl "extended_nnreal" extended_nnreal
     "extended_nnreal/")
    (mu_fin? const-decl "bool" measure_props nil)
    (sigma_algebra_difference formula-decl nil sigma_algebra nil)
    (difference_disjoint formula-decl nil sets_lemmas nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
(isf_scal 0
  (isf_scal-1 nil 3390785367
   ("" (skosimp)
    (("" (typepred "i!1")
      (("" (expand "*")
        (("" (expand "isf?")
          (("" (flatten)
            (("" (lemma "simple_scal" ("c" "c!1" "h" "i!1"))
              (("" (expand "*")
                (("" (split)
                  (("1" (propax) nil nil)
                   ("2" (hide -1 -2)
                    (("2" (case-replace "c!1=0")
                      (("1"
                        (case-replace
                         "nonzero_set?(LAMBDA (x: T): 0 * i!1(x)) = emptyset[T]")
                        (("1" (expand "mu_fin?")
                          (("1" (typepred "m")
                            (("1" (expand "measure?")
                              (("1"
                                (flatten)
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "measure_empty?")
                                    (("1"
                                      (replace -1)
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide-all-but 1)
                          (("2" (apply-extensionality :hide? t)
                            (("2" (expand "emptyset")
                              (("2"
                                (expand "nonzero_set?")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2"
                        (case-replace
                         "nonzero_set?(LAMBDA (x: T): c!1 * i!1(x)) = nonzero_set?(i!1)")
                        (("2" (hide-all-but (1 2))
                          (("2" (apply-extensionality :hide? t)
                            (("2" (expand "nonzero_set?")
                              (("2"
                                (expand "/=")
                                (("2"
                                  (assert)
                                  (("2"
                                    (case-replace "i!1(x!1) = 0")
                                    (("1" (assert) nil nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf 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)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (S formal-const-decl "sigma_algebra" isf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (simple nonempty-type-eq-decl nil measure_space nil)
    (simple? const-decl "bool" measure_space nil)
    (simple_scal judgement-tcc nil measure_space nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (measure_empty? const-decl "bool" generalized_measure_def nil)
    (m formal-const-decl "measure_type" isf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (null_emptyset name-judgement "null_set" isf nil)
    (subset_algebra_emptyset name-judgement "(S)" isf nil)
    (set type-eq-decl nil sets nil)
    (nonzero_set? const-decl "set[T]" isf nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (emptyset const-decl "set" sets nil)
    (/= const-decl "boolean" notequal nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(isf_opp 0
  (isf_opp-1 nil 3390790565
   ("" (skosimp)
    (("" (typepred "i!1")
      (("" (lemma "isf_scal" ("c" "-1" "i" "i!1"))
        (("" (expand "*")
          (("" (expand "-" 1) (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf 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)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (isf_scal judgement-tcc nil isf nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil))
   nil))
(isf_diff 0
  (isf_diff-1 nil 3390790565
   ("" (skosimp)
    (("" (lemma "isf_opp" ("i" "i2!1"))
      (("" (lemma "isf_add" ("i1" "i1!1" "i2" "-i2!1"))
        (("" (expand "-")
          (("" (expand "+") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (T formal-type-decl nil isf nil)
    (isf_opp judgement-tcc nil isf nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (isf_opp application-judgement "isf" isf nil)
    (isf_add judgement-tcc nil isf nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/"))
   nil))
(isf_abs 0
  (isf_abs-1 nil 3390785367
   ("" (skosimp)
    (("" (typepred "i!1")
      (("" (expand "isf?")
        (("" (flatten)
          (("" (lemma "simple_abs" ("h" "i!1"))
            (("" (expand "simple?")
              (("" (flatten)
                ((""
                  (lemma "m_monotone"
                   ("a" "nonzero_set?(abs[T](i!1))" "b"
                    "nonzero_set?(i!1)"))
                  (("" (split -1)
                    (("1" (expand "x_le")
                      (("1" (expand "mu_fin?")
                        (("1" (replace -6) (("1" (flatten) nil nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide-all-but 1)
                      (("2" (expand "nonzero_set?")
                        (("2" (expand "abs")
                          (("2" (expand "subset?")
                            (("2" (expand "member")
                              (("2"
                                (skosimp*)
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (expand "abs")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf 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)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (m formal-const-decl "measure_type" isf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nonzero_set? const-decl "set[T]" isf nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (set type-eq-decl nil sets nil)
    (m_monotone formula-decl nil measure_props nil)
    (member const-decl "bool" sets nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (subset? const-decl "bool" sets nil)
    (x_le const-decl "bool" extended_nnreal "extended_nnreal/")
    (mu_fin? const-decl "bool" measure_props nil)
    (simple_abs judgement-tcc nil measure_space nil)
    (simple? const-decl "bool" measure_space nil)
    (simple nonempty-type-eq-decl nil measure_space nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" isf nil)
    (simple_abs application-judgement "simple" isf nil)
    (abs_measurable application-judgement "measurable_function[T, S]"
     isf nil))
   nil))
(isf_min 0
  (isf_min-1 nil 3390785367
   ("" (skosimp)
    (("" (typepred "i1!1")
      (("" (typepred "i2!1")
        (("" (expand "isf?")
          (("" (flatten)
            (("" (lemma "simple_min" ("h1" "i1!1" "h2" "i2!1"))
              (("" (expand "min")
                (("" (hide -1 -2 -4)
                  (("" (expand "mu_fin?")
                    ((""
                      (case "subset?(nonzero_set?(LAMBDA (x: T): min(i1!1(x), i2!1(x))),union(nonzero_set?(i1!1),nonzero_set?(i2!1)))")
                      (("1"
                        (lemma "m_union"
                         ("a" "nonzero_set?(i1!1)" "b"
                          "nonzero_set?(i2!1)"))
                        (("1"
                          (lemma "m_monotone"
                           ("a"
                            "nonzero_set?(LAMBDA (x: T): min(i1!1(x), i2!1(x)))"
                            "b"
                            "union(nonzero_set?(i1!1), nonzero_set?(i2!1))"))
                          (("1" (replace -3 -1 LR)
                            (("1"
                              (name-replace "NZM"
                               "nonzero_set?(LAMBDA (x: T): min(i1!1(x), i2!1(x)))")
                              (("1"
                                (hide -3)
                                (("1"
                                  (expand "x_le")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (expand "x_add")
                                      (("1" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "measurable_set?")
                            (("2"
                              (lemma "sigma_algebra_union"
                               ("x"
                                "nonzero_set?(i1!1)"
                                "y"
                                "nonzero_set?(i2!1)"))
                              (("2" (assert) nil nil)) nil))
                            nil)
                           ("3" (rewrite "nonzero_measurable")
                            (("3"
                              (lemma "min_measurable"
                               ("g1" "i1!1" "g2" "i2!1"))
                              (("3"
                                (expand "min" -1)
                                (("3" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (lemma "nonzero_measurable" ("g" "i2!1"))
                          (("2" (propax) nil nil)) nil)
                         ("3" (lemma "nonzero_measurable" ("g" "i1!1"))
                          (("3" (propax) nil nil)) nil))
                        nil)
                       ("2" (hide-all-but 1) (("2" (grind) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf 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)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (min_measurable application-judgement "measurable_function[T, S]"
     isf nil)
    (simple_min application-judgement "simple" isf nil)
    (S formal-const-decl "sigma_algebra" isf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (simple nonempty-type-eq-decl nil measure_space nil)
    (simple? const-decl "bool" measure_space nil)
    (simple_min judgement-tcc nil measure_space nil)
    (set type-eq-decl nil sets nil)
    (subset? const-decl "bool" sets nil)
    (nonzero_set? const-decl "set[T]" isf nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (union const-decl "set" sets nil)
    (m_monotone formula-decl nil measure_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (x_le const-decl "bool" extended_nnreal "extended_nnreal/")
    (x_add const-decl "extended_nnreal" extended_nnreal
     "extended_nnreal/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_algebra_union formula-decl nil sigma_algebra nil)
    (member const-decl "bool" sets nil)
    (min_measurable judgement-tcc nil measure_space nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (nonzero_measurable formula-decl nil isf nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (m formal-const-decl "measure_type" isf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (m_union formula-decl nil measure_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (min const-decl "[T -> real]" real_fun_ops_aux "reals/"))
   nil))
(isf_max 0
  (isf_max-1 nil 3390785367
   ("" (skosimp)
    (("" (typepred "i1!1")
      (("" (typepred "i2!1")
        (("" (lemma "isf_scal" ("c" "-1" "i" "i1!1"))
          (("" (lemma "isf_scal" ("c" "-1" "i" "i2!1"))
            ((""
              (lemma "isf_min"
               ("i1" "*[T](-1, i1!1)" "i2" "*[T](-1, i2!1)"))
              (("" (expand "*")
                (("" (expand "min")
                  ((""
                    (lemma "isf_scal"
                     ("c" "-1" "i"
                      "LAMBDA (x_1: T): min(-1 * i1!1(x_1), -1 * i2!1(x_1))"))
                    (("1" (expand "*" -1)
                      (("1" (expand "min")
                        (("1" (expand "max")
                          (("1" (expand "max")
                            (("1"
                              (case-replace "(LAMBDA (x: T):
             -1 *
              IF -1 * i1!1(x) > -1 * i2!1(x) THEN -1 * i2!1(x)
              ELSE -1 * i1!1(x)
              ENDIF)=(LAMBDA (x: T):
             IF i1!1(x) < i2!1(x) THEN i2!1(x) ELSE i1!1(x) ENDIF)")
                              (("1"
                                (apply-extensionality :hide? t)
                                (("1"
                                  (hide-all-but 1)
                                  (("1" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf 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)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (isf_scal judgement-tcc nil isf nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (isf_scal application-judgement "isf" isf nil)
    (isf_min judgement-tcc nil isf nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (min const-decl "[T -> real]" real_fun_ops_aux "reals/")
    (max const-decl "[T -> real]" real_fun_ops_aux "reals/")
    (< const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(isf_minimum 0
  (isf_minimum-1 nil 3409635960
   ("" (induct "n")
    (("1" (expand "minimum") (("1" (propax) nil nil)) nil)
     ("2" (skosimp*)
      (("2" (inst - "w!1")
        (("2" (expand "minimum" 1)
          (("2" (assert) (("2" (rewrite "isf_min") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((min_measurable application-judgement "measurable_function[T, S]"
     isf nil)
    (simple_min application-judgement "simple" isf nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (isf_min judgement-tcc nil isf nil)
    (minimum_measurable application-judgement
     "measurable_function[T, S]" isf nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (minimum def-decl "[T -> real]" real_fun_ops_aux "reals/")
    (sequence type-eq-decl nil sequences nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil) (T formal-type-decl nil isf nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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))
   nil))
(isf_maximum 0
  (isf_maximum-1 nil 3409635960
   ("" (induct "n")
    (("1" (expand "maximum") (("1" (propax) nil nil)) nil)
     ("2" (skosimp*)
      (("2" (inst - "w!1")
        (("2" (expand "maximum" 1) (("2" (rewrite "isf_max") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((max_measurable application-judgement "measurable_function[T, S]"
     isf nil)
    (simple_max application-judgement "simple" isf nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (maximum_measurable application-judgement
     "measurable_function[T, S]" isf nil)
    (isf_max judgement-tcc nil isf nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (maximum def-decl "[T -> real]" real_fun_ops_aux "reals/")
    (sequence type-eq-decl nil sequences nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil) (T formal-type-decl nil isf nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
--> --------------------

--> maximum size reached

--> --------------------

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