Problem:
 app (abs (\x. y x)) z -> y z
 abs (\x. app z x) -> z
 or tt x -> tt
 or x tt -> tt

Proof:
 Modularity Decomposition: 
 0:app (abs (\x. y x)) z -> y z
   abs (\x. app z x) -> z
 1:or tt x -> tt
   or x tt -> tt
 -----
 0:app (abs (\x. y x)) z -> y z
   abs (\x. app z x) -> z
   Higher-Order Church Rosser Processor:
    app (abs (\x. y x)) z -> y z
    abs (\x. app z x) -> z
    critical peaks: 2
     abs (\13. 12 13) <-[1,0]-> abs (\11. 12 11)
     app 23 z <-[0,1]-> app 23 z
     
     Higher-Order Closedness Processor:
       all critical pairs are trivial
      
      Qed
   
   
   1:or tt x -> tt
     or x tt -> tt
     Higher-Order Church Rosser Processor:
      or tt x -> tt
      or x tt -> tt
      critical peaks: 2
       tt <-[]-> tt
       tt <-[]-> tt
       
       Higher-Order Closedness Processor:
         all critical pairs are trivial
        
        Qed