Quelle continuity.prf Sprache: Lisp

(continuity
(continuous_open_sets 0
  (continuous_open_sets-1 nil 3300514488
   ("" (expand "continuous?")
    (("" (expand "continuous_at?")
      (("" (skosimp*)
        (("" (split)
          (("1" (skosimp*)
            (("1" (lemma "image_inverse_image" ("f" "f!1" "Y" "Y!1"))
              (("1" (rewrite "open_def[T1,S]" 1)
                (("1" (skosimp)
                  (("1" (typepred "x!1")
                    (("1" (inst - "x!1")
                      (("1" (inst - "Y!1")
                        (("1" (split)
                          (("1" (propax) nil nil)
                           ("2" (hide 2)
                            (("2" (expand "neighbourhood?")
                              (("2"
                                (expand "interior_point?")
                                (("2"
                                  (expand "inverse_image")
                                  (("2"
                                    (inst + "Y!1")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (expand "subset?")
                                        (("2" (skosimp) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (lemma "topology1") (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "neighbourhood?")
            (("2" (expand "interior_point?")
              (("2" (skosimp*)
                (("2" (typepred "U!2")
                  (("2" (inst - "U!2")
                    (("2" (assert)
                      (("2" (inst + "inverse_image(f!1, U!2)")
                        (("2"
                          (lemma "inverse_image_subset"
                           ("Y1" "U!2" "Y2" "U!1" "f" "f!1"))
                          (("2" (assert)
                            (("2" (expand "inverse_image")
                              (("2"
                                (expand "member")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_at? const-decl "bool" continuity_def nil)
    (T2 formal-type-decl nil continuity nil)
    (T1 formal-type-decl nil continuity nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (image_inverse_image formula-decl nil function_image nil)
    (neighbourhood? const-decl "bool" topology nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (open nonempty-type-eq-decl nil topology nil)
    (Y!1 skolem-const-decl "set[T2]" continuity nil)
    (open? const-decl "bool" topology nil)
    (T formal-const-decl "topology[T2]" continuity nil)
    (interior_point? const-decl "bool" topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (S formal-const-decl "topology[T1]" continuity nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (open_def formula-decl nil topology nil)
    (inverse_image_subset formula-decl nil function_image nil)
    (continuous? const-decl "bool" continuity_def nil))
   shostak))
(continuous_closed_sets 0
  (continuous_closed_sets-1 nil 3300515647
   ("" (skosimp)
    (("" (rewrite "continuous_open_sets")
      (("" (split)
        (("1" (skosimp*)
          (("1" (expand "closed?")
            (("1" (expand "member")
              (("1" (inst - "complement(Y!1)")
                (("1" (assert)
                  (("1" (expand "open?")
                    (("1" (expand "member")
                      (("1" (rewrite "inverse_image_complement") nil
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (expand "closed?")
            (("2" (expand "open?")
              (("2" (expand "member")
                (("2" (inst - "complement(Y!1)")
                  (("2" (rewrite "complement_complement")
                    (("2" (assert)
                      (("2" (rewrite "inverse_image_complement")
                        (("2" (rewrite "complement_complement") nil
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_open_sets formula-decl nil continuity nil)
    (T1 formal-type-decl nil continuity nil)
    (T2 formal-type-decl nil continuity nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (inverse_image_complement formula-decl nil function_image nil)
    (open? const-decl "bool" topology nil)
    (complement const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (closed? const-decl "bool" topology nil))
   shostak))
(continuous_basis 0
  (continuous_basis-1 nil 3364124090
   ("" (skosimp)
    (("" (rewrite "continuous_open_sets")
      (("" (split)
        (("1" (skosimp*)
          (("1" (typepred "Y!1")
            (("1" (typepred "B!1")
              (("1" (expand "base?")
                (("1" (flatten)
                  (("1" (inst -4 "Y!1")
                    (("1" (split -4)
                      (("1" (propax) nil nil)
                       ("2" (hide 2)
                        (("2" (expand "subset?")
                          (("2" (expand "open?")
                            (("2" (expand "member")
                              (("2"
                                (inst - "Y!1")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (typepred "B!1")
            (("2" (expand "base?")
              (("2" (flatten)
                (("2" (expand "open?" -4)
                  (("2" (expand "member")
                    (("2" (inst - "Y!1")
                      (("2" (skosimp)
                        (("2" (replace -3 * rl)
                          (("2"
                            (case-replace
                             "inverse_image(f!1, Union(V!1)) =
       Union({X | EXISTS Y: V!1(Y) & X=inverse_image(f!1, Y)})")
                            (("1" (hide -1)
                              (("1"
                                (lemma
                                 "open_Union"
                                 ("Y"
                                  "{X | EXISTS Y: V!1(Y) & X = inverse_image(f!1, Y)}"))
                                (("1"
                                  (split -1)
                                  (("1" (propax) nil nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (expand "every")
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (typepred "x!1")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (replace -2)
                                              (("2"
                                                (hide -2)
                                                (("2"
                                                  (inst - "Y!2")
                                                  (("2"
                                                    (expand "subset?")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (inst -3 "Y!2")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2)
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                (("2"
                                  (expand "Union")
                                  (("2"
                                    (expand "inverse_image")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (case-replace
                                         "EXISTS (a: (V!1)): a(f!1(x!1))")
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (typepred "a!1")
                                            (("1"
                                              (inst
                                               +
                                               "inverse_image(f!1, a!1)")
                                              (("1"
                                                (expand
                                                 "inverse_image")
                                                (("1"
                                                  (expand "member")
                                                  (("1"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (inst + "a!1")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (replace 1 2)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (typepred "a!1")
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (inst + "Y!2")
                                                    (("2"
                                                      (replace -2 -3)
                                                      (("2"
                                                        (expand
                                                         "inverse_image")
                                                        (("2"
                                                          (expand
                                                           "member")
                                                          (("2"
                                                            (propax)
                                                            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)
   ((continuous_open_sets formula-decl nil continuity nil)
    (T1 formal-type-decl nil continuity nil)
    (T2 formal-type-decl nil continuity nil)
    (Y!1 skolem-const-decl "set[T2]" continuity nil)
    (Y!2 skolem-const-decl "set[T2]" continuity nil)
    (V!1 skolem-const-decl "setofsets[T2]" continuity nil)
    (f!1 skolem-const-decl "[T1 -> T2]" continuity nil)
    (a!1 skolem-const-decl "(V!1)" continuity nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (every const-decl "bool" sets nil)
    (B!1 skolem-const-decl "(base?[T2](T))" continuity nil)
    (Y!2 skolem-const-decl "set[T2]" continuity nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (S formal-const-decl "topology[T1]" continuity nil)
    (open_Union formula-decl nil topology nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (Union const-decl "set" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (topology? const-decl "bool" topology_prelim nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (base? const-decl "bool" basis nil)
    (T formal-const-decl "topology[T2]" continuity nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.