Quelle  restriction_continuous.prf

(restriction_continuous
 (restrict_continuous 0
  (restrict_continuous-1 nil 3473169490
   ("" (skosimp*)
    (("" (expand "continuous?")
      (("" (skosimp*)
        (("" (inst?)
          (("" (expand "continuous?")
            (("" (skosimp*)
              (("" (inst - "epsilon!1")
                (("" (skosimp*)
                  (("" (inst + "delta!1")
                    (("" (skosimp*)
                      (("" (inst - x!1)
                        (("" (assert)
                          (("" (expand "restrict")
                            (("" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous? const-decl "bool" continuous_functions 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)
    (T1_pred const-decl "[real -> boolean]" restriction_continuous nil)
    (T1 formal-subtype-decl nil restriction_continuous nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (restrict const-decl "R" restrict nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)))