products/Sources/formale Sprachen/PVS/reals/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: sigma_fseq.pvs   Sprache: Lisp

Original von: PVS©
(sigma_swap
 (IMP_sigma_TCC1 0
  (IMP_sigma_TCC1-1 nil 3479639154
   ("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
   ((connected_domain formula-decl nil sigma_swap nil)) nil))
 (sigma_swap 0
  (sigma_swap-1 nil 3479639154
   (""
    (case "NOT (FORALL (lowz: T_low, highz: T_high): NOT lowz > highz IMPLIES T_pred(highz))")
    (("1" (hide 2)
      (("1" (skosimp* t)
        (("1" (assert)
          (("1" (skosimp*)
            (("1" (typepred "j!1")
              (("1" (lemma "connected_domain")
                (("1" (inst - "lowz!1" "j!1" "highz!1")
                  (("1" (assert) nil nil)
                   ("2" (prop)
                    (("2" (skosimp*)
                      (("2" (lemma "connected_domain")
                        (("2" (assert)
                          (("2" (inst - "j!2" "j!1" "lowz!1")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (label "Tplem" -1)
      (("2" (hide "Tplem")
        (("2" (skeep)
          (("2" (case "high1 >= low1 AND high2 >= low2")
            (("1" (flatten)
              (("1" (name "k1" "high1-low1")
                (("1" (name "k2" "high2-low2")
                  (("1"
                    (case "high1 = low1 + k1 AND high2 = low2 + k2")
                    (("1" (flatten)
                      (("1" (replace -1)
                        (("1" (replace -2)
                          (("1"
                            (case "FORALL (kk1: nat): T_high?(low1+kk1) IMPLIES sigma(low1,low1+kk1,LAMBDA (i: T): sigma(low2, low2 + k2, LAMBDA (j: T): F(i, j))) = sigma(low2, low2 + k2,
                                                           LAMBDA (j: T): sigma(low1, low1 + kk1, LAMBDA (i: T): F(i, j)))")
                            (("1" (inst - "k1")
                              (("1"
                                (assert)
                                (("1"
                                  (typepred "high1")
                                  (("1"
                                    (split -)
                                    (("1"
                                      (inst + "high1")
                                      (("1" (assert) nil nil))
                                      nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (assert) nil nil))
                              nil)
                             ("2" (hide 2)
                              (("2"
                                (induct "kk1")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (expand "sigma" 1 1)
                                      (("1"
                                        (expand "sigma" 1 1)
                                        (("1"
                                          (expand "sigma" 1 3)
                                          (("1"
                                            (expand "sigma" 1 3)
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skosimp*)
                                  (("2"
                                    (split -)
                                    (("1"
                                      (case "NOT T_pred(low1+(j!1+1))")
                                      (("1"
                                        (reveal "Tplem")
                                        (("1"
                                          (inst - "low1" "1+j!1+low1")
                                          (("1" (assert) nil nil)
                                           ("2"
                                            (assert)
                                            (("2"
                                              (inst + "j!2")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (lemma "sigma_split")
                                        (("2"
                                          (inst
                                           -
                                           "LAMBDA (i: T): sigma(low2, low2 + k2, LAMBDA (j: T): F(i, j))"
                                           "low1 + (j!1+1)"
                                           "low1"
                                           "low1 + j!1")
                                          (("2"
                                            (assert)
                                            (("2"
                                              (replace -1)
                                              (("2"
                                                (hide -1)
                                                (("2"
                                                  (expand "sigma" 1 1)
                                                  (("2"
                                                    (expand
                                                     "sigma"
                                                     1
                                                     1)
                                                    (("2"
                                                      (replace -2)
                                                      (("2"
                                                        (hide -2)
                                                        (("2"
                                                          (rewrite
                                                           "sigma_sum")
                                                          (("1"
                                                            (expand
                                                             "sigma"
                                                             1
                                                             4)
                                                            (("1"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (inst
                                                               +
                                                               "j!2")
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (inst + "j!2")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (skosimp*)
                                  (("3" (inst + "j!1") nil nil))
                                  nil)
                                 ("4"
                                  (skosimp*)
                                  (("4"
                                    (typepred "high2")
                                    (("4" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("5"
                                  (skosimp*)
                                  (("5"
                                    (typepred "high2")
                                    (("5" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("6" (skosimp*) nil nil))
                                nil))
                              nil)
                             ("3" (skosimp*)
                              (("3" (inst + "j!1") nil nil)) nil)
                             ("4" (skosimp*) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (split)
              (("1" (expand "sigma" 2 1)
                (("1" (assert)
                  (("1" (expand "sigma" 2 2)
                    (("1" (lemma "sigma_zero")
                      (("1" (inst - "high2" "low2")
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "sigma" 2 2)
                (("2" (assert)
                  (("2" (expand "sigma" 2 2)
                    (("2" (lemma "sigma_zero")
                      (("2" (inst - "high1" "low1") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_zero formula-decl nil sigma nil)
    (sigma_nat application-judgement "nat" sigma_swap nil)
    (sigma_nnreal application-judgement "nnreal" sigma_swap nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (j!1 skolem-const-decl "nat" sigma_swap nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (sigma_sum formula-decl nil sigma nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sigma_split formula-decl nil sigma nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (low2 skolem-const-decl "T_low[T]" sigma_swap nil)
    (k2 skolem-const-decl "int" sigma_swap nil)
    (low1 skolem-const-decl "T_low[T]" sigma_swap nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (k1 skolem-const-decl "int" sigma_swap nil)
    (high1 skolem-const-decl "T_high[T]" sigma_swap nil)
    (sigma def-decl "real" sigma nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (>= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lowz!1 skolem-const-decl "T_low[T]" sigma_swap nil)
    (integer nonempty-type-from-decl nil integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected_domain formula-decl nil sigma_swap nil)
    (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)
    (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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" sigma_swap nil)
    (T formal-subtype-decl nil sigma_swap nil)
    (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma nil)
    (T_high type-eq-decl nil sigma nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil))
   shostak))
 (sigma_swap_triangle 0
  (sigma_swap_triangle-1 nil 3479644309
   ("" (skeep)
    (("" (label "highge" -1)
      (("" (hide "highge")
        (("" (lemma "sigma_swap")
          ((""
            (name "G"
                  "LAMBDA (i,j: T): IF j)
            (("" (inst - "G" "high1" "high2" "low1" "low1")
              (("" (lemma "sigma_restrict_eq")
                ((""
                  (inst-cp -
                   "LAMBDA (i: T): sigma(low1, high2, LAMBDA (j: T): G(i, j))"
                   "LAMBDA (i: T): sigma(i, high2, LAMBDA (j: T): F(i, j))"
                   "high1" "low1")
                  ((""
                    (inst -
                     "LAMBDA (j: T): sigma(low1, high1, LAMBDA (i: T): G(i, j))"
                     "LAMBDA (j: T): sigma(low1, j, LAMBDA (i: T): F(i, j))"
                     "high2" "low1")
                    (("" (split -)
                      (("1" (split -)
                        (("1" (assert) nil nil)
                         ("2" (hide 2)
                          (("2" (decompose-equality)
                            (("2" (expand "restrict")
                              (("2"
                                (lift-if)
                                (("2"
                                  (ground)
                                  (("2"
                                    (lemma "sigma_split")
                                    (("2"
                                      (inst
                                       -
                                       "LAMBDA (j: T): G(x!1, j)"
                                       "high2"
                                       "low1"
                                       "x!1-1")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (split -)
                                          (("1"
                                            (replace -1)
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (lemma
                                                 "sigma_restrict_eq")
                                                (("1"
                                                  (inst
                                                   -
                                                   "LAMBDA (j: T): G(x!1, j)"
                                                   "LAMBDA (j: T): 0"
                                                   "x!1-1"
                                                   "low1")
                                                  (("1"
                                                    (split -1)
                                                    (("1"
                                                      (replace -1)
                                                      (("1"
                                                        (lemma
                                                         "sigma_zero")
                                                        (("1"
                                                          (inst?)
                                                          (("1"
                                                            (replace
                                                             -1)
                                                            (("1"
                                                              (hide -1)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "sigma_restrict_eq")
                                                                  (("1"
                                                                    (inst?)
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (hide
                                                                         4)
                                                                        (("1"
                                                                          (decompose-equality)
                                                                          (("1"
                                                                            (expand
                                                                             "restrict")
                                                                            (("1"
                                                                              (lift-if)
                                                                              (("1"
                                                                                (ground)
                                                                                (("1"
                                                                                  (replace
                                                                                   -3
                                                                                   +
                                                                                   :dir
                                                                                   rl)
                                                                                  (("1"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide 4)
                                                      (("2"
                                                        (decompose-equality)
                                                        (("2"
                                                          (expand
                                                           "restrict")
                                                          (("2"
                                                            (lift-if)
                                                            (("2"
                                                              (ground)
                                                              (("2"
                                                                (replace
                                                                 -2
                                                                 +
                                                                 :dir
                                                                 rl)
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "sigma" + 2)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (lemma "sigma_zero")
                                                (("2"
                                                  (inst
                                                   -
                                                   "high2"
                                                   "low1")
                                                  (("2"
                                                    (replace
                                                     -1
                                                     +
                                                     :dir
                                                     rl)
                                                    (("2"
                                                      (lemma
                                                       "sigma_restrict_eq")
                                                      (("2"
                                                        (inst?)
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (decompose-equality)
                                                            (("2"
                                                              (expand
                                                               "restrict")
                                                              (("2"
                                                                (lift-if)
                                                                (("2"
                                                                  (ground)
                                                                  (("2"
                                                                    (replace
                                                                     -3
                                                                     :dir
                                                                     rl)
                                                                    (("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)
                       ("2" (hide 2)
                        (("2" (hide -1)
                          (("2" (decompose-equality)
                            (("2" (expand "restrict")
                              (("2"
                                (lift-if)
                                (("2"
                                  (ground)
                                  (("2"
                                    (lemma "sigma_split")
                                    (("2"
                                      (inst
                                       -
                                       "LAMBDA (i: T): G(i, x!1)"
                                       "high1"
                                       "low1"
                                       "x!1")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (split -)
                                          (("1"
                                            (replace -1)
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (lemma
                                                 "sigma_restrict_eq")
                                                (("1"
                                                  (inst
                                                   -
                                                   "LAMBDA (i: T): G(i, x!1)"
                                                   "LAMBDA (i: T): 0"
                                                   "high1"
                                                   "1+x!1")
                                                  (("1"
                                                    (split -)
                                                    (("1"
                                                      (replace -1)
                                                      (("1"
                                                        (hide -1)
                                                        (("1"
                                                          (lemma
                                                           "sigma_zero")
                                                          (("1"
                                                            (inst?)
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (hide
                                                                 -1)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (lemma
                                                                     "sigma_restrict_eq")
                                                                    (("1"
                                                                      (inst?)
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (hide
                                                                           4)
                                                                          (("1"
                                                                            (decompose-equality)
                                                                            (("1"
                                                                              (expand
                                                                               "restrict")
                                                                              (("1"
                                                                                (lift-if)
                                                                                (("1"
                                                                                  (ground)
                                                                                  (("1"
                                                                                    (replace
                                                                                     -1
                                                                                     :dir
                                                                                     rl)
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (decompose-equality)
                                                      (("2"
                                                        (expand
                                                         "restrict")
                                                        (("2"
                                                          (lift-if)
                                                          (("2"
                                                            (ground)
                                                            (("2"
                                                              (replace
                                                               -1
                                                               :dir
                                                               rl)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (reveal "highge")
                                            (("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)
   ((sigma_swap formula-decl nil sigma_swap nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma nil)
    (T_low type-eq-decl nil sigma nil)
    (sigma def-decl "real" sigma nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sigma_nat application-judgement "nat" sigma_swap nil)
    (sigma_nnreal application-judgement "nnreal" sigma_swap nil)
    (sigma_zero formula-decl nil sigma nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_split formula-decl nil sigma nil)
    (restrict const-decl "[T -> real]" sigma nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_restrict_eq formula-decl nil sigma 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)
    (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)
    (T_pred const-decl "[int -> boolean]" sigma_swap nil)
    (T formal-subtype-decl nil sigma_swap nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil)))


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


Bot Zugriff