Quelle  integral.prf   Sprache: Lisp

(integral
 (IMP_integral_def_TCC1 0
  (IMP_integral_def_TCC1-1 nil 3610459517
   ("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
   ((connected_domain formula-decl nil integral nil)) nil))
 (IMP_integral_def_TCC2 0
  (IMP_integral_def_TCC2-1 nil 3610459517
   ("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
   ((not_one_element formula-decl nil integral nil)) nil))
 (Integrable?_a_to_a 0
  (Integrable?_a_to_a-1 nil 3253535925
   ("" (skosimp*)
    (("" (expand "Integrable?") (("" (propax) nil nil)) nil)) nil)
   ((Integrable? const-decl "bool" integral_def nil)) nil))
 (Integral_a_to_a_TCC1 0
  (Integral_a_to_a_TCC1-1 nil 3253535925
   ("" (skeep)
    (("" (lemma "Integrable?_a_to_a") (("" (inst?) nil nil)) nil)) nil)
   ((Integrable?_a_to_a formula-decl nil integral 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)
    (T_pred const-decl "[real -> boolean]" integral nil)
    (T formal-nonempty-subtype-decl nil integral nil))
   nil))
 (Integral_a_to_a 0
  (Integral_a_to_a-1 nil 3253535925
   ("" (skosimp*)
    (("" (expand "Integral") (("" (propax) nil nil)) nil)) nil)
   ((Integral const-decl "real" integral_def nil)) nil))
 (Integral_const_fun 0
  (Integral_const_fun-1 nil 3253535925
   ("" (skosimp*)
    (("" (lemma "trichotomy")
      (("" (inst - "b!1-a!1")
        (("" (lemma "integral_const_fun")
          (("" (expand "Integrable?")
            (("" (expand "Integral")
              (("" (split -2)
                (("1" (assert)
                  (("1" (inst - "D!1" "a!1" "b!1")
                    (("1" (assert) nil nil)) nil))
                  nil)
                 ("2" (assert) nil nil)
                 ("3" (inst - "D!1" "b!1" "a!1")
                  (("3" (assert)
                    (("3" (flatten) (("3" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integral const-decl "real" integral_def nil)
    (Integrable? const-decl "bool" integral_def nil))
   nil))
 (Integral_const_restrict 0
  (Integral_const_restrict-1 nil 3292336721
   ("" (skosimp*)
    (("" (lemma "trichotomy")
      (("" (inst - "b!1-a!1")
        (("" (lemma "integral_const_restrict")
          (("" (expand "Integral")
            (("" (expand "Integrable?")
              (("" (assert)
                (("" (split -2)
                  (("1" (assert)
                    (("1" (inst - "D!1" "a!1" "b!1" "f!1")
                      (("1" (assert)
                        (("1" (split -2)
                          (("1" (lemma "integral_def")
                            (("1" (inst?) (("1" (assert) nil nil))
                              nil))
                            nil)
                           ("2" (hide 2)
                            (("2" (skosimp*) (("2" (inst?) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil)
                   ("3" (assert)
                    (("3" (inst - "D!1" "b!1" "a!1" "f!1")
                      (("3" (assert)
                        (("3" (split -2)
                          (("1" (lemma "integral_def")
                            (("1" (inst?)
                              (("1"
                                (assert)
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (inst?)
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide 2)
                            (("2" (skosimp*) (("2" (inst?) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integrable? const-decl "bool" integral_def nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (Closed_interval type-eq-decl nil intervals_real "reals/")
    (Integral const-decl "real" integral_def nil))
   shostak))
 (Integral_rev 0
  (Integral_rev-1 nil 3253535925
   ("" (skosimp*)
    (("" (grind :exclude "Integrable?")
      (("" (expand "Integrable?") (("" (prop) nil nil)) nil)) nil))
    nil)
   ((Integral const-decl "real" integral_def nil)
    (Integrable? const-decl "bool" integral_def nil))
   nil))
 (continuous_Integrable? 0
  (continuous_Integrable?-3 nil 3292321430
   ("" (skosimp*)
    (("" (lemma "continuous_integrable")
      (("" (lemma "trichotomy")
        (("" (inst -1 "b!1-a!1")
          (("" (expand "Integrable?")
            (("" (split -1)
              (("1" (assert)
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (skosimp*) (("1" (inst?) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil)
               ("3" (assert)
                (("3" (inst?)
                  (("3" (assert)
                    (("3" (skosimp*) (("3" (inst?) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((closed_interval type-eq-decl nil intervals_real "reals/")
    (Closed_interval type-eq-decl nil intervals_real "reals/")
    (Integrable? const-decl "bool" integral_def nil))
   nil)
  (continuous_Integrable?-2 nil 3292320550
   ("" (skosimp*)
    (("" (lemma "cont_integrable")
      (("" (lemma "trichotomy")
        (("" (inst -1 "b!1-a!1")
          (("" (expand "Integrable?")
            (("" (split -1)
              (("1" (assert)
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (skosimp*) (("1" (inst?) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil)
               ("3" (assert)
                (("3" (inst?)
                  (("3" (assert)
                    (("3" (skosimp*) (("3" (inst?) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integrable? const-decl "bool" integral_def nil)) nil)
  (continuous_Integrable?-1 nil 3253535925
   ("" (skosimp*)
    (("" (lemma "continuous_integrable")
      (("" (lemma "trichotomy")
        (("" (inst -1 "b!1-a!1")
          (("" (expand "Integrable?")
            (("" (split -1)
              (("1" (assert)
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (skosimp*) (("1" (inst?) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil)
               ("3" (assert)
                (("3" (inst?)
                  (("3" (assert)
                    (("3" (skosimp*) (("3" (inst?) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integrable? const-decl "bool" integral_def nil)) nil))
 (cont_Integrable? 0
  (cont_Integrable?-1 nil 3320592805
   ("" (skosimp*)
    (("" (lemma "continuous_Integrable?[T]")
      (("" (inst?)
        (("" (assert)
          (("" (skosimp*)
            (("" (expand "continuous?" -1) (("" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_Integrable? formula-decl nil integral nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (Closed_interval type-eq-decl nil intervals_real "reals/")
    (T formal-nonempty-subtype-decl nil integral nil)
    (T_pred const-decl "[real -> boolean]" integral 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))
   shostak))
 (cont_fun_Integrable? 0
  (cont_fun_Integrable?-1 nil 3313938422
   ("" (skosimp*)
    (("" (lemma "continuous_Integrable?")
      (("" (inst?)
        (("" (assert)
          (("" (skosimp*)
            (("" (expand "continuous?" -1) (("" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_Integrable? formula-decl nil integral nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (Closed_interval type-eq-decl nil intervals_real "reals/")
    (T formal-nonempty-subtype-decl nil integral nil)
    (T_pred const-decl "[real -> boolean]" integral 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))
 (Integral_scal 0
  (Integral_scal-1 nil 3253535925
   ("" (skosimp*)
    (("" (case-replace "D!1 = 0")
      (("1" (assert)
        (("1" (expand "*")
          (("1" (lemma "Integral_const_fun")
            (("1" (inst - "0" "a!1" "b!1")
              (("1" (flatten)
                (("1" (expand "const_fun") (("1" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "trichotomy")
        (("2" (inst -1 "b!1 - a!1")
          (("2" (expand "Integrable?")
            (("2" (expand "Integral")
              (("2" (split -1)
                (("1" (assert)
                  (("1" (rewrite "integral_scal") nil nil)) nil)
                 ("2" (assert) nil nil)
                 ("3" (assert)
                  (("3" (lemma "integral_scal")
                    (("3" (inst -1 "D!1" "b!1" "a!1" "f!1")
                      (("3" (assert)
                        (("3" (flatten) (("3" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (Integral const-decl "real" integral_def nil)
    (Integrable? const-decl "bool" integral_def nil))
   nil))
 (Integral_sum 0
  (Integral_sum-1 nil 3253535925
   ("" (skosimp*)
    (("" (lemma "integral_sum")
      (("" (lemma "trichotomy")
        (("" (inst -1 "b!1-a!1")
          (("" (expand "Integrable?")
            (("" (expand "Integral")
              (("" (split -1)
                (("1" (assert)
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
                 ("2" (assert) nil nil)
                 ("3" (assert)
                  (("3" (inst -2 "b!1" "a!1" "f!1" "g!1")
                    (("3" (assert)
                      (("3" (flatten) (("3" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integral const-decl "real" integral_def nil)
    (Integrable? const-decl "bool" integral_def nil))
   nil))
 (Integral_diff 0
  (Integral_diff-1 nil 3253535925
   ("" (skosimp*)
    (("" (lemma "Integral_sum")
      (("" (inst -1 "a!1" "b!1" "f!1" "-g!1")
        (("" (assert)
          (("" (split -1)
            (("1" (flatten)
              (("1" (expand "-")
                (("1" (assert)
                  (("1" (replace -2)
                    (("1" (assert)
                      (("1" (lemma "Integral_scal")
                        (("1" (inst?)
                          (("1" (assert)
                            (("1" (flatten)
                              (("1"
                                (assert)
                                (("1"
                                  (case-replace
                                   "(LAMBDA (x: T): -g!1(x)) = -1* g!1")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (hide-all-but 1)
                                    (("2"
                                      (apply-extensionality 1 :hide? t)
                                      (("2"
                                        (expand "*")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide -1 2)
              (("2" (lemma "Integral_scal")
                (("2" (inst -1 "-1" "a!1" "b!1" "g!1")
                  (("2" (assert)
                    (("2" (flatten)
                      (("2" (assert)
                        (("2" (expand "-")
                          (("2"
                            (case-replace
                             "(LAMBDA (x: T): -g!1(x)) = -1* g!1")
                            (("2" (hide-all-but 1)
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                (("2"
                                  (expand "*")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integral_sum formula-decl nil integral nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (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/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Integral_scal formula-decl nil integral nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (T formal-nonempty-subtype-decl nil integral nil)
    (T_pred const-decl "[real -> boolean]" integral 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))
 (Integral_split 0
  (Integral_split-1 nil 3253535925
   ("" (skosimp*)
    (("" (case-replace "a!1 = b!1")
      (("1" (expand "Integral") (("1" (propax) nil nil)) nil)
       ("2" (case-replace "b!1 = c!1")
        (("1" (expand "Integral") (("1" (propax) nil nil)) nil)
         ("2" (case-replace "a!1 = c!1")
          (("1" (expand "Integral")
            (("1" (assert)
              (("1" (expand "Integrable?")
                (("1" (assert)
                  (("1" (case-replace "c!1 < b!1")
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (lemma "integral_split")
            (("2" (case "a!1 < b!1 AND b!1 < c!1")
              (("1" (inst - "a!1" "b!1" "c!1" "f!1")
                (("1" (flatten)
                  (("1" (assert)
                    (("1" (expand "Integrable?")
                      (("1" (expand "Integral")
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (case "a!1 < c!1 AND c!1 < b!1")
                (("1" (inst - "a!1" "c!1" "b!1" "f!1")
                  (("1" (expand "Integrable?")
                    (("1" (expand "Integral")
                      (("1" (flatten)
                        (("1" (assert)
                          (("1" (assert)
                            (("1" (case "integrable?(a!1, c!1, f!1)")
                              (("1" (assert) nil nil)
                               ("2"
                                (hide -3 6)
                                (("2"
                                  (lemma "integrable?_split")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (inst -1 "b!1")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (case "b!1 < a!1 AND a!1 < c!1")
                  (("1" (inst - "b!1" "a!1" "c!1" "f!1")
                    (("1" (expand "Integrable?")
                      (("1" (expand "Integral")
                        (("1" (flatten)
                          (("1" (assert)
                            (("1" (assert)
                              (("1"
                                (case "integrable?(a!1, c!1, f!1)")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (hide -3 7)
                                  (("2"
                                    (lemma "integrable?_split")
                                    (("2"
                                      (inst -1 "b!1" "a!1" "c!1" "f!1")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (case "b!1 < c!1 AND c!1 < a!1")
                    (("1" (inst - "b!1" "c!1" "a!1" "f!1")
                      (("1" (flatten)
                        (("1" (expand "Integrable?")
                          (("1" (expand "Integral")
                            (("1" (assert)
                              (("1"
                                (assert)
                                (("1"
                                  (case "integrable?(c!1, a!1, f!1)")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (hide -3 8)
                                    (("2"
                                      (lemma "integrable?_split")
                                      (("2"
                                        (inst
                                         -1
                                         "b!1"
                                         "c!1"
                                         "a!1"
                                         "f!1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (case "c!1 < a!1 AND a!1 < b!1")
                      (("1" (inst - "c!1" "a!1" "b!1" "f!1")
                        (("1" (flatten)
                          (("1" (expand "Integrable?")
                            (("1" (expand "Integral")
                              (("1"
                                (assert)
                                (("1"
                                  (assert)
                                  (("1"
                                    (case "integrable?(c!1, a!1, f!1)")
                                    (("1" (assert) nil nil)
                                     ("2"
                                      (hide -3 9)
                                      (("2"
                                        (lemma "integrable?_split")
                                        (("2"
                                          (inst
                                           -1
                                           "c!1"
                                           "a!1"
                                           "b!1"
                                           "f!1")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (case "c!1 < b!1 AND b!1 < a!1")
                        (("1" (inst - "c!1" "b!1" "a!1" "f!1")
                          (("1" (expand "Integrable?")
                            (("1" (expand "Integral")
                              (("1"
                                (flatten)
                                (("1"
                                  (assert)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (flatten)
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide -1 -2 -3 10)
                          (("2" (ground) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integral const-decl "real" integral_def nil)
    (Integrable? const-decl "bool" integral_def nil))
   nil))
 (Integral_chg_one_pt 0
  (Integral_chg_one_pt-1 nil 3292336972
   ("" (skosimp*)
    (("" (lemma "trichotomy")
      (("" (inst - "b!1-a!1")
        (("" (lemma "integral_chg_one_pt")
          (("" (expand "Integrable?")
            (("" (expand "Integral")
              (("" (split -2)
                (("1" (assert)
                  (("1" (inst - "a!1" "b!1" "f!1" "yv!1")
                    (("1" (assert)
                      (("1" (inst - "y!1")
                        (("1" (typepred "y!1")
                          (("1" (assert)
                            (("1" (flatten)
                              (("1"
                                (assert)
                                (("1"
                                  (flatten)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil)
                 ("3" (assert)
                  (("3" (inst - "b!1" "a!1" "f!1" "yv!1")
                    (("3" (assert)
                      (("3" (inst - "y!1")
                        (("3" (typepred "y!1")
                          (("3" (assert)
                            (("3" (flatten)
                              (("3"
                                (assert)
                                (("3"
                                  (flatten)
                                  (("3" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integral const-decl "real" integral_def nil)
    (Closed_interval type-eq-decl nil intervals_real "reals/")
    (Integrable? const-decl "bool" integral_def nil))
   shostak))
 (Integral_ge_0 0
  (Integral_ge_0-1 nil 3292337187
   ("" (skosimp*)
    (("" (lemma "integral_ge_0")
      (("" (inst?)
        (("" (inst?)
          (("" (assert)
            (("" (expand "Integrable?")
              (("" (expand "Integral")
                (("" (assert)
                  (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integrable? const-decl "bool" integral_def nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (Closed_interval type-eq-decl nil intervals_real "reals/")
    (Integral const-decl "real" integral_def nil))
   shostak))
 (Integral_ge_0_open 0
  (Integral_ge_0_open-2 nil 3322385346
   ("" (expand "Integrable?")
    (("" (expand "Integral")
      (("" (skosimp*)
        (("" (expand "<=" -1)
          (("" (split -1)
            (("1" (assert)
              (("1"
                (lemma "integral_chg_one_pt"
                 ("a" "a!1" "b" "b!1" "f" "f!1" "yv" "1"))
                (("1" (assert)
                  (("1" (inst - "a!1")
                    (("1" (assert)
                      (("1" (flatten)
                        (("1"
                          (lemma "integral_chg_one_pt"
                           ("a" "a!1" "b" "b!1" "f"
                            "f!1 WITH [(a!1) := 1]" "yv" "1"))
                          (("1" (assert)
                            (("1" (inst - "b!1")
                              (("1"
                                (assert)
                                (("1"
                                  (flatten)
                                  (("1"
                                    (lemma
                                     "integral_ge_0"
                                     ("a"
                                      "a!1"
                                      "b"
                                      "b!1"
                                      "f"
                                      "f!1 WITH [(a!1) := 1, (b!1) := 1]"))
                                    (("1"
                                      (assert)
                                      (("1"
                                        (hide-all-but (-7 1))
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (case-replace "x!1=a!1")
                                            (("1" (assert) nil nil)
                                             ("2"
                                              (case-replace "x!1=b!1")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (inst - "x!1")
                                                (("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))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integral const-decl "real" integral_def nil)
    (Open_interval type-eq-decl nil intervals_real "reals/")
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (Integrable? const-decl "bool" integral_def nil))
   nil)
  (Integral_ge_0_open-1 nil 3322385296 ("" (postpone) nil nil) nil
   shostak))
 (Integral_bound 0
  (Integral_bound-1 nil 3253535925
   ("" (skosimp*)
    (("" (lemma "integral_bound")
      (("" (inst?)
        (("" (inst -1 "M!1" "f!1")
          (("" (assert)
            (("" (expand "Integrable?")
              (("" (expand "Integral")
                (("" (assert)
                  (("" (split -1)
                    (("1" (propax) nil nil)
                     ("2" (hide 2)
                      (("2" (skosimp*) (("2" (inst?) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Integrable? const-decl "bool" integral_def nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (Closed_interval type-eq-decl nil intervals_real "reals/")
    (Integral const-decl "real" integral_def nil))
   nil))
 (Integral_bounded 0
  (Integral_bounded-1 nil 3253535925
   ("" (skosimp*)
    (("" (lemma "integral_bound")
      (("" (expand "Integral")
        (("" (lemma "trichotomy")
          (("" (inst -1 "b!1-a!1")
            (("" (split -1)
              (("1" (expand "Integrable?")
                (("1" (assert)
                  (("1" (inst -2 "M!1" "a!1" "b!1" "f!1" "-M!1")
                    (("1" (assert)
                      (("1" (split -2)
                        (("1" (hide -3 -4)
                          (("1" (expand "abs")
                            (("1" (lift-if) (("1" (ground) nil nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skosimp*)
                          (("2" (inst?)
                            (("2" (expand "abs")
                              (("2"
                                (assert)
                                (("2"
                                  (lift-if)
                                  (("2" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (expand "abs") (("2" (assert) nil nil)) nil))
                nil)
               ("3" (inst -2 "M!1" "b!1" "a!1" "f!1" "-M!1")
                (("3" (assert)
                  (("3" (split -2)
                    (("1" (hide -3 -4)
                      (("1" (expand "abs")
                        (("1" (lift-if) (("1" (ground) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (expand "Integrable?")
                      (("2" (propax) nil nil)) nil)
                     ("3" (skosimp*)
                      (("3" (inst?)
                        (("3" (hide 2)
                          (("3" (expand "abs")
                            (("3" (lift-if) (("3" (ground) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Closed_interval type-eq-decl nil intervals_real "reals/")
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (Integrable? const-decl "bool" integral_def nil)
    (Integral const-decl "real" integral_def nil))
   nil))
 (Integral_le 0
  (Integral_le-1 nil 3297783496
   ("" (skosimp*)
    (("" (expand "Integral")
      (("" (assert)
        (("" (expand "Integrable?")
          (("" (rewrite "integral_le") nil nil)) nil))
        nil))
      nil))
    nil)
   ((Integral const-decl "real" integral_def nil)
    (Integrable? const-decl "bool" integral_def nil))
   shostak))
 (Integral_neg 0
  (Integral_neg-1 nil 3322385450
   ("" (skosimp)
    (("" (lemma "Integral_const_fun" ("a" "a!1" "b" "b!1" "D" "0"))
      (("" (flatten)
        (("" (expand "const_fun")
          ((""
            (lemma "Integral_diff"
             ("a" "a!1" "b" "b!1" "g" "f!1" "f" "LAMBDA (x: T): 0"))
            (("" (assert)
              (("" (flatten)
                (("" (assert)
                  (("" (replace -4)
                    (("" (expand "-" 1) (("" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-subtype-decl nil integral nil)
    (T_pred const-decl "[real -> boolean]" integral 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)
    (Integral_const_fun formula-decl nil integral nil)
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (Integral_diff formula-decl nil integral nil))
   nil))
 (Integral_restr_eq 0
  (Integral_restr_eq-2 nil 3610459029
   ("" (skeep)
    (("" (case-replace "b = a")
      (("1" (rewrite "Integrable?_a_to_a")
        (("1" (rewrite "Integrable?_a_to_a")
          (("1" (rewrite "Integral_a_to_a")
            (("1" (rewrite "Integral_a_to_a") nil)))))))
       ("2" (lemma "integral_restr_eq")
        (("2" (case "a < b")
          (("1" (inst - "a" "b" "f" "g")
            (("1" (assert)
              (("1" (split -2)
                (("1" (flatten)
                  (("1" (expand "Integrable?")
                    (("1" (expand "Integral") (("1" (assert) nil)))))))
                 ("2" (hide 3)
                  (("2" (skosimp*)
                    (("2" (inst?) (("2" (assert) nil)))))))
                 ("3" (expand "Integrable?")
                  (("3" (propax) nil)))))))))
           ("2" (expand "Integrable?")
            (("2" (assert)
              (("2" (expand "Integral")
                (("2" (inst - "b" "a" "f" "g")
                  (("2" (assert)
                    (("2" (split -1)
                      (("1" (flatten) (("1" (assert) nil)))
                       ("2" (hide 4)
                        (("2" (skosimp*)
                          (("2" (inst?)
                            (("2" (assert)
                              nil))))))))))))))))))))))))))
    nil)
   nil nil)
  (Integral_restr_eq-1 nil 3610458938
   ("" (skeep)
    (("" (case-replace "b = a")
      (("1" (rewrite "Integrable?_a_to_a")
        (("1" (rewrite "Integrable?_a_to_a")
          (("1" (rewrite "Integral_a_to_a")
            (("1" (rewrite "Integral_a_to_a") nil)))))))
       ("2" (lemma "integral_restr_eq")
        (("2" (case "a < b")
          (("1" (inst - "a" "b" "f" "g")
            (("1" (assert)
              (("1" (split -2)
                (("1" (flatten)
                  (("1" (expand "Integrable?")
                    (("1" (expand "Integral") (("1" (assert) nil)))))))
                 ("2" (hide 3)
                  (("2" (skosimp*)
                    (("2" (inst?) (("2" (assert) nil)))))))
                 ("3" (expand "Integrable?")
                  (("3" (propax) nil)))))))))
           ("2" (expand "Integrable?")
            (("2" (assert)
              (("2" (expand "Integral")
                (("2" (inst - "b" "a" "f" "g")
                  (("2" (assert)
                    (("2" (split -1)
                      (("1" (flatten) (("1" (assert) nil)))
                       ("2" (hide 4)
                        (("2" (skosimp*)
                          (("2" (inst?)
                            (("2" (assert)
                              nil))))))))))))))))))))))))))
    nil)
   nil nil)))