Problem:
 altmap (\z. pls z Y) (cons X XS) -> cons (pls X Y) (altmap (\z. mlt z Y) XS)
 altmap (\z. mlt z Y) (cons X XS) -> cons (mlt X Y) (altmap (\z. pls z Y) XS)
 altmap (\z. F z) nil -> nil
 pls X Y -> + X Y
 mlt X Y -> * X Y
 pls 2 2 -> mlt 2 2

Proof:
 Higher-Order Church Rosser Processor:
  altmap (\z. pls z Y) (cons X XS) -> cons (pls X Y) (altmap (\z. mlt z Y) XS)
  altmap (\z. mlt z Y) (cons X XS) -> cons (mlt X Y) (altmap (\z. pls z Y) XS)
  altmap (\z. F z) nil -> nil
  pls X Y -> + X Y
  mlt X Y -> * X Y
  pls 2 2 -> mlt 2 2
  critical peaks: 4
   altmap (\z. + z 85) (cons X XS) <-[0,1,0]-> cons (pls X 85) (altmap (\z. mlt z 85) XS)
   + 2 2 <-[]-> mlt 2 2
   altmap (\z. * z 108) (cons X XS) <-[0,1,0]-> cons (mlt X 108) (altmap (\z. pls z 108) XS)
   mlt 2 2 <-[]-> + 2 2
   
   Higher-Order Nonconfluence Processor:
    non-joinable conversion:
    altmap (\z. + z 85) (cons X XS) *<- altmap (\z. + z 85) (cons X XS) <- . -> 
    cons (pls X 85) (altmap (\z. mlt z 85) XS) ->* cons (+ X 85) (altmap (\z. * z 85) XS)
    Qed