Problem:
 rec (\x y. F x y) a 0 -> a
 rec (\x y. F x y) a (s n) -> F n (rec (\x y. F x y) a n)

Proof:
 Higher-Order Church Rosser Processor:
  rec (\x y. F x y) a 0 -> a
  rec (\x y. F x y) a (s n) -> F n (rec (\x y. F x y) a n)
  critical peaks: 0
   
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed