Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: product_fseq.prf Sprache: Lisp

Original von: PVS^©

(vertical_cr
(hor_circle_horizontal_only 0
  (hor_circle_horizontal_only-1 nil 3471199310
   ("" (skeep)
    (("" (expand "hor_circle?")
      (("" (split)
        (("1" (expand "gs_vertical?")
          (("1" (flatten)
            (("1" (typepred "gs_vertical(sp, vo, vi, epsh, epsv)")
              (("1" (assert) nil nil)) nil))
            nil))
          nil)
         ("2" (expand "trk_vertical?")
          (("2" (flatten)
            (("2" (skeep -1)
              (("2"
                (typepred
                 "trk_vertical_irt(sp, vo, vi, epsh, epsv, irt)")
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil)
         ("3" (expand "opt_vertical?")
          (("3" (flatten)
            (("3" (typepred "opt_vertical(sp, vo, vi, epsh, epsv)")
              (("3" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((hor_circle? const-decl "bool" vertical_cr nil)
    (opt_vertical? const-decl "bool" opt_vertical nil)
    (opt_vertical const-decl
     "{nvo | vect2(nvo) /= zero => vo`z = nvo`z}" opt_vertical nil)
    (trk_vertical? const-decl "bool" trk_circle nil)
    (trk_only? const-decl "bool" definitions nil)
    (trk_vertical_irt const-decl "{nvo |
         vect2(nvo) /= zero =>
          trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}"
     trk_circle nil)
    (gs_vertical? const-decl "bool" gs_circle nil)
    (Sp_vect3 type-eq-decl nil space_3D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (gs_vertical const-decl "{nvo |
         vect2(nvo) /= zero =>
          gs_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" gs_circle
     nil)
    (H formal-const-decl "posreal" vertical_cr nil)
    (D formal-const-decl "posreal" vertical_cr nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (gs_only? const-decl "bool" definitions nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nzint nonempty-type-eq-decl nil integers 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_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)
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(vertical_cr_meets_vertical_criterion 0
  (vertical_cr_meets_vertical_criterion-1 nil 3471192580
   ("" (skeep)
    (("" (expand "vertical_cr?")
      (("" (split -2)
        (("1" (lemma "vs_circle_meets_vertical_criterion")
          (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
         ("2" (expand "hor_circle?")
          (("2" (split)
            (("1" (lemma "gs_vertical_meets_vertical_criterion")
              (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
             ("2" (lemma "trk_vertical_meets_vertical_criterion")
              (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)
             ("3" (lemma "opt_vertical_meets_vertical_criterion")
              (("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((vertical_cr? const-decl "bool" vertical_cr nil)
    (hor_circle? const-decl "bool" vertical_cr nil)
    (opt_vertical_meets_vertical_criterion formula-decl nil
     opt_vertical nil)
    (trk_vertical_meets_vertical_criterion formula-decl nil trk_circle
     nil)
    (gs_vertical_meets_vertical_criterion formula-decl nil gs_circle
     nil)
    (H formal-const-decl "posreal" vertical_cr nil)
    (D formal-const-decl "posreal" vertical_cr nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (vs_circle_meets_vertical_criterion formula-decl nil vs_circle nil)
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Sp_vect3 type-eq-decl nil space_3D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal 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))
   shostak))
(hor_circle_meets_horizontal_criterion 0
  (hor_circle_meets_horizontal_criterion-1 nil 3471200403
   ("" (skeep)
    (("" (expand "hor_circle?")
      (("" (split)
        (("1" (lemma "gs_vertical_meets_horizontal_criterion")
          (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
         ("2" (lemma "trk_vertical_meets_horizontal_criterion")
          (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)
         ("3" (lemma "opt_vertical_meets_horizontal_criterion")
          (("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((hor_circle? const-decl "bool" vertical_cr nil)
    (opt_vertical_meets_horizontal_criterion formula-decl nil
     opt_vertical nil)
    (trk_vertical_meets_horizontal_criterion formula-decl nil
     trk_circle nil)
    (H formal-const-decl "posreal" vertical_cr nil)
    (D formal-const-decl "posreal" vertical_cr nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (gs_vertical_meets_horizontal_criterion formula-decl nil gs_circle
     nil)
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Sp2_vect3 type-eq-decl nil space_3D nil)
    (Sign type-eq-decl nil sign "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal 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)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Sp_vect3 type-eq-decl nil space_3D nil)
    (sp skolem-const-decl "Sp_vect3[D, H]" vertical_cr nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/"))
   nil)))

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.