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

Proof:
 Higher-Order Church Rosser Processor:
  app (abs (\x. T x)) S -> T S
  abs (\x. app (abs (\y. M y x)) S) -> app (abs (\y. abs (\x. M y x))) S
  app (app (abs (\x. T x)) S) U -> app (abs (\x. app (T x) U)) S
  app (abs (\y. app (abs (\x. M x y)) S)) U -> app (abs (\x. app (abs (\y. M x y)) U)) S
  critical peaks: 13
   abs (\x. 15 x 16) <-[1,0]-> app (abs (\y. abs (\x. 15 x y))) 16
   app (35 36) U <-[0,1]-> app (abs (\x. app (35 x) U)) 36
   app (abs (\45. 46 45 48)) 47 <-[]-> app (abs (\x. app (abs (\y. 46 x y)) 48)) 47
   app (abs (\y. 58 y 59)) U <-[0,1,1,0]-> app (abs (\x. app (abs (\y. 58 y x)) U)) 59
   app (app (abs (\y. abs (\x. 68 y x))) 69) S <-[0,1]-> app (abs (\y. 68 y S)) 69
   abs (\x. app (app (abs (\y. abs (\79. 80 x y 79))) (81 x)) S) <-[1,0,0,1]->
     app (abs (\y. abs (\x. app (abs (\82. 80 x 82 y)) (81 x)))) S
   app (app (app (abs (\y. abs (\x. 90 y x))) 91) S) U <-[0,1,0,1]->
     app (abs (\x. app (app (abs (\y. 90 y x)) 91) U)) S
   app (app (abs (\y. abs (\x. 98 y x))) 99) U <-[0,1]->
     app (abs (\x. app (abs (\y. 98 x y)) U)) 99
   app (abs (\y. app (app (abs (\107. abs (\x. 108 y 107 x))) (109 y)) S)) U <-[
     0,1,1,0,0,1]-> app (abs (\x. app (abs (\y. app (abs (\106. 108 y 106 x)) (109 y))) U)) S
   app (abs (\x. app (abs (\y. 187 x y)) 189)) 188 <-[]-> app (abs (\x. 187 x 189)) 188
   abs (\x. app (abs (\202. app (abs (\y. 203 x 202 y)) 205)) (204 x)) <-[
     1,0]-> app (abs (\y. abs (\x. app (abs (\201. 203 x 201 y)) (204 x)))) 205
   app (app (abs (\x. app (abs (\y. 232 x y)) 234)) 233) U <-[0,1]->
     app (abs (\x. app (app (abs (\235. 232 235 x)) 233) U)) 234
   app (abs (\y. app (abs (\x. app (abs (\256. 257 y x 256)) 259)) (258 y))) U <-[
     0,1,1,0]-> app (abs (\x. app (abs (\y. app (abs (\260. 257 y 260 x)) (258 y))) U)) 259
   
   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