products/sources/formale Sprachen/PVS/while/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: Lisp

Original von: PVS©
(gs_line
 (gs_line_eps_TCC1 0
  (gs_line_eps_TCC1-1 nil 3429885199
   ("" (skeep)
    (("" (typepred "gs_only_line(tangent_line(sp, eps),vo, vi)")
      (("" (assert) nil nil)) nil))
    nil)
   ((tangent_line const-decl "Nz_vect2" tangent_line nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (gs_only_line const-decl "{k: real, nvo: Vect2 |
         nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}"
     gs_only nil)
    (D formal-const-decl "posreal" gs_line 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)
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (gs_only? const-decl "bool" definitions nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (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)
    (Vect2 type-eq-decl nil vectors_2D_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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (gs_line_eps_TCC2 0
  (gs_line_eps_TCC2-1 nil 3429885199 ("" (skosimp*) nil nil) nil nil))
 (gs_line_eps_tangent_line 0
  (gs_line_eps_tangent_line-1 nil 3433243037
   ("" (skeep)
    (("" (expand "gs_line_eps?")
      (("" (flatten)
        (("" (expand "gs_line_eps" :assert? none)
          (("" (skoletin -1 :postfix "a")
            (("" (lift-if)
              (("" (split -)
                (("1" (flatten)
                  (("1"
                    (typepred
                     "gs_only_line(tangent_line(sp, eps),vo, vi)")
                    (("1" (replaces (-4 -5) :dir rl)
                      (("1" (assert)
                        (("1" (flatten)
                          (("1" (expand "tangent_line?")
                            (("1" (inst?) (("1" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((gs_line_eps? const-decl "bool" gs_line nil)
    (gs_line_eps const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo)}"
     gs_line nil)
    (tangent_line? const-decl "bool" tangent_line nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (tangent_line const-decl "Nz_vect2" tangent_line nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (gs_only_line const-decl "{k: real, nvo: Vect2 |
         nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}"
     gs_only nil)
    (D formal-const-decl "posreal" gs_line 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)
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (gs_only? const-decl "bool" definitions nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil))
   nil))
 (gs_line_is_line_solution 0
  (gs_line_is_line_solution-1 nil 3471194277
   ("" (skeep)
    (("" (lemma "gs_line_eps_tangent_line")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "tangent_line_solution")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((gs_line_eps_tangent_line formula-decl nil gs_line nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (tangent_line_solution formula-decl nil tangent_line nil)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (D formal-const-decl "posreal" gs_line nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (>= const-decl "bool" reals nil)
    (Vect2 type-eq-decl nil vectors_2D_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)
    (bool nonempty-type-eq-decl nil 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)
    (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))
   nil))
 (gs_line_complete 0
  (gs_line_complete-1 nil 3443974345
   ("" (skeep)
    (("" (skeep -2)
      (("" (rewrite "tangent_line_solution" :dir rl)
        (("" (expand "tangent_line?")
          (("" (skeep -2)
            (("" (lemma "gs_only_line_complete")
              ((""
                (inst -1 "nnk" "nvo" "tangent_line(sp,eps)" "vi" "vo")
                (("" (assert)
                  (("" (expand "gs_only_line?")
                    (("" (split -1)
                      (("1" (flatten)
                        (("1" (expand "gs_line?")
                          (("1" (assert)
                            (("1" (inst 3 "eps")
                              (("1"
                                (expand "gs_line_eps")
                                (("1"
                                  (decompose-equality -1)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (flatten)
                        (("2" (expand "two_parallel?")
                          (("2" (assert) (("2" (inst 1 "eps") nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tangent_line? const-decl "bool" tangent_line nil)
    (gs_only_line_complete formula-decl nil gs_only nil)
    (gs_line? const-decl "bool" gs_line nil)
    (gs_only_line const-decl "{k: real, nvo: Vect2 |
         nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}"
     gs_only nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (gs_only? const-decl "bool" definitions nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (gs_line_eps const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo)}"
     gs_line nil)
    (two_parallel? const-decl "bool" gs_line nil)
    (gs_only_line? const-decl "bool" gs_only nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (tangent_line const-decl "Nz_vect2" tangent_line nil)
    (D formal-const-decl "posreal" gs_line 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)
    (- const-decl "Vector" vectors_2D "vectors/")
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_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)
    (tangent_line_solution formula-decl nil tangent_line nil))
   nil)))


¤ Dauer der Verarbeitung: 0.38 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff