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

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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: sigma_below.prf   Sprache: Lisp

Original von: PVS©
(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)))


¤ Dauer der Verarbeitung: 0.27 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff

                                                                                                                                                                                                                                                                                                                                                                                                     

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