Problem:
 app succ m -> s m
 app pred (s m) -> m
 app iszero 0 -> tt
 app iszero (s m) -> ff
 app (app (app if tt) x) y -> x
 app (app (app if ff) x) y -> y
 app (abs (\x. z x)) y -> z y
 app Y x -> app x (app Y x)

Proof:
 Higher-Order Church Rosser Processor:
  app succ m -> s m
  app pred (s m) -> m
  app iszero 0 -> tt
  app iszero (s m) -> ff
  app (app (app if tt) x) y -> x
  app (app (app if ff) x) y -> y
  app (abs (\x. z x)) y -> z y
  app Y x -> app x (app Y x)
  critical peaks: 0
   
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed