Quelle  safe_arith.prf

(safe_arith
 (Proper_Safe1 0
  (Proper_Safe1-1 nil 3579699197 ("" (grind) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Proper? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (Safe1 const-decl "Interval" safe_arith nil))
   shostak))
 (Proper_Safe1_pre 0
  (Proper_Safe1_pre-1 nil 3579718621 ("" (grind) nil nil)
   ((Proper? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (Safe1 const-decl "Interval" safe_arith nil)
    (Safe1 const-decl "Interval" safe_arith nil))
   shostak))
 (Proper_Safe2 0
  (Proper_Safe2-1 nil 3579699135 ("" (grind) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Proper? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (Safe2 const-decl "Interval" safe_arith nil))
   shostak)))