Problem:
 f x x -> a
 f x (s x) -> b

Proof:
 Higher-Order Church Rosser Processor (kb):
  f x x -> a
  f x (s x) -> b
  critical peaks: 0, all joinable
   
   
   HORPO Processor:
    precedence:
     f > b ~ a ~ s
    problem:
     
    Qed