Problem:
 pi1 (pi z1 z2) -> z1
 pi2 (pi z1 z2) -> z2
 pi (pi1 z) (pi2 z) -> z

Proof:
 Higher-Order Church Rosser Processor (kb):
  pi1 (pi z1 z2) -> z1
  pi2 (pi z1 z2) -> z2
  pi (pi1 z) (pi2 z) -> z
  critical peaks: 4, all joinable
   pi 52 (pi2 (pi 52 53)) <-[0,1]-> pi 52 53
   pi (pi1 (pi 62 63)) 63 <-[1]-> pi 62 63
   pi1 69 <-[1]-> pi1 69
   pi2 76 <-[1]-> pi2 76
   
   HORPO Processor:
    precedence:
     pi ~ pi2 ~ pi1
    problem:
     
    Qed