products/sources/formale Sprachen/Java/openjdk-20-36_src/test/jdk/tools/launcher/modules/limitmods/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: denumerable_enumeration.pvs   Sprache: Lisp

Original von: PVS©
(inverse_fun_ms_continuous
 (IMP_uniform_continuity_TCC1 0
  (IMP_uniform_continuity_TCC1-1 nil 3465727308
   ("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil)
   ((fullset_metric_space1 formula-decl nil inverse_fun_ms_continuous
     nil))
   nil))
 (IMP_uniform_continuity_TCC2 0
  (IMP_uniform_continuity_TCC2-1 nil 3465727308
   ("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil)
   ((fullset_metric_space2 formula-decl nil inverse_fun_ms_continuous
     nil))
   nil))
 (image_function_continuous 0
  (image_function_continuous-1 nil 3465647899
   ("" (skeep)
    (("" (label "bijf" -3)
      (("" (lemma "continuous_open_sets[T2,d2,T1,d1]")
        (("" (inst - "fullset[T2]" "inverse(f)")
          (("" (expand "continuous?" +)
            (("" (assert)
              (("" (hide 2)
                (("" (skosimp*)
                  (("" (rewrite "intersection_full")
                    (("" (lemma "open_in_fullset[T2,d2]")
                      (("" (inst - "inverse_image(inverse(f), Y!1)")
                        (("" (assert)
                          (("" (hide 2)
                            ((""
                              (case "closed?[T1,d1](complement(Y!1))")
                              (("1"
                                (lemma
                                 "closed_subset_of_compact[T1,d1]")
                                (("1"
                                  (inst
                                   -
                                   "fullset[T1]"
                                   "complement(Y!1)")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (rewrite "subset_fullset")
                                      (("1"
                                        (lemma
                                         "continuous_image_of_compact")
                                        (("1"
                                          (inst
                                           -
                                           "complement(Y!1)"
                                           "f")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (lemma
                                               "compact_closed[T2,d2]")
                                              (("1"
                                                (inst
                                                 -
                                                 "image(f,complement(Y!1))")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (expand
                                                     "closed?"
                                                     -1)
                                                    (("1"
                                                      (case
                                                       "complement(image(f, complement(Y!1))) = inverse_image(inverse(f), Y!1)")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil)
                                                       ("2"
                                                        (hide 2)
                                                        (("2"
                                                          (hide-all-but
                                                           ("bijf" 1))
                                                          (("2"
                                                            (lemma
                                                             "inverse_image_complement[T2,T1]")
                                                            (("2"
                                                              (inst
                                                               -
                                                               "complement(Y!1)"
                                                               "inverse(f)")
                                                              (("2"
                                                                (lemma
                                                                 "complement_complement[T1]")
                                                                (("2"
                                                                  (inst
                                                                   -
                                                                   "Y!1")
                                                                  (("2"
                                                                    (replace
                                                                     -1)
                                                                    (("2"
                                                                      (hide
                                                                       -1)
                                                                      (("2"
                                                                        (replace
                                                                         -1)
                                                                        (("2"
                                                                          (rewrite
                                                                           "complement_equal")
                                                                          (("2"
                                                                            (name
                                                                             "X"
                                                                             "complement(Y!1)")
                                                                            (("2"
                                                                              (replace
                                                                               -1)
                                                                              (("2"
                                                                                (expand
                                                                                 "image")
                                                                                (("2"
                                                                                  (expand
                                                                                   "inverse_image")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("2"
                                                                                      (decompose-equality
                                                                                       1)
                                                                                      (("2"
                                                                                        (iff)
                                                                                        (("2"
                                                                                          (lemma
                                                                                           "bijective_inverse[T1,T2]")
                                                                                          (("2"
                                                                                            (ground)
                                                                                            (("1"
                                                                                              (skosimp*)
                                                                                              (("1"
                                                                                                (typepred
                                                                                                 "x!2")
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   -
                                                                                                   "x!2"
                                                                                                   "x!1"
                                                                                                   "f")
                                                                                                  (("1"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (inst
                                                                                               +
                                                                                               "inverse(f)(x!1)")
                                                                                              (("2"
                                                                                                (inst
                                                                                                 -
                                                                                                 "inverse(f)(x!1)"
                                                                                                 "x!1"
                                                                                                 "f")
                                                                                                (("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))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "closed?")
                                (("2"
                                  (rewrite "complement_complement")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inverse const-decl "D" function_inverse nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (open_in_fullset formula-decl nil metric_spaces nil)
    (closed? const-decl "bool" metric_spaces nil)
    (complement const-decl "set" sets nil)
    (subset_fullset formula-decl nil sets_lemmas nil)
    (compact_closed formula-decl nil compactness nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (complement_equal formula-decl nil sets_lemmas nil)
    (bijective_inverse formula-decl nil function_inverse nil)
    (bijective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (inverse_image_complement formula-decl nil function_image nil)
    (image const-decl "set[R]" function_image nil)
    (continuous_image_of_compact formula-decl nil uniform_continuity
     nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (closed_subset_of_compact formula-decl nil compactness nil)
    (intersection_full formula-decl nil sets_lemmas nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (continuous? const-decl "bool" continuity_ms_def nil)
    (continuous_open_sets formula-decl nil continuity_ms nil)
    (T2 formal-nonempty-type-decl nil inverse_fun_ms_continuous nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (d2 formal-const-decl "[T2, T2 -> nnreal]"
     inverse_fun_ms_continuous nil)
    (T1 formal-nonempty-type-decl nil inverse_fun_ms_continuous nil)
    (d1 formal-const-decl "[T1, T1 -> nnreal]"
     inverse_fun_ms_continuous nil))
   shostak)))


¤ Dauer der Verarbeitung: 0.4 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff