products/Sources/formale Sprachen/PVS/topology/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: connected_def.prf   Sprache: Lisp

Original von: PVS©
(connected_def
 (connected_def 0
  (connected_def-1 nil 3364275454
   ("" (skosimp*)
    (("" (typepred "U!1")
      (("" (expand "connected?")
        (("" (split)
          (("1" (skosimp*)
            (("1" (typepred "A!1")
              (("1" (typepred "B!1")
                (("1" (case-replace "B!1=complement(A!1)")
                  (("1" (inst - "A!1")
                    (("1" (assert)
                      (("1" (hide-all-but (-4 -5 -6))
                        (("1" (split)
                          (("1" (replace -1)
                            (("1" (hide-all-but -2)
                              (("1" (grind) nil nil)) nil))
                            nil)
                           ("2" (replace -1)
                            (("2" (hide-all-but -3)
                              (("2" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2"
                    (lemma "extensionality_postulate"
                     ("f" "Union(U!1)" "g" "union(A!1, B!1)"))
                    (("2" (replace -1 -8 rl)
                      (("2" (hide -1 -4)
                        (("2" (expand "union")
                          (("2" (expand "member")
                            (("2" (apply-extensionality 1 :hide? t)
                              (("2"
                                (case-replace "B!1(x!1)")
                                (("1"
                                  (expand "disjoint?")
                                  (("1"
                                    (expand "intersection")
                                    (("1"
                                      (expand "empty?")
                                      (("1"
                                        (inst - "x!1")
                                        (("1"
                                          (inst - "x!1")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (expand "complement")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (assert)
                                  (("2"
                                    (expand "complement")
                                    (("2"
                                      (inst - "x!1")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "topology?")
                                          (("2"
                                            (flatten)
                                            (("2"
                                              (expand "topology_full?")
                                              (("2"
                                                (expand "Union")
                                                (("2"
                                                  (inst + "fullset[T]")
                                                  (("1"
                                                    (expand "fullset")
                                                    (("1"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skosimp*)
            (("2" (inst - "A!1" "complement(A!1)")
              (("2" (rewrite "emptyset_is_empty?" 1 :dir rl)
                (("2" (rewrite "fullset_is_full?" 2 :dir rl)
                  (("2" (expand "nonempty?")
                    (("2" (assert)
                      (("2" (expand "disjoint?")
                        (("2" (expand "complement" -1 2)
                          (("2" (expand "complement" -1 2)
                            (("2" (expand "intersection")
                              (("2"
                                (expand "union")
                                (("2"
                                  (expand "empty?" -1 2)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (split -1)
                                      (("1" (skosimp) nil nil)
                                       ("2"
                                        (apply-extensionality
                                         1
                                         :hide?
                                         t)
                                        (("2"
                                          (typepred "A!1")
                                          (("2"
                                            (case-replace "A!1(x!1)")
                                            (("1"
                                              (expand "Union")
                                              (("1"
                                                (inst + "A!1")
                                                nil
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "Union")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (inst
                                                   +
                                                   "complement(A!1)")
                                                  (("2"
                                                    (expand
                                                     "complement")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("3"
                                        (expand "full?")
                                        (("3"
                                          (skosimp)
                                          (("3"
                                            (expand "empty?")
                                            (("3"
                                              (inst - "x!1")
                                              (("3"
                                                (expand "complement")
                                                (("3"
                                                  (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)
   ((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)
    (T formal-type-decl nil connected_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (complement const-decl "set" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (nonempty? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (fullset const-decl "set" sets nil)
    (topology_full? const-decl "bool" topology_prelim nil)
    (U!1 skolem-const-decl "topology[T]" connected_def nil)
    (disjoint? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (union const-decl "set" sets nil) (Union const-decl "set" sets nil)
    (extensionality_postulate formula-decl nil functions nil)
    (A!1 skolem-const-decl "(U!1)" connected_def nil)
    (fullset_is_full? formula-decl nil sets_lemmas nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (full? const-decl "bool" sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (connected? const-decl "bool" topology_prelim nil))
   shostak))
 (connected_def2 0
  (connected_def2-1 nil 3364277745
   ("" (skosimp)
    (("" (typepred "U!1")
      (("" (rewrite "connected_def")
        (("" (split)
          (("1" (skosimp*)
            (("1" (typepred "f!1")
              (("1" (rewrite "continuous_open_sets")
                (("1" (expand "surjective?")
                  (("1" (inst-cp - "false")
                    (("1" (inst - "true")
                      (("1" (skosimp*)
                        (("1" (inst-cp -4 "singleton(false)")
                          (("1" (inst -4 "singleton(true)")
                            (("1" (split -4)
                              (("1"
                                (split -5)
                                (("1"
                                  (case-replace
                                   "inverse_image(f!1, singleton(FALSE)) = complement(inverse_image(f!1, singleton(TRUE)))")
                                  (("1"
                                    (name-replace
                                     "AA"
                                     "inverse_image(f!1, singleton(TRUE))")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (case "AA(x!1)")
                                        (("1"
                                          (case "complement(AA)(x!2)")
                                          (("1"
                                            (hide -5 -6)
                                            (("1"
                                              (expand "open?")
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (inst
                                                   -
                                                   "AA"
                                                   "complement(AA)")
                                                  (("1"
                                                    (split -5)
                                                    (("1"
                                                      (expand
                                                       "disjoint?")
                                                      (("1"
                                                        (expand
                                                         "complement")
                                                        (("1"
                                                          (expand
                                                           "intersection")
                                                          (("1"
                                                            (expand
                                                             "empty?")
                                                            (("1"
                                                              (skosimp)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (flatten)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (apply-extensionality
                                                       1
                                                       :hide?
                                                       t)
                                                      (("2"
                                                        (expand
                                                         "complement")
                                                        (("2"
                                                          (expand
                                                           "union")
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (case-replace
                                                               "AA(x!3)")
                                                              (("1"
                                                                (expand
                                                                 "Union")
                                                                (("1"
                                                                  (inst
                                                                   +
                                                                   "AA")
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                (("2"
                                                                  (expand
                                                                   "Union")
                                                                  (("2"
                                                                    (inst
                                                                     +
                                                                     "{x: T | NOT AA(x)}")
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (expand
                                                       "nonempty?")
                                                      (("3"
                                                        (expand
                                                         "empty?")
                                                        (("3"
                                                          (inst
                                                           -
                                                           "x!1")
                                                          (("3"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("4"
                                                      (expand
                                                       "nonempty?")
                                                      (("4"
                                                        (expand
                                                         "empty?")
                                                        (("4"
                                                          (inst
                                                           -
                                                           "x!2")
                                                          (("4"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide-all-but (-5 1))
                                            (("2"
                                              (grind)
                                              (("2"
                                                (expand "AA")
                                                (("2"
                                                  (expand
                                                   "inverse_image")
                                                  (("2"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but (-3 1))
                                          (("2"
                                            (grind)
                                            (("2"
                                              (expand "AA")
                                              (("2" (grind) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (apply-extensionality 1 :hide? t)
                                    (("2"
                                      (hide-all-but 1)
                                      (("2"
                                        (expand "complement")
                                        (("2"
                                          (expand "singleton")
                                          (("2"
                                            (expand "inverse_image")
                                            (("2"
                                              (expand "member")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but 1)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (hide-all-but 1)
                                (("2" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skosimp*)
            (("2" (name "F" "lambda (x:T): A!1(x)")
              (("2" (typepred "B!1")
                (("2" (case-replace "B!1=complement(A!1)")
                  (("1" (hide-all-but (-2 -4 -5 -6 -9))
                    (("1" (typepred "A!1")
                      (("1" (case "surjective?[T,bool](A!1)")
                        (("1" (inst - "A!1")
                          (("1" (rewrite "continuous_open_sets")
                            (("1" (skosimp)
                              (("1"
                                (case
                                 "Y!1=emptyset[bool] OR Y!1=singleton(true) OR Y!1=singleton(false) OR Y!1=fullset[bool]")
                                (("1"
                                  (split -1)
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (case-replace
                                       "inverse_image(A!1, emptyset[bool]) = emptyset[T]")
                                      (("1"
                                        (expand "topology?")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (expand "topology_empty?")
                                            (("1"
                                              (expand "open?")
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide-all-but 1)
                                        (("2"
                                          (apply-extensionality
                                           1
                                           :hide?
                                           t)
                                          (("2"
                                            (expand "emptyset")
                                            (("2"
                                              (expand "inverse_image")
                                              (("2"
                                                (expand "member")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (replace -1)
                                    (("2"
                                      (case-replace
                                       "inverse_image(A!1, singleton(TRUE)) = A!1")
                                      (("1"
                                        (expand "open?")
                                        (("1" (assert) nil nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (apply-extensionality
                                           1
                                           :hide?
                                           t)
                                          (("2"
                                            (expand "singleton")
                                            (("2"
                                              (expand "inverse_image")
                                              (("2"
                                                (expand "member")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (replace -1)
                                    (("3"
                                      (case-replace
                                       "inverse_image(A!1, singleton(FALSE)) = complement(A!1)")
                                      (("1"
                                        (expand "open?")
                                        (("1" (assert) nil nil))
                                        nil)
                                       ("2"
                                        (apply-extensionality
                                         1
                                         :hide?
                                         t)
                                        (("2"
                                          (expand "complement")
                                          (("2"
                                            (expand "singleton")
                                            (("2"
                                              (expand "inverse_image")
                                              (("2"
                                                (expand "member")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("4"
                                    (replace -1)
                                    (("4"
                                      (case-replace
                                       "inverse_image(A!1, fullset[bool]) = fullset[T]")
                                      (("1"
                                        (expand "topology?")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (expand "topology_full?")
                                            (("1"
                                              (expand "open?")
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (apply-extensionality
                                         1
                                         :hide?
                                         t)
                                        (("2"
                                          (expand "fullset")
                                          (("2"
                                            (expand "inverse_image")
                                            (("2"
                                              (expand "member")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide -2 -3 2)
                                  (("2"
                                    (flatten)
                                    (("2"
                                      (apply-extensionality 2 :hide? t)
                                      (("2"
                                        (apply-extensionality
                                         3
                                         :hide?
                                         t)
                                        (("2"
                                          (expand "singleton")
                                          (("2"
                                            (case-replace "x!1")
                                            (("1"
                                              (case-replace "x!2")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (assert)
                                                (("2"
                                                  (apply-extensionality
                                                   4
                                                   :hide?
                                                   t)
                                                  (("2"
                                                    (expand "emptyset")
                                                    (("2"
                                                      (hide-all-but
                                                       (-1 2 3))
                                                      (("2"
                                                        (ground)
                                                        (("2"
                                                          (case-replace
                                                           "x!3")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (assert)
                                              (("2"
                                                (case-replace "x!2")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (apply-extensionality
                                                     3
                                                     :hide?
                                                     t)
                                                    (("1"
                                                      (expand
                                                       "fullset")
                                                      (("1"
                                                        (case-replace
                                                         "x!3")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "surjective?")
                          (("2" (skosimp)
                            (("2" (case-replace "y!1")
                              (("1"
                                (expand "nonempty?" -5)
                                (("1"
                                  (expand "empty?")
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (inst + "x!1")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "nonempty?" -5)
                                (("2"
                                  (expand "complement")
                                  (("2"
                                    (expand "empty?")
                                    (("2"
                                      (skosimp)
                                      (("2"
                                        (inst + "x!1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -1 -2 -3)
                    (("2" (apply-extensionality 1 :hide? t)
                      (("2" (expand "disjoint?")
                        (("2" (expand "empty?")
                          (("2" (inst - "x!1")
                            (("2" (expand "intersection")
                              (("2"
                                (expand "member")
                                (("2"
                                  (expand "complement")
                                  (("2"
                                    (case-replace "A!1(x!1)")
                                    (("1" (assert) nil nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (lemma
                                         "extensionality_postulate"
                                         ("f"
                                          "Union(U!1)"
                                          "g"
                                          "union(A!1, B!1)"))
                                        (("2"
                                          (replace -1 -4 rl)
                                          (("2"
                                            (inst -4 "x!1")
                                            (("2"
                                              (expand "union")
                                              (("2"
                                                (expand "member")
                                                (("2"
                                                  (expand "Union")
                                                  (("2"
                                                    (expand
                                                     "topology?")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (expand
                                                         "topology_full?")
                                                        (("2"
                                                          (expand
                                                           "member")
                                                          (("2"
                                                            (inst
                                                             +
                                                             "fullset[T]")
                                                            (("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))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (T formal-type-decl nil connected_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil)
    (TRUE const-decl "bool" booleans nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (nonempty_powerset application-judgement "(nonempty?[set[T]])"
     sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (powerset const-decl "setofsets" sets nil)
    (subset? const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (discrete_topology_set const-decl "setofsets[T]" topology_prelim
     nil)
    (complement const-decl "set" sets nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (open? const-decl "bool" topology nil)
    (U!1 skolem-const-decl "topology[T]" connected_def nil)
    (AA skolem-const-decl "set[T]" connected_def nil)
    (nonempty? const-decl "bool" sets nil)
    (Union const-decl "set" sets nil) (union const-decl "set" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (disjoint? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (FALSE const-decl "bool" booleans nil)
    (discrete_topology const-decl "topology" topology_prelim nil)
    (continuous_open_sets formula-decl nil continuity nil)
    (A!1 skolem-const-decl "(U!1)" connected_def nil)
    (topology_empty? const-decl "bool" topology_prelim nil)
    (topology_full? const-decl "bool" topology_prelim nil)
    (emptyset const-decl "set" sets nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (extensionality_postulate formula-decl nil functions nil)
    (connected_def formula-decl nil connected_def nil))
   shostak)))


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