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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: well_foundedness.prf   Sprache: Lisp

Original von: PVS©
(well_foundedness
 (no_infinite_descending_sequence 0
  (no_infinite_descending_sequence-1 nil 3318615614
   ("" (skolem!)
    (("" (expand* "empty?" "member" "descending?" "well_founded?")
      (("" (prop)
        (("1" (skolem!)
          (("1" (inst - "LAMBDA x: EXISTS n: x = x!1(n)")
            (("1" (split)
              (("1" (skosimp* t)
                (("1" (replace -2 :hide? t)
                  (("1" (inst - "x!1(1 + n!1)")
                    (("1" (inst?) nil nil) ("2" (inst?) nil nil)) nil))
                  nil))
                nil)
               ("2" (inst + "x!1(0)") (("2" (inst?) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (rewrite "skolemize_forall[(p!1), (p!1)]")
            (("2" (skolem!)
              (("2" (inst - "LAMBDA n: iterate(f!1, n)(y!1)")
                (("2" (skolem!)
                  (("2" (expand "iterate" 1 1) (("2" (inst?) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (well_founded? const-decl "bool" orders nil)
    (descending? const-decl "bool" monotone_sequences nil)
    (empty? const-decl "bool" sets nil)
    (iterate def-decl "T" function_iterate nil)
    (y!1 skolem-const-decl "T" well_foundedness nil)
    (p!1 skolem-const-decl "pred[T]" well_foundedness nil)
    (skolemize_forall formula-decl nil skolemization nil)
    (n!1 skolem-const-decl "nat" well_foundedness nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (x!1 skolem-const-decl "sequence[T]" well_foundedness nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil well_foundedness nil))
   shostak))
 (well_founded_is_irreflexive 0
  (well_founded_is_irreflexive-1 nil 3318615593
   ("" (skolem-typepred)
    (("" (rewrite "no_infinite_descending_sequence")
      (("" (expand* "empty?" "member" "descending?" "irreflexive?")
        (("" (skolem!)
          (("" (inst - "LAMBDA n: x!2") (("" (skolem!) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((no_infinite_descending_sequence formula-decl nil well_foundedness
     nil)
    (sequence type-eq-decl nil sequences 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)
    (empty? const-decl "bool" sets nil)
    (descending? const-decl "bool" monotone_sequences nil)
    (irreflexive? const-decl "bool" relations nil)
    (member const-decl "bool" sets nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil well_foundedness nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (well_order_is_well_founded_order 0
  (well_order_is_well_founded_order-1 nil 3318615593
   ("" (judgement-tcc) nil 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 well_foundedness nil)
    (pred type-eq-decl nil defined_types nil)
    (well_ordered? const-decl "bool" orders nil)
    (strict_total_order? const-decl "bool" orders nil)
    (trichotomous? const-decl "bool" orders nil)
    (strict_order? const-decl "bool" orders nil)
    (irreflexive? const-decl "bool" relations nil)
    (well_founded? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (well_founded_order? const-decl "bool" well_foundedness nil))
   nil))
 (well_founded_order_is_well_founded 0
  (well_founded_order_is_well_founded-1 nil 3318615593
   ("" (judgement-tcc) nil 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 well_foundedness nil)
    (pred type-eq-decl nil defined_types nil)
    (well_founded_order? const-decl "bool" well_foundedness nil)
    (transitive? const-decl "bool" relations nil)
    (well_founded? const-decl "bool" orders nil))
   nil))
 (well_founded_order_is_strict_order 0
  (well_founded_order_is_strict_order-1 nil 3318615593
   ("" (skolem-typepred)
    (("" (expand* "strict_order?" "well_founded_order?")
      (("" (prop)
        (("" (rewrite "well_founded_is_irreflexive") nil nil)) nil))
      nil))
    nil)
   ((strict_order? const-decl "bool" orders nil)
    (well_founded_is_irreflexive judgement-tcc nil well_foundedness
     nil)
    (well_founded? const-decl "bool" orders nil)
    (well_founded_order? const-decl "bool" well_foundedness nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil well_foundedness nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (transitive_closure_preserves_well_foundedness 0
  (transitive_closure_preserves_well_foundedness-1 nil 3318615593
   ("" (skolem-typepred)
    (("" (expand* "well_founded_order?" "well_founded?")
      (("" (skosimp*)
        ((""
          (inst -
           "LAMBDA (y: T): EXISTS (x: T): preorder_closure[T](rel!1)(x, y) & p!1(x)")
          (("" (prop)
            (("1" (skosimp* t)
              (("1" (rewrite "preorder_closure_reflexive_transitive")
                (("1" (expand* "reflexive_closure" "union" "member")
                  (("1" (split)
                    (("1" (hide 1)
                      (("1" (rewrite "transitive_closure_step_r")
                        (("1" (expand "o")
                          (("1" (skosimp)
                            (("1" (inst - "y!3")
                              (("1"
                                (inst + "x!1")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (inst + "x!1")
                      (("2" (skolem!)
                        (("2" (rewrite "transitive_closure_step_r")
                          (("2" (expand "o")
                            (("2" (skosimp)
                              (("2"
                                (inst - "y!3")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (inst?)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst? 2)
              (("2" (skolem!)
                (("2" (inst + "y!1")
                  (("2" (inst + "x!1")
                    (("2"
                      (expand* "preorder_closure" "transitive_closure"
                       "IUnion")
                      (("2" (skolem!) (("2" (inst?) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((well_founded_order? const-decl "bool" well_foundedness nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (preorder? const-decl "bool" orders nil)
    (preorder_closure const-decl "(preorder?)" closure_ops nil)
    (y!1 skolem-const-decl "T" well_foundedness nil)
    (transitive_closure const-decl "(transitive?)" closure_ops nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (x!1 skolem-const-decl "T" well_foundedness nil)
    (y!3 skolem-const-decl "T" well_foundedness nil)
    (O const-decl "bool" relation_props nil)
    (rel!1 skolem-const-decl "(well_founded?[T])" well_foundedness nil)
    (y!3 skolem-const-decl "T" well_foundedness nil)
    (p!1 skolem-const-decl "pred[T]" well_foundedness nil)
    (transitive_closure_step_r formula-decl nil closure_ops nil)
    (reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" well_foundedness nil)
    (preorder_closure_reflexive_transitive formula-decl nil closure_ops
     nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil well_foundedness nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)))


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