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: Unknown

(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.3 Sekunden  (vorverarbeitet)  ]