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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: inexact_reduce_stage.prf   Sprache: Lisp

Original von: PVS©

(restriction_integral
 (restrict_Integrable_TCC1 0
  (restrict_Integrable_TCC1-1 nil 3432062629
   ("" (lemma "sub_domain")
    (("" (skosimp)
      (("" (inst - "a!1") (("" (skosimp) (("" (assertnil nil)) nil))
        nil))
      nil))
    nil)
   ((T1 formal-subtype-decl nil restriction_integral nil)
    (T1_pred const-decl "[real -> boolean]" restriction_integral nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (sub_domain formula-decl nil restriction_integral nil))
   nil))
 (restrict_Integrable_TCC2 0
  (restrict_Integrable_TCC2-1 nil 3432062629
   ("" (expand "connected?")
    (("" (skosimp)
      (("" (lemma "connected_domain_T2" ("x" "x!1" "y" "y!1"))
        (("" (inst - "z!1") (("" (assertnil nil)) nil)) nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected_domain_T2 formula-decl nil restriction_integral nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T2_pred const-decl "[real -> boolean]" restriction_integral nil)
    (T2 formal-subtype-decl nil restriction_integral nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
 (restrict_Integrable_TCC3 0
  (restrict_Integrable_TCC3-1 nil 3432062629
   ("" (expand "not_one_element?")
    (("" (lemma "not_one_element_T2") (("" (propax) nil nil)) nil))
    nil)
   ((not_one_element_T2 formula-decl nil restriction_integral nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
 (restrict_Integrable_TCC4 0
  (restrict_Integrable_TCC4-1 nil 3432062629
   ("" (expand "connected?")
    (("" (lemma "connected_domain_T1") (("" (propax) nil nil)) nil))
    nil)
   ((connected_domain_T1 formula-decl nil restriction_integral nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
 (restrict_Integrable_TCC5 0
  (restrict_Integrable_TCC5-1 nil 3432062629
   ("" (lemma "not_one_element_T1")
    (("" (expand "not_one_element?") (("" (propax) nil nil)) nil)) nil)
   ((not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element_T1 formula-decl nil restriction_integral nil))
   nil))
 (restrict_Integrable 0
  (restrict_Integrable-1 nil 3432063069
   ("" (auto-rewrite "xis_lem")
    ((""
      (case "FORALL (a, b: T1, f: [T2 -> real]): a
               (integrable?[T2](a, b, f) <=>
                integrable?[T1](a, b, restrict[T2, T1, real](f)))")
      (("1" (skosimp)
        (("1" (expand "Integrable?")
          (("1" (case-replace "a!1=b!1")
            (("1" (assertnil nil)
             ("2" (case-replace "a!1)
              (("1" (inst - "a!1" "b!1" "f!1") (("1" (assertnil nil))
                nil)
               ("2" (inst - "b!1" "a!1" "f!1") (("2" (assertnil nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp)
          (("2" (split)
            (("1" (flatten)
              (("1" (expand "integrable?")
                (("1" (skosimp)
                  (("1" (inst + "S!1")
                    (("1" (expand "integral?")
                      (("1" (skosimp)
                        (("1" (inst - "epsi!1")
                          (("1" (skosimp)
                            (("1" (inst + "delta!1")
                              (("1"
                                (skosimp)
                                (("1"
                                  (inst - "P!1")
                                  (("1"
                                    (split)
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (inst - "R!1")
                                        (("1"
                                          (typepred "R!1")
                                          (("1"
                                            (hide -2 2)
                                            (("1"
                                              (expand "Riemann_sum?")
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (inst + "xis!1")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (hide -1)
                                                      (("1"
                                                        (expand
                                                         "Rie_sum")
                                                        (("1"
                                                          (expand
                                                           "finseq_appl")
                                                          (("1"
                                                            (expand
                                                             "restrict")
                                                            (("1"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide -1)
                                                    (("2"
                                                      (split)
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
                                                          (typepred
                                                           "xis!1(x1!1)")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lemma
                                                               "sub_domain"
                                                               ("x"
                                                                "xis!1(x1!1)"))
                                                              (("1"
                                                                (skosimp)
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (typepred
                                                         "xis!1")
                                                        (("2"
                                                          (expand
                                                           "xis?")
                                                          (("2"
                                                            (expand
                                                             "finseq_appl")
                                                            (("2"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (expand "width")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (split)
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (typepred "P!1`seq(x1!1)")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (lemma
                                               "sub_domain"
                                               ("x" "P!1`seq(x1!1)"))
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (skosimp)
                                        (("2"
                                          (typepred "P!1")
                                          (("2"
                                            (inst - "ii!1")
                                            nil
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (flatten)
              (("2" (expand "integrable?")
                (("2" (skosimp)
                  (("2" (inst + "S!1")
                    (("2" (expand "integral?")
                      (("2" (skosimp)
                        (("2" (inst - "epsi!1")
                          (("2" (skosimp)
                            (("2" (inst + "delta!1")
                              (("2"
                                (skosimp)
                                (("2"
                                  (inst - "P!1")
                                  (("1"
                                    (split)
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (inst - "R!1")
                                        (("1"
                                          (hide -1 2)
                                          (("1"
                                            (typepred "R!1")
                                            (("1"
                                              (expand "Riemann_sum?")
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (inst + "xis!1")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (hide -1)
                                                      (("1"
                                                        (expand
                                                         "Rie_sum")
                                                        (("1"
                                                          (expand
                                                           "restrict")
                                                          (("1"
                                                            (expand
                                                             "finseq_appl")
                                                            (("1"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (split)
                                                    (("1"
                                                      (skosimp)
                                                      (("1"
                                                        (typepred
                                                         "xis!1(x1!1)")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (lemma
                                                             "connected_domain_T1"
                                                             ("x"
                                                              "a!1"
                                                              "y"
                                                              "b!1"
                                                              "z"
                                                              "xis!1(x1!1)"))
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (typepred
                                                       "xis!1")
                                                      (("2"
                                                        (expand "xis?")
                                                        (("2"
                                                          (expand
                                                           "finseq_appl")
                                                          (("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (expand "width")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2 -1)
                                    (("2"
                                      (split)
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (typepred "P!1`seq(x1!1)")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (lemma
                                               "connected_domain_T1"
                                               ("x"
                                                "a!1"
                                                "y"
                                                "b!1"
                                                "z"
                                                "P!1`seq(x1!1)"))
                                              (("1" (assertnil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (skosimp)
                                        (("2"
                                          (typepred "P!1")
                                          (("2"
                                            (inst - "ii!1")
                                            nil
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (hide 2)
        (("3" (skosimp*)
          (("3" (lemma "sub_domain" ("x" "x!1"))
            (("3" (skolem!) (("3" (assertnil nil)) nil)) nil))
          nil))
        nil)
       ("4" (skosimp)
        (("4" (lemma "sub_domain" ("x" "b!1"))
          (("4" (skolem!) (("4" (assertnil nil)) nil)) nil))
        nil)
       ("5" (hide 2)
        (("5" (skosimp)
          (("5" (lemma "sub_domain" ("x" "a!1"))
            (("5" (skolem!) (("5" (assertnil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((restrict const-decl "R" restrict nil)
    (integrable? const-decl "bool" integral_def "analysis/")
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-subtype-decl nil restriction_integral nil)
    (T2_pred const-decl "[real -> boolean]" restriction_integral nil)
    (T1 formal-subtype-decl nil restriction_integral nil)
    (T1_pred const-decl "[real -> boolean]" restriction_integral nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (Integrable? const-decl "bool" integral_def "analysis/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (P!1 skolem-const-decl "partition[T2](a!1, b!1)"
     restriction_integral nil)
    (xis!1 skolem-const-decl "(xis?(a!1, b!1, P!1))"
     restriction_integral nil)
    (connected_domain_T1 formula-decl nil restriction_integral nil)
    (R!1 skolem-const-decl "(Riemann_sum?(a!1, b!1, P!1, f!1))"
     restriction_integral nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (integral? const-decl "bool" integral_def "analysis/")
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (P!1 skolem-const-decl "partition[T1](a!1, b!1)"
     restriction_integral nil)
    (partition type-eq-decl nil integral_def "analysis/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil naturalnumbers 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/")
    (b!1 skolem-const-decl "T1" restriction_integral nil)
    (a!1 skolem-const-decl "T1" restriction_integral nil)
    (<= const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (width const-decl "posreal" integral_def "analysis/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (xis? const-decl "bool" integral_def "analysis/")
    (xis!1 skolem-const-decl "(xis?(a!1, b!1, P!1))"
     restriction_integral nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (Rie_sum const-decl "real" integral_def "analysis/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (sub_domain formula-decl nil restriction_integral nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (R!1 skolem-const-decl
     "(Riemann_sum?(a!1, b!1, P!1, restrict[T2, T1, real](f!1)))"
     restriction_integral nil)
    (f!1 skolem-const-decl "[T2 -> real]" restriction_integral nil)
    (Riemann_sum? const-decl "bool" integral_def "analysis/"))
   shostak))
 (restrict_Integral_TCC1 0
  (restrict_Integral_TCC1-1 nil 3432062629
   ("" (skosimp)
    (("" (hide -1)
      (("" (typepred "b!1")
        (("" (lemma "sub_domain" ("x" "b!1"))
          (("" (skosimp) (("" (assertnil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((sub_domain formula-decl nil restriction_integral nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T1_pred const-decl "[real -> boolean]" restriction_integral nil)
    (T1 formal-subtype-decl nil restriction_integral nil))
   nil))
 (restrict_Integral_TCC2 0
  (restrict_Integral_TCC2-1 nil 3432062629
   ("" (skosimp)
    (("" (skosimp)
      (("" (lemma "sub_domain" ("x" "x!1"))
        (("" (skosimp) (("" (assertnil nil)) nil)) nil))
      nil))
    nil)
   ((sub_domain formula-decl nil restriction_integral nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T1_pred const-decl "[real -> boolean]" restriction_integral nil)
    (T1 formal-subtype-decl nil restriction_integral nil))
   nil))
 (restrict_Integral_TCC3 0
  (restrict_Integral_TCC3-1 nil 3432189764
   ("" (skosimp)
    (("" (lemma "restrict_Integrable" ("a" "a!1" "b" "b!1" "f" "f!1"))
      (("" (assertnil nil)) nil))
    nil)
   ((T2 formal-subtype-decl nil restriction_integral nil)
    (T2_pred const-decl "[real -> boolean]" restriction_integral nil)
    (T1 formal-subtype-decl nil restriction_integral nil)
    (T1_pred const-decl "[real -> boolean]" restriction_integral nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (restrict_Integrable formula-decl nil restriction_integral nil))
   nil))
 (restrict_Integral 0
  (restrict_Integral-1 nil 3432064068
   (""
    (case "forall a,b,f: a
         integral[T2](a, b, f) =
          integral[T1](a, b, restrict[T2, T1, real](f))")
    (("1" (skosimp)
      (("1"
        (lemma "restrict_Integrable" ("a" "a!1" "b" "b!1" "f" "f!1"))
        (("1" (assert)
          (("1" (expand "Integrable?")
            (("1" (expand "Integral")
              (("1" (case-replace "a!1=b!1")
                (("1" (assert)
                  (("1" (case-replace "a!1)
                    (("1" (assert)
                      (("1" (inst - "a!1" "b!1" "f!1")
                        (("1" (assertnil nil)) nil))
                      nil)
                     ("2" (assert)
                      (("2" (inst - "b!1" "a!1" "f!1")
                        (("2" (assertnil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp*)
        (("2" (typepred "integral[T2](a!1, b!1, f!1)")
          (("2"
            (typepred
             "integral[T1](a!1, b!1, restrict[T2, T1, real](f!1))")
            (("1" (expand "integral?")
              (("1" (name-replace "LHS" "integral[T2](a!1, b!1, f!1)")
                (("1"
                  (name-replace "RHS"
                   "integral[T1](a!1, b!1, restrict[T2, T1, real](f!1))")
                  (("1" (typepred "abs(LHS-RHS)")
                    (("1" (hide -2 -3)
                      (("1" (expand ">=" -1)
                        (("1" (expand "<=" -1)
                          (("1" (split -1)
                            (("1" (name "EPS" "abs(LHS-RHS)")
                              (("1"
                                (replace -1)
                                (("1"
                                  (inst - "EPS/2")
                                  (("1"
                                    (inst - "EPS/2")
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (name
                                         "DELTA"
                                         "min(delta!1,delta!2)")
                                        (("1"
                                          (name
                                           "N"
                                           "floor((b!1-a!1)/DELTA)+2")
                                          (("1"
                                            (lemma
                                             "width_eq_part[T1]"
                                             ("a"
                                              "a!1"
                                              "b"
                                              "b!1"
                                              "N"
                                              "N"))
                                            (("1"
                                              (lemma
                                               "width_eq_part[T2]"
                                               ("a"
                                                "a!1"
                                                "b"
                                                "b!1"
                                                "N"
                                                "N"))
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (case
                                                   "(b!1-a!1)/(N-1))
                                                  (("1"
                                                    (case
                                                     "DELTA <= delta!1 & DELTA<=delta!2")
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (inst
                                                         -
                                                         "eq_partition[T1](a!1, b!1, N)")
                                                        (("1"
                                                          (inst
                                                           -
                                                           "eq_partition[T2](a!1, b!1, N)")
                                                          (("1"
                                                            (replace
                                                             -4)
                                                            (("1"
                                                              (replace
                                                               -5)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (hide
                                                                   -4
                                                                   -5)
                                                                  (("1"
                                                                    (split
                                                                     -8)
                                                                    (("1"
                                                                      (split
                                                                       -9)
                                                                      (("1"
                                                                        (lemma
                                                                         "Riemann?_Rie[T2]"
                                                                         ("a"
                                                                          "a!1"
                                                                          "b"
                                                                          "b!1"
                                                                          "f"
                                                                          "f!1"))
                                                                        (("1"
                                                                          (lemma
                                                                           "Riemann?_Rie[T1]"
                                                                           ("a"
                                                                            "a!1"
                                                                            "b"
                                                                            "b!1"
                                                                            "f"
                                                                            "restrict[T2, T1, real](f!1)"))
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "eq_partition[T1](a!1, b!1, N)"
                                                                               "gen_xis[T1](a!1,b!1,eq_partition[T1](a!1, b!1, N))")
                                                                              (("1"
                                                                                (inst
                                                                                 -
                                                                                 "eq_partition[T1](a!1, b!1, N)"
                                                                                 "_")
                                                                                (("1"
                                                                                  (case
                                                                                   "N>=1")
                                                                                  (("1"
                                                                                    (name
                                                                                     "R1"
                                                                                     "Rie_sum(a!1, b!1, eq_partition[T1](a!1, b!1, N),
                           gen_xis[T1]
                               (a!1, b!1, eq_partition[T1](a!1, b!1, N)),
                           restrict[T2, T1, real](f!1))")
                                                                                    (("1"
                                                                                      (replace
                                                                                       -1)
                                                                                      (("1"
                                                                                        (inst
                                                                                         -6
                                                                                         "R1")
                                                                                        (("1"
                                                                                          (inst
                                                                                           -4
                                                                                           "gen_xis[T1](a!1, b!1, eq_partition[T1](a!1, b!1, N))")
                                                                                          (("1"
                                                                                            (name
                                                                                             "R2"
                                                                                             "Rie_sum[T2](a!1, b!1, eq_partition[T1](a!1, b!1, N),
                           gen_xis[T1]
                               (a!1, b!1, eq_partition[T1](a!1, b!1, N)),
                           f!1)")
                                                                                            (("1"
                                                                                              (replace
                                                                                               -1)
                                                                                              (("1"
                                                                                                (case
                                                                                                 "eq_partition[T1](a!1, b!1, N)=eq_partition[T2](a!1, b!1, N)")
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   -7
                                                                                                   "R2")
                                                                                                  (("1"
                                                                                                    (case-replace
                                                                                                     "R1=R2")
                                                                                                    (("1"
                                                                                                      (hide-all-but
                                                                                                       (-8
                                                                                                        -9
                                                                                                        -15))
                                                                                                      (("1"
                                                                                                        (grind)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (hide
                                                                                                       -3
                                                                                                       -5
                                                                                                       2
                                                                                                       -17
                                                                                                       -18
                                                                                                       -7
                                                                                                       -8
                                                                                                       -9
                                                                                                       -10
                                                                                                       -11
                                                                                                       -12
                                                                                                       -13
                                                                                                       -14
                                                                                                       -15)
                                                                                                      (("2"
                                                                                                        (hide
                                                                                                         -2
                                                                                                         -4)
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "R1")
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "R2")
                                                                                                            (("2"
                                                                                                              (name-replace
                                                                                                               "FF"
                                                                                                               "gen_xis[T1](a!1, b!1, eq_partition[T1](a!1, b!1, N))")
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "Rie_sum")
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   "finseq_appl")
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "restrict")
                                                                                                                    (("2"
                                                                                                                      (propax)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (expand
                                                                                                   "eq_partition")
                                                                                                  (("2"
                                                                                                    (propax)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide
                                                                                             -1
                                                                                             -3
                                                                                             -4
                                                                                             2)
                                                                                            (("2"
                                                                                              (typepred
                                                                                               "gen_xis[T1](a!1, b!1, eq_partition[T1](a!1, b!1, N))")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "xis?")
                                                                                                (("2"
                                                                                                  (split)
                                                                                                  (("1"
                                                                                                    (skosimp)
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "finseq_appl")
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         -
                                                                                                         "x1!1")
                                                                                                        (("1"
                                                                                                          (flatten)
                                                                                                          (("1"
                                                                                                            (lemma
                                                                                                             "parts_order_le[T1]"
                                                                                                             ("P"
                                                                                                              "eq_partition[T1](a!1, b!1, N)"
                                                                                                              "a"
                                                                                                              "a!1"
                                                                                                              "b"
                                                                                                              "b!1"))
                                                                                                            (("1"
                                                                                                              (inst-cp
                                                                                                               -
                                                                                                               "0"
                                                                                                               "x1!1")
                                                                                                              (("1"
                                                                                                                (assert)
                                                                                                                (("1"
                                                                                                                  (hide
                                                                                                                   -1
                                                                                                                   -2
                                                                                                                   -3
                                                                                                                   -4)
                                                                                                                  (("1"
                                                                                                                    (lemma
                                                                                                                     "sub_domain"
                                                                                                                     ("x"
                                                                                                                      "gen_xis[T1](a!1, b!1, eq_partition[T1](a!1, b!1, N))(x1!1)"))
                                                                                                                    (("1"
                                                                                                                      (skosimp)
                                                                                                                      (("1"
                                                                                                                        (assert)
                                                                                                                        nil
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (skosimp)
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "finseq_appl")
                                                                                                      (("2"
                                                                                                        (inst
                                                                                                         -
                                                                                                         "ii!1")
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (hide-all-but
                                                                                     (1
                                                                                      -12
                                                                                      -8
                                                                                      -7
                                                                                      -9))
                                                                                    (("2"
                                                                                      (lemma
                                                                                       "posreal_div_posreal_is_posreal"
                                                                                       ("px"
                                                                                        "b!1-a!1"
                                                                                        "py"
                                                                                        "DELTA"))
                                                                                      (("2"
                                                                                        (lemma
                                                                                         "nonneg_floor_is_nat")
                                                                                        (("2"
                                                                                          (inst
                                                                                           -
                                                                                           "(b!1 - a!1) / DELTA")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide
                                                                                   -1
                                                                                   -2
                                                                                   -3
                                                                                   2)
                                                                                  (("2"
                                                                                    (split)
                                                                                    (("1"
                                                                                      (skosimp)
                                                                                      (("1"
                                                                                        (typepred
                                                                                         "eq_partition[T1](a!1, b!1, N)`seq(x1!1)")
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (lemma
                                                                                             "sub_domain"
                                                                                             ("x"
                                                                                              "eq_partition[T1](a!1, b!1, N)`seq(x1!1)"))
                                                                                            (("1"
                                                                                              (skosimp)
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (typepred
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.86 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



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik