Problem:
 avg (s x) y -> avg x (s y)
 avg x (s (s (s y))) -> s (avg (s x) y)
 avg 0 0 -> 0
 avg 0 (s 0) -> 0
 avg 0 (s (s 0)) -> s 0
 apply (fun (\x. F x)) y -> F (check y)
 check (s x) -> s (check x)
 check 0 -> 0

Proof:
 Higher-Order Church Rosser Processor:
  avg (s x) y -> avg x (s y)
  avg x (s (s (s y))) -> s (avg (s x) y)
  avg 0 0 -> 0
  avg 0 (s 0) -> 0
  avg 0 (s (s 0)) -> s 0
  apply (fun (\x. F x)) y -> F (check y)
  check (s x) -> s (check x)
  check 0 -> 0
  critical peaks: 2
   avg 11 (s (s (s (s 12)))) <-[]-> s (avg (s (s 11)) 12)
   s (avg (s (s 45)) 46) <-[]-> avg 45 (s (s (s (s 46))))
   
   Higher-Order Closedness Processor:
     all critical pairs are (almost) development closed
    
    Qed