Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: unif_cont_fun.prf Sprache: Lisp

Original von: PVS^©

(continuity_def
(continuous_function_witness_TCC1 0
  (continuous_function_witness_TCC1-1 nil 3358738874 3358739024
   ("" (lemma "functions_exist")
    (("" (flatten)
      (("" (split)
        (("1" (skosimp)
          (("1" (expand "empty?")
            (("1" (inst - "y!1")
              (("1" (expand "fullset")
                (("1" (expand "member") (("1" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "fullset")
          (("2" (expand "nonempty?")
            (("2" (expand "empty?")
              (("2" (expand "member")
                (("2" (lemma "fun_exists[T1,T2]")
                  (("2" (assert)
                    (("2" (replace 1 -1)
                      (("2" (skosimp) (("2" (inst -2 "f!1") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((fun_exists formula-decl nil function_image nil)
    (T1 formal-type-decl nil continuity_def nil)
    (nonempty? const-decl "bool" sets nil)
    (T2 formal-type-decl nil continuity_def nil)
    (member const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (functions_exist formula-decl nil continuity_def nil))
   130567 2610 t nil))
(continuous_function_witness_TCC2 0
  (continuous_function_witness_TCC2-1 nil 3358738874 3358738875
   ("" (subtype-tcc) nil nil) unchecked
   ((nonempty? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil))
   73 70 nil nil))
(continuous_function_witness_is_continuous? 0
  (continuous_function_witness_is_continuous?-1 nil 3358739096
   3358739446
   ("" (expand "continuous?")
    (("" (skosimp)
      (("" (expand "continuous_function_witness")
        (("" (case-replace "empty?(fullset[T2])")
          (("1" (name "F" "choose(fullset[[T1 -> T2]])")
            (("1" (replace -1)
              (("1" (expand "empty?")
                (("1" (inst - "F(x!1)")
                  (("1" (expand "member")
                    (("1" (expand "fullset") (("1" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert)
            (("2" (expand "continuous_at?")
              (("2" (skosimp)
                (("2" (name "Y" "choose(fullset[T2])")
                  (("2" (replace -1)
                    (("2" (case-replace "U!1(Y)")
                      (("1"
                        (case-replace
                         "inverse_image(LAMBDA x: Y, U!1) = fullset[T1]")
                        (("1" (expand "neighbourhood?")
                          (("1" (expand "interior_point?")
                            (("1" (inst + "fullset[T1]")
                              (("1"
                                (rewrite "subset_reflexive")
                                (("1"
                                  (expand "fullset")
                                  (("1"
                                    (expand "member")
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (apply-extensionality 1 :hide? t)
                          (("2" (expand "fullset")
                            (("2" (expand "inverse_image")
                              (("2"
                                (expand "member")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2"
                        (case-replace
                         "inverse_image(LAMBDA x: Y, U!1) = emptyset[T1]")
                        (("1" (expand "neighbourhood?")
                          (("1" (expand "interior_point?")
                            (("1" (skosimp)
                              (("1"
                                (expand "member")
                                (("1"
                                  (expand "subset?")
                                  (("1"
                                    (inst - "Y")
                                    (("1"
                                      (expand "member")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (apply-extensionality 1 :hide? t)
                          (("2" (expand "emptyset")
                            (("2" (expand "inverse_image")
                              (("2"
                                (expand "member")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((T2 formal-type-decl nil continuity_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (empty? const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (T1 formal-type-decl nil continuity_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nonempty? const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil)
    (continuous_at? const-decl "bool" continuity_def nil)
    (neighbourhood? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (S formal-const-decl "topology[T1]" continuity_def nil)
    (topology nonempty-type-eq-decl nil topology_def nil)
    (topology? const-decl "bool" topology_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (subset_reflexive formula-decl nil sets_lemmas nil)
    (interior_point? const-decl "bool" topology nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (subset? const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (continuous_function_witness const-decl "[T1 -> T2]" continuity_def
     nil)
    (continuous? const-decl "bool" continuity_def nil))
   347561 7100 t nil)))

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