Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: admissible.prf Sprache: Lisp

Original von: PVS^©

(admissible
(IMP_scott_TCC1 0
  (IMP_scott_TCC1-1 nil 3352441523
   ("" (expand "directed_complete_partial_order?")
    (("" (expand "partial_order?")
      (("" (expand "preorder?")
        (("" (split)
          (("1" (expand "reflexive?") (("1" (skosimp) nil nil)) nil)
           ("2" (expand "transitive?")
            (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)
           ("3" (expand "antisymmetric?")
            (("3" (skosimp)
              (("3" (assert)
                (("3" (case-replace "x!1") (("3" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (expand "directed_complete?")
            (("4" (skosimp)
              (("4" (typepred "D!1")
                (("4" (expand "least_bounded_above?")
                  (("4" (case "D!1(FALSE)")
                    (("1" (inst + "FALSE")
                      (("1" (expand "least_upper_bound?")
                        (("1" (split)
                          (("1" (expand "upper_bound?")
                            (("1" (propax) nil nil)) nil)
                           ("2" (skosimp)
                            (("2" (expand "upper_bound?")
                              (("2" (inst - "FALSE") nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (inst + "TRUE")
                      (("2" (expand "least_upper_bound?")
                        (("2" (expand "upper_bound?")
                          (("2" (skosimp)
                            (("2" (typepred "r!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((partial_order? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (antisymmetric? const-decl "bool" relations nil)
    (least_bounded_above? const-decl "bool" bounded_orders "orders/")
    (TRUE const-decl "bool" booleans nil)
    (upper_bound? const-decl "bool" bounded_orders "orders/")
    (D!1 skolem-const-decl "(directed?(WHEN))" admissible nil)
    (least_upper_bound? const-decl "bool" bounded_orders "orders/")
    (FALSE const-decl "bool" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (pred type-eq-decl nil defined_types nil)
    (directed? const-decl "bool" directed_orders "orders/")
    (WHEN const-decl "[bool, bool -> bool]" booleans nil)
    (directed_complete? const-decl "bool" directed_orders "orders/")
    (preorder? const-decl "bool" orders nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/"))
   nil))
(admissible_pred?_TCC1 0
  (admissible_pred?_TCC1-1 nil 3355370441 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   nil))
(admissible_pred?_TCC2 0
  (admissible_pred?_TCC2-1 nil 3355370441
   ("" (skosimp)
    (("" (hide -1)
      (("" (split)
        (("1" (expand "lub_set?")
          (("1" (expand "least_bounded_above?")
            (("1" (typepred "<=")
              (("1" (expand "pointed_directed_complete_partial_order?")
                (("1" (flatten)
                  (("1" (expand "fullset")
                    (("1" (expand "has_least?")
                      (("1" (skosimp)
                        (("1" (expand "least?")
                          (("1" (expand "lower_bound?")
                            (("1" (inst + "t!1")
                              (("1"
                                (expand "least_upper_bound?")
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (split)
                                    (("1"
                                      (expand "upper_bound?")
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (typepred "r!1")
                                          (("1"
                                            (expand "empty?")
                                            (("1"
                                              (inst -3 "r!1")
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (expand "upper_bound?")
                                      (("2"
                                        (skosimp*)
                                        (("2" (inst -2 "r!1") nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "directed_is_lub_set[T,<=]")
          (("2" (inst - "D!1") nil nil)) nil))
        nil))
      nil))
    nil)
   ((directed_is_lub_set judgement-tcc nil directed_order_props
     "orders/")
    (D!1 skolem-const-decl "set[T]" admissible nil)
    (directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (nonempty? const-decl "bool" sets nil)
    (lub_set? const-decl "bool" bounded_order_props "orders/")
    (<= formal-const-decl
        "(pointed_directed_complete_partial_order?[T])" admissible nil)
    (pointed_directed_complete_partial_order? const-decl "bool"
     directed_orders "orders/")
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil admissible nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (has_least? const-decl "bool" minmax_orders "orders/")
    (least? const-decl "bool" minmax_orders "orders/")
    (TRUE const-decl "bool" booleans nil)
    (upper_bound? const-decl "bool" bounded_orders "orders/")
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (least_upper_bound? const-decl "bool" bounded_orders "orders/")
    (lower_bound? const-decl "bool" bounded_orders "orders/")
    (fullset const-decl "set" sets nil)
    (least_bounded_above? const-decl "bool" bounded_orders "orders/"))
   nil))
(admissible_pred_TCC1 0
  (admissible_pred_TCC1-1 nil 3352441523
   ("" (expand "admissible_pred?")
    (("" (expand "lub_preserving?")
      (("" (skosimp)
        (("" (typepred "D!1")
          (("" (typepred "lub(image((LAMBDA x: TRUE), D!1))")
            (("1" (expand "least_upper_bound?")
              (("1" (flatten)
                (("1" (expand "upper_bound?")
                  (("1" (inst -2 "TRUE")
                    (("1" (split -2)
                      (("1" (propax) nil nil)
                       ("2" (skosimp)
                        (("2" (typepred "r!1")
                          (("2" (expand "image")
                            (("2" (skosimp) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((admissible_pred? const-decl "bool" admissible nil)) nil))
(fixpoint_induction 0
  (fixpoint_induction-1 nil 3352753630
   ("" (skosimp)
    (("" (typepred "p!1")
      (("" (expand "admissible_pred?")
        (("" (inst-cp - "emptyset[T]")
          (("" (rewrite "lub_emptyset")
            (("" (split -2)
              (("1" (inst - "FIX_APPROX(phi!1)")
                (("1" (lemma "fix_approx_nonempty" ("phi" "phi!1"))
                  (("1" (lemma "fix_approx_chain" ("phi" "phi!1"))
                    (("1"
                      (lemma "ne_chain_is_directed"
                       ("X" "FIX_APPROX(phi!1)"))
                      (("1" (expand "directed?" -5)
                        (("1" (assert)
                          (("1" (expand "fix")
                            (("1" (split -5)
                              (("1" (propax) nil nil)
                               ("2"
                                (hide-all-but (-4 -5 1))
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (typepred "x!1")
                                    (("2"
                                      (expand "FIX_APPROX")
                                      (("2"
                                        (expand "image")
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (replace -1)
                                            (("2"
                                              (hide -1)
                                              (("2"
                                                (case
                                                 "forall (n:nat): p!1(power(phi!1,n)(bottom))")
                                                (("1"
                                                  (inst - "x!2")
                                                  nil
                                                  nil)
                                                 ("2"
                                                  (hide 2)
                                                  (("2"
                                                    (induct "n")
                                                    (("1"
                                                      (expand "power")
                                                      (("1"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (skosimp*)
                                                      (("2"
                                                        (expand
                                                         "power"
                                                         1)
                                                        (("2"
                                                          (expand "o")
                                                          (("2"
                                                            (inst
                                                             -
                                                             "power(phi!1, j!1)(bottom)")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (skosimp)
                (("2" (typepred "x!1")
                  (("2" (expand "emptyset") (("2" (propax) nil nil))
                    nil))
                  nil))
                nil)
               ("3" (expand "empty?")
                (("3" (flatten)
                  (("3" (skosimp)
                    (("3" (expand "member")
                      (("3" (expand "emptyset")
                        (("3" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((admissible_pred nonempty-type-eq-decl nil admissible nil)
    (admissible_pred? const-decl "bool" admissible nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil admissible nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (fix_approx_nonempty formula-decl nil fixpoints nil)
    (ne_chain_is_directed formula-decl nil fixpoints nil)
    (nonempty? const-decl "bool" sets nil)
    (nat_induction formula-decl nil naturalnumbers 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)
    (O const-decl "T3" function_props nil)
    (power def-decl "T" monoid_def "algebra/")
    (least? const-decl "bool" minmax_orders "orders/")
    (fullset const-decl "set" sets nil)
    (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))"
     fixpoints nil)
    (image const-decl "set[R]" function_image nil)
    (fix const-decl "T" fixpoints nil)
    (directed? const-decl "bool" directed_order_props "orders/")
    (fix_approx_chain formula-decl nil fixpoints nil)
    (increasing? const-decl "bool" fun_preds_partial nil)
    (FIX_APPROX const-decl "set[T]" fixpoints nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_emptyset name-judgement "finite_set[T]" admissible nil)
    (emptyset_is_clopen name-judgement "clopen[T, scott_open_sets]"
     admissible nil)
    (finite_emptyset name-judgement "finite_set[T]" bounded_orders
     "orders/")
    (finite_emptyset name-judgement "finite_set[T]" directed_orders
     "orders/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (lub_emptyset formula-decl nil fixpoints nil)
    (pointed_directed_complete_partial_order? const-decl "bool"
     directed_orders "orders/")
    (<= formal-const-decl
        "(pointed_directed_complete_partial_order?[T])" admissible
        nil))
   shostak)))

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