Problem:
 f x x -> a
 f x (s x) -> b
 mu (\x. Z x) -> Z (mu (\x. Z x))

Proof:
 Higher-Order Church Rosser Processor:
  f x x -> a
  f x (s x) -> b
  mu (\x. Z x) -> Z (mu (\x. Z x))
  critical peaks: 0
   
   
   Redundant Rules Transformation for Pattern Rewrite Systems:
    f x x -> a
    f x (s x) -> b
    mu (\x. Z x) -> Z (mu (\x. Z x))
    mu (\x. 70 x) -> 70 (70 (mu (\x. 70 x)))
    f (mu (\x. s x)) (mu (\x. s x)) -> b
    Higher-Order Church Rosser Processor:
     f x x -> a
     f x (s x) -> b
     mu (\x. Z x) -> Z (mu (\x. Z x))
     mu (\x. 70 x) -> 70 (70 (mu (\x. 70 x)))
     f (mu (\x. s x)) (mu (\x. s x)) -> b
     critical peaks: 8
      a <-[]-> b
      105 (mu (\x. 105 x)) <-[]-> 105 (105 (mu (\x. 105 x)))
      f (s (mu (\x. s x))) (mu (\x. s x)) <-[0,1]-> b
      f (mu (\x. s x)) (s (mu (\x. s x))) <-[1]-> b
      115 (115 (mu (\x. 115 x))) <-[]-> 115 (mu (\x. 115 x))
      f (s (s (mu (\x. s x)))) (mu (\x. s x)) <-[0,1]-> b
      f (mu (\x. s x)) (s (s (mu (\x. s x)))) <-[1]-> b
      b <-[]-> a
      
      Higher-Order Nonconfluence Processor:
       non-joinable conversion:
       a *<- a <- . -> b ->* b
       Qed