Quelle homeomorphism_def.prf Sprache: Lisp

(homeomorphism_def
(homeomorphism?_TCC1 0
  (homeomorphism?_TCC1-1 nil 3300961357
   ("" (skosimp)
    (("" (skosimp)
      (("" (expand "bijective?")
        (("" (flatten)
          (("" (expand "surjective?")
            (("" (inst - "r!1")
              (("" (skosimp) (("" (inst + "x!1") nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil homeomorphism_def nil)
    (T1 formal-type-decl nil homeomorphism_def nil)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions nil))
   shostak))
(homeomorphism_def 0
  (homeomorphism_def-1 nil 3346477468
   ("" (skosimp)
    (("" (expand "homeomorphism?")
      (("" (case-replace "bijective?[T1, T2](f!1)")
        (("1" (case "nonempty?(fullset[T1])")
          (("1" (case "nonempty?(fullset[T2])")
            (("1" (case "EXISTS (x:T1): TRUE")
              (("1"
                (case "forall (y:T2): f!1(inverse_alt(f!1)(y)) = y")
                (("1"
                  (case "forall (x:T1): inverse_alt(f!1)(f!1(x)) = x")
                  (("1" (split 1)
                    (("1" (flatten)
                      (("1" (skosimp)
                        (("1" (split)
                          (("1" (flatten)
                            (("1" (rewrite "continuous_open_sets" -3)
                              (("1"
                                (inst - "X!1")
                                (("1"
                                  (assert)
                                  (("1"
                                    (lemma
                                     "extensionality"
                                     ("f"
                                      "inverse_image(inverse_alt(f!1), X!1)"
                                      "g"
                                      "image(f!1, X!1)"))
                                    (("1"
                                      (split -1)
                                      (("1" (assert) nil nil)
                                       ("2"
                                        (hide-all-but (-4 -5 -6 1 -9))
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (expand "inverse_image")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (case-replace
                                                 "image(f!1, X!1)(x!1)")
                                                (("1"
                                                  (expand "image")
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (replace -1)
                                                      (("1"
                                                        (typepred
                                                         "x!2")
                                                        (("1"
                                                          (inst
                                                           -3
                                                           "x!2")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (replace 1 2)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (expand "image")
                                                      (("2"
                                                        (inst
                                                         +
                                                         "inverse_alt(f!1)(x!1)")
                                                        (("1"
                                                          (inst
                                                           -3
                                                           "x!1")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (flatten)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (flatten) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (flatten) nil nil))
                              nil))
                            nil)
                           ("2" (flatten)
                            (("2" (rewrite "continuous_open_sets" -2)
                              (("2"
                                (inst - "image(f!1,X!1)")
                                (("2"
                                  (assert)
                                  (("2"
                                    (rewrite
                                     "injective_inverse_image_image")
                                    (("2"
                                      (expand "bijective?")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (flatten)
                      (("2" (split)
                        (("1" (rewrite "continuous_open_sets" 1)
                          (("1" (skosimp)
                            (("1" (inst - "inverse_image(f!1, Y!1)")
                              (("1"
                                (replace -2)
                                (("1"
                                  (rewrite
                                   "surjective_image_inverse_image"
                                   1)
                                  (("1"
                                    (expand "bijective?")
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (rewrite "continuous_open_sets" 1)
                          (("1" (skosimp)
                            (("1" (inst - "Y!1")
                              (("1"
                                (assert)
                                (("1"
                                  (lemma
                                   "extensionality"
                                   ("f"
                                    "image(f!1, Y!1)"
                                    "g"
                                    "inverse_image(inverse_alt(f!1), Y!1)"))
                                  (("1"
                                    (split -1)
                                    (("1" (assert) nil nil)
                                     ("2"
                                      (hide 2 -1 -2)
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (case-replace
                                           "image(f!1, Y!1)(x!1)")
                                          (("1"
                                            (expand "image")
                                            (("1"
                                              (skosimp)
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (expand
                                                   "inverse_image")
                                                  (("1"
                                                    (expand "member")
                                                    (("1"
                                                      (inst -2 "x!2")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (replace 1 2)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (expand
                                                 "inverse_image")
                                                (("2"
                                                  (expand "member")
                                                  (("2"
                                                    (expand "image")
                                                    (("2"
                                                      (inst
                                                       +
                                                       "inverse_alt(f!1)(x!1)")
                                                      (("1"
                                                        (inst -3 "x!1")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (flatten)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (flatten) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (flatten) nil nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp)
                    (("2" (expand "bijective?")
                      (("2" (flatten)
                        (("2" (expand "injective?")
                          (("2" (inst - "f!1(x!1)")
                            (("2"
                              (inst - "inverse_alt(f!1)(f!1(x!1))"
                               "x!1")
                              (("1" (assert) nil nil)
                               ("2" (flatten) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("3" (skosimp) nil nil))
                  nil)
                 ("2" (hide-all-but (-1 -4 1))
                  (("2" (skosimp)
                    (("2" (typepred "inverse_alt(f!1)")
                      (("1" (expand "inverse?")
                        (("1" (inst - "y!1")
                          (("1" (split -1)
                            (("1" (propax) nil nil)
                             ("2" (expand "bijective?")
                              (("2"
                                (flatten)
                                (("2"
                                  (expand "surjective?")
                                  (("2" (inst -3 "y!1") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (flatten) nil nil))
                      nil))
                    nil))
                  nil)
                 ("3" (skosimp) nil nil))
                nil)
               ("2" (hide-all-but (-2 1))
                (("2" (expand "fullset")
                  (("2" (expand "nonempty?")
                    (("2" (expand "empty?")
                      (("2" (skosimp) (("2" (inst + "x!1") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but (-1 1))
              (("2" (expand "fullset")
                (("2" (expand "nonempty?")
                  (("2" (expand "empty?")
                    (("2" (skosimp)
                      (("2" (inst - "f!1(x!1)")
                        (("2" (expand "member")
                          (("2" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "nonempty?")
            (("2" (case "empty?(fullset[T2])")
              (("1" (rewrite "emptyset_is_empty?")
                (("1" (rewrite "emptyset_is_empty?")
                  (("1" (split)
                    (("1" (flatten)
                      (("1" (skosimp)
                        (("1" (case-replace "X!1=emptyset[T1]")
                          (("1" (rewrite "image_emptyset")
                            (("1" (expand "open?")
                              (("1"
                                (expand "member")
                                (("1"
                                  (typepred "S")
                                  (("1"
                                    (typepred "T")
                                    (("1"
                                      (expand "topology?")
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (expand "topology_empty?")
                                          (("1"
                                            (expand "member")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (apply-extensionality 1 :hide? t)
                            (("2" (expand "emptyset")
                              (("2"
                                (rewrite
                                 "extensionality_postulate"
                                 -5
                                 :dir
                                 rl)
                                (("2"
                                  (inst -5 "x!1")
                                  (("2"
                                    (expand "fullset")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp*)
                      (("2" (expand "continuous?")
                        (("2" (split)
                          (("1" (skosimp)
                            (("1"
                              (rewrite "extensionality_postulate" -3
                               :dir rl)
                              (("1"
                                (inst -3 "x!1")
                                (("1"
                                  (expand "emptyset")
                                  (("1"
                                    (expand "fullset")
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skosimp)
                            (("2"
                              (rewrite "extensionality_postulate" -2
                               :dir rl)
                              (("2"
                                (inst -2 "x!1")
                                (("2"
                                  (expand "emptyset")
                                  (("2"
                                    (expand "fullset")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (expand "fullset")
                  (("2" (expand "empty?")
                    (("2" (skosimp)
                      (("2" (expand "member")
                        (("2" (expand "bijective?")
                          (("2" (flatten)
                            (("2" (expand "surjective?")
                              (("2"
                                (inst -3 "x!1")
                                (("2"
                                  (skosimp)
                                  (("2" (inst - "x!2") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((homeomorphism? const-decl "bool" homeomorphism_def nil)
    (fullset_is_clopen name-judgement "clopen" homeomorphism_def nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (TRUE const-decl "bool" booleans nil)
    (Y!1 skolem-const-decl "set[T1]" homeomorphism_def nil)
    (f!1 skolem-const-decl "[T1 -> T2]" homeomorphism_def nil)
    (x!1 skolem-const-decl "T2" homeomorphism_def nil)
    (surjective? const-decl "bool" functions nil)
    (surjective_image_inverse_image formula-decl nil function_image_bis
     "structures/")
    (S formal-const-decl "topology[T1]" homeomorphism_def nil)
    (T formal-const-decl "topology[T2]" homeomorphism_def 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)
    (continuous_open_sets formula-decl nil continuity nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (image const-decl "set[R]" function_image nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (extensionality formula-decl nil functions nil)
    (injective_inverse_image_image formula-decl nil function_image_bis
     "structures/")
    (injective? const-decl "bool" functions nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (FALSE const-decl "bool" booleans nil)
    (inverse_alt const-decl "inverses(f)" function_inverse_alt nil)
    (inverses nonempty-type-eq-decl nil function_inverse_alt nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (empty? const-decl "bool" sets nil)
    (fullset_is_clopen name-judgement "clopen" homeomorphism_def nil)
    (emptyset_is_compact name-judgement "compact" homeomorphism_def
     nil)
    (emptyset_is_clopen name-judgement "clopen" homeomorphism_def nil)
    (continuous? const-decl "bool" continuity_def nil)
    (emptyset const-decl "set" sets nil)
    (open? const-decl "bool" topology nil)
    (topology_empty? const-decl "bool" topology_prelim nil)
    (image_emptyset formula-decl nil function_image_bis "structures/")
    (extensionality_postulate formula-decl nil functions nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_clopen name-judgement "clopen" homeomorphism_def nil)
    (emptyset_is_compact name-judgement "compact" homeomorphism_def
     nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil homeomorphism_def nil)
    (T1 formal-type-decl nil homeomorphism_def nil))
   shostak)))

quality97%

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