Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/sources/formale Sprachen/PVS/reals/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 17 kB image not shown  

Quelle  real_orders.prf   Sprache: Lisp

 
(real_orders
 (le_realorder 0
  (le_realorder-1 nil 3567699173 ("" (judgement-tcc) nil nil)
   ((realorder? const-decl "bool" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (lt_realorder 0
  (lt_realorder-1 nil 3567699173 ("" (judgement-tcc) nil nil)
   ((realorder? const-decl "bool" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (ge_realorder 0
  (ge_realorder-1 nil 3567699173 ("" (judgement-tcc) nil nil)
   ((realorder? const-decl "bool" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (gt_realorder 0
  (gt_realorder-1 nil 3567699173 ("" (judgement-tcc) nil nil)
   ((realorder? const-decl "bool" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (neg_rel_le_gt 0
  (neg_rel_le_gt-1 nil 3567700168
   ("" (decompose-equality) (("" (grind) nil nil)) 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)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (neg_rel const-decl "bool" real_orders nil)
    (RealOrder type-eq-decl nil real_orders nil)
    (realorder? const-decl "bool" real_orders nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (le_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (neg_rel_lt_ge 0
  (neg_rel_lt_ge-1 nil 3567700235
   ("" (decompose-equality) (("" (grind) nil nil)) 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)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (neg_rel const-decl "bool" real_orders nil)
    (RealOrder type-eq-decl nil real_orders nil)
    (realorder? const-decl "bool" real_orders nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (neg_rel_ge_lt 0
  (neg_rel_ge_lt-1 nil 3567700243
   ("" (decompose-equality) (("" (grind) nil nil)) 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)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (neg_rel const-decl "bool" real_orders nil)
    (RealOrder type-eq-decl nil real_orders nil)
    (realorder? const-decl "bool" real_orders nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (neg_rel_gt_le 0
  (neg_rel_gt_le-1 nil 3567700252
   ("" (decompose-equality) (("" (grind) nil nil)) 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)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (neg_rel const-decl "bool" real_orders nil)
    (RealOrder type-eq-decl nil real_orders nil)
    (realorder? const-decl "bool" real_orders nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (neg_rel_order 0
  (neg_rel_order-1 nil 3567700390
   ("" (skeep :preds? t)
    (("" (expand "realorder?")
      (("" (flatten)
        (("" (lemma "neg_rel_le_gt")
          (("" (lemma "neg_rel_lt_ge")
            (("" (lemma "neg_rel_ge_lt")
              (("" (lemma "neg_rel_gt_le") (("" (ground) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((realorder? const-decl "bool" real_orders nil)
    (neg_rel_le_gt formula-decl nil real_orders nil)
    (neg_rel_ge_lt formula-decl nil real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders nil)
    (neg_rel_gt_le formula-decl nil real_orders nil)
    (neg_rel_lt_ge formula-decl nil real_orders nil))
   nil))
 (le_ne_lt 0
  (le_ne_lt-1 nil 3613991212
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,1)") (("" (assert) nil nil)) nil)) nil)
   ((le_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (le_ne_ge 0
  (le_ne_ge-1 nil 3613991224
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,2)") (("" (assert) nil nil)) nil)) nil)
   ((le_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (le_ne_gt 0
  (le_ne_gt-1 nil 3613991237
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,1)") (("" (assert) nil nil)) nil)) nil)
   ((le_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (lt_ne_le 0
  (lt_ne_le-1 nil 3613991251
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,1)") (("" (assert) nil nil)) nil)) nil)
   ((lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (lt_ne_ge 0
  (lt_ne_ge-1 nil 3613991262
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,1)") (("" (assert) nil nil)) nil)) nil)
   ((lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (lt_ne_gt 0
  (lt_ne_gt-1 nil 3613991278
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,2)") (("" (assert) nil nil)) nil)) nil)
   ((lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (ge_ne_gt 0
  (ge_ne_gt-1 nil 3613991068
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,1)") (("" (assert) nil nil)) nil)) nil)
   ((ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (ge_ne_le 0
  (ge_ne_le-1 nil 3613991094
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,2)") (("" (assert) nil nil)) nil)) nil)
   ((ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (ge_ne_lt 0
  (ge_ne_lt-1 nil 3613991120
   ("" (decompose-equality -1)
    (("" (inst -1 "(1,1)") (("" (assert) nil nil)) nil)) nil)
   ((ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (gt_ne_ge 0
  (gt_ne_ge-1 nil 3613990145
   ("" (decompose-equality)
    (("" (inst -1 "(1,1)") (("" (assert) nil nil)) nil)) nil)
   ((gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (gt_ne_le 0
  (gt_ne_le-1 nil 3613990164
   ("" (decompose-equality)
    (("" (inst -1 "(1,1)") (("" (assert) nil nil)) nil)) nil)
   ((gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak))
 (gt_ne_lt 0
  (gt_ne_lt-1 nil 3613990180
   ("" (decompose-equality)
    (("" (inst -1 "(1,2)") (("" (assert) nil nil)) nil)) nil)
   ((gt_realorder name-judgement "RealOrder" real_orders nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
   shostak)))

100%


¤ Dauer der Verarbeitung: 0.24 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.





                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge