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

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
  critical peaks: 5
   abs (\x. 17 x 18) <-[1,0]-> app (abs (\y. abs (\x. 17 x y))) 18
   app (39 40) U <-[0,1]-> app (abs (\x. app (39 x) U)) 40
   app (app (abs (\y. abs (\x. 50 y x))) 51) S <-[0,1]-> app (abs (\y. 50 y S)) 51
   abs (\x. app (app (abs (\y. abs (\63. 64 x y 63))) (65 x)) S) <-[1,0,0,1]->
     app (abs (\y. abs (\x. app (abs (\66. 64 x 66 y)) (65 x)))) S
   app (app (app (abs (\y. abs (\x. 75 y x))) 76) S) U <-[0,1,0,1]->
     app (abs (\x. app (app (abs (\y. 75 y x)) 76) U)) S
   
   Redundant Rules Transformation for Pattern Rewrite Systems:
    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
    abs (\x. app (abs (\y. M y x)) S) -> abs (\x. M S x)
    app (app (abs (\x. T x)) S) U -> app (abs (\x. app (T x) U)) S
    app (app (abs (\x. T x)) S) U -> app (T S) U
    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
     abs (\x. app (abs (\y. M y x)) S) -> abs (\x. M S x)
     app (app (abs (\x. T x)) S) U -> app (abs (\x. app (T x) U)) S
     app (app (abs (\x. T x)) S) U -> app (T S) U
     critical peaks: 18
      abs (\x. 158 x 159) <-[1,0]-> app (abs (\y. abs (\x. 158 x y))) 159
      abs (\x. 171 x 172) <-[1,0]-> abs (\x. 171 x 172)
      app (191 192) U <-[0,1]-> app (abs (\x. app (191 x) U)) 192
      app (209 210) U <-[0,1]-> app (209 210) U
      app (app (abs (\y. abs (\x. 219 y x))) 220) S <-[0,1]-> app (abs (\y. 219 y S)) 220
      abs (\x. app (app (abs (\y. abs (\230. 231 x y 230))) (232 x)) S) <-[
        1,0,0,1]-> app (abs (\y. abs (\x. app (abs (\233. 231 x 233 y)) (232 x)))) S
      app (abs (\y. abs (\x. 241 y x))) 242 <-[]-> abs (\x. 241 242 x)
      abs (\x. app (app (abs (\y. abs (\249. 250 x y 249))) (251 x)) S) <-[
        1,0,0,1]-> abs (\x. app (abs (\y. 250 x y S)) (251 x))
      app (app (app (abs (\y. abs (\x. 259 y x))) 260) S) U <-[0,1,0,1]->
        app (abs (\x. app (app (abs (\y. 259 y x)) 260) U)) S
      app (app (app (abs (\y. abs (\x. 266 y x))) 267) S) U <-[0,1,0,1]->
        app (app (abs (\y. 266 y S)) 267) U
      app (abs (\x. 273 274 x)) S <-[0,1]-> app (abs (\y. 273 y S)) 274
      abs (\x. 280 281 x) <-[]-> app (abs (\y. abs (\x. 280 y x))) 281
      abs (\x. app (abs (\288. 289 x (290 x) 288)) S) <-[1,0,0,1]->
        app (abs (\y. abs (\x. app (abs (\291. 289 x 291 y)) (290 x)))) S
      abs (\x. app (abs (\303. 304 x (305 x) 303)) S) <-[1,0,0,1]->
        abs (\x. app (abs (\y. 304 x y S)) (305 x))
      app (app (abs (\x. 313 314 x)) S) U <-[0,1,0,1]->
        app (abs (\x. app (app (abs (\y. 313 y x)) 314) U)) S
      app (app (abs (\x. 320 321 x)) S) U <-[0,1,0,1]-> app (app (abs (\y. 320 y S)) 321) U
      app (abs (\x. app (392 x) 394)) 393 <-[]-> app (392 393) 394
      app (456 457) 458 <-[]-> app (abs (\x. app (456 x) 458)) 457
      
      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