Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: tarski_query_matrix.prf Sprache: Lisp

Original von: PVS^©

(cross_metric_cont
(IMP_cross_metric_spaces_TCC1 0
  (IMP_cross_metric_spaces_TCC1-1 nil 3459693207
   ("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil)
   ((fullset_metric_space1 formula-decl nil cross_metric_cont nil))
   nil))
(IMP_cross_metric_spaces_TCC2 0
  (IMP_cross_metric_spaces_TCC2-1 nil 3459693207
   ("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil)
   ((fullset_metric_space2 formula-decl nil cross_metric_cont nil))
   nil))
(IMP_continuity_ms_def_TCC1 0
  (IMP_continuity_ms_def_TCC1-1 nil 3459693207
   ("" (lemma "product_is_metric") (("" (propax) nil nil)) nil)
   ((product_is_metric formula-decl nil cross_metric_spaces nil)
    (T1 formal-nonempty-type-decl nil cross_metric_cont 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)
    (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_cont nil)
    (T2 formal-nonempty-type-decl nil cross_metric_cont nil)
    (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_cont nil))
   nil))
(IMP_continuity_ms_def_TCC2 0
  (IMP_continuity_ms_def_TCC2-1 nil 3459693207
   ("" (lemma "fullset_metric_space3") (("" (propax) nil nil)) nil)
   ((fullset_metric_space3 formula-decl nil cross_metric_cont nil))
   nil))
(product_cont_equiv 0
  (product_cont_equiv-1 nil 3459694386
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "continuous?")
        (("1" (expand "continuous_at?")
          (("1" (skosimp*)
            (("1" (inst - "x!1")
              (("1" (inst - "epsilon!1/4")
                (("1" (skosimp*)
                  (("1" (expand "member")
                    (("1" (expand "ball")
                      (("1" (inst + "delta!1/4")
                        (("1" (skosimp*)
                          (("1" (inst - "y!1")
                            (("1" (prop)
                              (("1"
                                (cross-mult -1)
                                (("1" (grind) nil nil))
                                nil)
                               ("2"
                                (expand "d")
                                (("2" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "continuous?")
        (("2" (expand "continuous_at?")
          (("2" (expand "member")
            (("2" (expand "ball")
              (("2" (skosimp*)
                (("2" (typepred "x!1")
                  (("2" (inst - "x!1" "epsilon!1")
                    (("2" (skosimp*)
                      (("2" (inst + "delta!1")
                        (("2" (skosimp*)
                          (("2" (inst - "y!1")
                            (("2" (expand "d") (("2" (grind) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_at? const-decl "bool" continuity_ms_def nil)
    (T1 formal-nonempty-type-decl nil cross_metric_cont nil)
    (T2 formal-nonempty-type-decl nil cross_metric_cont nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (ball const-decl "set[T]" metric_spaces nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (d3 formal-const-decl "[T3, T3 -> nnreal]" cross_metric_cont nil)
    (nnreal type-eq-decl nil real_types nil)
    (T3 formal-nonempty-type-decl nil cross_metric_cont nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (d const-decl "nnreal" cross_metric_spaces nil)
    (member const-decl "bool" sets nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (continuous? const-decl "bool" continuity_ms_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   shostak))
(product_cont_product_subset 0
  (product_cont_product_subset-1 nil 3459695893
   ("" (skosimp*)
    (("" (prop)
      (("1" (skosimp*)
        (("1" (lemma "product_cont_equiv")
          (("1" (assert)
            (("1" (inst - "fullset[[(X!1),(Y!1)]]" "f!1")
              (("1" (prop)
                (("1" (typepred "x!1")
                  (("1" (inst - "(x!1,y!1)" "epsilon!1")
                    (("1" (skosimp*)
                      (("1" (inst + "delta!1")
                        (("1" (skosimp*)
                          (("1" (typepred "z!1")
                            (("1" (typepred "w!1")
                              (("1"
                                (inst - "(z!1,w!1)")
                                (("1" (prop) nil nil)
                                 ("2"
                                  (expand "extend")
                                  (("2"
                                    (expand "fullset")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "extend")
                      (("2" (expand "fullset") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "continuous?")
        (("2" (skosimp*)
          (("2" (expand "continuous_at?")
            (("2" (expand "member")
              (("2" (expand "ball")
                (("2" (skosimp*)
                  (("2" (typepred "x!1")
                    (("2" (inst - "x!1`1" "x!1`2" "epsilon !1")
                      (("1" (skosimp*)
                        (("1" (inst + "delta!1")
                          (("1" (skosimp*)
                            (("1" (typepred "y!1")
                              (("1"
                                (expand "d")
                                (("1"
                                  (inst - "y!1`1" "y!1`2")
                                  (("1"
                                    (prop)
                                    (("1"
                                      (case "x!1 = (x!1`1,x!1`2)")
                                      (("1"
                                        (replace -1 1)
                                        (("1"
                                          (case "y!1 = (y!1`1,y!1`2)")
                                          (("1"
                                            (replace -1 1)
                                            (("1"
                                              (expand "restrict")
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "restrict")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (assert) nil nil))
                                      nil)
                                     ("2"
                                      (expand "restrict")
                                      (("2" (grind) nil nil))
                                      nil)
                                     ("3"
                                      (expand "restrict")
                                      (("3" (grind) nil nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (assert)
                                    (("2" (grind) nil nil))
                                    nil)
                                   ("3"
                                    (expand "restrict")
                                    (("3" (grind) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (grind) nil nil) ("3" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((product_cont_equiv formula-decl nil cross_metric_cont nil)
    (T1 formal-nonempty-type-decl nil cross_metric_cont nil)
    (T2 formal-nonempty-type-decl nil cross_metric_cont nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (fullset const-decl "set" sets nil)
    (T3 formal-nonempty-type-decl nil cross_metric_cont nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (w!1 skolem-const-decl "(Y!1)" cross_metric_cont nil)
    (z!1 skolem-const-decl "(X!1)" cross_metric_cont 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)
    (X!1 skolem-const-decl "set[T1]" cross_metric_cont nil)
    (Y!1 skolem-const-decl "set[T2]" cross_metric_cont nil)
    (x!1 skolem-const-decl "(X!1)" cross_metric_cont nil)
    (y!1 skolem-const-decl "(Y!1)" cross_metric_cont nil)
    (member const-decl "bool" sets nil)
    (x!1 skolem-const-decl
     "(extend[[T1, T2], [(X!1), (Y!1)], bool, FALSE](fullset[[(X!1), (Y!1)]]))"
     cross_metric_cont nil)
    (y!1 skolem-const-decl
     "(extend[[T1, T2], [(X!1), (Y!1)], bool, FALSE](fullset[[(X!1), (Y!1)]]))"
     cross_metric_cont nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (d const-decl "nnreal" cross_metric_spaces nil)
    (ball const-decl "set[T]" metric_spaces nil)
    (continuous_at? const-decl "bool" continuity_ms_def nil)
    (continuous? const-decl "bool" continuity_ms_def nil))
   shostak))
(one_variable_unif_cont_sequence 0
  (one_variable_unif_cont_sequence-1 nil 3460215379
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "uniformly_continuous_in_first?")
        (("1" (skosimp*)
          (("1" (inst 2 "epsilon!1/2")
            (("1" (inst 2 "y1!1")
              (("1"
                (inst 2
                 "(LAMBDA (n: posint): Let pointy = choose({point: [T1,T1,T2] | X!1(point`1) AND X!1(point`2) AND Y!1(point`3)
                AND d1(point`1, point`2) < 1 / n
                AND d2(y1!1, point`3) < 1 / n
                AND d3(f!1(point`1, y1!1), f!1(point`2, point`3)) >
                     epsilon!1 / 2}) in pointy)")
                (("1" (skosimp*)
                  (("1" (prop)
                    (("1" (assert) nil nil) ("2" (assert) nil nil)
                     ("3" (assert) nil nil) ("4" (assert) nil nil)
                     ("5" (assert) nil nil) ("6" (assert) nil nil))
                    nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (expand "nonempty?")
                    (("2" (expand "empty?")
                      (("2" (expand "member")
                        (("2" (inst + "1/(n!1+1)")
                          (("2" (skosimp*)
                            (("2" (inst - "(x1!1,x2!1,y2!1)")
                              (("2"
                                (prop)
                                (("1" (assert) nil nil)
                                 ("2" (assert) nil nil)
                                 ("3" (assert) nil nil)
                                 ("4"
                                  (case "1/(n!1+1) < 1/n!1")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (cross-mult +)
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("5"
                                  (case "1/(n!1+1) < 1/n!1")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (cross-mult +)
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("6" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "uniformly_continuous_in_first?")
        (("2" (skosimp*)
          (("2" (inst -2 "y!1" "epsilon!1/2")
            (("2" (skosimp*)
              (("2" (lemma "archimedean")
                (("2" (inst - "delta!1")
                  (("2" (skosimp*)
                    (("2" (inst - "n!1")
                      (("2" (prop)
                        (("2"
                          (inst - "seq!1(n!1)`1" "seq!1(n!1)`2"
                           "seq!1(n!1)`3")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((set type-eq-decl nil sets nil)
    (T2 formal-nonempty-type-decl nil cross_metric_cont nil)
    (empty? const-decl "bool" sets nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (times_div2 formula-decl nil real_props nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (member const-decl "bool" sets 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)
    (choose const-decl "(p)" sets nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (T1 formal-nonempty-type-decl nil cross_metric_cont nil)
    (nonempty? const-decl "bool" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (X!1 skolem-const-decl "set[T1]" cross_metric_cont nil)
    (Y!1 skolem-const-decl "set[T2]" cross_metric_cont nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_cont nil)
    (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_cont nil)
    (y1!1 skolem-const-decl "(Y!1)" cross_metric_cont nil)
    (T3 formal-nonempty-type-decl nil cross_metric_cont nil)
    (d3 formal-const-decl "[T3, T3 -> nnreal]" cross_metric_cont nil)
    (f!1 skolem-const-decl "[[T1, T2] -> T3]" cross_metric_cont nil)
    (epsilon!1 skolem-const-decl "posreal" cross_metric_cont nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (uniformly_continuous_in_first? const-decl "bool" cross_metric_cont
     nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (seq!1 skolem-const-decl "[posint -> [T1, T1, T2]]"
     cross_metric_cont nil)
    (n!1 skolem-const-decl "posnat" cross_metric_cont nil)
    (archimedean formula-decl nil real_props nil))
   shostak))
(curried_is_uniform 0
  (curried_is_uniform-1 nil 3460387624
   ("" (skosimp*)
    (("" (expand "uniformly_continuous?")
      (("" (expand "uniformly_continuous_in_first?")
        (("" (skosimp*)
          (("" (inst - "y!1" "epsilon!1")
            (("" (skosimp*)
              (("" (inst + "delta!1")
                (("" (skosimp*)
                  (("" (inst - "x!1" "p!1" "y!1")
                    (("" (assert)
                      (("" (lemma "fullset_metric_space2")
                        (("" (expand "metric_space?")
                          (("" (expand "space_zero?")
                            (("" (prop)
                              ((""
                                (inst - "y!1" "y!1")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (expand "fullset")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((uniformly_continuous? const-decl "bool" uniform_continuity nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (metric_space? const-decl "bool" metric_spaces_def nil)
    (y!1 skolem-const-decl "(Y!1)" cross_metric_cont nil)
    (Y!1 skolem-const-decl "set[T2]" cross_metric_cont nil)
    (fullset const-decl "set" sets nil)
    (space_zero? const-decl "bool" metric_spaces_def nil)
    (fullset_metric_space2 formula-decl nil cross_metric_cont nil)
    (T1 formal-nonempty-type-decl nil cross_metric_cont 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)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-nonempty-type-decl nil cross_metric_cont nil)
    (uniformly_continuous_in_first? const-decl "bool" cross_metric_cont
     nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.