Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: metric_subspace.prf Sprache: Lisp

Original von: PVS^©

(metric_subspace
(IMP_metric_space_TCC1 0
  (IMP_metric_space_TCC1-1 nil 3454238656
   ("" (typepred "d")
    (("" (expand "restrict")
      (("" (expand "metric?")
        (("" (flatten)
          (("" (split)
            (("1" (expand "metric_zero?")
              (("1" (skosimp) (("1" (inst - "x!1" "y!1") nil nil))
                nil))
              nil)
             ("2" (expand "metric_symmetric?")
              (("2" (skosimp) (("2" (inst - "x!1" "y!1") nil nil))
                nil))
              nil)
             ("3" (expand "metric_triangle?")
              (("3" (skosimp)
                (("3" (inst - "x!1" "y!1" "z!1") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((restrict const-decl "R" restrict nil)
    (metric_triangle? const-decl "bool" metric_def nil)
    (metric_symmetric? const-decl "bool" metric_def nil)
    (metric_zero? const-decl "bool" metric_def nil)
    (S formal-subtype-decl nil metric_subspace nil)
    (S_pred const-decl "[T -> boolean]" metric_subspace 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-type-decl nil metric_subspace 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)
    (nnreal type-eq-decl nil real_types nil)
    (metric? const-decl "bool" metric_def nil)
    (metric nonempty-type-eq-decl nil metric_def nil)
    (d formal-const-decl "metric" metric_subspace nil))
   nil))
(complete_subspace 0
  (complete_subspace-1 nil 3407434200
   ("" (flatten)
    (("" (expand "metric_complete?")
      (("" (skosimp)
        (("" (inst - "u!1")
          (("1" (split)
            (("1" (expand "fullset")
              (("1" (expand "extend")
                (("1" (expand "metric_closed?")
                  (("1" (expand "complement")
                    (("1" (expand "member")
                      (("1" (expand "metric_open?")
                        (("1" (expand "metric_convergent?")
                          (("1" (skosimp)
                            (("1" (inst - "x!1")
                              (("1"
                                (assert)
                                (("1"
                                  (lift-if -2)
                                  (("1"
                                    (prop)
                                    (("1"
                                      (inst 2 "x!1")
                                      (("1"
                                        (hide-all-but (-2 2))
                                        (("1"
                                          (expand
                                           "metric_converges_to")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (inst - "r!1")
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (inst + "n!1")
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (inst - "i!1")
                                                      (("1"
                                                        (expand "ball")
                                                        (("1"
                                                          (expand
                                                           "member")
                                                          (("1"
                                                            (expand
                                                             "restrict")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (skosimp)
                                      (("2"
                                        (expand "cauchy?")
                                        (("2"
                                          (hide 2)
                                          (("2"
                                            (expand "subset?")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (inst -3 "r!1/2")
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (expand
                                                     "metric_converges_to")
                                                    (("2"
                                                      (inst -2 "r!1/2")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (expand
                                                           "member")
                                                          (("2"
                                                            (inst
                                                             -2
                                                             "n!1+n!2")
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (inst
                                                                 -
                                                                 "u!1(n!1+n!2)")
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (expand
                                                                     "ball")
                                                                    (("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)
             ("2" (hide-all-but (-2 1))
              (("2" (expand "cauchy?")
                (("2" (skosimp)
                  (("2" (inst - "r!1")
                    (("2" (skosimp)
                      (("2" (inst + "n!1")
                        (("2" (skosimp)
                          (("2" (inst - "i!1" "j!1")
                            (("2" (expand "member")
                              (("2"
                                (expand "ball")
                                (("2"
                                  (expand "restrict")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "fullset") (("2" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((metric_complete? const-decl "bool" metric_space_def nil)
    (u!1 skolem-const-decl "sequence[(fullset[S])]" metric_subspace
     nil)
    (sequence type-eq-decl nil sequences nil)
    (S formal-subtype-decl nil metric_subspace nil)
    (S_pred const-decl "[T -> boolean]" metric_subspace nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (T formal-type-decl nil metric_subspace nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (metric_closed? const-decl "bool" metric_space_def nil)
    (member const-decl "bool" sets nil)
    (metric_convergent? const-decl "bool" metric_space_def nil)
    (TRUE const-decl "bool" booleans nil)
    (ball_is_metric_open application-judgement "metric_open"
     metric_subspace nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (subset? const-decl "bool" sets nil)
    (cauchy? const-decl "bool" metric_space_def nil)
    (x!1 skolem-const-decl "({x | TRUE})" metric_subspace nil)
    (metric_converges_to const-decl "bool" metric_space_def 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)
    (real_lt_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)
    (restrict const-decl "R" restrict nil)
    (ball const-decl "set[T]" metric_space_def nil)
    (metric_open? const-decl "bool" metric_space_def nil)
    (complement const-decl "set" sets nil)
    (extend const-decl "R" extend nil))
   shostak)))

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