Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: indefinite_integral.prf Sprache: Lisp

Original von: PVS^©

(indefinite_integral
(deriv_domain 0
  (deriv_domain-1 nil 3472399769
   ("" (lemma "connected_domain")
    (("" (lemma "connected_deriv_domain[T]")
      (("" (lemma not_one_element) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (T_pred const-decl "[real -> boolean]" indefinite_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)
    (connected_deriv_domain formula-decl nil deriv_domain_def nil)
    (not_one_element formula-decl nil indefinite_integral nil)
    (connected_domain formula-decl nil indefinite_integral nil))
   nil))
(IMP_integral_TCC1 0
  (IMP_integral_TCC1-1 nil 3393924105
   ("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
   ((connected_domain formula-decl nil indefinite_integral nil)) nil))
(IMP_integral_TCC2 0
  (IMP_integral_TCC2-1 nil 3393924105
   ("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
   ((not_one_element formula-decl nil indefinite_integral nil)) nil))
(antiderivative?_TCC1 0
  (antiderivative?_TCC1-1 nil 3610702294
   ("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
   ((deriv_domain formula-decl nil indefinite_integral nil)) nil))
(antiderivative_lem 0
  (antiderivative_lem-1 nil 3393924909
   ("" (skosimp*)
    (("" (expand "antiderivative?")
      (("" (flatten)
        ((""
          (case "derivable?(G!1-F!1) AND deriv(G!1-F!1) = const_fun(0)")
          (("1" (flatten)
            (("1" (expand "const_fun")
              (("1" (lemma "null_derivative[T]")
                (("1" (inst -1 "G!1-F!1")
                  (("1" (assert)
                    (("1" (flatten)
                      (("1" (hide -1)
                        (("1" (split -1)
                          (("1" (expand "constant?")
                            (("1" (hide-all-but (-1 1))
                              (("1"
                                (name "xa" "choose({x: T | true})")
                                (("1"
                                  (inst + "(F!1-G!1)(xa)")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (expand "+ ")
                                        (("1"
                                          (expand "-")
                                          (("1"
                                            (inst - "x!1" "xa")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but 1)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skosimp*)
                            (("2"
                              (case-replace
                               "deriv(G!1 - F!1)(x!1) = 0")
                              (("1"
                                (expand "deriv" -1)
                                (("1" (propax) nil nil))
                                nil)
                               ("2"
                                (hide 2 3)
                                (("2"
                                  (replace -2)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (lemma "derivable_diff[T]")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (hide -1)
                    (("2" (rewrite "deriv_diff_fun[T]")
                      (("2" (assert)
                        (("2" (expand "const_fun")
                          (("2" (replace -2)
                            (("2" (replace -4)
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                (("2"
                                  (expand "-")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((antiderivative? const-decl "bool" indefinite_integral nil)
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv const-decl "[T -> real]" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable? const-decl "bool" derivatives nil)
    (T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (T_pred const-decl "[real -> boolean]" indefinite_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)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (derivable_const application-judgement "deriv_fun" derivatives nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (constant? const-decl "bool" real_fun_preds "reals/")
    (null_derivative formula-decl nil derivative_props nil)
    (derivable_diff judgement-tcc nil derivatives nil)
    (deriv_diff_fun formula-decl nil derivatives nil))
   nil))
(derivs_eq 0
  (derivs_eq-1 nil 3393930788
   ("" (skosimp*)
    (("" (lemma "antiderivative_lem")
      (("" (inst?)
        (("" (inst -1 "deriv(F!1)")
          (("" (assert)
            (("" (split -1)
              (("1" (propax) nil nil)
               ("2" (hide 2)
                (("2" (expand "antiderivative?")
                  (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((antiderivative_lem formula-decl nil indefinite_integral nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (antiderivative? const-decl "bool" indefinite_integral nil)
    (T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (T_pred const-decl "[real -> boolean]" indefinite_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))
(cont_fun_integrable? 0
  (cont_fun_integrable?-1 nil 3393943252
   ("" (skosimp*)
    (("" (lemma "fundamental2")
      (("" (inst?)
        (("" (assert)
          (("" (skosimp*)
            (("" (expand "integrable?")
              (("" (inst?)
                (("" (expand "antiderivative?") (("" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (T_pred const-decl "[real -> boolean]" indefinite_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)
    (fundamental2 formula-decl nil fundamental_theorem nil)
    (integrable? const-decl "bool" indefinite_integral nil)
    (antiderivative? const-decl "bool" indefinite_integral nil))
   nil))
(integral_TCC1 0
  (integral_TCC1-2 nil 3393924197
   ("" (lemma "connected_domain")
    (("" (lemma "not_one_element")
      (("" (lemma "connected_deriv_domain[T]")
        (("" (assert)
          ((""
            (inst +
             "(LAMBDA (f: integrable_fun): choose({F: [T -> real] |
                                          derivable?[T](F) AND deriv[T](F) = f}))")
            (("" (assert)
              (("" (skosimp*)
                (("" (expand "nonempty?")
                  (("" (expand "empty?")
                    (("" (assert)
                      (("" (typepred "f!1")
                        (("" (expand "integrable?")
                          (("" (skosimp*)
                            (("" (expand "antiderivative?")
                              ((""
                                (flatten)
                                ((""
                                  (inst - "F!1")
                                  (("" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((not_one_element formula-decl nil indefinite_integral nil)
    (member const-decl "bool" sets nil)
    (antiderivative? const-decl "bool" indefinite_integral nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (derivable? const-decl "bool" derivatives nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (integrable_fun type-eq-decl nil indefinite_integral nil)
    (integrable? const-decl "bool" indefinite_integral nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (connected_deriv_domain formula-decl nil deriv_domain_def 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]" indefinite_integral nil)
    (T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (connected_domain formula-decl nil indefinite_integral nil))
   nil)
  (integral_TCC1-1 nil 3393924105 ("" (existence-tcc) nil nil) nil
   nil))
(integral_lem 0
  (integral_lem-1 nil 3393926748
   ("" (skosimp*)
    (("" (lemma "antiderivative_lem")
      (("" (inst?)
        (("" (inst - "f!1")
          (("" (expand "antiderivative?") (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((antiderivative_lem formula-decl nil indefinite_integral nil)
    (antiderivative? const-decl "bool" indefinite_integral nil)
    (T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (T_pred const-decl "[real -> boolean]" indefinite_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))
(deriv_integ 0
  (deriv_integ-2 nil 3423992737
   ("" (skosimp*)
    (("" (expand "integrable?")
      (("" (expand "antiderivative?") (("" (inst + "F!1") nil nil))
        nil))
      nil))
    nil)
   ((integrable? const-decl "bool" indefinite_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]" indefinite_integral nil)
    (T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (antiderivative? const-decl "bool" indefinite_integral nil))
   nil)
  (deriv_integ-1 nil 3423992362
   ("" (skosimp*)
    (("" (expand "integrable?")
      (("" (expand "antiderivative?") (("" (inst + "F!1") nil nil))
        nil))
      nil))
    nil)
   nil nil))
(indef_integral_thm_TCC1 0
  (indef_integral_thm_TCC1-1 nil 3423992373 ("" (subtype-tcc) nil 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]" indefinite_integral nil)
    (T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (derivable? const-decl "bool" derivatives nil)
    (antiderivative? const-decl "bool" indefinite_integral nil)
    (integrable? const-decl "bool" indefinite_integral nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
(indef_integral_thm 0
  (indef_integral_thm-2 nil 3423992748
   ("" (skosimp*)
    (("" (lemma "integral_lem[T]")
      (("" (inst - "integral(deriv(F!1))" "F!1" "deriv(F!1)")
        (("1" (assert)
          (("1" (split -1)
            (("1" (propax) nil nil)
             ("2" (rewrite "deriv_integ") nil nil))
            nil))
          nil)
         ("2" (rewrite "deriv_integ") nil nil))
        nil))
      nil))
    nil)
   ((integral_lem formula-decl nil indefinite_integral nil)
    (deriv_integ formula-decl nil indefinite_integral nil)
    (integral const-decl
     "{F: [T -> real] | derivable?(F) AND deriv(F) = f}"
     indefinite_integral nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (integrable_fun type-eq-decl nil indefinite_integral nil)
    (integrable? const-decl "bool" indefinite_integral nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (deriv const-decl "[T -> real]" derivatives 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]" indefinite_integral nil)
    (T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (F!1 skolem-const-decl "[T -> real]" indefinite_integral nil))
   nil)
  (indef_integral_thm-1 nil 3423992321
   ("" (skosimp*)
    (("" (lemma "integral_lem[T]")
      (("" (inst - "integral(deriv(F!1))" "F!1" "deriv(F!1)")
        (("1" (assert)
          (("1" (split -1)
            (("1" (propax) nil nil)
             ("2" (rewrite "deriv_integ") nil nil))
            nil))
          nil)
         ("2" (rewrite "deriv_integ") nil nil))
        nil))
      nil))
    nil)
   ((deriv const-decl "[T -> real]" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil))
(fundamental_indef_TCC1 0
  (fundamental_indef_TCC1-2 nil 3393943321
   ("" (skosimp*) (("" (rewrite "cont_fun_integrable?") nil nil)) nil)
   ((cont_fun_integrable? formula-decl nil indefinite_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]" indefinite_integral nil)
    (T formal-nonempty-subtype-decl nil indefinite_integral nil))
   nil)
  (fundamental_indef_TCC1-1 nil 3393936480
   ("" (skosimp*) (("" (rewrite "cont_integrable?") nil nil)) nil) nil
   nil))
(fundamental_indef 0
  (fundamental_indef-1 nil 3393933020
   ("" (skosimp*)
    (("" (lemma "cont_Integrable?[T]")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "fundamental3")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-subtype-decl nil indefinite_integral nil)
    (T_pred const-decl "[real -> boolean]" indefinite_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)
    (cont_Integrable? formula-decl nil integral nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (integrable? const-decl "bool" indefinite_integral nil)
    (integrable_fun type-eq-decl nil indefinite_integral nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (integral const-decl
     "{F: [T -> real] | derivable?(F) AND deriv(F) = f}"
     indefinite_integral nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (fundamental3 formula-decl nil fundamental_theorem nil))
   nil)))

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.