Problem:
 sum 0 (\i. F i) -> F 0
 sum (s n) (\i. F i) -> a (sum n (\i. F i)) (F (s n))

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