Problem:
 f a y -> y
 f y' b -> y'

Proof:
 Higher-Order Church Rosser Processor:
  f a y -> y
  f y' b -> y'
  critical peaks: 2
   b <-[]-> a
   a <-[]-> b
   
   Higher-Order Nonconfluence Processor:
    non-joinable conversion:
    b *<- b <- . -> a ->* a
    Qed