Quelle  bounded_reals.prf

(bounded_reals
 (sup_exists 0
  (sup_exists-1 nil 3506273121
   ("" (skosimp*)
    (("" (lemma "real_complete2")
      (("" (inst?)
        (("" (typepred "Su!1")
          (("" (expand "above_bounded")
            (("" (skosimp*)
              (("" (prop) (("" (inst 1 "n!1") nil))))))))))))))
    nil)
   ((T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals 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)
    (real_complete2 formula-decl nil reals_complete_more nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil))
   nil))
 (sup_TCC1 0
  (sup_TCC1-1 nil 3506273121
   (""
    (inst 1 "(LAMBDA (s: sup_set): choose({x: real
                      | least_upper_bound(<=)(x, s)}))")
    (("" (skosimp*)
      (("" (lemma "sup_exists")
        (("" (inst?)
          (("" (skosimp*)
            (("" (grind :exclude "least_upper_bound") nil))))))))))
    nil)
   ((empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (sup_exists formula-decl nil bounded_reals nil)
    (choose const-decl "(p)" sets nil) (<= const-decl "bool" reals nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (sup_def 0
  (sup_def-1 nil 3506273121
   ("" (skosimp*)
    (("" (typepred "sup(Su!1)")
      (("" (prop)
        (("1" (assert) nil)
         ("2" (expand "least_upper_bound")
          (("2" (flatten)
            (("2" (inst -4 "x!1")
              (("2" (inst -2 "sup(Su!1)")
                (("2" (assert) nil))))))))))))))
    nil)
   ((sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
     nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals nil)
    (pred type-eq-decl nil defined_types 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (max_TCC1 0
  (max_TCC1-1 nil 3506273121 ("" (subtype-tcc) 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]" bounded_reals nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (setof type-eq-decl nil defined_types nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (in_set const-decl "bool" bounded_reals nil)
    (pred type-eq-decl nil defined_types nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (<= const-decl "bool" reals nil)
    (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
     nil)
    (max_set type-eq-decl nil bounded_reals nil)
    (upper_bound const-decl "bool" bound_defs nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil))
   nil))
 (max_def 0
  (max_def-1 nil 3506273121
   ("" (skolem-typepred)
    (("" (expand "max")
      (("" (typepred "sup(W!1)")
        (("" (prop)
          (("1" (grind :exclude "upper_bound") nil)
           ("2" (grind :exclude "upper_bound")
            (("2" (expand "upper_bound" -5)
              (("2" (inst -5 "t!1")
                (("2" (grind :exclude "upper_bound") nil))))))))))))))
    nil)
   ((max const-decl "T" bounded_reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (maximum? const-decl "bool" bounded_reals nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (upper_bound const-decl "bool" bound_defs nil)
    (max_set type-eq-decl nil bounded_reals nil)
    (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
     nil)
    (<= const-decl "bool" reals nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (in_set const-decl "bool" bounded_reals nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals 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))
   nil))
 (inf_exists 0
  (inf_exists-1 nil 3506273121
   ("" (skosimp*)
    (("" (lemma "real_lower_complete2")
      (("" (inst?)
        (("" (typepred "Sl!1")
          (("" (expand "below_bounded")
            (("" (skosimp*)
              (("" (prop) (("" (inst 1 "n!1") nil))))))))))))))
    nil)
   ((T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals 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)
    (real_lower_complete2 formula-decl nil reals_complete_more nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil))
   nil))
 (inf_TCC1 0
  (inf_TCC1-1 nil 3506273121
   (""
    (inst 1 "(LAMBDA Sl: choose({x: real
                      | greatest_lower_bound(<=)(x, Sl)}))")
    (("" (skosimp*)
      (("" (lemma "inf_exists")
        (("" (inst?)
          (("" (grind :exclude "greatest_lower_bound") nil))))))))
    nil)
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (inf_exists formula-decl nil bounded_reals nil)
    (choose const-decl "(p)" sets nil) (<= const-decl "bool" reals nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (inf_def 0
  (inf_def-1 nil 3506273121
   ("" (skosimp*)
    (("" (typepred "inf(Sl!1)")
      (("" (prop)
        (("1" (assert) nil)
         ("2" (expand "greatest_lower_bound")
          (("2" (flatten)
            (("2" (inst -4 "x!1")
              (("2" (inst -2 "inf(Sl!1)")
                (("2" (assert) nil))))))))))))))
    nil)
   ((inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
     bounded_reals nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals nil)
    (pred type-eq-decl nil defined_types 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (min_TCC1 0
  (min_TCC1-1 nil 3506273121 ("" (subtype-tcc) 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]" bounded_reals nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (setof type-eq-decl nil defined_types nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (ext const-decl "set[real]" bounded_reals nil)
    (pred type-eq-decl nil defined_types nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (<= const-decl "bool" reals nil)
    (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
     bounded_reals nil)
    (min_set type-eq-decl nil bounded_reals nil)
    (lower_bound const-decl "bool" bound_defs nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil))
   nil))
 (min_def 0
  (min_def-1 nil 3506273121
   ("" (skolem-typepred)
    (("" (expand "min")
      (("" (typepred "inf(X!1)")
        (("" (prop)
          (("1" (grind :exclude "lower_bound") nil)
           ("2" (grind :exclude "lower_bound")
            (("2" (expand "lower_bound" -5)
              (("2" (inst -5 "t!1") (("2" (assert) nil))))))))))))))
    nil)
   ((min const-decl "T" bounded_reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minimum? const-decl "bool" bounded_reals nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (lower_bound const-decl "bool" bound_defs nil)
    (min_set type-eq-decl nil bounded_reals nil)
    (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
     bounded_reals nil)
    (<= const-decl "bool" reals nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (ext const-decl "set[real]" bounded_reals nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals 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))
   nil)))