products/sources/formale sprachen/PVS/measure_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: complex_integral.pvs   Sprache: Lisp

Original von: PVS©
(complex_topology
 (IMP_metric_space_TCC1 0
  (IMP_metric_space_TCC1-1 nil 3503063305
   ("" (expand "metric?")
    (("" (split)
      (("1" (expand "metric_zero?")
        (("1" (skosimp)
          (("1" (expand "-")
            (("1" (expand "abs")
              (("1" (expand "sq_abs")
                (("1" (assert)
                  (("1"
                    (lemma "sqrt_lem"
                     ("nny"
                      "sq(Im(x!1) - Im(y!1)) + sq(Re(x!1) - Re(y!1))"
                      "nnz" "0"))
                    (("1" (replace -1)
                      (("1" (hide -1)
                        (("1"
                          (lemma "sq_plus_eq_0"
                           ("a" "Im(x!1) - Im(y!1)" "b"
                            "Re(x!1) - Re(y!1)"))
                          (("1" (assert)
                            (("1"
                              (name-replace "SQS"
                               "sq(Im(x!1) - Im(y!1)) + sq(Re(x!1) - Re(y!1))")
                              (("1"
                                (assert)
                                (("1"
                                  (split)
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (flatten)
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (flatten)
                                    (("2"
                                      (replace -1)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "metric_symmetric?")
        (("2" (skosimp)
          (("2" (lemma "abs_neg" ("z" "y!1-x!1"))
            (("2" (replace -1 1 rl)
              (("2" (expand "-")
                (("2" (hide -1)
                  (("2" (expand "abs")
                    (("2" (expand "sq_abs") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (expand "metric_triangle?")
        (("3" (skosimp)
          (("3" (lemma "abs_triangle" ("z1" "x!1-y!1" "z2" "y!1-z!1"))
            (("3"
              (name-replace "RHS" "abs(x!1 - y!1) + abs(y!1 - z!1)")
              (("3" (expand "+ ")
                (("3" (expand "-")
                  (("3" (expand "abs")
                    (("3" (expand "sq_abs") (("3" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((abs const-decl "nnreal" polar "complex_alt/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (Im_rew formula-decl nil complex_types "complex_alt/")
    (Re_rew formula-decl nil complex_types "complex_alt/")
    (eq_rew formula-decl nil complex_types "complex_alt/")
    (sq_plus_eq_0 formula-decl nil sq "reals/")
    (nnreal type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (sqrt_lem formula-decl nil sqrt "reals/")
    (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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (complex type-decl nil complex_types "complex_alt/")
    (Im const-decl "real" complex_types "complex_alt/")
    (Re const-decl "real" complex_types "complex_alt/")
    (sq_abs const-decl "nnreal" complex_types "complex_alt/")
    (- const-decl "complex" complex_types "complex_alt/")
    (metric_zero? const-decl "bool" metric_def "metric_space/")
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "complex" complex_types "complex_alt/")
    (abs_neg formula-decl nil polar "complex_alt/")
    (metric_symmetric? const-decl "bool" metric_def "metric_space/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "complex" complex_types "complex_alt/")
    (abs_triangle formula-decl nil polar "complex_alt/")
    (metric_triangle? const-decl "bool" metric_def "metric_space/")
    (metric? const-decl "bool" metric_def "metric_space/"))
   nil))
 (complex_is_complete 0
  (complex_is_complete-1 nil 3503071004
   ("" (typepred "fullset[real]")
    (("" (hide -1)
      (("" (expand "fullset")
        (("" (expand "complete_metric_space?")
          (("" (flatten)
            (("" (split)
              (("1" (hide -1 -2)
                (("1" (expand "metric_space?")
                  (("1" (split)
                    (("1" (expand "metric_zero?")
                      (("1" (skosimp)
                        (("1" (rewrite "abs_is_0")
                          (("1" (assert)
                            (("1" (split)
                              (("1"
                                (flatten)
                                (("1" (assert) nil nil))
                                nil)
                               ("2"
                                (flatten)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "metric_symmetric?")
                      (("2" (skosimp)
                        (("2" (expand "abs")
                          (("2" (expand "sq_abs")
                            (("2" (assert)
                              (("2"
                                (rewrite "sq_neg_minus")
                                (("2"
                                  (assert)
                                  (("2"
                                    (name-replace
                                     "SQ1"
                                     "sq(Im(y!1) - Im(x!1))")
                                    (("2"
                                      (rewrite "sq_neg_minus")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("3" (expand "metric_triangle?")
                      (("3" (skosimp)
                        (("3"
                          (lemma "abs_triangle"
                           ("z1" "x!1-y!1" "z2" "y!1-z!1"))
                          (("3" (assert)
                            (("3" (expand "+" -1 1)
                              (("3"
                                (assert)
                                (("3"
                                  (expand "-" 1 1)
                                  (("3" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide -1)
                (("2" (expand "metric_complete?")
                  (("2" (skosimp)
                    (("2" (inst-cp - "lambda (n:nat): Im(u!1(n))")
                      (("2" (inst - "lambda (n:nat): Re(u!1(n))")
                        (("2" (split -2)
                          (("1" (split -3)
                            (("1" (hide -3)
                              (("1"
                                (expand "metric_convergent?")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (inst + "complex_(x!2,x!1)")
                                    (("1"
                                      (expand "metric_converges_to")
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (expand "ball")
                                          (("1"
                                            (expand "member")
                                            (("1"
                                              (expand "abs" 1)
                                              (("1"
                                                (expand "sq_abs")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (inst - "r!1/2")
                                                    (("1"
                                                      (inst - "r!1/2")
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst
                                                           +
                                                           "n!1+n!2")
                                                          (("1"
                                                            (skosimp)
                                                            (("1"
                                                              (inst
                                                               -
                                                               "i!1")
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "i!1")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (rewrite
                                                                     "sq_lt"
                                                                     +
                                                                     :dir
                                                                     rl)
                                                                    (("1"
                                                                      (rewrite
                                                                       "sq_lt"
                                                                       -1
                                                                       :dir
                                                                       rl)
                                                                      (("1"
                                                                        (rewrite
                                                                         "sq_lt"
                                                                         -2
                                                                         :dir
                                                                         rl)
                                                                        (("1"
                                                                          (rewrite
                                                                           "sq_div")
                                                                          (("1"
                                                                            (expand
                                                                             "sq"
                                                                             -1
                                                                             3)
                                                                            (("1"
                                                                              (expand
                                                                               "sq"
                                                                               -2
                                                                               3)
                                                                              (("1"
                                                                                (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)
                             ("2" (hide -1 2)
                              (("2"
                                (expand "cauchy?")
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (expand "ball")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (inst - "r!1")
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (inst + "n!1")
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (inst - "i!1" "j!1")
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (expand "abs" -)
                                                    (("2"
                                                      (expand "sq_abs")
                                                      (("2"
                                                        (rewrite
                                                         "sq_lt"
                                                         -3
                                                         :dir
                                                         rl)
                                                        (("2"
                                                          (rewrite
                                                           "sq_sqrt")
                                                          (("2"
                                                            (rewrite
                                                             "sq_lt"
                                                             1
                                                             :dir
                                                             rl)
                                                            (("2"
                                                              (assert)
                                                              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 "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"
                                                (assert)
                                                (("2"
                                                  (expand "abs" -3)
                                                  (("2"
                                                    (expand "sq_abs")
                                                    (("2"
                                                      (rewrite
                                                       "sq_lt"
                                                       1
                                                       :dir
                                                       rl)
                                                      (("2"
                                                        (rewrite
                                                         "sq_lt"
                                                         -3
                                                         :dir
                                                         rl)
                                                        (("2"
                                                          (rewrite
                                                           "sq_sqrt")
                                                          (("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)
   ((metric_space? const-decl "bool" metric_space_def "metric_space/")
    (metric_triangle? const-decl "bool" metric_space_def
     "metric_space/")
    (abs_triangle formula-decl nil polar "complex_alt/")
    (+ const-decl "complex" complex_types "complex_alt/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (metric_symmetric? const-decl "bool" metric_space_def
     "metric_space/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (Re const-decl "real" complex_types "complex_alt/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_neg_minus formula-decl nil sq "reals/")
    (Im const-decl "real" complex_types "complex_alt/")
    (sq_abs const-decl "nnreal" complex_types "complex_alt/")
    (metric_zero? const-decl "bool" metric_space_def "metric_space/")
    (TRUE const-decl "bool" booleans nil)
    (- const-decl "complex" complex_types "complex_alt/")
    (complex type-decl nil complex_types "complex_alt/")
    (abs_is_0 formula-decl nil polar "complex_alt/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (Re_sub1 formula-decl nil complex_types "complex_alt/")
    (Im_sub1 formula-decl nil complex_types "complex_alt/")
    (c_eq3 formula-decl nil complex_types "complex_alt/")
    (eq_rew formula-decl nil complex_types "complex_alt/")
    (metric_complete? const-decl "bool" metric_space_def
     "metric_space/")
    (sequence type-eq-decl nil sequences 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)
    (cauchy? const-decl "bool" metric_space_def "metric_space/")
    (metric_converges_to const-decl "bool" metric_space_def
     "metric_space/")
    (ball const-decl "set[T]" metric_space_def "metric_space/")
    (Im_rew formula-decl nil complex_types "complex_alt/")
    (Re_rew formula-decl nil complex_types "complex_alt/")
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (sq_abs formula-decl nil sq "reals/")
    (sq_div formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sq_lt formula-decl nil sq "reals/")
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types 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)
    (member const-decl "bool" sets nil)
    (complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
     "complex_alt/")
    (complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
     complex_types "complex_alt/")
    (metric_convergent? const-decl "bool" metric_space_def
     "metric_space/")
    (fullset_is_clopen name-judgement
     "clopen[real, (metric_induced_topology)]" real_topology
     "metric_space/")
    (real_is_complete name-judgement "metric_complete" real_topology
     "metric_space/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (set type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     "metric_space/")
    (clopen? const-decl "bool" topology "topology/")
    (fullset const-decl "set" sets nil)
    (complete_metric_space? const-decl "bool" metric_space_def
     "metric_space/"))
   nil)))


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


Bot Zugriff