Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: Lisp

Original von: PVS©

(integration_by_parts
 (IMP_fundamental_theorem_TCC1 0
  (IMP_fundamental_theorem_TCC1-1 nil 3603208137
   ("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
   ((connected_domain formula-decl nil integration_by_parts nil)) nil))
 (IMP_fundamental_theorem_TCC2 0
  (IMP_fundamental_theorem_TCC2-1 nil 3603208137
   ("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
   ((not_one_element formula-decl nil integration_by_parts nil)) nil))
 (integ_parts_prep_TCC1 0
  (integ_parts_prep_TCC1-1 nil 3603197586
   ("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
   ((deriv_domain formula-decl nil fundamental_theorem 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]" integration_by_parts nil)
    (T formal-nonempty-subtype-decl nil integration_by_parts nil))
   nil))
 (integ_parts_prep 0
  (integ_parts_prep-2 nil 3603197701
   ("" (skosimp*)
    (("" (name "F" "(LAMBDA (x: T): v!1(x) * deriv[T](u!1)(x))")
      (("" (replace -1)
        (("" (case "continuous?(F)")
          (("1" (lemma "cont_fun_Integrable?[T]")
            (("1" (inst?) (("1" (assertnil nil)) nil)
             ("2" (lemma "not_one_element") (("2" (propax) nil nil))
              nil)
             ("3" (lemma "connected_domain") (("3" (propax) nil nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (lemma "prod_fun_continuous[T]")
              (("2" (inst -1 "v!1" "deriv(u!1)")
                (("1" (expand "*") (("1" (assertnil nil)) nil)
                 ("2" (lemma "derivable_cont_fun[T]")
                  (("2" (inst?) (("2" (assertnil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv const-decl "[T -> real]" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (T formal-nonempty-subtype-decl nil integration_by_parts nil)
    (T_pred const-decl "[real -> boolean]" integration_by_parts 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (connected_domain formula-decl nil integration_by_parts nil)
    (not_one_element formula-decl nil integration_by_parts nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil)
    (connected? const-decl "bool" deriv_domain_def nil)
    (cont_fun_Integrable? formula-decl nil integral nil)
    (prod_fun_continuous judgement-tcc nil continuous_functions nil)
    (derivable_cont_fun formula-decl nil derivatives nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
    (v!1 skolem-const-decl "[T -> real]" integration_by_parts nil)
    (u!1 skolem-const-decl "[T -> real]" integration_by_parts nil))
   nil)
  (integ_parts_prep-1 nil 3603197589
   ("" (skosimp*)
    (("" (name "F" "(LAMBDA (x: T): u!1(x) * deriv[T](v!1)(x))")
      (("" (replace -1)
        (("" (case "continuous?(F)")
          (("1" (lemma "cont_fun_Integrable?[T]")
            (("1" (inst?) (("1" (assertnil)))
             ("2" (lemma "not_one_element") (("2" (propax) nil)))
             ("3" (lemma "connected_domain")
              (("3" (expand "connected?") (("3" (propax) nil)))))))
           ("2" (hide 2)
            (("2" (lemma "prod_fun_continuous[T]")
              (("2" (inst -1 "u!1" "deriv(v!1)")
                (("1" (expand "*") (("1" (assertnil)))
                 ("2" (lemma "derivable_cont_fun[T]")
                  (("2" (inst?) (("2" (assertnil))))))))))))))))))
    nil)
   nil nil))
 (integ_parts_TCC1 0
  (integ_parts_TCC1-1 nil 3393862614
   ("" (skosimp*)
    (("" (lemma "integ_parts_prep")
      (("" (inst?) (("" (assertnil nil)) nil)) nil))
    nil)
   ((integ_parts_prep formula-decl nil integration_by_parts nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (T formal-nonempty-subtype-decl nil integration_by_parts nil)
    (T_pred const-decl "[real -> boolean]" integration_by_parts 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))
 (integ_parts_TCC2 0
  (integ_parts_TCC2-1 nil 3393862614
   ("" (skosimp*)
    (("" (name "F" "(LAMBDA (x: T): v!1(x) * deriv[T](u!1)(x))")
      (("" (replace -1)
        (("" (case "continuous?(F)")
          (("1" (lemma "cont_fun_Integrable?[T]")
            (("1" (inst?) (("1" (assertnil nil)) nil)
             ("2" (lemma "not_one_element") (("2" (propax) nil nil))
              nil)
             ("3" (lemma "connected_domain")
              (("3" (hide 2)
                (("3" (expand "connected?") (("3" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (lemma "prod_fun_continuous[T]")
              (("2" (inst -1 "v!1" "deriv(u!1)")
                (("1" (expand "*") (("1" (assertnil nil)) nil)
                 ("2" (lemma "derivable_cont_fun[T]")
                  (("2" (inst?) (("2" (assertnil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv const-decl "[T -> real]" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (T formal-nonempty-subtype-decl nil integration_by_parts nil)
    (T_pred const-decl "[real -> boolean]" integration_by_parts 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (connected_domain formula-decl nil integration_by_parts nil)
    (not_one_element formula-decl nil integration_by_parts nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil)
    (connected? const-decl "bool" deriv_domain_def nil)
    (cont_fun_Integrable? formula-decl nil integral nil)
    (prod_fun_continuous judgement-tcc nil continuous_functions nil)
    (derivable_cont_fun formula-decl nil derivatives nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
    (v!1 skolem-const-decl "[T -> real]" integration_by_parts nil)
    (u!1 skolem-const-decl "[T -> real]" integration_by_parts nil))
   nil))
 (integ_parts 0
  (integ_parts-4 nil 3477655234
   ("" (skosimp*)
    (("" (lemma "deriv_prod_fun[T]")
      (("" (inst -1 "u!1" "v!1")
        (("" (lemma "prod_derivable_fun[T]")
          (("" (inst?)
            (("" (assert)
              (("" (assert)
                (("" (case "continuous?(deriv(u!1)*v!1)")
                  (("1" (case "continuous?(deriv(v!1)*u!1)")
                    (("1" (case "continuous?(deriv(u!1 * v!1))")
                      (("1"
                        (case "Integral(a!1,b!1,deriv(u!1 * v!1)) = Integral(a!1,b!1,deriv(u!1) * v!1 + deriv(v!1) * u!1)")
                        (("1" (lemma "fundamental3b")
                          (("1" (inst -1 "u!1 * v!1" "a!1" "b!1")
                            (("1" (assert)
                              (("1"
                                (flatten)
                                (("1"
                                  (replace -2)
                                  (("1"
                                    (hide -2)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (lemma "Integral_sum[T]")
                                        (("1"
                                          (inst
                                           -1
                                           "a!1"
                                           "b!1"
                                           "deriv(u!1) * v!1"
                                           "deriv(v!1) * u!1")
                                          (("1"
                                            (split -1)
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (case-replace
                                                 "(LAMBDA (x: T): (deriv(u!1) * v!1)(x) + (deriv(v!1) * u!1)(x)) = deriv(u!1) * v!1 + deriv(v!1) * u!1")
                                                (("1"
                                                  (replace -3)
                                                  (("1"
                                                    (hide -1 -3)
                                                    (("1"
                                                      (case-replace
                                                       "(LAMBDA (x_1: T): u!1(x_1) * deriv(v!1)(x_1)) = u!1 * deriv(v!1)")
                                                      (("1"
                                                        (case-replace
                                                         "(LAMBDA (x_2: T): v!1(x_2) * deriv(u!1)(x_2)) = v!1 * deriv(u!1)")
                                                        (("1"
                                                          (expand "*")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide 2)
                                                          (("2"
                                                            (expand
                                                             "*")
                                                            (("2"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide 2)
                                                        (("2"
                                                          (expand "*")
                                                          (("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (hide 2)
                                                    (("2"
                                                      (expand "*")
                                                      (("2"
                                                        (expand "+ ")
                                                        (("2"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (lemma
                                                 "cont_Integrable?[T]")
                                                (("2"
                                                  (inst?)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (hide 2)
                                              (("3"
                                                (lemma
                                                 "cont_Integrable?[T]")
                                                (("3"
                                                  (inst?)
                                                  (("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide 2) (("2" (assertnil nil)) nil)
                         ("3" (hide 2)
                          (("3" (lemma "cont_Integrable?[T]")
                            (("1" (inst?) (("1" (assertnil nil)) nil)
                             ("2" (lemma "not_one_element")
                              (("2" (propax) nil nil)) nil)
                             ("3" (assert)
                              (("3"
                                (lemma "connected_domain")
                                (("3" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("4" (lemma "not_one_element")
                          (("4" (propax) nil nil)) nil)
                         ("5" (lemma "connected_domain")
                          (("5" (propax) nil nil)) nil)
                         ("6" (hide 2)
                          (("6" (lemma "cont_Integrable?[T]")
                            (("1" (inst?) (("1" (assertnil nil)) nil)
                             ("2" (lemma "not_one_element")
                              (("2" (propax) nil nil)) nil)
                             ("3" (lemma "connected_domain")
                              (("3" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide 2)
                        (("2" (lemma "sum_cont_fun[T]")
                          (("2" (inst?) (("2" (assertnil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (lemma "prod_cont_fun[T]")
                        (("2" (inst?)
                          (("2" (assert)
                            (("2" (lemma "derivable_cont[T]")
                              (("2" (inst?) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (lemma "prod_cont_fun[T]")
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (lemma "derivable_cont[T]")
                            (("2" (inst?) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-subtype-decl nil integration_by_parts nil)
    (T_pred const-decl "[real -> boolean]" integration_by_parts 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)
    (deriv_prod_fun formula-decl nil derivatives nil)
    (prod_derivable_fun formula-decl nil derivatives nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv const-decl "[T -> real]" derivatives nil)
    (derivable_cont judgement-tcc nil derivatives nil)
    (prod_cont_fun formula-decl nil continuous_functions nil)
    (connected_domain formula-decl nil integration_by_parts nil)
    (not_one_element formula-decl nil integration_by_parts nil)
    (fundamental3b formula-decl nil fundamental_theorem nil)
    (cont_Integrable? formula-decl nil integral nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Integral_sum formula-decl nil integral nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil)
    (connected? const-decl "bool" deriv_domain_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Integrable? const-decl "bool" integral_def nil)
    (Integrable_funs type-eq-decl nil integral_def nil)
    (Integral const-decl "real" integral_def nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (sum_cont_fun formula-decl nil continuous_functions nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil))
   nil)
  (integ_parts-3 nil 3445337156
   (";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
    (skosimp*)
    ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
      (lemma "deriv_prod_fun[T]")
      ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
        (inst -1 "u!1" "v!1")
        ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
          (lemma "prod_derivable_fun[T]")
          ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
            (inst?)
            ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
              (assert)
              ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                (lemma "derivable_cont_fun")
                ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                  (inst - "u!1*v!1")
                  ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                    (assert)
                    ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                      (lemma "derivable_cont_fun")
                      ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                        (inst - "u!1")
                        ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                          (assert)
                          ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                            (lemma "derivable_cont_fun")
                            ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                              (inst - "v!1")
                              ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                                (assert)
                                ((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
                                  (case "continuous?(deriv(u!1)*v!1)")
                                  (("1"
                                    (case
                                     "continuous?(deriv(v!1)*u!1)")
                                    (("1"
                                      (case
                                       "continuous?(deriv(u!1 * v!1))")
                                      (("1"
                                        (case
                                         "Integral(a!1,b!1,deriv(u!1 * v!1)) = Integral(a!1,b!1,deriv(u!1) * v!1 + deriv(v!1) * u!1)")
                                        (("1"
                                          (lemma "fundamental3b")
                                          (("1"
                                            (inst
                                             -1
                                             "u!1 * v!1"
                                             "a!1"
                                             "b!1")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (replace -2)
                                                  (("1"
                                                    (hide -2)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (lemma
                                                         "Integral_sum[T]")
                                                        (("1"
                                                          (inst
                                                           -1
                                                           "a!1"
                                                           "b!1"
                                                           "deriv(u!1) * v!1"
                                                           "deriv(v!1) * u!1")
                                                          (("1"
                                                            (split -1)
                                                            (("1"
                                                              (flatten)
                                                              (("1"
                                                                (case-replace
                                                                 "(LAMBDA (x: T): (deriv(u!1) * v!1)(x) + (deriv(v!1) * u!1)(x)) = deriv(u!1) * v!1 + deriv(v!1) * u!1")
                                                                (("1"
                                                                  (replace
                                                                   -3)
                                                                  (("1"
                                                                    (hide
                                                                     -1
                                                                     -3)
                                                                    (("1"
                                                                      (case-replace
                                                                       "(LAMBDA (x_1: T): u!1(x_1) * deriv(v!1)(x_1)) = u!1 * deriv(v!1)")
                                                                      (("1"
                                                                        (case-replace
                                                                         "(LAMBDA (x_2: T): v!1(x_2) * deriv(u!1)(x_2)) = v!1 * deriv(u!1)")
                                                                        (("1"
                                                                          (expand
                                                                           "*")
                                                                          (("1"
                                                                            (assert)
                                                                            nil)))
                                                                         ("2"
                                                                          (hide
                                                                           2)
                                                                          (("2"
                                                                            (expand
                                                                             "*")
                                                                            (("2"
                                                                              (propax)
                                                                              nil)))))))
                                                                       ("2"
                                                                        (hide
                                                                         2)
                                                                        (("2"
                                                                          (expand
                                                                           "*")
                                                                          (("2"
                                                                            (propax)
                                                                            nil)))))))))))
                                                                 ("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (expand
                                                                       "*")
                                                                      (("2"
                                                                        (expand
                                                                         "+ ")
                                                                        (("2"
                                                                          (propax)
                                                                          nil)))))))))))))
                                                             ("2"
                                                              (hide 2)
                                                              (("2"
                                                                (lemma
                                                                 "cont_Integrable?[T]")
                                                                (("2"
                                                                  (inst?)
                                                                  (("2"
                                                                    (assert)
                                                                    nil)))))))
                                                             ("3"
                                                              (hide 2)
                                                              (("3"
                                                                (lemma
                                                                 "cont_Integrable?[T]")
                                                                (("3"
                                                                  (inst?)
                                                                  (("3"
                                                                    (assert)
                                                                    nil)))))))))))))))))))))))))))
                                         ("2"
                                          (hide 2)
                                          (("2" (assertnil)))
                                         ("3"
                                          (hide 2)
                                          (("3"
                                            (lemma
                                             "cont_Integrable?[T]")
                                            (("1"
                                              (inst?)
                                              (("1" (assertnil)))
                                             ("2"
                                              (lemma "not_one_element")
                                              (("2" (propax) nil)))
                                             ("3"
                                              (assert)
                                              (("3"
                                                (lemma
                                                 "connected_domain")
                                                (("3"
                                                  (propax)
                                                  nil)))))))))
                                         ("4"
                                          (lemma "not_one_element")
                                          (("4" (propax) nil)))
                                         ("5"
                                          (lemma "connected_domain")
                                          (("5" (propax) nil)))
                                         ("6"
                                          (hide 2)
                                          (("6"
                                            (lemma
                                             "cont_Integrable?[T]")
                                            (("1"
                                              (inst?)
                                              (("1" (assertnil)))
                                             ("2"
                                              (lemma "not_one_element")
                                              (("2" (propax) nil)))
                                             ("3"
                                              (lemma
                                               "connected_domain")
                                              (("3"
                                                (propax)
                                                nil)))))))))
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (replace -7)
                                          (("2"
                                            (lemma "sum_cont_fun[T]")
                                            (("2"
                                              (inst?)
                                              (("2"
                                                (assert)
                                                nil)))))))))))
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (lemma "prod_cont_fun[T]")
                                        (("2"
                                          (inst?)
                                          (("2" (assertnil)))))))))
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (lemma "prod_cont_fun[T]")
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (assert)
                                          nil))))))))))))))))))))))))))))))))))))))
    ";;; developed with shostak decision procedures")
   nil nil)
  (integ_parts-2 nil 3393933493
   ("" (skosimp*)
    (("" (lemma "deriv_prod_fun[T]")
      (("" (inst -1 "u!1" "v!1")
        (("" (lemma "prod_derivable_fun[T]")
          (("" (inst?)
            (("" (assert)
              (("" (lemma "derivable_cont_fun")
                (("" (inst - "u!1*v!1")
                  (("" (assert)
                    (("" (lemma "derivable_cont_fun")
                      (("" (inst - "u!1")
                        (("" (assert)
                          (("" (lemma "derivable_cont_fun")
                            (("" (inst - "v!1")
                              ((""
                                (assert)
                                ((""
                                  (case "continuous?(deriv(u!1)*v!1)")
                                  (("1"
                                    (case
                                     "continuous?(deriv(v!1)*u!1)")
                                    (("1"
                                      (case "(deriv(u!1 * v!1))")
                                      (("1"
                                        (case
                                         "Integral(a!1,b!1,deriv(u!1 * v!1)) = Integral(a!1,b!1,deriv(u!1) * v!1 + deriv(v!1) * u!1)")
                                        (("1"
                                          (lemma "fundamental3b")
                                          (("1"
                                            (inst
                                             -1
                                             "u!1 * v!1"
                                             "a!1"
                                             "b!1")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (replace -2)
                                                  (("1"
                                                    (hide -2)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (lemma
                                                         "Integral_sum[T]")
                                                        (("1"
                                                          (inst
                                                           -1
                                                           "a!1"
                                                           "b!1"
                                                           "deriv(u!1) * v!1"
                                                           "deriv(v!1) * u!1")
                                                          (("1"
                                                            (split -1)
                                                            (("1"
                                                              (flatten)
                                                              (("1"
                                                                (case-replace
                                                                 "(LAMBDA (x: T): (deriv(u!1) * v!1)(x) + (deriv(v!1) * u!1)(x)) = deriv(u!1) * v!1 + deriv(v!1) * u!1")
                                                                (("1"
                                                                  (replace
                                                                   -3)
                                                                  (("1"
                                                                    (hide
                                                                     -1
                                                                     -3)
                                                                    (("1"
                                                                      (case-replace
                                                                       "(LAMBDA (x_1: T): u!1(x_1) * deriv(v!1)(x_1)) = u!1 * deriv(v!1)")
                                                                      (("1"
                                                                        (case-replace
                                                                         "(LAMBDA (x_2: T): v!1(x_2) * deriv(u!1)(x_2)) = v!1 * deriv(u!1)")
                                                                        (("1"
                                                                          (expand
                                                                           "*")
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide
                                                                           2)
                                                                          (("2"
                                                                            (expand
                                                                             "*")
                                                                            (("2"
                                                                              (propax)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide
                                                                         2)
                                                                        (("2"
                                                                          (expand
                                                                           "*")
                                                                          (("2"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (expand
                                                                       "*")
                                                                      (("2"
                                                                        (expand
                                                                         "+ ")
                                                                        (("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (hide 2)
                                                              (("2"
                                                                (lemma
                                                                 "cont_Integrable?[T]")
                                                                (("2"
                                                                  (inst?)
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("3"
                                                              (hide 2)
                                                              (("3"
                                                                (lemma
                                                                 "cont_Integrable?[T]")
                                                                (("3"
                                                                  (inst?)
                                                                  (("3"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide 2)
                                          (("2" (assertnil nil))
                                          nil)
                                         ("3"
                                          (hide 2)
                                          (("3"
                                            (lemma
                                             "cont_Integrable?[T]")
                                            (("1"
                                              (inst?)
                                              (("1" (assertnil nil))
                                              nil)
                                             ("2"
                                              (lemma "not_one_element")
                                              (("2" (propax) nil nil))
                                              nil)
                                             ("3"
                                              (assert)
                                              (("3"
                                                (lemma
                                                 "connected_domain")
                                                (("3"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("4"
                                          (lemma "not_one_element")
                                          (("4" (propax) nil nil))
                                          nil)
                                         ("5"
                                          (lemma "connected_domain")
                                          (("5" (propax) nil nil))
                                          nil)
                                         ("6"
                                          (hide 2)
                                          (("6"
                                            (lemma
                                             "cont_Integrable?[T]")
                                            (("1"
                                              (inst?)
                                              (("1" (assertnil nil))
                                              nil)
                                             ("2"
                                              (lemma "not_one_element")
                                              (("2" (propax) nil nil))
                                              nil)
                                             ("3"
                                              (lemma
                                               "connected_domain")
                                              (("3" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (replace -7)
                                          (("2"
                                            (lemma "sum_cont_fun[T]")
                                            (("2"
                                              (inst?)
                                              (("2" (assertnil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (lemma "prod_cont_fun[T]")
                                        (("2"
                                          (inst?)
                                          (("2" (assertnil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (lemma "prod_cont_fun[T]")
                                      (("2"
                                        (inst?)
                                        (("2" (assertnil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_prod_fun formula-decl nil derivatives nil)
    (prod_derivable_fun formula-decl nil derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (prod_cont_fun formula-decl nil continuous_functions nil)
    (fundamental3b formula-decl nil fundamental_theorem nil)
    (cont_Integrable? formula-decl nil integral nil)
    (Integral_sum formula-decl nil integral nil)
    (Integrable? const-decl "bool" integral_def nil)
    (Integrable_funs type-eq-decl nil integral_def nil)
    (Integral const-decl "real" integral_def nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (sum_cont_fun formula-decl nil continuous_functions nil)
    (derivable_cont_fun formula-decl nil derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil)
  (integ_parts-1 nil 3393863589
   ("" (skosimp*)
    (("" (lemma "deriv_prod_fun[T]")
      (("" (inst -1 "u!1" "v!1")
        ((""
          (case "Integral(a!1,b!1,deriv(u!1 * v!1)) = Integral(a!1,b!1,deriv(u!1) * v!1 + deriv(v!1) * u!1)")
          (("1" (hide -2)
            (("1" (lemma "fundamental5")
              (("1" (inst -1 "u!1 * v!1" "a!1" "b!1")
                (("1" (assert)
                  (("1" (split -1)
                    (("1" (flatten)
                      (("1" (replace -2)
                        (("1" (hide -2)
                          (("1" (lemma "Integral_sum[T]")
                            (("1"
                              (inst -1 "a!1" "b!1" "deriv(u!1) * v!1"
                               "deriv(v!1) * u!1")
                              (("1"
                                (split -1)
                                (("1"
                                  (flatten)
                                  (("1"
                                    (case-replace
                                     "(LAMBDA (x: T): (deriv(u!1) * v!1)(x) + (deriv(v!1) * u!1)(x)) = deriv(u!1) * v!1 + deriv(v!1) * u!1")
                                    (("1"
                                      (replace -3)
                                      (("1"
                                        (hide -1 -3)
                                        (("1"
                                          (case-replace
                                           "(LAMBDA (x_1: T): u!1(x_1) * deriv(v!1)(x_1)) = u!1 * deriv(v!1)")
                                          (("1"
                                            (case-replace
                                             "(LAMBDA (x_2: T): v!1(x_2) * deriv(u!1)(x_2)) = v!1 * deriv(u!1)")
                                            (("1"
                                              (expand "*")
                                              (("1" (assertnil nil))
                                              nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (expand "*")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 2)
                                            (("2"
                                              (expand "*")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (hide 2)
                                        (("2"
                                          (expand "*")
                                          (("2"
                                            (expand "+ ")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (lemma "derivable_cont_fun[T]")
                                    (("2"
                                      (inst -1 "v!1")
                                      (("2"
                                        (assert)
                                        (("2" (postpone) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (hide 2)
                                  (("3" (postpone) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (lemma "prod_derivable_fun")
                        (("2" (inst?) (("2" (assertnil nil)) nil))
                        nil))
                      nil)
                     ("3" (hide 2) (("3" (postpone) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2) (("2" (assertnil nil)) nil)
           ("3" (hide 2) (("3" (postpone) nil nil)) nil)
           ("4" (lemma "not_one_element") (("4" (propax) nil nil)) nil)
           ("5" (lemma "connected_domain") (("5" (propax) nil nil))
            nil)
           ("6" (hide 2) (("6" (postpone) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.152Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik