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: outer_syntax.ML   Sprache: Lisp

Original von: PVS©
(finite_pointwise_orders
 (IMP_infinite_pigeonhole_TCC1 0
  (IMP_infinite_pigeonhole_TCC1-1 nil 3314641151
   ("" (forward-chain "nat_infinite") nil nil)
   ((nat_infinite formula-decl nil numbers_infinite nil)) nil))
 (IMP_infinite_pigeonhole_TCC2 0
  (IMP_infinite_pigeonhole_TCC2-1 nil 3314641151
   ("" (forward-chain "domain_finiteness") nil nil)
   ((domain_finiteness formula-decl nil finite_pointwise_orders nil))
   nil))
 (infinite_pigeonhole 0
  (infinite_pigeonhole-1 nil 3314641222
   ("" (skolem!)
    (("" (use "infinite_pigeonhole")
      (("" (skolem!)
        (("" (inst?)
          (("" (use "enumerable")
            (("1" (skolem-typepred)
              (("1" (inst?)
                (("1" (skolem!)
                  (("1" (decompose-equality)
                    (("1" (inst - "f!2(n!1)")
                      (("1"
                        (expand* "image" "inverse_image" "singleton"
                         "member")
                        (("1" (replace*)
                          (("1" (assert)
                            (("1" (inst?)
                              (("1"
                                (expand "fullset")
                                (("1" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2"
                  (expand* "strictly_monotone?" "preserves" "preserves"
                   "restrict")
                  nil nil))
                nil))
              nil)
             ("2" (expand* "enumerable?" "bounded_below?")
              (("2" (assert)
                (("2" (inst + 0)
                  (("2" (expand* "lower_bound?" "restrict") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((infinite_pigeonhole formula-decl nil infinite_pigeonhole 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)
    (D formal-type-decl nil finite_pointwise_orders nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (strictly_monotone? const-decl "bool" integer_enumerations nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (preserves const-decl "bool" functions nil)
    (n!1 skolem-const-decl "nat" finite_pointwise_orders nil)
    (member const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (image const-decl "set[R]" function_image nil)
    (fullset const-decl "set" sets nil)
    (f!2 skolem-const-decl "(strictly_monotone?)"
     finite_pointwise_orders nil)
    (< const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (preserves const-decl "bool" functions nil)
    (PRED type-eq-decl nil defined_types nil)
    (strict_total_order_restrict application-judgement
     "(strict_total_order?[S])" restrict_order_props nil)
    (trichotomous_restrict application-judgement "(trichotomous?[S])"
     restrict_order_props nil)
    (strict_order_restrict application-judgement "(strict_order?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (irreflexive_restrict application-judgement "(irreflexive?[S])"
     restrict_order_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" bounded_orders nil)
    (r!1 skolem-const-decl "D" finite_pointwise_orders nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (f!1 skolem-const-decl "[nat -> D]" finite_pointwise_orders nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (enumerable formula-decl nil integer_enumerations nil))
   shostak))
 (descending_exists 0
  (descending_exists-1 nil 3314641512
   ("" (skosimp)
    (("" (expand "descending?")
      (("" (inst?)
        ((""
          (expand* "strictly_pointwise" "irreflexive_kernel"
           "difference" "member")
          (("" (flatten)
            (("" (decompose-equality)
              ((""
                (expand* "pointwise" "reflexive_closure" "union"
                 "member")
                (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((descending? const-decl "bool" monotone_sequences nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (strictly_pointwise const-decl "pred[[[D -> R], [D -> R]]]"
     pointwise_orders nil)
    (reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" well_foundedness nil)
    (pointwise_preserves_preorder application-judgement
     "(preorder?[[D -> R]])" finite_pointwise_orders nil)
    (pointwise_preserves_transitive application-judgement
     "(transitive?[[D -> R]])" finite_pointwise_orders nil)
    (pointwise_preserves_reflexive application-judgement
     "(reflexive?[[D -> R]])" finite_pointwise_orders nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (D formal-type-decl nil finite_pointwise_orders nil)
    (R formal-type-decl nil finite_pointwise_orders nil)
    (pointwise const-decl "bool" pointwise_orders nil)
    (union const-decl "set" sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (descending_reflexive_closure 0
  (descending_reflexive_closure-1 nil 3314641603
   ("" (expand "descending?")
    (("" (skosimp*)
      (("" (inst?)
        ((""
          (expand* "strictly_pointwise" "irreflexive_kernel"
           "difference" "member" "pointwise")
          (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (pointwise const-decl "bool" pointwise_orders nil)
    (difference const-decl "set" sets nil)
    (strictly_pointwise const-decl "pred[[[D -> R], [D -> R]]]"
     pointwise_orders nil)
    (D formal-type-decl nil finite_pointwise_orders 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)
    (descending? const-decl "bool" monotone_sequences nil))
   shostak))
 (pointwise_pigeonhole 0
  (pointwise_pigeonhole-1 nil 3314641647
   ("" (skosimp)
    (("" (use "infinite_pigeonhole")
      ((""
        (inst -
         "LAMBDA n: epsilon({d | rel!1(seq!1(n + 1)(d), seq!1(n)(d))})")
        (("1" (skolem-typepred)
          (("1" (inst? +)
            (("1" (inst? +)
              (("1" (expand "descending?" +)
                (("1" (skolem!)
                  (("1" (inst - "n!1")
                    (("1" (use "epsilon_ax[D]")
                      (("1" (replace -3 :hide? t)
                        (("1" (split)
                          (("1" (lemma "descending_lem[R]")
                            (("1"
                              (inst - "reflexive_closure(rel!1)"
                               "LAMBDA n: seq!1(n)(d!1)")
                              (("1"
                                (expand*
                                 "preserves"
                                 "restrict"
                                 "converse"
                                 "reflexive_closure"
                                 "union"
                                 "member")
                                (("1"
                                  (inst
                                   -
                                   "g!1(n!1) + 1"
                                   "g!1(1 + n!1)")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (split)
                                      (("1"
                                        (lemma "transitive[R]")
                                        (("1"
                                          (inst
                                           -
                                           "rel!1"
                                           "seq!1(g!1(1 + n!1))(d!1)"
                                           "seq!1(g!1(n!1) + 1)(d!1)"
                                           "seq!1(g!1(n!1))(d!1)")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand*
                                         "preserves"
                                         "preserves"
                                         "restrict")
                                        (("2"
                                          (inst - "n!1" "n!1 + 1")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (rewrite
                                 "descending_reflexive_closure")
                                nil
                                nil))
                              nil))
                            nil)
                           ("2" (rewrite "descending_exists") nil nil))
                          nil))
                        nil)
                       ("2" (inst + "d!1") nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (use "descending_exists")
          (("2" (assert) (("2" (skolem!) (("2" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((infinite_pigeonhole formula-decl nil finite_pointwise_orders nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (< const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (preserves const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" well_foundedness nil)
    (sequence type-eq-decl nil sequences nil)
    (reflexive? const-decl "bool" relations nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (rel!1 skolem-const-decl "(transitive?[R])" finite_pointwise_orders
     nil)
    (seq!1 skolem-const-decl "[nat -> [D -> R]]"
     finite_pointwise_orders nil)
    (d!1 skolem-const-decl "D" finite_pointwise_orders nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (transitive formula-decl nil relations_extra nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (preserves const-decl "bool" functions nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (descending_reflexive_closure formula-decl nil
     finite_pointwise_orders nil)
    (descending_lem formula-decl nil monotone_sequences nil)
    (descending_exists formula-decl nil finite_pointwise_orders nil)
    (descending? const-decl "bool" monotone_sequences nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (R formal-type-decl nil finite_pointwise_orders nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types 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)
    (D formal-type-decl nil finite_pointwise_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   shostak))
 (strictly_pointwise_well_founded_order 0
  (strictly_pointwise_well_founded_order-1 nil 3314641151
   ("" (skolem-typepred)
    (("" (expand "well_founded_order?")
      (("" (prop)
        (("1" (rewrite "no_infinite_descending_sequence[R]")
          (("1" (rewrite "no_infinite_descending_sequence[[D->R]]")
            (("1" (expand* "empty?" "member")
              (("1" (skolem!)
                (("1" (forward-chain "pointwise_pigeonhole")
                  (("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "strictly_pointwise")
          (("2" (invoke (typepred "%1") (! 1 1))
            (("2" (expand "strict_order?") (("2" (flatten) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((order_to_strict_order application-judgement "(strict_order?)"
     well_foundedness nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (reflexive? const-decl "bool" relations nil)
    (pointwise const-decl "bool" pointwise_orders nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (irreflexive? const-decl "bool" relations nil)
    (strict_order? const-decl "bool" orders nil)
    (pointwise_preserves_reflexive application-judgement
     "(reflexive?[[D -> R]])" finite_pointwise_orders nil)
    (order_to_partial_order application-judgement "(partial_order?)"
     well_foundedness nil)
    (no_infinite_descending_sequence formula-decl nil well_foundedness
     nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (pointwise_pigeonhole formula-decl nil finite_pointwise_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations 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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (preserves const-decl "bool" functions nil)
    (restrict const-decl "R" restrict nil)
    (< const-decl "bool" reals nil)
    (D formal-type-decl nil finite_pointwise_orders nil)
    (strictly_pointwise const-decl "pred[[[D -> R], [D -> R]]]"
     pointwise_orders nil)
    (well_founded_order? const-decl "bool" well_foundedness nil)
    (pred type-eq-decl nil defined_types nil)
    (R formal-type-decl nil finite_pointwise_orders 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.31 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