Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: number_fields_sq.prf Sprache: Lisp

Original von: PVS^©

(number_fields_sq
(sq_nz_pos 0
  (sq_nz_pos-1 nil 3280147667
   ("" (expand "sq")
    (("" (skosimp*)
      ((""
        (lemma "nznum_times_nznum_is_nznum"
         ("nzx" "nz!1" "nzy" "nz!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((nznum_times_nznum_is_nznum application-judgement "nznum"
     number_fields_bis nil)
    (nznum_times_nznum_is_nznum judgement-tcc nil number_fields_bis
     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)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (sq const-decl "numfield" number_fields_sq nil))
   shostak))
(sq_rew 0
  (sq_rew-1 nil 3280147747
   ("" (expand "sq") (("" (propax) nil nil)) nil)
   ((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_neg 0
  (sq_neg-1 nil 3280147757
   ("" (expand "sq")
    (("" (skosimp*) (("" (rewrite "neg_times_neg") nil nil)) nil)) nil)
   ((numfield nonempty-type-eq-decl nil number_fields 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)
    (neg_times_neg formula-decl nil number_fields_bis nil)
    (sq const-decl "numfield" number_fields_sq nil))
   shostak))
(sq_times 0
  (sq_times-1 nil 3280147791
   ("" (expand "sq") (("" (propax) nil nil)) nil)
   ((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_plus 0
  (sq_plus-1 nil 3280147801
   ("" (expand "sq") (("" (grind) nil nil)) nil)
   ((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_minus 0
  (sq_minus-1 nil 3280147819 ("" (grind) nil nil)
   ((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_neg_minus 0
  (sq_neg_minus-1 nil 3280147827
   ("" (expand "sq") (("" (propax) nil nil)) nil)
   ((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_0 0
  (sq_0-1 nil 3280147836 ("" (expand "sq") (("" (propax) nil nil)) nil)
   ((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_1 0
  (sq_1-1 nil 3280147845 ("" (expand "sq") (("" (propax) nil nil)) nil)
   ((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_eq_0 0
  (sq_eq_0-1 nil 3280147908
   ("" (skosimp*)
    (("" (expand "sq")
      (("" (split)
        (("1" (flatten)
          (("1" (lemma "zero_times3" ("x" "a!1" "y" "a!1"))
            (("1" (assert) nil nil)) nil))
          nil)
         ("2" (flatten)
          (("2" (assert)
            (("2" (replace -1) (("2" (rewrite "zero_times1") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq const-decl "numfield" number_fields_sq nil)
    (zero_times1 formula-decl nil number_fields_bis nil)
    (zero_times3 formula-decl nil number_fields_bis 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)
    (numfield nonempty-type-eq-decl nil number_fields nil))
   shostak))
(sq_div 0
  (sq_div-1 nil 3280147989
   ("" (expand "sq")
    (("" (skosimp*) (("" (rewrite "div_times") nil nil)) nil)) nil)
   ((numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal 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)
    (div_times formula-decl nil number_fields_bis nil)
    (sq const-decl "numfield" number_fields_sq nil))
   shostak)))

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