| products/Sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: real_orders.prf Sprache: LispOriginal 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.6 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
