Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 254 kB image not shown  

Quelle  integral_convergence_scaf.prf   Sprache: Lisp

 
(integral_convergence_scaf
 (monotone_convergence_scaf 0
  (monotone_convergence_scaf-1 nil 3409476910
   (""
    (case "FORALL (F: sequence[nn_integrable], f: [T -> nnreal]):
        pointwise_converges_upto?(F, f)&bounded?(nn_integral o F) =>(nn_integrable?(f) AND converges_upto?((nn_integral o F), nn_integral(f)))")
    (("1" (skosimp)
      (("1" (inst - "lambda (n:nat): F!1(n)-F!1(0)" "f!1-F!1(0)")
        (("1" (split -1)
          (("1" (flatten)
            (("1" (lemma "nn_integrable_is_integrable")
              (("1" (inst - "f!1 - F!1(0)")
                (("1"
                  (lemma "integrable_add"
                   ("f1" "f!1 - F!1(0)" "f2" "F!1(0)"))
                  (("1"
                    (case-replace "((+[T])(f!1 - F!1(0), F!1(0)))=f!1")
                    (("1" (hide -1)
                      (("1" (replace -1)
                        (("1" (expand "o ")
                          (("1" (expand "converges_upto?")
                            (("1" (flatten)
                              (("1"
                                (split)
                                (("1"
                                  (rewrite "integral_nn" -4 :dir rl)
                                  (("1"
                                    (rewrite "integral_diff")
                                    (("1"
                                      (rewrite
                                       "metric_convergence_def")
                                      (("1"
                                        (rewrite
                                         "metric_convergence_def")
                                        (("1"
                                          (expand
                                           "metric_converges_to")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (inst - "r!1")
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (inst + "n!1")
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (inst - "i!1")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (rewrite
                                                           "integral_nn"
                                                           -5
                                                           :dir
                                                           rl)
                                                          (("1"
                                                            (rewrite
                                                             "integral_diff")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (expand
                                                                 "ball")
                                                                (("1"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide 2)
                                          (("2"
                                            (skolem + ("n!1"))
                                            (("2"
                                              (lemma
                                               "integrable_diff"
                                               ("f1"
                                                "F!1(n!1)"
                                                "f2"
                                                "F!1(0)"))
                                              (("2"
                                                (lemma
                                                 "nn_integrable_is_nn_integrable"
                                                 ("f"
                                                  "(-[T])(F!1(n!1), F!1(0))"))
                                                (("2"
                                                  (case-replace
                                                   "(FORALL (x1: T): ((-[T])(F!1(n!1), F!1(0)))(x1) >= 0)")
                                                  (("2"
                                                    (expand
                                                     "pointwise_converges_upto?")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (hide-all-but
                                                         (1 -9))
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (expand
                                                             "-")
                                                            (("2"
                                                              (expand
                                                               "pointwise_increasing?")
                                                              (("2"
                                                                (inst
                                                                 -
                                                                 "x1!1")
                                                                (("2"
                                                                  (expand
                                                                   "increasing?")
                                                                  (("2"
                                                                    (inst
                                                                     -
                                                                     "0"
                                                                     "n!1")
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "increasing?")
                                  (("2"
                                    (skolem + ("i!1" "j!1"))
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (inst - "i!1" "j!1")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (hide -5 -8 -3 -4)
                                            (("2"
                                              (rewrite
                                               "integral_nn"
                                               -3
                                               :dir
                                               rl)
                                              (("2"
                                                (rewrite
                                                 "integral_nn"
                                                 -3
                                                 :dir
                                                 rl)
                                                (("2"
                                                  (rewrite
                                                   "integral_diff")
                                                  (("2"
                                                    (rewrite
                                                     "integral_diff")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide-all-but 1)
                      (("2" (apply-extensionality :hide? t)
                        (("2" (expand "+")
                          (("2" (expand "-") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (expand "pointwise_converges_upto?")
              (("2" (flatten)
                (("2" (split)
                  (("1" (expand "pointwise_convergence?")
                    (("1" (skosimp)
                      (("1" (inst - "x!1")
                        (("1" (rewrite "metric_convergence_def")
                          (("1" (rewrite "metric_convergence_def")
                            (("1" (expand "metric_converges_to")
                              (("1"
                                (skosimp)
                                (("1"
                                  (inst - "r!1")
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (inst + "n!1")
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (inst - "i!1")
                                          (("1"
                                            (expand "ball")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (expand "-")
                                                (("1"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "pointwise_increasing?")
                    (("2" (skosimp)
                      (("2" (inst - "x!1")
                        (("2" (expand "increasing?")
                          (("2" (skolem + ("i!1" "j!1"))
                            (("2" (flatten)
                              (("2"
                                (inst - "i!1" "j!1")
                                (("2"
                                  (expand "-")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (hide 2)
            (("3" (expand "o ")
              (("3" (expand "bounded?")
                (("3" (flatten)
                  (("3" (split)
                    (("1" (expand "bounded_above?")
                      (("1" (skosimp)
                        (("1" (expand "pointwise_converges_upto?")
                          (("1" (flatten)
                            (("1" (hide -1)
                              (("1"
                                (expand "bounded_below?")
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (inst + "a!1-a!2")
                                    (("1"
                                      (skolem + ("n!1"))
                                      (("1"
                                        (inst - "n!1")
                                        (("1"
                                          (inst - "0")
                                          (("1"
                                            (rewrite
                                             "integral_nn"
                                             1
                                             :dir
                                             rl)
                                            (("1"
                                              (rewrite "integral_diff")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "bounded_below?")
                      (("2" (skosimp)
                        (("2" (expand "bounded_above?")
                          (("2" (expand "pointwise_converges_upto?")
                            (("2" (flatten)
                              (("2"
                                (hide -1)
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (inst + "a!1-a!2")
                                    (("2"
                                      (skolem + ("n!1"))
                                      (("2"
                                        (inst - "0")
                                        (("2"
                                          (inst - "n!1")
                                          (("2"
                                            (rewrite
                                             "integral_nn"
                                             1
                                             :dir
                                             rl)
                                            (("2"
                                              (rewrite "integral_diff")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (skosimp)
            (("2" (expand "-")
              (("2" (expand "pointwise_converges_upto?")
                (("2" (expand "pointwise_increasing?")
                  (("2" (flatten)
                    (("2" (inst - "x1!1")
                      (("2" (hide -3)
                        (("2" (expand "pointwise_convergence?")
                          (("2" (inst - "x1!1")
                            (("2" (rewrite "metric_convergence_def")
                              (("2"
                                (expand "metric_converges_to")
                                (("2"
                                  (inst - "F!1(0)(x1!1)-f!1(x1!1)")
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (expand "ball")
                                      (("1"
                                        (expand "member")
                                        (("1"
                                          (inst - "n!1")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (expand "increasing?")
                                              (("1"
                                                (inst - "0" "n!1")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (hide 2)
          (("3" (skosimp)
            (("3" (split)
              (("1" (skosimp)
                (("1" (expand "pointwise_converges_upto?")
                  (("1" (flatten)
                    (("1" (expand "pointwise_increasing?")
                      (("1" (inst - "x1!1")
                        (("1" (expand "increasing?")
                          (("1" (inst - "0" "n!1")
                            (("1" (expand "-") (("1" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2"
                (lemma "integrable_diff"
                 ("f1" "F!1(n!1)" "f2" "F!1(0)"))
                (("2" (expand "pointwise_converges_upto?")
                  (("2" (flatten)
                    (("2" (rewrite "nn_integrable_is_nn_integrable")
                      (("2" (skosimp)
                        (("2" (expand "pointwise_increasing?")
                          (("2" (inst - "x!1")
                            (("2" (expand "-")
                              (("2"
                                (expand "increasing?")
                                (("2"
                                  (inst - "0" "n!1")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp)
        (("2" (lemma "pointwise_measurable" ("u" "F!1" "f" "f!1"))
          (("2" (split -1)
            (("1"
              (name "ISF"
                    "lambda (n:nat): choose({u:increasing_nn_isf | pointwise_convergence?(u,F!1(n))})")
              (("1" (hide -1)
                (("1"
                  (case "forall (n:nat): increasing_nn_isf?(ISF(n))")
                  (("1"
                    (case "forall (n:nat): pointwise_convergence?(ISF(n), F!1(n))")
                    (("1"
                      (name "G"
                            "lambda (n:nat): maximum(lambda (i:nat): ISF(i)(n),n)")
                      (("1"
                        (case "forall (n:nat,x:T): G(n)(x)<=F!1(n)(x)")
                        (("1"
                          (case "forall (n:nat, x: T): F!1(n)(x)<=f!1(x)")
                          (("1"
                            (case "forall (n:nat,x:T): 0 <= G(n)(x)")
                            (("1" (case "pointwise_increasing?(G)")
                              (("1"
                                (case
                                 "nonempty?({nn:nn_isf | exists (n:nat): nn = G(n)})")
                                (("1"
                                  (case "pointwise_bounded_above?(G)")
                                  (("1"
                                    (case
                                     "pointwise_converges_upto?(G, f!1)")
                                    (("1"
                                      (case-replace
                                       "nn_integrable?(f!1)")
                                      (("1"
                                        (expand "converges_upto?")
                                        (("1"
                                          (case-replace
                                           "increasing?(nn_integral o F!1)")
                                          (("1"
                                            (case
                                             "convergence?((nn_integral o G), nn_integral(f!1))")
                                            (("1"
                                              (expand
                                               "pointwise_converges_upto?")
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (rewrite
                                                   "metric_convergence_def")
                                                  (("1"
                                                    (rewrite
                                                     "metric_convergence_def")
                                                    (("1"
                                                      (case
                                                       "forall (n:nat): (nn_integral o G)(n)<=(nn_integral o F!1)(n)")
                                                      (("1"
                                                        (case
                                                         "increasing?(nn_integral o G)")
                                                        (("1"
                                                          (case
                                                           "forall (n:nat): (nn_integral o F!1)(n)<=nn_integral(f!1)")
                                                          (("1"
                                                            (name-replace
                                                             "LIMIT"
                                                             "nn_integral(f!1)")
                                                            (("1"
                                                              (name-replace
                                                               "INT_F"
                                                               "nn_integral o F!1")
                                                              (("1"
                                                                (name-replace
                                                                 "INT_G"
                                                                 "nn_integral o G")
                                                                (("1"
                                                                  (hide-all-but
                                                                   (-1
                                                                    -2
                                                                    -3
                                                                    -4
                                                                    -5
                                                                    1))
                                                                  (("1"
                                                                    (expand
                                                                     "metric_converges_to")
                                                                    (("1"
                                                                      (skosimp)
                                                                      (("1"
                                                                        (inst
                                                                         -4
                                                                         "r!1")
                                                                        (("1"
                                                                          (skosimp)
                                                                          (("1"
                                                                            (inst
                                                                             +
                                                                             "n!1")
                                                                            (("1"
                                                                              (skosimp)
                                                                              (("1"
                                                                                (inst
                                                                                 -4
                                                                                 "i!1")
                                                                                (("1"
                                                                                  (expand
                                                                                   "ball")
                                                                                  (("1"
                                                                                    (assert)
                                                                                    (("1"
                                                                                      (inst
                                                                                       -
                                                                                       "i!1")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "abs")
                                                                                        (("1"
                                                                                          (inst
                                                                                           -
                                                                                           "i!1")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (1
                                                              -5
                                                              -12))
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (expand
                                                                 "o ")
                                                                (("2"
                                                                  (lemma
                                                                   "nn_integrable_le"
                                                                   ("g"
                                                                    "F!1(n!1)"
                                                                    "f"
                                                                    "f!1"))
                                                                  (("2"
                                                                    (split
                                                                     -1)
                                                                    (("1"
                                                                      (flatten)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (skosimp)
                                                                      (("2"
                                                                        (inst
                                                                         -
                                                                         "n!1"
                                                                         "x!1")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide-all-but
                                                           (1 -6 -10))
                                                          (("2"
                                                            (expand
                                                             "pointwise_increasing?")
                                                            (("2"
                                                              (expand
                                                               "increasing?")
                                                              (("2"
                                                                (expand
                                                                 "o ")
                                                                (("2"
                                                                  (skolem
                                                                   +
                                                                   ("i!1"
                                                                    "j!1"))
                                                                  (("2"
                                                                    (flatten)
                                                                    (("2"
                                                                      (lemma
                                                                       "nn_integrable_le"
                                                                       ("g"
                                                                        "G(i!1)"
                                                                        "f"
                                                                        "G(j!1)"))
                                                                      (("2"
                                                                        (split
                                                                         -1)
                                                                        (("1"
                                                                          (flatten)
                                                                          nil
                                                                          nil)
                                                                         ("2"
                                                                          (hide
                                                                           2)
                                                                          (("2"
                                                                            (skosimp)
                                                                            (("2"
                                                                              (inst
                                                                               -
                                                                               "x!1")
                                                                              (("2"
                                                                                (inst
                                                                                 -
                                                                                 "i!1"
                                                                                 "j!1")
                                                                                (("2"
                                                                                  (inst
                                                                                   -
                                                                                   "i!1"
                                                                                   "x!1")
                                                                                  (("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide-all-but
                                                         (1 -9 -11))
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (expand
                                                             "o ")
                                                            (("2"
                                                              (lemma
                                                               "nn_integrable_le"
                                                               ("g"
                                                                "G(n!1)"
                                                                "f"
                                                                "F!1(n!1)"))
                                                              (("2"
                                                                (split
                                                                 -1)
                                                                (("1"
                                                                  (flatten)
                                                                  nil
                                                                  nil)
                                                                 ("2"
                                                                  (skosimp)
                                                                  (("2"
                                                                    (inst
                                                                     -
                                                                     "n!1"
                                                                     "x!1")
                                                                    (("2"
                                                                      (inst
                                                                       -
                                                                       "n!1"
                                                                       "x!1")
                                                                      (("2"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (expand
                                                 "pointwise_converges_upto?")
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (hide
                                                     -1
                                                     -14
                                                     -15
                                                     -16
                                                     -17
                                                     -11)
                                                    (("2"
                                                      (copy -1)
                                                      (("2"
                                                        (expand
                                                         "nn_integrable?"
                                                         -1)
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (lemma
                                                             "nn_convergence"
                                                             ("u1"
                                                              "u!1"
                                                              "f"
                                                              "f!1"
                                                              "u2"
                                                              "choose({u:increasing_nn_isf | pointwise_convergence?(u,f!1)})"))
                                                            (("1"
                                                              (replace
                                                               -2)
                                                              (("1"
                                                                (replace
                                                                 -3)
                                                                (("1"
                                                                  (split
                                                                   -1)
                                                                  (("1"
                                                                    (flatten)
                                                                    (("1"
                                                                      (expand
                                                                       "nn_integral"
                                                                       1
                                                                       2)
                                                                      (("1"
                                                                        (replace
                                                                         -2
                                                                         1
                                                                         rl)
                                                                        (("1"
                                                                          (hide
                                                                           -2)
                                                                          (("1"
                                                                            (hide
                                                                             -1)
                                                                            (("1"
                                                                              (lemma
                                                                               "nn_convergence"
                                                                               ("u1"
                                                                                "u!1"
                                                                                "f"
                                                                                "f!1"
                                                                                "u2"
                                                                                "G"))
                                                                              (("1"
                                                                                (replace
                                                                                 -2)
                                                                                (("1"
                                                                                  (replace
                                                                                   -3)
                                                                                  (("1"
                                                                                    (replace
                                                                                     -5)
                                                                                    (("1"
                                                                                      (flatten)
                                                                                      (("1"
                                                                                        (replace
                                                                                         -2)
                                                                                        (("1"
                                                                                          (expand
                                                                                           "o"
                                                                                           1
                                                                                           1)
                                                                                          (("1"
                                                                                            (case-replace
                                                                                             "(LAMBDA (x: nat): nn_integral(G(x)))=isf_integral o G")
                                                                                            (("1"
                                                                                              (rewrite
                                                                                               "hausdorff_convergence.limit_def"
                                                                                               1
                                                                                               :dir
                                                                                               rl)
                                                                                              nil
                                                                                              nil)
                                                                                             ("2"
                                                                                              (hide
                                                                                               2)
                                                                                              (("2"
                                                                                                (apply-extensionality
                                                                                                 :hide?
                                                                                                 t)
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "o"
                                                                                                   1)
                                                                                                  (("1"
                                                                                                    (rewrite
                                                                                                     "nn_integral_isf")
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "nn_isf?")
                                                                                                      (("1"
                                                                                                        (skosimp)
                                                                                                        (("1"
                                                                                                          (inst
                                                                                                           -11
                                                                                                           "x!1"
                                                                                                           "x!2")
                                                                                                          (("1"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (expand
                                                                                                   "o")
                                                                                                  (("2"
                                                                                                    (skolem
                                                                                                     +
                                                                                                     "n!1")
                                                                                                    (("2"
                                                                                                      (lemma
                                                                                                       "isf_integral_pos"
                                                                                                       ("i"
                                                                                                        "G(n!1)"))
                                                                                                      (("2"
                                                                                                        (assert)
                                                                                                        (("2"
                                                                                                          (skosimp)
                                                                                                          (("2"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "n!1"
                                                                                                             "x!1")
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("3"
                                                                                                  (skolem
                                                                                                   +
                                                                                                   "n!1")
                                                                                                  (("3"
                                                                                                    (split)
                                                                                                    (("1"
                                                                                                      (skosimp)
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         -
                                                                                                         "n!1"
                                                                                                         "x1!1")
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (lemma
                                                                                                       "nn_isf_is_nn_integrable"
                                                                                                       ("x"
                                                                                                        "G(n!1)"))
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil)
                                                                                                       ("2"
                                                                                                        (expand
                                                                                                         "nn_isf?")
                                                                                                        (("2"
                                                                                                          (skosimp)
                                                                                                          (("2"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "n!1"
                                                                                                             "x!1")
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
--> --------------------

--> maximum size reached

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

100%


¤ Dauer der Verarbeitung: 0.38 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.