SSL RealInt.prf   Interaktion und
Portierbarkeitunbekannt

(RealInt
 (in_ninf_inf 0
  (in_ninf_inf-1 nil 3602583209 ("" (grind) nil nil)
   ((- const-decl "nInf" RealInt nil)
    ([\|\|] const-decl "RealInt" RealInt nil)
    (contains? const-decl "bool" RealInt nil)
    (|##| const-decl "bool" RealInt nil))
   shostak))
 (in_ninf_open 0
  (in_ninf_open-1 nil 3602583215 ("" (grind) nil nil)
   ((- const-decl "nInf" RealInt nil)
    ([\|\|] const-decl "RealInt" RealInt nil)
    (contains? const-decl "bool" RealInt nil)
    (|##| const-decl "bool" RealInt nil))
   shostak))
 (in_open_inf 0
  (in_open_inf-1 nil 3602544027 ("" (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    ([\|\|] const-decl "RealInt" RealInt nil)
    (contains? const-decl "bool" RealInt nil)
    (|##| const-decl "bool" RealInt nil))
   shostak))
 (in_open_open 0
  (in_open_open-1 nil 3602544033 ("" (grind) nil nil)
   (([\|\|] const-decl "RealInt" RealInt nil)
    (contains? const-decl "bool" RealInt nil)
    (|##| const-decl "bool" RealInt nil))
   shostak))
 (in_ninf_close 0
  (in_ninf_close-1 nil 3602583227 ("" (grind) nil nil)
   ((- const-decl "nInf" RealInt nil)
    ([\|\|] const-decl "RealInt" RealInt nil)
    (contains? const-decl "bool" RealInt nil)
    (|##| const-decl "bool" RealInt nil))
   shostak))
 (in_close_inf 0
  (in_close_inf-1 nil 3602544103 ("" (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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    ([\|\|] const-decl "RealInt" RealInt nil)
    (contains? const-decl "bool" RealInt nil)
    (|##| const-decl "bool" RealInt nil))
   shostak)))