Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: real_fun_props.prf Sprache: Lisp

Original von: PVS^©

(real_fun_props
(strict_incr_to_incr 0
  (strict_incr_to_incr-1 nil 3506273132
   ("" (grind :if-match nil)
    (("" (inst -3 "x!1" "y!1") (("" (assert) nil nil)) nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (increasing? const-decl "bool" real_fun_preds nil)
    (strict_increasing? const-decl "bool" real_fun_preds nil))
   nil))
(strict_decr_to_decr 0
  (strict_decr_to_decr-1 nil 3506273132
   ("" (grind :if-match nil)
    (("" (inst -3 "x!1" "y!1") (("" (assert) nil nil)) nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (decreasing? const-decl "bool" real_fun_preds nil)
    (strict_decreasing? const-decl "bool" real_fun_preds nil))
   nil))
(incr_neg 0
  (incr_neg-1 nil 3506273132 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (increasing? const-decl "bool" real_fun_preds nil)
    (decreasing? const-decl "bool" real_fun_preds nil))
   nil))
(decr_neg 0
  (decr_neg-1 nil 3506273132 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (decreasing? const-decl "bool" real_fun_preds nil)
    (increasing? const-decl "bool" real_fun_preds nil))
   nil))
(strict_incr_neg 0
  (strict_incr_neg-1 nil 3506273132 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (strict_increasing? const-decl "bool" real_fun_preds nil)
    (strict_decreasing? const-decl "bool" real_fun_preds nil))
   nil))
(strict_decr_neg 0
  (strict_decr_neg-1 nil 3506273132 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (strict_decreasing? const-decl "bool" real_fun_preds nil)
    (strict_increasing? const-decl "bool" real_fun_preds nil))
   nil))
(constant_to_incr 0
  (constant_to_incr-1 nil 3506273132 ("" (grind :if-match all) nil nil)
   ((f!1 skolem-const-decl "[T -> real]" real_fun_props nil)
    (x!1 skolem-const-decl "T" real_fun_props nil)
    (y!1 skolem-const-decl "T" real_fun_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (T_pred const-decl "[real -> boolean]" real_fun_props 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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (constant? const-decl "bool" real_fun_preds nil)
    (increasing? const-decl "bool" real_fun_preds nil))
   nil))
(constant_to_decr 0
  (constant_to_decr-1 nil 3506273132 ("" (grind :if-match all) nil nil)
   ((f!1 skolem-const-decl "[T -> real]" real_fun_props nil)
    (y!1 skolem-const-decl "T" real_fun_props nil)
    (x!1 skolem-const-decl "T" real_fun_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (T_pred const-decl "[real -> boolean]" real_fun_props 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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (constant? const-decl "bool" real_fun_preds nil)
    (decreasing? const-decl "bool" real_fun_preds nil))
   nil))
(constant_neg 0
  (constant_neg-1 nil 3506273132 ("" (grind :if-match all) nil nil)
   ((x!1 skolem-const-decl "T" real_fun_props nil)
    (y!1 skolem-const-decl "T" real_fun_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (f!1 skolem-const-decl "[T -> real]" real_fun_props nil)
    (x!1 skolem-const-decl "T" real_fun_props nil)
    (y!1 skolem-const-decl "T" real_fun_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (constant? const-decl "bool" real_fun_preds nil))
   nil))
(bounded_above_neg 0
  (bounded_above_neg-1 nil 3506273132
   ("" (grind :if-match nil)
    (("1" (inst + "-a!1")
      (("1" (skolem!) (("1" (inst?) (("1" (assert) nil nil)) nil))
        nil))
      nil)
     ("2" (inst + "-a!1")
      (("2" (skolem!) (("2" (inst?) (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (bounded_below? const-decl "bool" real_fun_preds nil)
    (bounded_above? const-decl "bool" real_fun_preds nil)
    (- const-decl "[T -> real]" real_fun_ops nil))
   nil))
(bounded_below_neg 0
  (bounded_below_neg-1 nil 3506273132
   ("" (grind :if-match nil)
    (("1" (inst + "-a!1")
      (("1" (skolem!) (("1" (inst?) (("1" (assert) nil nil)) nil))
        nil))
      nil)
     ("2" (inst + "-a!1")
      (("2" (skolem!) (("2" (inst?) (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (bounded_above? const-decl "bool" real_fun_preds nil)
    (bounded_below? const-decl "bool" real_fun_preds nil)
    (- const-decl "[T -> real]" real_fun_ops nil))
   nil))
(max_bounded 0
  (max_bounded-1 nil 3506273132
   ("" (grind :if-match nil) (("" (inst? +) nil nil)) nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (bounded_above? const-decl "bool" real_fun_preds nil)
    (is_maximum? const-decl "bool" real_fun_preds nil))
   nil))
(min_bounded 0
  (min_bounded-1 nil 3506273132
   ("" (grind :if-match nil) (("" (inst? +) nil nil)) nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (bounded_below? const-decl "bool" real_fun_preds nil)
    (is_minimum? const-decl "bool" real_fun_preds nil))
   nil))
(max_neg 0
  (max_neg-1 nil 3506273132
   ("" (grind :if-match nil)
    (("1" (inst -3 "y!1") (("1" (assert) nil nil)) nil)
     ("2" (inst?) (("2" (assert) nil nil)) nil))
    nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (is_minimum? const-decl "bool" real_fun_preds nil)
    (is_maximum? const-decl "bool" real_fun_preds nil)
    (- const-decl "[T -> real]" real_fun_ops nil))
   nil))
(min_neg 0
  (min_neg-1 nil 3506273132
   ("" (skosimp*)
    (("" (rewrite "max_neg" :dir rl)
      (("" (case-replace "--f!1 = f!1")
        (("1" (assert) nil nil)
         ("2" (hide 2)
          (("2" (apply-extensionality 1 :hide? t)
            (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max_neg formula-decl nil real_fun_props 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)
    (T_pred const-decl "[real -> boolean]" real_fun_props nil)
    (T formal-subtype-decl nil real_fun_props nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil)))

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