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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: continuity_def.pvs   Sprache: PVS

Original von: PVS©
(integral_split
 (partition_join_TCC1 0
  (partition_join_TCC1-1 nil 3281885132
   ("" (lemma "connected_domain") (("" (skosimp*) nil nil)) nil)
   ((connected_domain formula-decl nil integral_split nil)) shostak))
 (partition_join_TCC2 0
  (partition_join_TCC2-1 nil 3282313772
   ("" (lemma "not_one_element") (("" (assert) nil nil)) nil)
   ((not_one_element formula-decl nil integral_split nil)) shostak))
 (partition_join_TCC3 0
  (partition_join_TCC3-1 nil 3282313772
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (partition_join 0
  (partition_join-3 nil 3399973962
   ("" (auto-rewrite "xis?")
    (("" (auto-rewrite "xis_lem")
      (("" (skosimp*)
        (("" (typepred "xisa!1")
          (("" (typepred "xisb!1")
            (("" (expand "xis?")
              (("" (assert)
                ((""
                  (inst + "UUPart(a!1,b!1,c!1,Pa!1,Pb!1)"
                   "xisa!1 o xisb!1")
                  (("1" (split +)
                    (("1" (hide -1 -2)
                      (("1" (expand "width")
                        (("1" (lemma "connected_domain")
                          (("1"
                            (name "LUU" "{l: real |
                                    EXISTS (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)):
                                      l = seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii)
                                            - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii)}")
                            (("1" (replace -1)
                              (("1"
                                (case
                                 "is_finite[real](LUU) AND NOT empty?[real](LUU)")
                                (("1"
                                  (name
                                   "LA"
                                   "{l: real | EXISTS (ii: below(length(Pa!1) - 1)):
                                                           l = seq(Pa!1)(1 + ii) - seq(Pa!1)(ii)}")
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (name
                                       "LB"
                                       "{l: real | EXISTS (ii: below(length(Pb!1) - 1)):
                                                           l = seq(Pb!1)(1 + ii) - seq(Pb!1)(ii)}")
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (case
                                           "is_finite[real](LA) AND NOT empty?[real](LA)")
                                          (("1"
                                            (case
                                             "is_finite[real](LB) AND NOT empty?[real](LB)")
                                            (("1"
                                              (typepred "max(LUU)")
                                              (("1"
                                                (replace -8 -1 rl)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (replace -8)
                                                      (("1"
                                                        (replace -1)
                                                        (("1"
                                                          (hide -1)
                                                          (("1"
                                                            (expand
                                                             "UUPart")
                                                            (("1"
                                                              (ground)
                                                              (("1"
                                                                (lift-if)
                                                                (("1"
                                                                  (case
                                                                   "1 + ii!1 < length(Pa!1)")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (typepred
                                                                       "max(LA)")
                                                                      (("1"
                                                                        (inst
                                                                         -2
                                                                         "Pa!1`seq(1 + ii!1) - Pa!1`seq(ii!1)")
                                                                        (("1"
                                                                          (assert)
                                                                          (("1"
                                                                            (replace
                                                                             -7
                                                                             +
                                                                             rl)
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (inst?)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (lift-if)
                                                                      (("2"
                                                                        (case-replace
                                                                         "ii!1 = length(Pa!1) - 1")
                                                                        (("1"
                                                                          (case-replace
                                                                           "Pa!1`seq(length(Pa!1) - 1) = Pb!1`seq(0)")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (typepred
                                                                               "max(LB)")
                                                                              (("1"
                                                                                (replace
                                                                                 -8
                                                                                 -1
                                                                                 rl)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (skosimp*)
                                                                                    (("1"
                                                                                      (replace
                                                                                       -8)
                                                                                      (("1"
                                                                                        (inst
                                                                                         -2
                                                                                         "Pb!1`seq(1) - Pb!1`seq(0)")
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (replace
                                                                                             -7
                                                                                             +
                                                                                             rl)
                                                                                            (("1"
                                                                                              (assert)
                                                                                              (("1"
                                                                                                (inst
                                                                                                 1
                                                                                                 "0")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (assert)
                                                                          (("2"
                                                                            (typepred
                                                                             "max(LB)")
                                                                            (("2"
                                                                              (replace
                                                                               -6
                                                                               -1
                                                                               rl)
                                                                              (("2"
                                                                                (assert)
                                                                                (("2"
                                                                                  (skosimp*)
                                                                                  (("2"
                                                                                    (replace
                                                                                     -6)
                                                                                    (("2"
                                                                                      (inst
                                                                                       -2
                                                                                       "Pb!1`seq(2 - length(Pa!1) + ii!1) - Pb!1`seq(1 - length(Pa!1) + ii!1)")
                                                                                      (("2"
                                                                                        (assert)
                                                                                        (("2"
                                                                                          (replace
                                                                                           -5
                                                                                           1
                                                                                           rl)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (inst
                                                                                               1
                                                                                               "1-length(Pa!1)+ii!1")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil)
                                                                                               ("2"
                                                                                                (assert)
                                                                                                (("2"
                                                                                                  (hide
                                                                                                   -5
                                                                                                   -6
                                                                                                   -8)
                                                                                                  (("2"
                                                                                                    (hide
                                                                                                     -2
                                                                                                     -3
                                                                                                     -4
                                                                                                     -5
                                                                                                     -6)
                                                                                                    (("2"
                                                                                                      (typepred
                                                                                                       "ii!1")
                                                                                                      (("2"
                                                                                                        (assert)
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "UUPart")
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (replace -2 * rl)
                                              (("2"
                                                (hide-all-but 1)
                                                (("2"
                                                  (split +)
                                                  (("1"
                                                    (lemma
                                                     "is_finite_surj")
                                                    (("1"
                                                      (inst?)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (hide 2)
                                                          (("1"
                                                            (inst
                                                             +
                                                             "length(Pb!1)-1"
                                                             "(LAMBDA (ii: below(length(Pb!1) - 1)):
                                                    seq(Pb!1)(1 + ii) - seq(Pb!1)(ii))")
                                                            (("1"
                                                              (expand
                                                               "surjective?")
                                                              (("1"
                                                                (skosimp*)
                                                                (("1"
                                                                  (typepred
                                                                   "y!1")
                                                                  (("1"
                                                                    (skosimp*)
                                                                    (("1"
                                                                      (inst?)
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (skosimp*)
                                                              (("2"
                                                                (inst?)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (expand "empty?")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (inst
                                                         -
                                                         "seq(Pb!1)(1) - seq(Pb!1)(0)")
                                                        (("2"
                                                          (inst?)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (replace -2 * rl)
                                            (("2"
                                              (hide-all-but 1)
                                              (("2"
                                                (split +)
                                                (("1"
                                                  (lemma
                                                   "is_finite_surj")
                                                  (("1"
                                                    (inst?)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (hide 2)
                                                        (("1"
                                                          (inst
                                                           +
                                                           "length(Pa!1)-1"
                                                           "(LAMBDA (ii: below(length(Pa!1) - 1)):
                                              seq(Pa!1)(1 + ii) - seq(Pa!1)(ii))")
                                                          (("1"
                                                            (expand
                                                             "surjective?")
                                                            (("1"
                                                              (skosimp*)
                                                              (("1"
                                                                (typepred
                                                                 "y!1")
                                                                (("1"
                                                                  (skosimp*)
                                                                  (("1"
                                                                    (inst?)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (inst?)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand "empty?")
                                                  (("2"
                                                    (inst
                                                     -
                                                     "seq(Pa!1)(1) - seq(Pa!1)(0)")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (inst?)
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (replace -1 * rl)
                                  (("2"
                                    (hide-all-but 1)
                                    (("2"
                                      (split +)
                                      (("1"
                                        (lemma "is_finite_surj")
                                        (("1"
                                          (inst?)
                                          (("1"
                                            (assert)
                                            (("1"
                                              (hide 2)
                                              (("1"
                                                (inst
                                                 +
                                                 "length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))-1"
                                                 "(LAMBDA (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)):
                                             seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii)
                                                - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii))")
                                                (("1"
                                                  (expand
                                                   "surjective?")
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (typepred "y!1")
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst?)
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (skosimp*)
                                                  (("2"
                                                    (inst?)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (lemma
                                                   "connected_domain")
                                                  (("3"
                                                    (skosimp*)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("4"
                                                  (expand "UUPart")
                                                  (("4"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("5"
                                                  (lemma
                                                   "connected_domain")
                                                  (("5"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (skosimp*)
                                            (("2"
                                              (lemma
                                               "connected_domain")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "empty?")
                                        (("2"
                                          (expand "member")
                                          (("2"
                                            (inst
                                             -
                                             "seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1) -
                                            seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(0)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (inst + "0")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (expand "UUPart")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "UUPart")
                                              (("2" (assert) nil nil))
                                              nil)
                                             ("3"
                                              (lemma
                                               "connected_domain")
                                              (("3" (propax) nil nil))
                                              nil)
                                             ("4"
                                              (expand "UUPart")
                                              (("4" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (skosimp*) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide -1 -2)
                      (("2" (expand "Rie_sum")
                        (("2" (assert)
                          (("1"
                            (case " length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) = length(Pa!1) + length(Pb!1) - 1")
                            (("1"
                              (same-name "sigma[below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)]"
                                         "sigma[below(length(Pa!1) + length(Pb!1) - 2)]")
                              (("1"
                                (replace -1)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (lemma
                                       "sigma_split[below(length(Pa!1) + length(Pb!1) - 2)]")
                                      (("1"
                                        (inst?)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (inst - "length(Pa!1) - 2")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (replace -2)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (hide -1)
                                                      (("1"
                                                        (case-replace
                                                         "sigma[below(length(Pa!1) + length(Pb!1) - 2)].sigma(0, length(Pa!1) - 2,
                                        LAMBDA (n: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)):
                                           UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) *
                                             f!1((concat_arrays.o(xisa!1, xisb!1))(n))
                                               - UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) *
                                                 f!1((concat_arrays.o(xisa!1, xisb!1))(n)))
                                            = sigma[below(length(Pa!1) - 1)]
                                                 (0, length(Pa!1) - 2,
                                                  LAMBDA (n: below(length(Pa!1) - 1)):
                                                    Pa!1`seq(1 + n) * f!1(xisa!1(n)) -
                                                      Pa!1`seq(n) * f!1(xisa!1(n)))")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (lemma
                                                               "sigma_diff_shift[length(Pb!1) - 1,length(Pa!1) + length(Pb!1) - 2
                                                                         ]")
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "(LAMBDA (n: below(length(Pb!1) - 1)):
                                                                                      Pb!1`seq(1 + n) * f!1(xisb!1(n)) -
                                                                                       Pb!1`seq(n) * f!1(xisb!1(n)))"
                                                                 "(LAMBDA (n:
                                                                                              below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) -
                                                                                                     1)):
                                                                                      UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) *
                                                                                       f!1((concat_arrays.o(xisa!1, xisb!1))(n))
                                                                                       -
                                                                                       UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) *
                                                                                        f!1((concat_arrays.o(xisa!1, xisb!1))(n)))"
                                                                 "length(Pa!1) - 1"
                                                                 "length(Pb!1) - 2"
                                                                 "0")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (hide
                                                                     2)
                                                                    (("1"
                                                                      (skosimp*)
                                                                      (("1"
                                                                        (expand
                                                                         "UUPart")
                                                                        (("1"
                                                                          (assert)
                                                                          (("1"
                                                                            (expand
                                                                             "o ")
                                                                            (("1"
                                                                              (lift-if)
                                                                              (("1"
                                                                                (ground)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   2)
                                                                  (("2"
                                                                    (skosimp*)
                                                                    (("2"
                                                                      (assert)
                                                                      (("2"
                                                                        (ground)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("3"
                                                                  (hide
                                                                   2)
                                                                  (("3"
                                                                    (lemma
                                                                     "connected_domain")
                                                                    (("3"
                                                                      (skosimp*)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide 2)
                                                          (("2"
                                                            (lemma
                                                             "sigma_diff_eq[length(Pa!1) + length(Pb!1) - 2
                                                                         ,length(Pa!1) - 1]")
                                                            (("2"
                                                              (lemma
                                                               "connected_domain")
                                                              (("2"
                                                                (lemma
                                                                 "sigma_diff_eq[length(Pa!1) + length(Pb!1) - 2
                                                                                         ,length(Pa!1) - 1]")
                                                                (("2"
                                                                  (inst?)
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (hide
                                                                       2)
                                                                      (("1"
                                                                        (skosimp*)
                                                                        (("1"
                                                                          (expand
                                                                           "UUPart")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (expand
                                                                               "o ")
                                                                              (("1"
                                                                                (propax)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (ground)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("3"
                                                                    (hide
                                                                     2)
                                                                    (("3"
                                                                      (skosimp*)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("3"
                                                          (hide 2)
                                                          (("3"
                                                            (skosimp*)
                                                            (("3"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("4"
                                                          (hide 2)
                                                          (("4"
                                                            (lemma
                                                             "connected_domain")
                                                            (("4"
                                                              (skosimp*)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide 2)
                                          (("2"
                                            (lemma "connected_domain")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil)
                                         ("3"
                                          (assert)
                                          (("3"
                                            (hide 2)
                                            (("3"
                                              (skosimp*)
                                              (("3" (ground) nil nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("4"
                                          (hide 2)
                                          (("4"
                                            (lemma "connected_domain")
                                            (("4" (skosimp*) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (expand "UUPart")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (hide 2)
                                (("3"
                                  (skosimp*)
                                  (("3" (assert) nil nil))
                                  nil))
                                nil)
                               ("4"
                                (hide 2)
                                (("4"
                                  (skosimp*)
                                  (("4" (assert) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "UUPart")
                              (("2" (propax) nil nil)) nil)
                             ("3" (lemma "connected_domain")
                              (("3" (propax) nil nil)) nil))
                            nil)
                           ("2" (hide 2)
                            (("2" (assert) (("2" (assert) nil nil))
                              nil))
                            nil)
                           ("3" (lemma "connected_domain")
                            (("3" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (split +)
                    (("1" (skosimp*)
                      (("1" (expand "UUPart") (("1" (propax) nil nil))
                        nil))
                      nil)
                     ("2" (skosimp*)
                      (("2" (expand "o")
                        (("2" (assert)
                          (("2" (lift-if) (("2" (ground) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("3" (skosimp*)
                      (("3" (typepred "ii!1")
                        (("3" (expand "UUPart")
                          (("3" (expand "o")
                            (("3"
                              (case-replace "ii!1 < length(Pa!1) - 1")
                              (("1"
                                (inst -4 "ii!1")
                                (("1" (assert) nil nil))
                                nil)
                               ("2"
                                (assert)
                                (("2"
                                  (inst -2 "1 - length(Pa!1) + ii!1")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (lift-if)
                                        (("2" (ground) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("3" (lemma "connected_domain")
                    (("3" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((partition type-eq-decl nil integral_def nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (xis? const-decl "bool" integral_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (T formal-nonempty-subtype-decl nil integral_split nil)
    (T_pred const-decl "[real -> boolean]" integral_split 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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (connected? const-decl "bool" deriv_domain_def nil)
    (xisb!1 skolem-const-decl "(xis?(b!1, c!1, Pb!1))" integral_split
     nil)
    (xisa!1 skolem-const-decl "(xis?(a!1, b!1, Pa!1))" integral_split
     nil)
    (O const-decl "below_array[n + m, T]" concat_arrays "structures/")
    (below_array type-eq-decl nil below_arrays "structures/")
    (UUPart const-decl "partition[T](a, c)" step_fun_props nil)
    (Pb!1 skolem-const-decl "partition[T](b!1, c!1)" integral_split
     nil)
    (c!1 skolem-const-decl "T" integral_split nil)
    (Pa!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split
     nil)
    (b!1 skolem-const-decl "T" integral_split nil)
    (a!1 skolem-const-decl "T" integral_split nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (not_one_element formula-decl nil integral_split nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (sigma_split formula-decl nil sigma "reals/")
    (sigma_diff_eq formula-decl nil sigma_below_sub "reals/")
    (sigma_diff_shift formula-decl nil sigma_below_sub "reals/")
    (sigma def-decl "real" sigma "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (Rie_sum const-decl "real" integral_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (connected_domain formula-decl nil integral_split nil)
    (surjective? const-decl "bool" functions nil)
    (is_finite_surj formula-decl nil finite_sets nil)
    (member const-decl "bool" sets nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (max const-decl
         "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
--> --------------------

--> maximum size reached

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

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