Problem:
 app (abs (\x. T x)) S -> T S
 app (abs (\y. abs (\x. M y x))) S -> abs (\x. app (abs (\y. M y x)) S)
 app (app (abs (\x. T x)) S) U -> app (abs (\x. app (T x) U)) S

Proof:
 Higher-Order Church Rosser Processor:
  app (abs (\x. T x)) S -> T S
  app (abs (\y. abs (\x. M y x))) S -> abs (\x. app (abs (\y. M y x)) S)
  app (app (abs (\x. T x)) S) U -> app (abs (\x. app (T x) U)) S
  critical peaks: 4
   abs (\290. 291 292 290) <-[]-> abs (\x. app (abs (\y. 291 y x)) 292)
   app (309 310) U <-[0,1]-> app (abs (\x. app (309 x) U)) 310
   abs (\x. app (abs (\y. 319 y x)) 320) <-[]-> abs (\x. 319 320 x)
   app (abs (\x. app (abs (\y. 343 y x)) 344)) U <-[0,1]->
     app (abs (\x. app (abs (\345. 343 x 345)) U)) 344
   
   Redundant Rules Transformation for Pattern Rewrite Systems:
    app (abs (\x. T x)) S -> T S
    Higher-Order Church Rosser Processor:
     app (abs (\x. T x)) S -> T S
     critical peaks: 0
      
      
      Higher-Order Closedness Processor:
        all critical pairs are trivial
       
       Qed