SSL IEEE_854_remainder.prf   Interaktion und
PortierbarkeitLisp

(IEEE_854_remainder
 (REM_TCC1 0
  (REM_TCC1-1 nil 3321206042
   ("" (skolem-typepred)
    (("" (skosimp*)
      (("" (replace -6)
        (("" (expand "zero?") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((zero? const-decl "bool" IEEE_854_values nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (fp_num type-decl nil IEEE_854_values nil)
    (E_min formal-const-decl "{i: integer | E_max > i}"
     IEEE_854_remainder nil)
    (E_max formal-const-decl "integer" IEEE_854_remainder nil)
    (integer nonempty-type-from-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_remainder nil)
    (b formal-const-decl "above(1)" IEEE_854_remainder nil)
    (above nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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))
 (REM_TCC2 0
  (REM_TCC2-1 nil 3321206042 ("" (skosimp*) (("" (assert) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)))