Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: complete_product.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) (("" (assert) nil 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") (("" (assert) nil 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" (assert) nil nil)
             ("2" (case-replace "a!1)
              (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) nil nil))
                nil)
               ("2" (inst - "b!1" "a!1" "f!1") (("2" (assert) nil 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" (assert) 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))
            nil))
          nil))
        nil)
       ("3" (hide 2)
        (("3" (skosimp*)
          (("3" (lemma "sub_domain" ("x" "x!1"))
            (("3" (skolem!) (("3" (assert) nil nil)) nil)) nil))
          nil))
        nil)
       ("4" (skosimp)
        (("4" (lemma "sub_domain" ("x" "b!1"))
          (("4" (skolem!) (("4" (assert) nil nil)) nil)) nil))
        nil)
       ("5" (hide 2)
        (("5" (skosimp)
          (("5" (lemma "sub_domain" ("x" "a!1"))
            (("5" (skolem!) (("5" (assert) nil 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) (("" (assert) nil 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) (("" (assert) nil 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"))
      (("" (assert) nil 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" (assert) nil nil)) nil))
                      nil)
                     ("2" (assert)
                      (("2" (inst - "b!1" "a!1" "f!1")
                        (("2" (assert) nil 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.78 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.