Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: homeomorphic_transitive.prf Sprache: Lisp

Original von: PVS^©

(homeomorphic_transitive
(homeomorphic_transitive 0
  (homeomorphic_transitive-1 nil 3301538739
   ("" (expand "homeomorphic?")
    (("" (skosimp*)
      (("" (expand "homeomorphism?")
        (("" (flatten)
          (("" (inst + "f!2 o f!1")
            ((""
              (lemma "composition_bijective[T1,T2,T3]"
               ("f1" "f!1" "f2" "f!2"))
              (("1" (assert)
                (("1"
                  (lemma "composition_continuous[T1,S,T2,T,T3,U]"
                   ("f" "f!2" "g" "f!1"))
                  (("1" (assert)
                    (("1" (rewrite "composition_inverse_alt" 1)
                      (("1"
                        (lemma
                         "composition_continuous[T3,U,T2,T,T1,S]")
                        (("1" (case "nonempty?(fullset[T1])")
                          (("1" (case "EXISTS (x:T1): TRUE")
                            (("1" (case "EXISTS (y:T2): TRUE")
                              (("1"
                                (case "EXISTS (z:T3): TRUE")
                                (("1"
                                  (inst
                                   -
                                   "inverse_alt(f!1)"
                                   "inverse_alt(f!2)")
                                  (("1" (assert) nil nil)
                                   ("2" (flatten) nil nil)
                                   ("3" (flatten) nil nil))
                                  nil)
                                 ("2"
                                  (skolem! -)
                                  (("2" (inst + "f!2(y!1)") nil nil))
                                  nil))
                                nil)
                               ("2"
                                (skolem! -)
                                (("2" (inst + "f!1(x!1)") nil nil))
                                nil))
                              nil)
                             ("2" (hide-all-but (-1 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" (expand "nonempty?")
                            (("2" (rewrite "emptyset_is_empty?" -1)
                              (("2"
                                (hide -2 -3 -4 -6 -7 -9 -10)
                                (("2"
                                  (expand "bijective?")
                                  (("2"
                                    (flatten)
                                    (("2"
                                      (expand "continuous?")
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (expand "surjective?")
                                          (("2"
                                            (inst -5 "x!1")
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (inst - "x!2")
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (rewrite
                                                     "extensionality_postulate"
                                                     -1
                                                     :dir
                                                     rl)
                                                    (("2"
                                                      (inst - "x!3")
                                                      (("2"
                                                        (expand
                                                         "emptyset")
                                                        (("2"
                                                          (expand
                                                           "fullset")
                                                          (("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)
               ("2" (propax) nil nil) ("3" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (U formal-const-decl "topology[T3]" homeomorphic_transitive nil)
    (T formal-const-decl "topology[T2]" homeomorphic_transitive nil)
    (S formal-const-decl "topology[T1]" homeomorphic_transitive 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)
    (composition_continuous formula-decl nil composition_continuity
     nil)
    (composition_inverse_alt formula-decl nil function_props_aux
     "structures/")
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (empty? const-decl "bool" sets 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)
    (TRUE const-decl "bool" booleans nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (continuous? const-decl "bool" continuity_def nil)
    (surjective? const-decl "bool" functions nil)
    (extensionality_postulate formula-decl nil functions nil)
    (emptyset const-decl "set" sets nil)
    (O const-decl "T3" function_props nil)
    (T2 formal-type-decl nil homeomorphic_transitive nil)
    (T3 formal-type-decl nil homeomorphic_transitive nil)
    (T1 formal-type-decl nil homeomorphic_transitive nil)
    (homeomorphism? const-decl "bool" homeomorphism_def nil)
    (homeomorphic? const-decl "bool" homeomorphism_def nil))
   shostak)))

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