Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
products/sources/formale sprachen/PVS/structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: max_array_def.prf   Sprache: Lisp

Original von: PVS©
(max_array_def
 (imax_rec_TCC1 0
  (imax_rec_TCC1-1 nil 3506271669
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (imax_rec_TCC2 0
  (imax_rec_TCC2-1 nil 3506271669 ("" (termination-tcc) nil nil) nil
   nil))
 (imax_rec_lem 0
  (imax_rec_lem-1 nil 3506271669
   ("" (typepred "max_array_def.<=")
    (("" (expand "total_order?")
      (("" (expand "partial_order?")
        (("" (expand "preorder?")
          (("" (flatten)
            (("" (induct "jj")
              (("1" (flatten)
                (("1" (skosimp*)
                  (("1" (expand "imax_rec")
                    (("1" (expand "reflexive?")
                      (("1" (inst?) (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (skosimp*)
                (("2" (assert)
                  (("2" (expand "imax_rec" 1)
                    (("2" (inst?)
                      (("2" (inst -2 "ii!1")
                        (("2" (assert)
                          (("2" (lift-if)
                            (("2" (expand "amax" 1)
                              (("2"
                                (lift-if)
                                (("2"
                                  (expand "reflexive?")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (ground)
                                      (("2"
                                        (expand "dichotomous?")
                                        (("2"
                                          (inst
                                           -8
                                           "A!1(j!1) "
                                           " A!1(1 + jb!1)")
                                          (("2"
                                            (assert)
                                            (("2"
                                              (expand "transitive?")
                                              (("2"
                                                (inst
                                                 -6
                                                 "A!1(1 + jb!1)"
                                                 " A!1(j!1)"
                                                 "A!1(imax_rec(A!1, ii!1, jb!1))")
                                                (("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)
   ((preorder? const-decl "bool" orders nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (imax_rec def-decl "below(N)" max_array_def nil)
    (N formal-const-decl "nat" max_array_def nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (below_induction formula-decl nil bounded_nat_inductions nil)
    (reflexive? const-decl "bool" relations nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (amax const-decl "below(N)" max_array_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (transitive? const-decl "bool" relations nil)
    (dichotomous? const-decl "bool" orders nil)
    (partial_order? const-decl "bool" orders 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 max_array_def nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" max_array_def nil))
   nil))
 (imax_rec_rng 0
  (imax_rec_rng-1 nil 3506271669
   ("" (induct "jj")
    (("1" (skosimp*)
      (("1" (expand "imax_rec") (("1" (propax) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (assert)
        (("2" (expand "imax_rec" 1)
          (("2" (inst?)
            (("2" (lift-if)
              (("2" (expand "amax")
                (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (amax const-decl "below(N)" max_array_def nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (below_induction formula-decl nil bounded_nat_inductions 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "nat" max_array_def nil)
    (imax_rec def-decl "below(N)" max_array_def nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil max_array_def nil)
    (pred type-eq-decl nil defined_types nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil))
   nil))
 (Imax_rec_TCC1 0
  (Imax_rec_TCC1-1 nil 3506271669
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (Imax_rec_TCC2 0
  (Imax_rec_TCC2-1 nil 3507072889
   ("" (skosimp*) (("" (rewrite "imax_rec_rng") nil nil)) 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)
    (imax_rec_rng formula-decl nil max_array_def 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (N formal-const-decl "nat" max_array_def nil)
    (below type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil max_array_def nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (abv type-eq-decl nil max_array_def nil))
   nil))
 (Imax_TCC1 0
  (Imax_TCC1-1 nil 3506271669 ("" (subtype-tcc) nil nil) nil nil))
 (Imax_TCC2 0
  (Imax_TCC2-1 nil 3506271669
   (""
    (inst 1 "(LAMBDA (x: [[below(N) -> T], ii: below(N), abv(ii)]):
                   Imax_rec(Proj_1(x),Proj_2(x),Proj_3(x)))")
    (("" (skosimp*)
      (("" (expand "Imax_rec") (("" (rewrite "imax_rec_lem") nil nil))
        nil))
      nil))
    nil)
   ((imax_rec_lem formula-decl nil max_array_def nil)
    (Imax_rec const-decl "subrange(ii, jj)" max_array_def nil)
    (<= formal-const-decl "(total_order?[T])" max_array_def nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (abv type-eq-decl nil max_array_def nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil max_array_def nil)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "nat" max_array_def nil)
    (< const-decl "bool" reals 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))
   nil))
 (Imax_1_TCC1 0
  (Imax_1_TCC1-1 nil 3506271669 ("" (subtype-tcc) nil nil) nil nil))
 (Imax_1 0
  (Imax_1-1 nil 3506271669
   ("" (skosimp*)
    (("" (typepred "Imax(A!1, ii!1, ii!1)") (("" (assert) nil nil))
      nil))
    nil)
   ((Imax const-decl
     "{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(j) <= A(i))}"
     max_array_def nil)
    (<= formal-const-decl "(total_order?[T])" max_array_def nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (abv type-eq-decl nil max_array_def nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil max_array_def nil)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "nat" max_array_def nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (<= 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil)))


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