Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: metric_spaces.prf Sprache: Lisp

Original von: PVS^©

(metric_spaces
(fullset_metric_space 0
  (fullset_metric_space-1 nil 3459596594
   ("" (expand "metric_space?")
    (("" (expand "fullset")
      (("" (prop)
        (("1" (expand "space_zero?")
          (("1" (skeep) (("1" (rewrite "metric_zero") nil nil)) nil))
          nil)
         ("2" (expand "space_symmetric?")
          (("2" (skeep) (("2" (rewrite "metric_symmetric") nil nil))
            nil))
          nil)
         ("3" (expand "space_triangle?")
          (("3" (skeep) (("3" (rewrite "metric_triangle") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(open_emptyset 0
  (open_emptyset-1 nil 3295210933
   ("" (expand "open?")
    (("" (expand "interior")
      (("" (apply-extensionality :hide? t)
        (("" (lemma "empty_no_members" ("x" "x!1"))
          (("" (expand "member")
            (("" (replace 1 2)
              (("" (assert)
                (("" (expand "extend") (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((interior const-decl "set[T]" metric_spaces nil)
    (empty_no_members formula-decl nil sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (interior_point? const-decl "bool" metric_spaces nil)
    (emptyset const-decl "set" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (open? const-decl "bool" metric_spaces nil))
   shostak))
(closed_emptyset 0
  (closed_emptyset-1 nil 3295211053
   ("" (expand "closed?")
    (("" (expand "open?")
      (("" (rewrite "complement_emptyset")
        (("" (expand "interior")
          (("" (apply-extensionality :hide? t)
            (("" (lemma "fullset_member" ("x" "x!1"))
              (("" (expand "member")
                (("" (replace -1)
                  (("" (expand "extend")
                    (("" (expand "interior_point?")
                      (("" (assert)
                        (("" (inst + "1")
                          (("" (expand "subset?")
                            (("" (expand "member")
                              ((""
                                (expand "ball")
                                ((""
                                  (skosimp)
                                  ((""
                                    (expand "fullset")
                                    (("" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" metric_spaces nil)
    (interior const-decl "set[T]" metric_spaces nil)
    (fullset_member formula-decl nil sets_lemmas nil)
    (subset? const-decl "bool" sets nil)
    (ball const-decl "set[T]" metric_spaces 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (member const-decl "bool" sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (interior_point? const-decl "bool" metric_spaces nil)
    (fullset const-decl "set" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (complement_emptyset formula-decl nil sets_lemmas nil)
    (closed? const-decl "bool" metric_spaces nil))
   shostak))
(complement_open 0
  (complement_open-1 nil 3293868281
   ("" (expand "closed?")
    (("" (skosimp*)
      (("" (rewrite "complement_complement") (("" (assert) nil nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-type-decl nil metric_spaces nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (closed? const-decl "bool" metric_spaces nil))
   shostak))
(complement_closed 0
  (complement_closed-1 nil 3293868355
   ("" (expand "closed?") (("" (propax) nil nil)) nil)
   ((closed? const-decl "bool" metric_spaces nil)) shostak))
(open_fullset 0
  (open_fullset-1 nil 3295211327
   ("" (rewrite "complement_open")
    (("" (rewrite "complement_fullset")
      (("" (rewrite "closed_emptyset") nil nil)) nil))
    nil)
   ((complement_fullset formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (closed_emptyset formula-decl nil metric_spaces nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (complement_open formula-decl nil metric_spaces nil))
   shostak))
(closed_fullset 0
  (closed_fullset-1 nil 3295211390
   ("" (rewrite "complement_closed")
    (("" (rewrite "complement_fullset")
      (("" (rewrite "open_emptyset") nil nil)) nil))
    nil)
   ((complement_fullset formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (open_emptyset formula-decl nil metric_spaces nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (complement_closed formula-decl nil metric_spaces nil))
   shostak))
(open_in_fullset 0
  (open_in_fullset-1 nil 3459683046
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "open?")
        (("1" (expand "open_in?")
          (("1" (split)
            (("1" (expand "interior")
              (("1" (skosimp*)
                (("1" (decompose-equality)
                  (("1" (inst - "s!1")
                    (("1" (expand "interior_point?")
                      (("1" (skosimp*)
                        (("1" (inst?)
                          (("1" (expand "subset?")
                            (("1" (expand "intersection")
                              (("1"
                                (expand "member")
                                (("1"
                                  (expand "fullset")
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "fullset")
              (("2" (expand "subset?")
                (("2" (expand "member") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (auto-rewrite-theory "sets[T]")
        (("2" (expand "open_in?")
          (("2" (expand "open?")
            (("2" (assert)
              (("2" (expand "interior")
                (("2" (expand "interior_point?")
                  (("2" (apply-extensionality :hide? t)
                    (("2" (case "A!1(x!1)")
                      (("1" (inst - "x!1")
                        (("1" (skosimp*)
                          (("1" (iff)
                            (("1" (prop) (("1" (inst? +) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (iff) (("2" (prop) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open_in? const-decl "bool" metric_spaces nil)
    (interior const-decl "set[T]" metric_spaces nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (interior_point? const-decl "bool" metric_spaces 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (intersection const-decl "set" sets nil)
    (fullset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (open? const-decl "bool" metric_spaces nil)
    (x!1 skolem-const-decl "T" metric_spaces nil)
    (A!1 skolem-const-decl "set[T]" metric_spaces nil)
    (ball const-decl "set[T]" metric_spaces nil))
   shostak))
(closed_in_fullset 0
  (closed_in_fullset-1 nil 3459772443
   ("" (skosimp*)
    (("" (expand "closed_in?")
      (("" (lemma open_in_fullset)
        (("" (lemma "complement_closed")
          (("" (inst - "A!1")
            (("" (replace -1)
              (("" (hide -1)
                (("" (inst - "complement(A!1)")
                  (("" (replace -1)
                    (("" (lemma "intersection_full[T]")
                      (("" (inst - "complement(A!1)")
                        (("" (replace -1)
                          (("" (lemma "subset_fullset[T]")
                            (("" (inst - "A!1") (("" (prop) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((closed_in? const-decl "bool" metric_spaces nil)
    (complement_closed formula-decl nil metric_spaces nil)
    (complement const-decl "set" sets nil)
    (intersection_full formula-decl nil sets_lemmas nil)
    (subset_fullset formula-decl nil sets_lemmas nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (open_in_fullset formula-decl nil metric_spaces nil))
   shostak))
(ball_open 0
  (ball_open-2 nil 3459679048
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (expand "interior")
        (("" (apply-extensionality)
          (("" (hide 2)
            (("" (case "ball(x!1,r!1)(x!2)")
              (("1" (assert)
                (("1" (expand "interior_point?")
                  (("1" (expand "subset?")
                    (("1" (expand "ball")
                      (("1" (expand "member")
                        (("1" (inst + "r!1 - d(x!1,x!2)")
                          (("1" (skosimp*)
                            (("1" (lemma "fullset_metric_space")
                              (("1"
                                (expand "metric_space?")
                                (("1"
                                  (assert)
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (expand "space_triangle?")
                                      (("1"
                                        (inst - "x!1" "x!2" "x!3")
                                        (("1" (assert) nil nil)
                                         ("2"
                                          (expand "fullset")
                                          (("2" (propax) nil nil))
                                          nil)
                                         ("3"
                                          (expand "fullset")
                                          (("3" (propax) nil nil))
                                          nil)
                                         ("4"
                                          (expand "fullset")
                                          (("4" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" metric_spaces nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (boolean nonempty-type-decl nil booleans nil)
    (ball const-decl "set[T]" metric_spaces nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (interior_point? const-decl "bool" metric_spaces nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (r!1 skolem-const-decl "posreal" metric_spaces nil)
    (nnreal type-eq-decl nil real_types nil)
    (d formal-const-decl "[T, T -> nnreal]" metric_spaces nil)
    (x!1 skolem-const-decl "T" metric_spaces nil)
    (x!2 skolem-const-decl "T" metric_spaces nil)
    (fullset_metric_space formula-decl nil metric_spaces nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (space_triangle? const-decl "bool" metric_spaces_def nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (x!3 skolem-const-decl "T" metric_spaces nil)
    (fullset const-decl "set" sets nil)
    (metric_space? const-decl "bool" metric_spaces_def nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (interior const-decl "set[T]" metric_spaces nil))
   nil)
  (ball_open-1 nil 3459610701
   ("" (skeep)
    (("" (grind)
      (("" (expand "extend")
        (("" (expand "ball")
          (("" (apply-extensionality 1 :hide? t)
            (("" (lift-if)
              (("" (prop)
                (("" (iff 1)
                  (("" (prop)
                    (("" (inst + "d(x,x!1) + r")
                      (("" (skosimp*) (("" (postpone) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
(Complement_open 0
  (Complement_open-1 nil 3293869694
   ("" (skosimp*)
    (("" (expand "extend")
      (("" (expand "closed?")
        (("" (expand "Complement")
          (("" (expand "every")
            (("" (skosimp*)
              (("" (typepred "x!1")
                (("" (skosimp*)
                  (("" (typepred "b!1")
                    (("" (replace -3) (("" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((extend const-decl "R" extend nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (setof type-eq-decl nil defined_types nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (set type-eq-decl nil sets nil)
    (open? const-decl "bool" metric_spaces nil)
    (open_set type-eq-decl nil metric_spaces nil)
    (FALSE const-decl "bool" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (complement const-decl "set" sets nil)
    (every const-decl "bool" sets nil)
    (closed? const-decl "bool" metric_spaces nil))
   shostak))
(Complement_closed 0
  (Complement_closed-1 nil 3293869929
   ("" (expand "extend")
    (("" (expand "closed?")
      (("" (expand "Complement")
        (("" (expand "every")
          (("" (skosimp*)
            (("" (typepred "x!1")
              (("" (skolem!)
                (("" (typepred "b!1")
                  (("" (replace -3) (("" (propax) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((closed? const-decl "bool" metric_spaces nil)
    (every const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (FALSE const-decl "bool" booleans nil)
    (closed_set type-eq-decl nil metric_spaces nil)
    (complement const-decl "set" sets nil)
    (open? const-decl "bool" metric_spaces nil)
    (set type-eq-decl nil sets nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil)
    (extend const-decl "R" extend nil))
   shostak))
(subset_is_metric_space 0
  (subset_is_metric_space-1 nil 3293720850
   ("" (skosimp*)
    (("" (lemma "fullset_metric_space") (("" (grind) nil nil)) nil))
    nil)
   ((fullset_metric_space formula-decl nil metric_spaces nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (d formal-const-decl "[T, T -> nnreal]" metric_spaces nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (space_zero? const-decl "bool" metric_spaces_def nil)
    (space_symmetric? const-decl "bool" metric_spaces_def nil)
    (space_triangle? const-decl "bool" metric_spaces_def nil)
    (metric_space? const-decl "bool" metric_spaces_def nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (fullset const-decl "set" sets nil))
   shostak))
(open_Union_open 0
  (open_Union_open-1 nil 3293724671
   ("" (skosimp*)
    (("" (name "ZS" "extend[setof[T], open_set, bool, FALSE](XS!1)")
      (("" (replace -1)
        (("" (name "Y" "Union(ZS)")
          (("" (case "FORALL (x:T): Y(x) IFF (EXISTS (a:(ZS)): a(x))")
            (("1" (expand "open?")
              (("1" (replace -2)
                (("1" (apply-extensionality 1 :hide? t)
                  (("1" (inst - "x!1")
                    (("1" (case "Y(x!1)")
                      (("1" (expand "interior")
                        (("1" (expand "extend")
                          (("1" (replace -1)
                            (("1" (simplify -2)
                              (("1"
                                (skolem!)
                                (("1"
                                  (typepred "a!1")
                                  (("1"
                                    (replace -5 -1 rl)
                                    (("1"
                                      (simplify -1)
                                      (("1"
                                        (case "open?(a!1)")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "open?")
                                            (("1"
                                              (expand "interior")
                                              (("1"
                                                (expand "extend")
                                                (("1"
                                                  (copy -4)
                                                  (("1"
                                                    (replace -2 -1 rl)
                                                    (("1"
                                                      (simplify -1)
                                                      (("1"
                                                        (expand
                                                         "interior_point?")
                                                        (("1"
                                                          (skolem!)
                                                          (("1"
                                                            (inst
                                                             +
                                                             "r!1")
                                                            (("1"
                                                              (lemma
                                                               "Union_subset"
                                                               ("a"
                                                                "a!1"
                                                                "A"
                                                                "ZS"))
                                                              (("1"
                                                                (replace
                                                                 -7)
                                                                (("1"
                                                                  (hide-all-but
                                                                   (-1
                                                                    -2
                                                                    1))
                                                                  (("1"
                                                                    (expand
                                                                     "subset?")
                                                                    (("1"
                                                                      (skosimp*)
                                                                      (("1"
                                                                        (expand
                                                                         "member")
                                                                        (("1"
                                                                          (inst
                                                                           -
                                                                           "x!2")
                                                                          (("1"
                                                                            (inst
                                                                             -
                                                                             "x!2")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert)
                        (("2" (expand "interior")
                          (("2" (expand "extend")
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (skosimp*)
                (("2" (prop)
                  (("1" (hide -3)
                    (("1" (expand "Y")
                      (("1" (expand "Union") (("1" (propax) nil nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "Y" 1)
                    (("2" (expand "Union") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (open_set type-eq-decl nil metric_spaces nil)
    (open? const-decl "bool" metric_spaces nil)
    (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities 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-nonempty-type-decl nil metric_spaces nil)
    (setofsets type-eq-decl nil sets nil)
    (Union const-decl "set" sets nil)
    (Y skolem-const-decl "set[T]" metric_spaces nil)
    (interior const-decl "set[T]" metric_spaces nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (interior_point? const-decl "bool" metric_spaces nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (Union_subset formula-decl nil sets_lemmas nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
(open_Intersection_open 0
  (open_Intersection_open-1 nil 3293728199
   ("" (skosimp*)
    (("" (typepred "FS!1")
      ((""
        (lemma "Intersection_finite[T]"
         ("P" "open?" "A"
          "(extend[setof[T], open_set, bool, FALSE](FS!1))"))
        (("" (split -1)
          (("1" (propax) nil nil)
           ("2" (hide 2)
            (("2" (expand "open?")
              (("2" (expand "interior")
                (("2" (expand "extend")
                  (("2" (apply-extensionality 1 :hide? t)
                    (("2" (case "fullset[T](x!1)")
                      (("1" (assert)
                        (("1" (expand "interior_point?")
                          (("1" (inst + "1")
                            (("1" (hide -2) (("1" (grind) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (hide 2)
            (("3"
              (lemma "finite_extend[setof[T],open_set]" ("a" "FS!1"))
              (("3" (propax) nil nil)) nil))
            nil)
           ("4" (hide -1 2)
            (("4" (skosimp*)
              (("4" (typepred "a!1")
                (("4" (expand "extend") (("4" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("5" (hide -1 2)
            (("5" (skosimp*)
              (("5" (expand "open?")
                (("5" (apply-extensionality 1 :hide? t)
                  (("5" (expand "intersection")
                    (("5" (expand "member")
                      (("5" (expand "interior")
                        (("5" (expand "extend")
                          (("5" (case "a!1(x!1) AND b!1(x!1)")
                            (("1" (assert)
                              (("1"
                                (replace -1 1)
                                (("1"
                                  (expand "interior_point?")
                                  (("1"
                                    (copy -1)
                                    (("1"
                                      (replace -3 -2 rl)
                                      (("1"
                                        (replace -4 -2 rl)
                                        (("1"
                                          (hide -3 -4)
                                          (("1"
                                            (simplify -2)
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (skosimp*)
                                                  (("1"
                                                    (inst
                                                     +
                                                     "min(r!1,r!2)")
                                                    (("1"
                                                      (expand
                                                       "subset?")
                                                      (("1"
                                                        (expand
                                                         "member")
                                                        (("1"
                                                          (skosimp*)
                                                          (("1"
                                                            (expand
                                                             "ball")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "x!2")
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "x!2")
                                                                (("1"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (replace 1) (("2" (propax) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (open_set type-eq-decl nil metric_spaces nil)
    (open? const-decl "bool" metric_spaces nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (interior_point? const-decl "bool" metric_spaces nil)
    (fullset const-decl "set" sets nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (ball const-decl "set[T]" metric_spaces nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (interior const-decl "set[T]" metric_spaces nil)
    (finite_extend judgement-tcc nil extend_set_props nil)
    (intersection const-decl "set" sets nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Intersection_finite formula-decl nil prelude_sets_aux nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil))
   shostak))
(closed_Union_closed 0
  (closed_Union_closed-1 nil 3293865511
   ("" (skosimp*)
    (("" (typepred "FS!1")
      (("" (expand "closed?")
        (("" (rewrite "Demorgan1")
          ((""
            (name "CFS" "(Complement(extend[setof[T],
                                           closed_set,
                                           bool,
                                           FALSE]
                                    (FS!1)))")
            (("" (replace -1 1)
              (("" (case "is_finite[open_set](CFS)")
                (("1"
                  (lemma "open_Intersection_open"
                   ("FS" "restrict[set[T], open_set, boolean](CFS)"))
                  (("1" (expand "open?")
                    (("1" (apply-extensionality 1 :hide? t)
                      (("1" (expand "interior")
                        (("1" (expand "extend")
                          (("1" (case "Intersection(CFS)(x!1)")
                            (("1" (assert)
                              (("1"
                                (rewrite
                                 "extensionality_postulate[T,bool]"
                                 -2
                                 :dir
                                 rl)
                                (("1"
                                  (inst - "x!1")
                                  (("1"
                                    (expand "restrict")
                                    (("1"
                                      (expand "extend")
                                      (("1"
                                        (expand "interior_point?")
                                        (("1"
                                          (case-replace
                                           "Intersection(LAMBDA (t: setof[T]):
                        IF open?(t) THEN CFS(t) ELSE FALSE ENDIF)
                     (x!1)")
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (inst + "r!1")
                                              (("1"
                                                (expand "subset?")
                                                (("1"
                                                  (skosimp*)
                                                  (("1"
                                                    (inst - "x!2")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (expand
                                                         "Intersection")
                                                        (("1"
                                                          (skosimp*)
                                                          (("1"
                                                            (inst
                                                             -4
                                                             "a!1")
                                                            (("1"
                                                              (case
                                                               "open?[T, d](a!1)")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                (("2"
                                                                  (typepred
                                                                   "a!1")
                                                                  (("2"
                                                                    (replace
                                                                     -6
                                                                     -1
                                                                     rl)
                                                                    (("2"
                                                                      (expand
                                                                       "Complement"
                                                                       -1)
                                                                      (("2"
                                                                        (skosimp*)
                                                                        (("2"
                                                                          (replace
                                                                           -1)
                                                                          (("2"
                                                                            (typepred
                                                                             "b!1")
                                                                            (("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (expand
                                                                                 "closed?")
                                                                                (("2"
                                                                                  (propax)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 2 -2)
                                            (("2"
                                              (expand "Intersection")
                                              (("2"
                                                (skosimp*)
                                                (("2"
                                                  (typepred "a!1")
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (inst - "a!1")
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (expand "is_finite")
                    (("2" (skolem!)
                      (("2"
                        (inst + "N!1"
                         "lambda (a:(restrict[set[T], open_set, boolean](CFS))): f!1(complement(a))")
                        (("1" (expand "injective?")
                          (("1" (skosimp*)
                            (("1" (typepred "x1!1")
                              (("1"
                                (typepred "x2!1")
                                (("1"
                                  (expand "restrict")
                                  (("1"
                                    (replace -6 * rl)
                                    (("1"
                                      (hide -6)
                                      (("1"
                                        (expand "Complement")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (inst - "b!2" "b!1")
                                            (("1"
                                              (replace -4 -5)
                                              (("1"
                                                (replace -2 -5)
                                                (("1"
                                                  (rewrite
                                                   "complement_complement")
                                                  (("1"
                                                    (rewrite
                                                     "complement_complement")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "closed?")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (typepred "b!1")
                                                  (("2"
                                                    (expand "extend")
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (expand "closed?")
                                              (("3"
                                                (typepred "b!2")
                                                (("3"
                                                  (expand "extend")
                                                  (("3"
                                                    (assert)
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skosimp*)
                          (("2" (typepred "a!1")
                            (("2" (expand "closed?")
                              (("2"
                                (rewrite "complement_complement")
                                (("2"
                                  (assert)
                                  (("2"
                                    (replace -3 -2 rl)
                                    (("2"
                                      (expand "restrict")
                                      (("2"
                                        (expand "Complement")
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (typepred "b!1")
                                            (("2"
                                              (expand "extend")
                                              (("2"
                                                (expand "closed?")
                                                (("2"
                                                  (replace -3 * rl)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (replace -3 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))
        nil))
      nil))
    nil)
   ((finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (closed_set type-eq-decl nil metric_spaces nil)
    (closed? const-decl "bool" metric_spaces nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil metric_spaces nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Demorgan1 formula-decl nil sets_lemmas nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (finite_extend application-judgement "finite_set[T]"
     extend_set_props nil)
    (Complement_bijective name-judgement
     "(bijective?[setofsets[T], setofsets[T]])" sets_lemmas nil)
    (Complement_is_finite application-judgement "finite_set[set[T]]"
     finite_sets_of_sets nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (injective? const-decl "bool" functions nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (b!1 skolem-const-decl
     "(extend[setof[T], closed_set, bool, FALSE](FS!1))" metric_spaces
     nil)
    (b!2 skolem-const-decl
     "(extend[setof[T], closed_set, bool, FALSE](FS!1))" metric_spaces
     nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (FS!1 skolem-const-decl "finite_set[closed_set]" metric_spaces nil)
    (complement const-decl "set" sets nil)
    (finite_restrict application-judgement "finite_set[S]"
     restrict_set_props nil)
    (open_Intersection_open formula-decl nil metric_spaces nil)
    (interior const-decl "set[T]" metric_spaces nil)
    (Intersection const-decl "set" sets nil)
    (subset? const-decl "bool" sets nil)
    (CFS skolem-const-decl "finite_set[set[T]]" metric_spaces nil)
    (a!1 skolem-const-decl "(CFS)" metric_spaces nil)
    (TRUE const-decl "bool" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (member 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (extensionality_postulate formula-decl nil functions nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (interior_point? const-decl "bool" metric_spaces nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (restrict const-decl "R" restrict nil)
    (open_set type-eq-decl nil metric_spaces nil)
    (open? const-decl "bool" metric_spaces nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   shostak))
(closed_Intersection_closed 0
  (closed_Intersection_closed-1 nil 3293873210
   ("" (skosimp*)
    (("" (expand "closed?")
      (("" (rewrite "Demorgan2")
        ((""
          (name "CXS"
                "(Complement(extend[setof[T], closed_set, bool, FALSE]
                                 (XS!1)))")
          (("" (replace -1)
            ((""
              (lemma "open_Union_open"
               ("XS" "restrict[set[T], open_set, boolean](CXS)"))
              (("" (expand "open?")
                (("" (apply-extensionality 1 :hide? t)
                  (("" (expand "interior")
                    (("" (expand "extend")
                      (("" (case "Union(CXS)(x!1)")
                        (("1" (assert)
                          (("1"
                            (rewrite "extensionality_postulate[T,bool]"
                             -2 :dir rl)
                            (("1" (inst - "x!1")
                              (("1"
                                (expand "interior_point?")
                                (("1"
                                  (expand "restrict")
                                  (("1"
                                    (expand "extend")
                                    (("1"
                                      (case-replace
                                       "Union(LAMBDA (t: setof[T]): IF open?(t) THEN CXS(t) ELSE FALSE ENDIF)(x!1)")
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (inst + "r!1")
                                          (("1"
                                            (expand "subset?")
                                            (("1"
                                              (skosimp*)
                                              (("1"
                                                (inst - "x!2")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (expand "Union")
                                                    (("1"
                                                      (skosimp*)
                                                      (("1"
                                                        (typepred
                                                         "a!3")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (inst
                                                             +
                                                             "a!3")
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "Union")
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (typepred "a!1")
                                            (("2"
                                              (hide 2)
                                              (("2"
                                                (inst + "a!1")
                                                (("2"
                                                  (replace -4 -1 rl)
                                                  (("2"
                                                    (hide -3 -4)
                                                    (("2"
                                                      (expand
                                                       "Complement")
                                                      (("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (typepred
                                                           "b!1")
                                                          (("2"
                                                            (expand
                                                             "closed?")
                                                            (("2"
                                                              (replace
                                                               -3
                                                               *
                                                               rl)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((closed? const-decl "bool" metric_spaces nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil)
    (open_Union_open formula-decl nil metric_spaces nil)
    (open? const-decl "bool" metric_spaces nil)
    (open_set type-eq-decl nil metric_spaces nil)
    (restrict const-decl "R" restrict nil)
    (interior const-decl "set[T]" metric_spaces nil)
    (Union const-decl "set" sets nil)
    (CXS skolem-const-decl "setofsets[T]" metric_spaces nil)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.64 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.