products/sources/formale sprachen/PVS/analysis/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: lim_of_composition.pvs   Sprache: Lisp

Original von: PVS©
(integral_diff_doms
 (int_diff_dom_TCC1 0
  (int_diff_dom_TCC1-1 nil 3319997019
   ("" (skosimp*)
    (("" (lemma "connected_domain")
      (("" (inst - "x!1" "y!1" "z!1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((connected_domain formula-decl nil integral_diff_doms nil)) nil))
 (int_diff_dom_TCC2 0
  (int_diff_dom_TCC2-1 nil 3319997019
   ("" (lemma "not_one_element") (("" (skosimp*) nil nil)) nil)
   ((not_one_element formula-decl nil integral_diff_doms nil)) nil))
 (int_diff_dom_TCC3 0
  (int_diff_dom_TCC3-1 nil 3319997019
   ("" (lemma "con_dom_U") (("" (skosimp*) nil nil)) nil)
   ((con_dom_U formula-decl nil integral_diff_doms nil)) nil))
 (int_diff_dom_TCC4 0
  (int_diff_dom_TCC4-1 nil 3319997019
   ("" (lemma "not_one_U ") (("" (skosimp*) nil nil)) nil)
   ((not_one_U formula-decl nil integral_diff_doms nil)) nil))
 (int_diff_dom_TCC5 0
  (int_diff_dom_TCC5-1 nil 3319997019
   ("" (lemma "connected_domain")
    (("" (expand "connected?")
      (("" (skosimp*)
        (("" (inst - "a!1" "b!1" "x!1") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((connected? const-decl "bool" deriv_domain_def nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" integral_diff_doms nil)
    (T formal-nonempty-subtype-decl nil integral_diff_doms nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected_domain formula-decl nil integral_diff_doms nil))
   nil))
 (int_diff_dom_TCC6 0
  (int_diff_dom_TCC6-1 nil 3319997019
   ("" (lemma "con_dom_U")
    (("" (expand "connected?")
      (("" (skosimp*)
        (("" (inst - "a!1" "b!1" "x!1") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((connected? const-decl "bool" deriv_domain_def nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (U_pred const-decl "[real -> boolean]" integral_diff_doms nil)
    (U formal-nonempty-subtype-decl nil integral_diff_doms nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (con_dom_U formula-decl nil integral_diff_doms nil))
   nil))
 (int_diff_dom 0
  (int_diff_dom-2 nil 3477655792
   ("" (skosimp*)
    (("" (expand "integrable?")
      (("" (skosimp*)
        (("" (lemma "integral_def[T]")
          (("1" (inst?)
            (("1" (assert)
              (("1" (hide 2)
                (("1" (case-replace "integral(a!1, b!1, g!1) = S!2")
                  (("1" (expand "integral?")
                    (("1" (hide -1)
                      (("1" (skosimp*)
                        (("1" (inst -7 "epsi!1")
                          (("1" (skosimp*)
                            (("1" (inst + "delta!1")
                              (("1"
                                (skosimp*)
                                (("1"
                                  (typepred "P!1")
                                  (("1"
                                    (inst -12 "P!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (split -12)
                                        (("1"
                                          (inst -1 "R!1")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (typepred "R!1")
                                              (("1"
                                                (hide 2)
                                                (("1"
                                                  (expand
                                                   "Riemann_sum?")
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (inst + "xis!1")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (replace -1)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (expand
                                                               "Rie_sum")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (rewrite
                                                                   "sigma_restrict_eq")
                                                                  (("1"
                                                                    (rewrite
                                                                     "sigma_restrict_eq")
                                                                    (("1"
                                                                      (hide
                                                                       2)
                                                                      (("1"
                                                                        (expand
                                                                         "restrict")
                                                                        (("1"
                                                                          (hide
                                                                           2)
                                                                          (("1"
                                                                            (apply-extensionality
                                                                             1
                                                                             :hide?
                                                                             t)
                                                                            (("1"
                                                                              (hide
                                                                               -4
                                                                               -11)
                                                                              (("1"
                                                                                (inst?)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "finseq_appl")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (skosimp*)
                                                                              (("2"
                                                                                (hide
                                                                                 -11
                                                                                 -12)
                                                                                (("2"
                                                                                  (typepred
                                                                                   "xis!1")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "xis?")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (inst
                                                                                         -
                                                                                         "i!1")
                                                                                        (("2"
                                                                                          (flatten)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (lemma
                                                                                               "con_dom_U")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "connected?")
                                                                                                (("2"
                                                                                                  (inst
                                                                                                   -
                                                                                                   "a!1"
                                                                                                   "b!1"
                                                                                                   "xis!1(i!1)")
                                                                                                  (("2"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("3"
                                                                              (skosimp*)
                                                                              (("3"
                                                                                (assert)
                                                                                (("3"
                                                                                  (typepred
                                                                                   "P!1`seq(x1!1)")
                                                                                  (("3"
                                                                                    (lemma
                                                                                     "con_dom_U")
                                                                                    (("3"
                                                                                      (expand
                                                                                       "connected?")
                                                                                      (("3"
                                                                                        (inst
                                                                                         -
                                                                                         "a!1"
                                                                                         "b!1"
                                                                                         "P!1`seq(x1!1)")
                                                                                        (("3"
                                                                                          (assert)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       -11
                                                                       -12
                                                                       2)
                                                                      (("2"
                                                                        (skosimp*)
                                                                        (("2"
                                                                          (lemma
                                                                           "con_dom_U")
                                                                          (("2"
                                                                            (expand
                                                                             "connected?")
                                                                            (("2"
                                                                              (inst
                                                                               -
                                                                               "a!1"
                                                                               "b!1"
                                                                               "xis!1(n!1)")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("3"
                                                                      (hide
                                                                       2)
                                                                      (("3"
                                                                        (skosimp*)
                                                                        (("3"
                                                                          (assert)
                                                                          (("3"
                                                                            (assert)
                                                                            (("3"
                                                                              (hide
                                                                               2)
                                                                              (("3"
                                                                                (lemma
                                                                                 "con_dom_U")
                                                                                (("3"
                                                                                  (expand
                                                                                   "connected?")
                                                                                  (("3"
                                                                                    (inst
                                                                                     -
                                                                                     "a!1"
                                                                                     "b!1"
                                                                                     "P!1`seq(x1!1)")
                                                                                    (("3"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("4"
                                                                      (hide
                                                                       2
                                                                       3)
                                                                      (("4"
                                                                        (skosimp*)
                                                                        (("4"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     -11
                                                                     -12
                                                                     2)
                                                                    (("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (lemma
                                                                         "con_dom_U")
                                                                        (("2"
                                                                          (assert)
                                                                          (("2"
                                                                            (expand
                                                                             "connected?")
                                                                            (("2"
                                                                              (inst
                                                                               -
                                                                               "a!1"
                                                                               "b!1"
                                                                               "xis!1(n!1)")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("3"
                                                                    (hide
                                                                     2)
                                                                    (("3"
                                                                      (skosimp*)
                                                                      (("3"
                                                                        (assert)
                                                                        (("3"
                                                                          (lemma
                                                                           "con_dom_U")
                                                                          (("3"
                                                                            (expand
                                                                             "connected?")
                                                                            (("3"
                                                                              (inst
                                                                               -
                                                                               "a!1"
                                                                               "b!1"
                                                                               "P!1`seq(x1!1)")
                                                                              (("3"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("4"
                                                                    (skosimp*)
                                                                    (("4"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (prop)
                                                        (("1"
                                                          (skosimp*)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lemma
                                                               "con_dom_U")
                                                              (("1"
                                                                (expand
                                                                 "connected?")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "a!1"
                                                                   "b!1"
                                                                   "xis!1(x1!1)")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (typepred
                                                           "xis!1")
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (expand
                                                               "xis?")
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (skosimp*)
                                                                  (("2"
                                                                    (expand
                                                                     "finseq_appl")
                                                                    (("2"
                                                                      (inst?)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (expand "width")
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (prop)
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (lemma "parts_order[T]")
                                          (("2"
                                            (inst
                                             -
                                             "a!1"
                                             "b!1"
                                             "P!1"
                                             "0"
                                             "x1!1")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (case-replace
                                                 "x1!1 = 0")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (lemma "con_dom_U")
                                                    (("2"
                                                      (expand
                                                       "connected?")
                                                      (("2"
                                                        (inst
                                                         -
                                                         "a!1"
                                                         "b!1"
                                                         "P!1`seq(x1!1)")
                                                        (("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" (lemma "integral_def[U]")
                      (("1" (inst?) (("1" (assert) nil nil)) nil)
                       ("2" (lemma "not_one_U")
                        (("2" (propax) nil nil)) nil)
                       ("3" (lemma "con_dom_U")
                        (("3" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("3" (lemma "not_one_U") (("3" (propax) nil nil))
                    nil)
                   ("4" (lemma "con_dom_U") (("4" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (lemma "not_one_element")
              (("2" (lemma "connected_domain")
                (("2" (lemma "not_one_U") (("2" (propax) nil nil))
                  nil))
                nil))
              nil)
             ("3" (lemma "con_dom_U") (("3" (propax) nil nil)) nil))
            nil)
           ("2" (lemma "connected_domain")
            (("2" (lemma "not_one_element") (("2" (propax) nil nil))
              nil))
            nil)
           ("3" (lemma "connected_domain") (("3" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((integrable? const-decl "bool" integral_def nil)
    (T formal-nonempty-subtype-decl nil integral_diff_doms nil)
    (T_pred const-decl "[real -> boolean]" integral_diff_doms nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (integral_def formula-decl nil integral_def nil)
    (connected? const-decl "bool" deriv_domain_def nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (not_one_element formula-decl nil integral_diff_doms nil)
    (connected_domain formula-decl nil integral_diff_doms nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (partition type-eq-decl nil integral_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (parts_order formula-decl nil integral_def nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (width const-decl "posreal" integral_def nil)
    (Riemann_sum? const-decl "bool" integral_def nil)
    (g!1 skolem-const-decl "[U -> real]" integral_diff_doms nil)
    (f!1 skolem-const-decl "[T -> real]" integral_diff_doms nil)
    (R!1 skolem-const-decl "(Riemann_sum?(a!1, b!1, P!1, f!1))"
     integral_diff_doms nil)
    (xis? const-decl "bool" integral_def nil)
    (xis!1 skolem-const-decl "(xis?(a!1, b!1, P!1))" integral_diff_doms
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Rie_sum const-decl "real" integral_def nil)
    (integer nonempty-type-from-decl nil integers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T_low type-eq-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sigma_restrict_eq formula-decl nil sigma "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (con_dom_U formula-decl nil integral_diff_doms nil)
    (restrict const-decl "[T -> real]" sigma "reals/")
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_diff_doms
     nil)
    (b!1 skolem-const-decl "real" integral_diff_doms nil)
    (a!1 skolem-const-decl "real" integral_diff_doms nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (not_one_U formula-decl nil integral_diff_doms nil)
    (integral const-decl "{S: real | integral?(a, b, ff, S)}"
     integral_def nil)
    (integral? const-decl "bool" integral_def nil)
    (< const-decl "bool" reals nil)
    (U_pred const-decl "[real -> boolean]" integral_diff_doms nil)
    (U formal-nonempty-subtype-decl nil integral_diff_doms nil))
   nil)
  (int_diff_dom-1 nil 3321116320
   ("" (skosimp*)
    (("" (expand "integrable?")
      (("" (skosimp*)
        (("" (lemma "integral_def[T]")
          (("1" (inst?)
            (("1" (assert)
              (("1" (hide 2)
                (("1" (case-replace "integral(a!1, b!1, g!1) = S!2")
                  (("1" (expand "integral?")
                    (("1" (hide -1)
                      (("1" (skosimp*)
                        (("1" (inst -7 "epsi!1")
                          (("1" (skosimp*)
                            (("1" (inst + "delta!1")
                              (("1"
                                (skosimp*)
                                (("1"
                                  (typepred "P!1")
                                  (("1"
                                    (inst -12 "P!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (split -12)
                                        (("1"
                                          (inst -1 "R!1")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (typepred "R!1")
                                              (("1"
                                                (hide 2)
                                                (("1"
                                                  (expand
                                                   "Riemann_sum?")
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (inst + "xis!1")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (replace -1)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (expand
                                                               "Rie_sum")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (rewrite
                                                                   "sigma_restrict_eq")
                                                                  (("1"
                                                                    (hide
                                                                     2)
                                                                    (("1"
                                                                      (expand
                                                                       "restrict")
                                                                      (("1"
                                                                        (apply-extensionality
                                                                         1
                                                                         :hide?
                                                                         t)
                                                                        (("1"
                                                                          (hide
                                                                           -4
                                                                           -11)
                                                                          (("1"
                                                                            (inst?)
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (skosimp*)
                                                                          (("2"
                                                                            (hide
                                                                             -11
                                                                             -12)
                                                                            (("2"
                                                                              (typepred
                                                                               "xis!1")
                                                                              (("2"
                                                                                (expand
                                                                                 "xis?")
                                                                                (("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (inst
                                                                                     -
                                                                                     "i!1")
                                                                                    (("2"
                                                                                      (flatten)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        (("2"
                                                                                          (lemma
                                                                                           "con_dom_U")
                                                                                          (("2"
                                                                                            (inst
                                                                                             -
                                                                                             "a!1"
                                                                                             "b!1"
                                                                                             "xis!1(i!1)")
                                                                                            (("2"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     -11
                                                                     -12
                                                                     2)
                                                                    (("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (lemma
                                                                         "con_dom_U")
                                                                        (("2"
                                                                          (inst
                                                                           -
                                                                           "a!1"
                                                                           "b!1"
                                                                           "xis!1(n!1)")
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("3"
                                                                    (hide
                                                                     2)
                                                                    (("3"
                                                                      (skosimp*)
                                                                      (("3"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("4"
                                                                    (skosimp*)
                                                                    (("4"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil)
                                                                   ("5"
                                                                    (skosimp*)
                                                                    (("5"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (skosimp*)
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (prop)
                                                        (("1"
                                                          (skosimp*)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lemma
                                                               "con_dom_U")
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "a!1"
                                                                 "b!1"
                                                                 "xis!1(x1!1)")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (skosimp*)
                                                          (("2"
                                                            (typepred
                                                             "xis!1")
                                                            (("2"
                                                              (expand
                                                               "xis?")
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (inst?)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (expand "width")
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (prop)
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (lemma "parts_order[T]")
                                          (("2"
                                            (inst
                                             -
                                             "a!1"
                                             "b!1"
                                             "P!1"
                                             "0"
                                             "x1!1")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (case-replace
                                                 "x1!1 = 0")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (lemma "con_dom_U")
                                                    (("2"
                                                      (inst
                                                       -
                                                       "a!1"
                                                       "b!1"
                                                       "P!1`seq(x1!1)")
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (lemma "integral_def[U]")
                      (("1" (inst?) (("1" (assert) nil nil)) nil)
                       ("2" (lemma "not_one_U")
                        (("2" (propax) nil nil)) nil)
                       ("3" (lemma "con_dom_U")
                        (("3" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("3" (lemma "not_one_U") (("3" (propax) nil nil))
                    nil)
                   ("4" (lemma "con_dom_U") (("4" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (lemma "not_one_element")
              (("2" (lemma "connected_domain")
                (("2" (lemma "not_one_U") (("2" (propax) nil nil))
                  nil))
                nil))
              nil)
             ("3" (lemma "con_dom_U") (("3" (propax) nil nil)) nil))
            nil)
           ("2" (lemma "connected_domain")
            (("2" (lemma "not_one_element") (("2" (propax) nil nil))
              nil))
            nil)
           ("3" (lemma "connected_domain") (("3" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((integral? const-decl "bool" integral_def nil)
    (integral const-decl "{S: real | integral?(a, b, ff, S)}"
     integral_def nil)
    (restrict const-decl "[T -> real]" sigma "reals/")
    (sigma_restrict_eq formula-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (Rie_sum const-decl "real" integral_def nil)
    (xis? const-decl "bool" integral_def nil)
    (Riemann_sum? const-decl "bool" integral_def nil)
    (width const-decl "posreal" integral_def nil)
    (parts_order formula-decl nil integral_def nil)
    (partition type-eq-decl nil integral_def nil)
    (integral_def formula-decl nil integral_def nil)
    (integrable? const-decl "bool" integral_def nil))
   shostak))
 (Int_diff_dom_TCC1 0
  (Int_diff_dom_TCC1-1 nil 3320059104
   ("" (skosimp*)
    (("" (lemma "connected_domain")
      (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((connected_domain formula-decl nil integral_diff_doms nil)) nil))
 (Int_diff_dom_TCC2 0
  (Int_diff_dom_TCC2-1 nil 3320059104
   ("" (lemma "not_one_element") (("" (skosimp*) nil nil)) nil)
   ((not_one_element formula-decl nil integral_diff_doms nil)) nil))
 (Int_diff_dom_TCC3 0
  (Int_diff_dom_TCC3-1 nil 3320059104
   ("" (lemma "con_dom_U") (("" (skosimp*) nil nil)) nil)
   ((con_dom_U formula-decl nil integral_diff_doms nil)) nil))
 (Int_diff_dom_TCC4 0
  (Int_diff_dom_TCC4-1 nil 3320059104
   ("" (lemma "not_one_U") (("" (skosimp*) nil nil)) nil)
   ((not_one_U formula-decl nil integral_diff_doms nil)) nil))
 (Int_diff_dom_TCC5 0
  (Int_diff_dom_TCC5-1 nil 3320059104
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (ground)
        (("1" (lemma "connected_domain")
          (("1" (expand "connected?")
            (("1" (inst - "a!1" "b!1" "x!1") (("1" (assert) nil nil))
              nil))
            nil))
          nil)
         ("2" (lemma "connected_domain")
          (("2" (expand "connected?")
            (("2" (inst - "b!1" "a!1" "x!1") (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Closed_interval type-eq-decl nil intervals_real "reals/")
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.74 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff