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: hausdorff_convergence.prf   Sprache: Lisp

Original von: PVS©
(hausdorff_convergence
 (unique_limit 0
  (unique_limit-1 nil 3358828139
   ("" (skosimp)
    (("" (typepred "S")
      (("" (expand "hausdorff_space?")
        (("" (flatten)
          (("" (expand "hausdorff?")
            (("" (expand "is_T2?")
              (("" (inst - "l1!1" "l2!1")
                (("" (assert)
                  (("" (skosimp)
                    (("" (expand "convergence?")
                      (("" (inst - "U!1")
                        (("1" (inst - "V!1")
                          (("1" (assert)
                            (("1" (skosimp*)
                              (("1"
                                (inst - "max(n!1,n!2)")
                                (("1"
                                  (inst - "max(n!1,n!2)")
                                  (("1"
                                    (expand "disjoint?")
                                    (("1"
                                      (expand "empty?")
                                      (("1"
                                        (inst - "u!1(max(n!1, n!2))")
                                        (("1"
                                          (expand "intersection")
                                          (("1"
                                            (expand "member")
                                            (("1"
                                              (name-replace
                                               "DRL1"
                                               "u!1(max(n!1, n!2))")
                                              (("1"
                                                (hide-all-but
                                                 (-4 -5 1))
                                                (("1" (grind) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (typepred "V!1")
                            (("2" (expand "open?")
                              (("2"
                                (expand "member")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "open?")
                          (("2" (typepred "U!1")
                            (("2" (expand "member")
                              (("2" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "hausdorff" hausdorff_convergence nil)
    (hausdorff nonempty-type-eq-decl nil topology_prelim nil)
    (hausdorff_space? 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 hausdorff_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (is_T2? const-decl "bool" topology_prelim nil)
    (member const-decl "bool" sets nil)
    (convergence? const-decl "bool" topological_convergence nil)
    (V!1 skolem-const-decl "(S)" hausdorff_convergence nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sequence type-eq-decl nil sequences nil)
    (disjoint? const-decl "bool" sets nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (nat_max application-judgement "{k: nat | i <= k AND j <= k}"
     real_defs nil)
    (nonneg_rat_max application-judgement
     "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
    (open nonempty-type-eq-decl nil topology nil)
    (U!1 skolem-const-decl "(S)" hausdorff_convergence nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (hausdorff? const-decl "bool" topology_prelim nil))
   shostak))
 (limit_def 0
  (limit_def-1 nil 3358828249
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (replace -1 1 rl) (("1" (rewrite "limit_lemma") nil nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (lemma "limit_lemma" ("v" "v!1"))
          (("2"
            (lemma "unique_limit"
             ("u" "v!1" "l1" "limit(v!1)" "l2" "l!1"))
            (("1" (assert) nil nil)
             ("2" (typepred "S")
              (("2" (expand "hausdorff_space?")
                (("2" (flatten) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "hausdorff" hausdorff_convergence nil)
    (hausdorff nonempty-type-eq-decl nil topology_prelim nil)
    (hausdorff_space? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil hausdorff_convergence nil)
    (convergent type-eq-decl nil topological_convergence nil)
    (convergent? const-decl "bool" topological_convergence nil)
    (sequence type-eq-decl nil sequences nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (limit_lemma formula-decl nil topological_convergence nil)
    (unique_limit formula-decl nil hausdorff_convergence nil)
    (limit const-decl "T" topological_convergence nil))
   shostak))
 (singleton_is_closed 0
  (singleton_is_closed-1 nil 3364193951
   ("" (skosimp)
    (("" (typepred "S")
      (("" (expand "hausdorff_space?")
        (("" (flatten)
          (("" (expand "hausdorff?")
            (("" (expand "is_T2?")
              (("" (name "A" "{(U:(S)) | NOT U(x!1)}")
                (("" (case "forall (x:T): Union(A)(x) IFF x /= x!1")
                  (("1" (lemma "open_Union" ("Y" "A"))
                    (("1" (split -1)
                      (("1"
                        (case-replace
                         "Union(extend[setof[T], (S), bool, FALSE](A)) = complement(singleton(x!1))")
                        (("1" (expand "closed?")
                          (("1" (expand "open?")
                            (("1" (propax) nil nil)) nil))
                          nil)
                         ("2" (hide-all-but (-2 1))
                          (("2" (apply-extensionality 1 :hide? t)
                            (("2" (expand "singleton")
                              (("2"
                                (expand "complement")
                                (("2"
                                  (expand "member")
                                  (("2"
                                    (inst - "x!2")
                                    (("2"
                                      (replace -1)
                                      (("2"
                                        (hide -1)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand "A")
                        (("2" (expand "extend")
                          (("2" (expand "open?")
                            (("2" (expand "every")
                              (("2"
                                (expand "member")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (skosimp)
                      (("2" (case-replace "x!2=x!1")
                        (("1" (assert)
                          (("1" (expand "extend")
                            (("1" (expand "A")
                              (("1"
                                (expand "Union")
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (typepred "a!1")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (expand "extend")
                            (("2" (expand "A")
                              (("2"
                                (expand "Union")
                                (("2"
                                  (inst - "x!2" "x!1")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (skosimp)
                                      (("2"
                                        (inst + "U!1")
                                        (("2"
                                          (expand "disjoint?")
                                          (("2"
                                            (expand "intersection")
                                            (("2"
                                              (expand "empty?")
                                              (("2"
                                                (inst - "x!1")
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "hausdorff" hausdorff_convergence nil)
    (hausdorff nonempty-type-eq-decl nil topology_prelim nil)
    (hausdorff_space? 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 hausdorff_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (is_T2? const-decl "bool" topology_prelim nil)
    (/= const-decl "boolean" notequal nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (Union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (closed? const-decl "bool" topology nil)
    (open? const-decl "bool" topology nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (singleton_is_compact application-judgement "compact"
     hausdorff_convergence nil)
    (complement const-decl "set" sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (every const-decl "bool" sets nil)
    (A skolem-const-decl "[(S) -> bool]" hausdorff_convergence nil)
    (open_Union formula-decl nil topology nil)
    (disjoint? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (x!1 skolem-const-decl "T" hausdorff_convergence nil)
    (U!1 skolem-const-decl "(S)" hausdorff_convergence nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (hausdorff? const-decl "bool" topology_prelim nil))
   nil))
 (compact_is_closed 0
  (compact_is_closed-1 nil 3397556799
   ("" (skolem + ("X"))
    (("" (typepred "X")
      (("" (name "B" "difference(fullset[T],X)")
        (("" (case "nonempty?(B)")
          (("1"
            (case "forall x: B(x) => EXISTS (U:open): U(x) & subset?(U,B)")
            (("1"
              (name "BB" "Union({U:set[T] | open?(U) & subset?(U,B)})")
              (("1" (case-replace "BB=B")
                (("1"
                  (lemma "open_Union"
                   ("Y" "{U: set[T] | open?(U) & subset?(U, B)}"))
                  (("1" (replace -3)
                    (("1" (split -1)
                      (("1"
                        (lemma "difference_intersection"
                         ("a" "fullset[T]" "b" "X"))
                        (("1" (replace -7)
                          (("1" (lemma "closed_complement" ("A" "B"))
                            (("1" (assert)
                              (("1"
                                (replace -2 -1)
                                (("1"
                                  (rewrite "demorgan2")
                                  (("1"
                                    (rewrite "complement_complement")
                                    (("1"
                                      (rewrite "complement_fullset[T]")
                                      (("1"
                                        (rewrite "union_commutative")
                                        (("1"
                                          (rewrite "union_empty")
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand "every") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (apply-extensionality :hide? t)
                    (("2" (replace -1 1 rl)
                      (("2" (expand "Union")
                        (("2" (case-replace "B(x!1)")
                          (("1" (inst - "x!1")
                            (("1" (assert)
                              (("1"
                                (skosimp)
                                (("1" (inst + "U!1") nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (replace 1 2)
                            (("2" (assert)
                              (("2"
                                (skosimp)
                                (("2"
                                  (typepred "a!1")
                                  (("2"
                                    (expand "subset?")
                                    (("2"
                                      (inst - "x!1")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (typepred "S")
                (("2" (expand "hausdorff_space?")
                  (("2" (flatten) nil nil)) nil))
                nil))
              nil)
             ("2" (case-replace "X=emptyset[T]")
              (("1" (rewrite "emptyset_is_closed") nil nil)
               ("2" (case "nonempty?(X)")
                (("1" (hide 1 3)
                  (("1" (skosimp)
                    (("1" (expand "compact?")
                      (("1" (expand "compact_subset?")
                        (("1"
                          (name "UV"
                                "lambda (y:(X)): choose({uv:[set[T],set[T]]| open?(uv`1) & open?(uv`2) & uv`1(x!1) & uv`2(y) & disjoint?(uv`1,uv`2)})")
                          (("1"
                            (inst -6
                             "{a:set[T] | exists (y:(X)): UV(y)`2 = a}")
                            (("1" (split -6)
                              (("1"
                                (skosimp)
                                (("1"
                                  (case
                                   "forall (v:(V!1)): exists (u: open): disjoint?(v,u) & u(x!1)")
                                  (("1"
                                    (expand "finite_cover?")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (case
                                         "forall (v:(V!1)): nonempty?[open]({u: open | disjoint?(v, u) & u(x!1)})")
                                        (("1"
                                          (lemma
                                           "finite_image[(V!1),open]"
                                           ("f"
                                            "lambda (v: (V!1)): choose[open]({u:open | disjoint?(v, u) & u(x!1)})"
                                            "S"
                                            "V!1"))
                                          (("1"
                                            (lemma
                                             "open_Intersection"
                                             ("Y"
                                              "(image[(V!1), open]
               (LAMBDA (v: (V!1)):
                  choose[open]({u: open | disjoint?(v, u) & u(x!1)}),
                restrict[setof[T], ((V!1)), boolean](V!1)))"))
                                            (("1"
                                              (expand "restrict")
                                              (("1"
                                                (expand "image")
                                                (("1"
                                                  (expand "extend")
                                                  (("1"
                                                    (split -1)
                                                    (("1"
                                                      (hide -2 -6 -8)
                                                      (("1"
                                                        (inst
                                                         +
                                                         "(Intersection(LAMBDA (t: setof[T]):
                           IF open?[T, S](t)
                             THEN EXISTS (x:
                                          (LAMBDA (s: (((V!1)))): TRUE)):
                                    t
                                    =
                                    choose[open]
                                    ({u_1: open
                                      |
                                      disjoint?(x, u_1) & u_1(x!1)})
                           ELSE FALSE
                           ENDIF))")
                                                        (("1"
                                                          (hide -1)
                                                          (("1"
                                                            (split)
                                                            (("1"
                                                              (expand
                                                               "Intersection")
                                                              (("1"
                                                                (skosimp)
                                                                (("1"
                                                                  (typepred
                                                                   "a!1")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (skosimp)
                                                                      (("1"
                                                                        (typepred
                                                                         "x!2")
                                                                        (("1"
                                                                          (inst
                                                                           -4
                                                                           "x!2")
                                                                          (("1"
                                                                            (lemma
                                                                             "choose_member[open]"
                                                                             ("a"
                                                                              "{u_1: open | disjoint?(x!2, u_1) & u_1(x!1)}"))
                                                                            (("1"
                                                                              (expand
                                                                               "nonempty?")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "Intersection")
                                                              (("2"
                                                                (expand
                                                                 "subset?")
                                                                (("2"
                                                                  (expand
                                                                   "member")
                                                                  (("2"
                                                                    (skosimp*)
                                                                    (("2"
                                                                      (case
                                                                       "X(x!2)")
                                                                      (("1"
                                                                        (expand
                                                                         "cover?")
                                                                        (("1"
                                                                          (expand
                                                                           "subset?")
                                                                          (("1"
                                                                            (inst
                                                                             -6
                                                                             "x!2")
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (expand
                                                                                 "Union"
                                                                                 -6)
                                                                                (("1"
                                                                                  (skosimp)
                                                                                  (("1"
                                                                                    (typepred
                                                                                     "a!1")
                                                                                    (("1"
                                                                                      (inst
                                                                                       -
                                                                                       "choose[open]
                                 ({u_1: open |
                                     disjoint?(a!1, u_1) & u_1(x!1)})")
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "choose_member[open]"
                                                                                         ("a"
                                                                                          "{u_1: open | disjoint?(a!1, u_1) & u_1(x!1)}"))
                                                                                        (("1"
                                                                                          (split
                                                                                           -1)
                                                                                          (("1"
                                                                                            (expand
                                                                                             "member")
                                                                                            (("1"
                                                                                              (flatten)
                                                                                              (("1"
                                                                                                (name-replace
                                                                                                 "AA"
                                                                                                 "choose({u_1: open | disjoint?(a!1, u_1) & u_1(x!1)})")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "disjoint?")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "empty?")
                                                                                                    (("1"
                                                                                                      (inst
                                                                                                       -
                                                                                                       "x!2")
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "intersection")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "member")
                                                                                                          (("1"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (inst
                                                                                                   -
                                                                                                   "a!1")
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (inst
                                                                                             -
                                                                                             "a!1")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "nonempty?")
                                                                                              (("2"
                                                                                                (propax)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (inst
                                                                                         +
                                                                                         "a!1")
                                                                                        nil
                                                                                        nil)
                                                                                       ("3"
                                                                                        (inst
                                                                                         -
                                                                                         "a!1")
                                                                                        nil
                                                                                        nil)
                                                                                       ("4"
                                                                                        (typepred
                                                                                         "S")
                                                                                        (("4"
                                                                                          (expand
                                                                                           "hausdorff_space?")
                                                                                          (("4"
                                                                                            (flatten)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (expand
                                                                         "B"
                                                                         2)
                                                                        (("2"
                                                                          (expand
                                                                           "fullset")
                                                                          (("2"
                                                                            (expand
                                                                             "difference")
                                                                            (("2"
                                                                              (expand
                                                                               "member")
                                                                              (("2"
                                                                                (propax)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (skosimp)
                                                          nil
                                                          nil)
                                                         ("3"
                                                          (skosimp)
                                                          (("3"
                                                            (skosimp)
                                                            (("3"
                                                              (typepred
                                                               "S")
                                                              (("3"
                                                                (expand
                                                                 "hausdorff_space?")
                                                                (("3"
                                                                  (flatten)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("4"
                                                          (typepred
                                                           "S")
                                                          (("4"
                                                            (expand
                                                             "hausdorff_space?")
                                                            (("4"
                                                              (flatten)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide-all-but
                                                       (-1 1))
                                                      (("2"
                                                        (expand
                                                         "is_finite")
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (inst
                                                             +
                                                             "N!1"
                                                             "f!1")
                                                            (("1"
                                                              (expand
                                                               "injective?")
                                                              (("1"
                                                                (skosimp)
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "x1!1"
                                                                   "x2!1")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (skosimp)
                                                              (("2"
                                                                (case-replace
                                                                 "open?[T, S](x2!1)")
                                                                (("1"
                                                                  (split)
                                                                  (("1"
                                                                    (flatten)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (flatten)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (replace
                                                                   1)
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (hide -1 -5 -7 2)
                                                      (("3"
                                                        (expand
                                                         "every")
                                                        (("3"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (typepred "S")
                                              (("2"
                                                (expand
                                                 "hausdorff_space?")
                                                (("2"
                                                  (flatten)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2" (propax) nil nil)
                                           ("3"
                                            (hide-all-but (-4 1))
                                            (("3"
                                              (expand "restrict")
                                              (("3"
                                                (expand "is_finite")
                                                (("3"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but (-1 1))
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (inst - "v!1")
                                              (("2"
                                                (skosimp)
                                                (("2"
                                                  (expand "nonempty?")
                                                  (("2"
                                                    (expand "empty?")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (inst - "u!1")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (skosimp)
                                      (("2"
                                        (expand "subset?")
                                        (("2"
                                          (inst - "v!1")
                                          (("2"
                                            (assert)
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (inst + "UV(y!1)`1")
                                                (("1"
                                                  (typepred "UV(y!1)")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (expand
                                                       "disjoint?")
                                                      (("1"
                                                        (rewrite
                                                         "intersection_commutative")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (typepred "UV(y!1)")
                                                  (("2"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (skosimp)
                                    (("3"
                                      (typepred "S")
                                      (("3"
                                        (expand "hausdorff_space?")
                                        (("3" (flatten) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (expand "open_cover?")
                                  (("2"
                                    (split)
                                    (("1"
                                      (expand "subset?")
                                      (("1"
                                        (expand "member")
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (typepred "UV(y!1)")
                                              (("1"
                                                (replace -6)
                                                (("1"
                                                  (expand "open?")
                                                  (("1"
                                                    (expand "member")
                                                    (("1"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (expand "cover?")
                                      (("2"
                                        (expand "subset?")
                                        (("2"
                                          (expand "member")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (expand "Union")
                                              (("2"
                                                (inst + "UV(x!2)`2")
                                                (("1"
                                                  (typepred "UV(x!2)")
                                                  (("1"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (inst + "x!2")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide -5 2)
                            (("2" (skosimp)
                              (("2"
                                (typepred "y!1")
                                (("2"
                                  (typepred "S")
                                  (("2"
                                    (expand "hausdorff_space?")
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (expand "hausdorff?")
                                        (("2"
                                          (expand "is_T2?")
                                          (("2"
                                            (inst - "x!1" "y!1")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (split -2)
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (expand
                                                     "nonempty?"
                                                     1)
                                                    (("1"
                                                      (expand
                                                       "empty?"
                                                       -6)
                                                      (("1"
                                                        (expand
                                                         "member")
                                                        (("1"
                                                          (inst
                                                           -
                                                           "(U!1,V!1)")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (typepred
                                                               "U!1")
                                                              (("1"
                                                                (typepred
                                                                 "V!1")
                                                                (("1"
                                                                  (expand
                                                                   "open?")
                                                                  (("1"
                                                                    (expand
                                                                     "member")
                                                                    (("1"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 2)
                                                  (("2"
                                                    (replace -6 -4 rl)
                                                    (("2"
                                                      (expand
                                                       "fullset")
                                                      (("2"
                                                        (expand
                                                         "difference")
                                                        (("2"
                                                          (expand
                                                           "member")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (skosimp)
                            (("3" (typepred "S")
                              (("3"
                                (expand "hausdorff_space?")
                                (("3" (flatten) nil nil))
                                nil))
                              nil))
                            nil)
                           ("4" (skosimp)
                            (("4" (typepred "S")
                              (("4"
                                (expand "hausdorff_space?")
                                (("4" (flatten) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "nonempty?")
                  (("2" (rewrite "emptyset_is_empty?") nil nil)) nil))
                nil))
              nil)
             ("3" (skosimp)
              (("3" (typepred "S")
                (("3" (expand "hausdorff_space?")
--> --------------------

--> maximum size reached

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

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