Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: poly_strategy.prf Sprache: Lisp

Original von: PVS^©

(poly_strategy
(sturm_TCC1 0
  (sturm_TCC1-1 nil 3601816771
   ("" (skeep)
    (("" (assert)
      (("" (rewrite "list2array_sound")
        (("" (assert)
          (("" (typepred "deg(pl)") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rat nonempty-type-eq-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)
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (/= const-decl "boolean" notequal nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props 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)
    (> const-decl "bool" reals nil)
    (Polylist type-eq-decl nil polylist nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (list2array_sound formula-decl nil array2list "structures/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff nil)
    (listn_0 name-judgement "listn[real](0)" polynomial_division nil)
    (listn_0 name-judgement "listn[rat](0)" polylist nil))
   nil))
(sturm_def_TCC1 0
  (sturm_def_TCC1-1 nil 3601816771
   ("" (skeep)
    (("" (assert)
      (("" (typepred "deg(pl)") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (< const-decl "bool" reals nil) (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist 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)
    (length def-decl "nat" list_props nil)
    (below type-eq-decl nil naturalnumbers nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (/= const-decl "boolean" notequal nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist nil)
    (listn_0 name-judgement "listn[int](0)" gcd_coeff nil)
    (listn_0 name-judgement "listn[real](0)" polynomial_division nil)
    (listn_0 name-judgement "listn[rat](0)" polylist nil))
   nil))
(sturm_def 0
  (sturm_def-1 nil 3601816880
   ("" (skeep)
    (("" (case "NOT deg(pl)>0")
      (("1" (hide 2)
        (("1" (assert)
          (("1" (typepred "deg(pl)") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (hide -3)
        (("2" (assert)
          (("2" (expand "sturm")
            (("2" (lemma "compute_poly_sat_rational_def")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (split -1)
                    (("1" (replaces -1)
                      (("1" (ground)
                        (("1" (skeep)
                          (("1" (inst - "x")
                            (("1" (rewrite "polylist_eval" 1)
                              (("1"
                                (assert)
                                (("1"
                                  (rewrite
                                   "polylist_eval_deg"
                                   -1
                                   :dir
                                   rl)
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skeep)
                          (("2" (inst - "x")
                            (("2" (assert)
                              (("2"
                                (rewrite "polylist_eval" -1)
                                (("2"
                                  (rewrite
                                   "polylist_eval_deg"
                                   1
                                   :dir
                                   rl)
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (flatten)
                        (("2" (rewrite "list2array_sound")
                          (("2" (typepred "deg(pl)")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (/= const-decl "boolean" notequal nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props 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)
    (Polylist type-eq-decl nil polylist nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt 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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (compute_poly_sat_rational_def formula-decl nil compute_sturm nil)
    (list2array_sound formula-decl nil array2list "structures/")
    (polylist_eval formula-decl nil polylist nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (polylist_eval_deg formula-decl nil polylist nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (list2array def-decl "T" array2list "structures/")
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (SturmRel? const-decl "bool" compute_sturm nil)
    (sturm const-decl "bool" poly_strategy nil)
    (listn_0 name-judgement "listn[int](0)" gcd_coeff nil)
    (listn_0 name-judgement "listn[real](0)" polynomial_division nil)
    (listn_0 name-judgement "listn[rat](0)" polylist nil))
   shostak)))

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