MAYBE
ignored inputs:
(COMMENT a fragment of ML )
(COMMENT Example 43 of [ FG07 , doi:10.1016/j.ic.2006.12.002 ] )

NRS:
   [ (0):  |- (app <(lam [a][]X),[]Y>) -> (sub <[a][]X,[]Y>),
     (1):  |- (sub <[a](app <[]X,[]Y>),[]Z>) -> (app <(sub <[a][]X,[]Z>),(sub <[a][]Y,[]Z>)>),
     (2):  |- (sub <[a]a,[]X>) -> []X,
     (3): a#X |- (sub <[a][]X,[]Y>) -> []X,
     (4): b#Y |- (sub <[a](lam [b][]X),[]Y>) -> (lam [b](sub <[a][]X,[]Y>)),
     (5):  |- (let <[]X',[a][]X>) -> (sub <[a][]X,[]X'>),
     (6):  |- (letrec [f]<[a][]X',[]X>) -> (sub <[f][]X,(lam [a](letrec [f]<[a][]X',[]X'>))>),
     (7): a#Y |- (sub <[b](let <[]X',[a][]X>),[]Y>) -> (let <(sub <[b][]X',[]Y>),[a](sub <[b][]X,[]Y>)>),
     (8): f#Y,a#Y |- (sub <[b](letrec [f]<[a][]X',[]X>),[]Y>) -> (letrec [f]<[a](sub <[b][]X',[]Y>),(sub <[b][]X,[]Y>)>) ]
Check confluence by parallel closed criterion
left-linear
uniform
BCPs:
(0 on 0(out)): 
   {  |- < (sub <[a][]X_1,[]Y_1>) <= (app <(lam [a][]X_1),[]Y_1>) => (sub <[a][]X_1,[]Y_1>) >,
     a#X_1 |- < (sub <[a][(a b)]X_1,[]Y_1>) <= (app <(lam [b][]X_1),[]Y_1>) => (sub <[b][]X_1,[]Y_1>) > }
(0 on 1(in)): 
   {  |- < (sub <[a](sub <[a][]X,[]Y_1>),[]Z_1>) <= (sub <[a](app <(lam [a][]X),[]Y_1>),[]Z_1>) => (app <(sub <[a](lam [a][]X),[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) >,
      |- < (sub <[b](sub <[a][]X,[]Y_1>),[]Z_1>) <= (sub <[b](app <(lam [a][]X),[]Y_1>),[]Z_1>) => (app <(sub <[b](lam [a][]X),[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>) > }
(1 on 1(out)): 
   {  |- < (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) <= (sub <[a](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) >,
     a#Y_1,a#X_1 |- < (app <(sub <[a][(a b)]X_1,[]Z_1>),(sub <[a][(a b)]Y_1,[]Z_1>)>) <= (sub <[b](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[b][]X_1,[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>) > }
(1 on 3(out)): 
   { a#X,a#Y |- < (app <(sub <[a][]X,[]Y_1>),(sub <[a][]Y,[]Y_1>)>) <= (sub <[a](app <[]X,[]Y>),[]Y_1>) => (app <[]X,[]Y>) >,
     a#Y,a#X,b#Y,b#X |- < (app <(sub <[a][]X,[]Y_1>),(sub <[a][]Y,[]Y_1>)>) <= (sub <[b](app <[(a b)]X,[(a b)]Y>),[]Y_1>) => (app <[(a b)]X,[(a b)]Y>) > }
(2 on 2(out)): 
   {  |- < []X_1 <= (sub <[a]a,[]X_1>) => []X_1 >,
      |- < []X_1 <= (sub <[b]b,[]X_1>) => []X_1 > }
(3 on 1(out)): 
   { a#X_1,a#Y_1 |- < (app <[]X_1,[]Y_1>) <= (sub <[a](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) >,
     b#Y_1,a#X_1,a#Y_1,b#X_1 |- < (app <[(a b)]X_1,[(a b)]Y_1>) <= (sub <[b](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[b][]X_1,[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>) > }
(3 on 3(out)): 
   { a#X_1 |- < []X_1 <= (sub <[a][]X_1,[]Y_1>) => []X_1 >,
     b#X_1,a#X_1 |- < [(a b)]X_1 <= (sub <[b][]X_1,[]Y_1>) => []X_1 > }
(3 on 4(out)): 
   { a#X_1,b#Y_1 |- < (lam [b][]X_1) <= (sub <[a](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[a][]X_1,[]Y_1>)) >,
     a#X_1,c#Y_1 |- < (lam [c][]X_1) <= (sub <[a](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[a][]X_1,[]Y_1>)) >,
     a#Y_1,b#X_1 |- < (lam [b][(a b)]X_1) <= (sub <[b](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[b][]X_1,[]Y_1>)) >,
     a#Y_1,c#X_1 |- < (lam [c][(a c)]X_1) <= (sub <[c](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[c][]X_1,[]Y_1>)) >,
     c#Y_1,b#X_1,a#X_1 |- < (lam [c][(a b)]X_1) <= (sub <[b](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[b][]X_1,[]Y_1>)) >,
     b#Y_1,c#X_1,a#X_1 |- < (lam [b][(a c)]X_1) <= (sub <[c](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[c][]X_1,[]Y_1>)) >,
     d#Y_1,c#X_1,a#X_1 |- < (lam [d][(a c)]X_1) <= (sub <[c](lam [d][]X_1),[]Y_1>) => (lam [d](sub <[c][]X_1,[]Y_1>)) > }
(3 on 7(out)): 
   { a#X_1,b#Y_1,a#X'_1 |- < (let <[]X'_1,[b][]X_1>) <= (sub <[a](let <[]X'_1,[b][]X_1>),[]Y_1>) => (let <(sub <[a][]X'_1,[]Y_1>),[b](sub <[a][]X_1,[]Y_1>)>) >,
     a#X_1,c#Y_1,a#X'_1 |- < (let <[]X'_1,[c][]X_1>) <= (sub <[a](let <[]X'_1,[c][]X_1>),[]Y_1>) => (let <(sub <[a][]X'_1,[]Y_1>),[c](sub <[a][]X_1,[]Y_1>)>) >,
     a#Y_1,b#X_1,b#X'_1,a#X'_1 |- < (let <[(a b)]X'_1,[b][(a b)]X_1>) <= (sub <[b](let <[]X'_1,[a][]X_1>),[]Y_1>) => (let <(sub <[b][]X'_1,[]Y_1>),[a](sub <[b][]X_1,[]Y_1>)>) >,
     a#Y_1,c#X_1,c#X'_1,a#X'_1 |- < (let <[(a c)]X'_1,[c][(a c)]X_1>) <= (sub <[c](let <[]X'_1,[a][]X_1>),[]Y_1>) => (let <(sub <[c][]X'_1,[]Y_1>),[a](sub <[c][]X_1,[]Y_1>)>) >,
     c#Y_1,b#X_1,a#X_1,b#X'_1,a#X'_1 |- < (let <[(a b)]X'_1,[c][(a b)]X_1>) <= (sub <[b](let <[]X'_1,[c][]X_1>),[]Y_1>) => (let <(sub <[b][]X'_1,[]Y_1>),[c](sub <[b][]X_1,[]Y_1>)>) >,
     b#Y_1,c#X_1,a#X_1,c#X'_1,a#X'_1 |- < (let <[(a c)]X'_1,[b][(a c)]X_1>) <= (sub <[c](let <[]X'_1,[b][]X_1>),[]Y_1>) => (let <(sub <[c][]X'_1,[]Y_1>),[b](sub <[c][]X_1,[]Y_1>)>) >,
     d#Y_1,c#X_1,a#X_1,c#X'_1,a#X'_1 |- < (let <[(a c)]X'_1,[d][(a c)]X_1>) <= (sub <[c](let <[]X'_1,[d][]X_1>),[]Y_1>) => (let <(sub <[c][]X'_1,[]Y_1>),[d](sub <[c][]X_1,[]Y_1>)>) > }
(3 on 8(out)): 
   { b#Y_1,a#X_1,a#X'_1,f#Y_1 |- < (letrec [b]<[f][]X'_1,[]X_1>) <= (sub <[a](letrec [b]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[f](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     c#Y_1,a#X_1,a#X'_1,f#Y_1 |- < (letrec [c]<[f][]X'_1,[]X_1>) <= (sub <[a](letrec [c]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[f](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     f#Y_1,a#X_1,a#X'_1,b#Y_1 |- < (letrec [f]<[b][]X'_1,[]X_1>) <= (sub <[a](letrec [f]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[b](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     c#Y_1,a#X_1,a#X'_1,b#Y_1 |- < (letrec [c]<[b][]X'_1,[]X_1>) <= (sub <[a](letrec [c]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[b](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     b#Y_1,a#X_1,a#X'_1,c#Y_1 |- < (letrec [b]<[c][]X'_1,[]X_1>) <= (sub <[a](letrec [b]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[c](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     f#Y_1,a#X_1,a#X'_1,c#Y_1 |- < (letrec [f]<[c][]X'_1,[]X_1>) <= (sub <[a](letrec [f]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[c](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     d#Y_1,a#X_1,a#X'_1,c#Y_1 |- < (letrec [d]<[c][]X'_1,[]X_1>) <= (sub <[a](letrec [d]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[c](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     b#X'_1,b#X_1,a#Y_1,f#Y_1 |- < (letrec [b]<[f][(a b)]X'_1,[(a b)]X_1>) <= (sub <[b](letrec [a]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[f](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     c#X'_1,c#X_1,a#Y_1,f#Y_1 |- < (letrec [c]<[f][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [a]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[f](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     f#X'_1,f#X_1,a#Y_1,b#Y_1 |- < (letrec [f]<[b][(a f)]X'_1,[(a f)]X_1>) <= (sub <[f](letrec [a]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[b](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     c#X'_1,c#X_1,a#Y_1,b#Y_1 |- < (letrec [c]<[b][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [a]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[b](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     b#X'_1,b#X_1,a#Y_1,c#Y_1 |- < (letrec [b]<[c][(a b)]X'_1,[(a b)]X_1>) <= (sub <[b](letrec [a]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[c](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     f#X'_1,f#X_1,a#Y_1,c#Y_1 |- < (letrec [f]<[c][(a f)]X'_1,[(a f)]X_1>) <= (sub <[f](letrec [a]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[c](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     d#X'_1,d#X_1,a#Y_1,c#Y_1 |- < (letrec [d]<[c][(a d)]X'_1,[(a d)]X_1>) <= (sub <[d](letrec [a]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[c](sub <[d][]X'_1,[]Y_1>),(sub <[d][]X_1,[]Y_1>)>) >,
     a#Y_1,f#Y_1,b#X_1,b#X'_1,a#X_1 |- < (letrec [f]<[b][(a b)]X'_1,[(a b)]X_1>) <= (sub <[b](letrec [f]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[a](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#Y_1,c#Y_1,b#X_1,b#X'_1,a#X_1 |- < (letrec [c]<[b][(a b)]X'_1,[(a b)]X_1>) <= (sub <[b](letrec [c]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[a](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#Y_1,b#Y_1,f#X_1,f#X'_1,a#X_1 |- < (letrec [b]<[f][(a f)]X'_1,[(a f)]X_1>) <= (sub <[f](letrec [b]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[a](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#Y_1,c#Y_1,f#X_1,f#X'_1,a#X_1 |- < (letrec [c]<[f][(a f)]X'_1,[(a f)]X_1>) <= (sub <[f](letrec [c]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[a](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#Y_1,f#Y_1,c#X_1,c#X'_1,a#X_1 |- < (letrec [f]<[c][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [f]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[a](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#Y_1,b#Y_1,c#X_1,c#X'_1,a#X_1 |- < (letrec [b]<[c][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [b]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[a](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#Y_1,d#Y_1,c#X_1,c#X'_1,a#X_1 |- < (letrec [d]<[c][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [d]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[a](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,b#X'_1,b#X_1,c#Y_1,f#Y_1 |- < (letrec [c]<[f][(a b)]X'_1,[(a b)]X_1>) <= (sub <[b](letrec [c]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[f](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,b#X'_1,b#X_1,f#Y_1,c#Y_1 |- < (letrec [f]<[c][(a b)]X'_1,[(a b)]X_1>) <= (sub <[b](letrec [f]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[c](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,b#X'_1,b#X_1,d#Y_1,c#Y_1 |- < (letrec [d]<[c][(a b)]X'_1,[(a b)]X_1>) <= (sub <[b](letrec [d]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[c](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,f#X'_1,f#X_1,c#Y_1,b#Y_1 |- < (letrec [c]<[b][(a f)]X'_1,[(a f)]X_1>) <= (sub <[f](letrec [c]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[b](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,f#X'_1,f#X_1,b#Y_1,c#Y_1 |- < (letrec [b]<[c][(a f)]X'_1,[(a f)]X_1>) <= (sub <[f](letrec [b]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[c](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,f#X'_1,f#X_1,d#Y_1,c#Y_1 |- < (letrec [d]<[c][(a f)]X'_1,[(a f)]X_1>) <= (sub <[f](letrec [d]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[c](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,c#X'_1,c#X_1,b#Y_1,f#Y_1 |- < (letrec [b]<[f][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [b]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[f](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,c#X'_1,c#X_1,d#Y_1,f#Y_1 |- < (letrec [d]<[f][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [d]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[f](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,c#X'_1,c#X_1,f#Y_1,b#Y_1 |- < (letrec [f]<[b][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [f]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[b](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,c#X'_1,c#X_1,d#Y_1,b#Y_1 |- < (letrec [d]<[b][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [d]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[b](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,c#X'_1,c#X_1,b#Y_1,d#Y_1 |- < (letrec [b]<[d][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [b]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[d](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,c#X'_1,c#X_1,f#Y_1,d#Y_1 |- < (letrec [f]<[d][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [f]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[d](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X_1,a#X'_1,c#X'_1,c#X_1,e#Y_1,d#Y_1 |- < (letrec [e]<[d][(a c)]X'_1,[(a c)]X_1>) <= (sub <[c](letrec [e]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [e]<[d](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) > }
(4 on 3(out)): 
   { a#X,b#Y_1 |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[a](lam [b][]X),[]Y_1>) => (lam [b][]X) >,
     a#X,b#Y_1 |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[b](lam [a][(a b)]X),[]Y_1>) => (lam [a][(a b)]X) >,
     c#X,b#Y_1,a#X |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[c](lam [b][(a c)]X),[]Y_1>) => (lam [b][(a c)]X) > }
(4 on 4(out)): 
   { b#Y_1 |- < (lam [b](sub <[a][]X_1,[]Y_1>)) <= (sub <[a](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[a][]X_1,[]Y_1>)) >,
     b#X_1,b#Y_1,c#Y_1 |- < (lam [b](sub <[a][(b c)]X_1,[]Y_1>)) <= (sub <[a](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[a][]X_1,[]Y_1>)) >,
     a#Y_1,b#Y_1 |- < (lam [b](sub <[a][(a b)]X_1,[]Y_1>)) <= (sub <[b](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[b][]X_1,[]Y_1>)) >,
     a#X_1,b#Y_1 |- < (lam [b](sub <[a][(a c)]X_1,[]Y_1>)) <= (sub <[c](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[c][]X_1,[]Y_1>)) >,
     b#Y_1,a#Y_1,b#X_1 |- < (lam [b](sub <[a][(c a)(a b)]X_1,[]Y_1>)) <= (sub <[c](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[c][]X_1,[]Y_1>)) >,
     a#X_1,c#Y_1,b#Y_1 |- < (lam [b](sub <[a][(b a)(a c)]X_1,[]Y_1>)) <= (sub <[b](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[b][]X_1,[]Y_1>)) >,
     a#X_1,b#Y_1,d#Y_1,b#X_1 |- < (lam [b](sub <[a][(b d)(a c)]X_1,[]Y_1>)) <= (sub <[c](lam [d][]X_1),[]Y_1>) => (lam [d](sub <[c][]X_1,[]Y_1>)) > }
(5 on 5(out)): 
   {  |- < (sub <[a][]X_1,[]X'_1>) <= (let <[]X'_1,[a][]X_1>) => (sub <[a][]X_1,[]X'_1>) >,
     a#X_1 |- < (sub <[a][(a b)]X_1,[]X'_1>) <= (let <[]X'_1,[b][]X_1>) => (sub <[b][]X_1,[]X'_1>) > }
(5 on 7(in)): 
   { a#Y_1 |- < (sub <[b](sub <[a][]X_1,[]X'_1>),[]Y_1>) <= (sub <[b](let <[]X'_1,[a][]X_1>),[]Y_1>) => (let <(sub <[b][]X'_1,[]Y_1>),[a](sub <[b][]X_1,[]Y_1>)>) >,
     a#Y_1 |- < (sub <[c](sub <[a][]X_1,[]X'_1>),[]Y_1>) <= (sub <[c](let <[]X'_1,[a][]X_1>),[]Y_1>) => (let <(sub <[c][]X'_1,[]Y_1>),[a](sub <[c][]X_1,[]Y_1>)>) >,
     b#Y_1,a#X_1 |- < (sub <[a](sub <[a][(a b)]X_1,[]X'_1>),[]Y_1>) <= (sub <[a](let <[]X'_1,[b][]X_1>),[]Y_1>) => (let <(sub <[a][]X'_1,[]Y_1>),[b](sub <[a][]X_1,[]Y_1>)>) >,
     b#Y_1,a#X_1 |- < (sub <[c](sub <[a][(a b)]X_1,[]X'_1>),[]Y_1>) <= (sub <[c](let <[]X'_1,[b][]X_1>),[]Y_1>) => (let <(sub <[c][]X'_1,[]Y_1>),[b](sub <[c][]X_1,[]Y_1>)>) >,
     c#Y_1,a#X_1 |- < (sub <[a](sub <[a][(a c)]X_1,[]X'_1>),[]Y_1>) <= (sub <[a](let <[]X'_1,[c][]X_1>),[]Y_1>) => (let <(sub <[a][]X'_1,[]Y_1>),[c](sub <[a][]X_1,[]Y_1>)>) >,
     c#Y_1,a#X_1 |- < (sub <[b](sub <[a][(a c)]X_1,[]X'_1>),[]Y_1>) <= (sub <[b](let <[]X'_1,[c][]X_1>),[]Y_1>) => (let <(sub <[b][]X'_1,[]Y_1>),[c](sub <[b][]X_1,[]Y_1>)>) >,
     c#Y_1,a#X_1 |- < (sub <[d](sub <[a][(a c)]X_1,[]X'_1>),[]Y_1>) <= (sub <[d](let <[]X'_1,[c][]X_1>),[]Y_1>) => (let <(sub <[d][]X'_1,[]Y_1>),[c](sub <[d][]X_1,[]Y_1>)>) > }
(6 on 6(out)): 
   {  |- < (sub <[f][]X_1,(lam [a](letrec [f]<[a][]X'_1,[]X'_1>))>) <= (letrec [f]<[a][]X'_1,[]X_1>) => (sub <[f][]X_1,(lam [a](letrec [f]<[a][]X'_1,[]X'_1>))>) >,
     a#X'_1 |- < (sub <[f][]X_1,(lam [a](letrec [f]<[a][(a b)]X'_1,[(a b)]X'_1>))>) <= (letrec [f]<[b][]X'_1,[]X_1>) => (sub <[f][]X_1,(lam [b](letrec [f]<[b][]X'_1,[]X'_1>))>) >,
     f#X_1 |- < (sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(a f)]X'_1,[(a f)]X'_1>))>) <= (letrec [a]<[f][]X'_1,[]X_1>) => (sub <[a][]X_1,(lam [f](letrec [a]<[f][]X'_1,[]X'_1>))>) >,
     f#X_1,f#X'_1 |- < (sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(b f)]X'_1,[(b f)]X'_1>))>) <= (letrec [b]<[a][]X'_1,[]X_1>) => (sub <[b][]X_1,(lam [a](letrec [b]<[a][]X'_1,[]X'_1>))>) >,
     a#X'_1,f#X_1 |- < (sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(f a)(a b)]X'_1,[(f a)(a b)]X'_1>))>) <= (letrec [b]<[f][]X'_1,[]X_1>) => (sub <[b][]X_1,(lam [f](letrec [b]<[f][]X'_1,[]X'_1>))>) >,
     f#X'_1,f#X_1 |- < (sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(b a)(a f)]X'_1,[(b a)(a f)]X'_1>))>) <= (letrec [a]<[b][]X'_1,[]X_1>) => (sub <[a][]X_1,(lam [b](letrec [a]<[b][]X'_1,[]X'_1>))>) >,
     a#X'_1,f#X_1,f#X'_1 |- < (sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)(a b)]X'_1,[(c f)(a b)]X'_1>))>) <= (letrec [c]<[b][]X'_1,[]X_1>) => (sub <[c][]X_1,(lam [b](letrec [c]<[b][]X'_1,[]X'_1>))>) > }
(6 on 8(in)): 
   { a#Y_1,f#Y_1 |- < (sub <[b](sub <[f][]X_1,(lam [a](letrec [f]<[a][]X'_1,[]X'_1>))>),[]Y_1>) <= (sub <[b](letrec [f]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[a](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#Y_1,f#Y_1 |- < (sub <[c](sub <[f][]X_1,(lam [a](letrec [f]<[a][]X'_1,[]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [f]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[a](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     f#Y_1,a#X'_1,b#Y_1 |- < (sub <[a](sub <[f][]X_1,(lam [a](letrec [f]<[a][(a b)]X'_1,[(a b)]X'_1>))>),[]Y_1>) <= (sub <[a](letrec [f]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[b](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     f#Y_1,a#X'_1,b#Y_1 |- < (sub <[c](sub <[f][]X_1,(lam [a](letrec [f]<[a][(a b)]X'_1,[(a b)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [f]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[b](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     f#Y_1,a#X'_1,c#Y_1 |- < (sub <[a](sub <[f][]X_1,(lam [a](letrec [f]<[a][(a c)]X'_1,[(a c)]X'_1>))>),[]Y_1>) <= (sub <[a](letrec [f]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[c](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     f#Y_1,a#X'_1,c#Y_1 |- < (sub <[b](sub <[f][]X_1,(lam [a](letrec [f]<[a][(a c)]X'_1,[(a c)]X'_1>))>),[]Y_1>) <= (sub <[b](letrec [f]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[c](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     f#Y_1,a#X'_1,c#Y_1 |- < (sub <[d](sub <[f][]X_1,(lam [a](letrec [f]<[a][(a c)]X'_1,[(a c)]X'_1>))>),[]Y_1>) <= (sub <[d](letrec [f]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[c](sub <[d][]X'_1,[]Y_1>),(sub <[d][]X_1,[]Y_1>)>) >,
     f#Y_1,f#X_1,a#Y_1 |- < (sub <[b](sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(a f)]X'_1,[(a f)]X'_1>))>),[]Y_1>) <= (sub <[b](letrec [a]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[f](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     f#Y_1,f#X_1,a#Y_1 |- < (sub <[c](sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(a f)]X'_1,[(a f)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [a]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[f](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     b#Y_1,f#X_1,f#X'_1,a#Y_1 |- < (sub <[f](sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(b f)]X'_1,[(b f)]X'_1>))>),[]Y_1>) <= (sub <[f](letrec [b]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[a](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     b#Y_1,f#X_1,f#X'_1,a#Y_1 |- < (sub <[c](sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(b f)]X'_1,[(b f)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [b]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[a](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     c#Y_1,f#X_1,f#X'_1,a#Y_1 |- < (sub <[f](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)]X'_1,[(c f)]X'_1>))>),[]Y_1>) <= (sub <[f](letrec [c]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[a](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     c#Y_1,f#X_1,f#X'_1,a#Y_1 |- < (sub <[b](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)]X'_1,[(c f)]X'_1>))>),[]Y_1>) <= (sub <[b](letrec [c]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[a](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     c#Y_1,f#X_1,f#X'_1,a#Y_1 |- < (sub <[d](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)]X'_1,[(c f)]X'_1>))>),[]Y_1>) <= (sub <[d](letrec [c]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[a](sub <[d][]X'_1,[]Y_1>),(sub <[d][]X_1,[]Y_1>)>) >,
     a#X'_1,b#Y_1,f#X_1,f#Y_1 |- < (sub <[a](sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(f a)(a b)]X'_1,[(f a)(a b)]X'_1>))>),[]Y_1>) <= (sub <[a](letrec [b]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[f](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     a#X'_1,b#Y_1,f#X_1,f#Y_1 |- < (sub <[c](sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(f a)(a b)]X'_1,[(f a)(a b)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [b]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[f](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X'_1,c#Y_1,f#X_1,f#Y_1 |- < (sub <[a](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(f a)(a c)]X'_1,[(f a)(a c)]X'_1>))>),[]Y_1>) <= (sub <[a](letrec [c]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[f](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     a#X'_1,c#Y_1,f#X_1,f#Y_1 |- < (sub <[b](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(f a)(a c)]X'_1,[(f a)(a c)]X'_1>))>),[]Y_1>) <= (sub <[b](letrec [c]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[f](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#X'_1,c#Y_1,f#X_1,f#Y_1 |- < (sub <[d](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(f a)(a c)]X'_1,[(f a)(a c)]X'_1>))>),[]Y_1>) <= (sub <[d](letrec [c]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[f](sub <[d][]X'_1,[]Y_1>),(sub <[d][]X_1,[]Y_1>)>) >,
     b#Y_1,f#X_1,a#Y_1,f#X'_1 |- < (sub <[f](sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(b a)(a f)]X'_1,[(b a)(a f)]X'_1>))>),[]Y_1>) <= (sub <[f](letrec [a]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[b](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     c#Y_1,f#X_1,a#Y_1,f#X'_1 |- < (sub <[f](sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(c a)(a f)]X'_1,[(c a)(a f)]X'_1>))>),[]Y_1>) <= (sub <[f](letrec [a]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[c](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     c#Y_1,f#X_1,a#Y_1,f#X'_1 |- < (sub <[b](sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(c a)(a f)]X'_1,[(c a)(a f)]X'_1>))>),[]Y_1>) <= (sub <[b](letrec [a]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[c](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     b#Y_1,f#X_1,a#Y_1,f#X'_1 |- < (sub <[c](sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(b a)(a f)]X'_1,[(b a)(a f)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [a]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[b](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     d#Y_1,f#X_1,a#Y_1,f#X'_1 |- < (sub <[c](sub <[f][(a f)]X_1,(lam [a](letrec [f]<[a][(d a)(a f)]X'_1,[(d a)(a f)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [a]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[d](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X'_1,b#Y_1,f#X_1,f#X'_1,c#Y_1 |- < (sub <[f](sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(b f)(a c)]X'_1,[(b f)(a c)]X'_1>))>),[]Y_1>) <= (sub <[f](letrec [b]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[c](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#X'_1,c#Y_1,f#X_1,f#X'_1,b#Y_1 |- < (sub <[f](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)(a b)]X'_1,[(c f)(a b)]X'_1>))>),[]Y_1>) <= (sub <[f](letrec [c]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[b](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#X'_1,c#Y_1,f#X_1,f#X'_1,d#Y_1 |- < (sub <[f](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)(a d)]X'_1,[(c f)(a d)]X'_1>))>),[]Y_1>) <= (sub <[f](letrec [c]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[d](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#X'_1,b#Y_1,f#X_1,f#X'_1,c#Y_1 |- < (sub <[a](sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(b f)(a c)]X'_1,[(b f)(a c)]X'_1>))>),[]Y_1>) <= (sub <[a](letrec [b]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[c](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     a#X'_1,c#Y_1,f#X_1,f#X'_1,b#Y_1 |- < (sub <[a](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)(a b)]X'_1,[(c f)(a b)]X'_1>))>),[]Y_1>) <= (sub <[a](letrec [c]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[b](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     a#X'_1,c#Y_1,f#X_1,f#X'_1,d#Y_1 |- < (sub <[a](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)(a d)]X'_1,[(c f)(a d)]X'_1>))>),[]Y_1>) <= (sub <[a](letrec [c]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[d](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     a#X'_1,c#Y_1,f#X_1,f#X'_1,d#Y_1 |- < (sub <[b](sub <[f][(c f)]X_1,(lam [a](letrec [f]<[a][(c f)(a d)]X'_1,[(c f)(a d)]X'_1>))>),[]Y_1>) <= (sub <[b](letrec [c]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[d](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#X'_1,b#Y_1,f#X_1,f#X'_1,d#Y_1 |- < (sub <[c](sub <[f][(b f)]X_1,(lam [a](letrec [f]<[a][(b f)(a d)]X'_1,[(b f)(a d)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [b]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[d](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X'_1,d#Y_1,f#X_1,f#X'_1,b#Y_1 |- < (sub <[c](sub <[f][(d f)]X_1,(lam [a](letrec [f]<[a][(d f)(a b)]X'_1,[(d f)(a b)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [d]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[b](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X'_1,d#Y_1,f#X_1,f#X'_1,e#Y_1 |- < (sub <[c](sub <[f][(d f)]X_1,(lam [a](letrec [f]<[a][(d f)(a e)]X'_1,[(d f)(a e)]X'_1>))>),[]Y_1>) <= (sub <[c](letrec [d]<[e][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[e](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) > }
(7 on 3(out)): 
   { b#X,a#Y_1,b#X' |- < (let <(sub <[b][]X',[]Y_1>),[a](sub <[b][]X,[]Y_1>)>) <= (sub <[b](let <[]X',[a][]X>),[]Y_1>) => (let <[]X',[a][]X>) >,
     b#X,a#Y_1,b#X',a#X' |- < (let <(sub <[b][]X',[]Y_1>),[a](sub <[b][]X,[]Y_1>)>) <= (sub <[a](let <[(a b)]X',[b][(a b)]X>),[]Y_1>) => (let <[(a b)]X',[b][(a b)]X>) >,
     c#X',c#X,b#X',a#Y_1,b#X |- < (let <(sub <[b][]X',[]Y_1>),[a](sub <[b][]X,[]Y_1>)>) <= (sub <[c](let <[(b c)]X',[a][(b c)]X>),[]Y_1>) => (let <[(b c)]X',[a][(b c)]X>) > }
(7 on 7(out)): 
   { a#Y_1 |- < (let <(sub <[b][]X'_1,[]Y_1>),[a](sub <[b][]X_1,[]Y_1>)>) <= (sub <[b](let <[]X'_1,[a][]X_1>),[]Y_1>) => (let <(sub <[b][]X'_1,[]Y_1>),[a](sub <[b][]X_1,[]Y_1>)>) >,
     a#X_1,a#Y_1,c#Y_1 |- < (let <(sub <[b][]X'_1,[]Y_1>),[a](sub <[b][(a c)]X_1,[]Y_1>)>) <= (sub <[b](let <[]X'_1,[c][]X_1>),[]Y_1>) => (let <(sub <[b][]X'_1,[]Y_1>),[c](sub <[b][]X_1,[]Y_1>)>) >,
     b#X'_1,b#Y_1,a#Y_1 |- < (let <(sub <[b][(a b)]X'_1,[]Y_1>),[a](sub <[b][(a b)]X_1,[]Y_1>)>) <= (sub <[a](let <[]X'_1,[b][]X_1>),[]Y_1>) => (let <(sub <[a][]X'_1,[]Y_1>),[b](sub <[a][]X_1,[]Y_1>)>) >,
     b#X_1,a#Y_1,b#X'_1 |- < (let <(sub <[b][(b c)]X'_1,[]Y_1>),[a](sub <[b][(b c)]X_1,[]Y_1>)>) <= (sub <[c](let <[]X'_1,[a][]X_1>),[]Y_1>) => (let <(sub <[c][]X'_1,[]Y_1>),[a](sub <[c][]X_1,[]Y_1>)>) >,
     a#Y_1,b#Y_1,b#X'_1,a#X_1 |- < (let <(sub <[b][(b c)]X'_1,[]Y_1>),[a](sub <[b][(b a)(a c)]X_1,[]Y_1>)>) <= (sub <[c](let <[]X'_1,[b][]X_1>),[]Y_1>) => (let <(sub <[c][]X'_1,[]Y_1>),[b](sub <[c][]X_1,[]Y_1>)>) >,
     b#X_1,b#X'_1,c#Y_1,a#Y_1 |- < (let <(sub <[b][(a b)]X'_1,[]Y_1>),[a](sub <[b][(c a)(a b)]X_1,[]Y_1>)>) <= (sub <[a](let <[]X'_1,[c][]X_1>),[]Y_1>) => (let <(sub <[a][]X'_1,[]Y_1>),[c](sub <[a][]X_1,[]Y_1>)>) >,
     b#X_1,a#Y_1,d#Y_1,b#X'_1,a#X_1 |- < (let <(sub <[b][(b c)]X'_1,[]Y_1>),[a](sub <[b][(b c)(a d)]X_1,[]Y_1>)>) <= (sub <[c](let <[]X'_1,[d][]X_1>),[]Y_1>) => (let <(sub <[c][]X'_1,[]Y_1>),[d](sub <[c][]X_1,[]Y_1>)>) > }
(8 on 3(out)): 
   { b#X,b#X',f#Y_1,a#Y_1 |- < (letrec [f]<[a](sub <[b][]X',[]Y_1>),(sub <[b][]X,[]Y_1>)>) <= (sub <[b](letrec [f]<[a][]X',[]X>),[]Y_1>) => (letrec [f]<[a][]X',[]X>) >,
     b#X,b#X',f#Y_1,a#Y_1 |- < (letrec [f]<[a](sub <[b][]X',[]Y_1>),(sub <[b][]X,[]Y_1>)>) <= (sub <[f](letrec [b]<[a][(b f)]X',[(b f)]X>),[]Y_1>) => (letrec [b]<[a][(b f)]X',[(b f)]X>) >,
     b#X,b#X',f#Y_1,a#Y_1,a#X |- < (letrec [f]<[a](sub <[b][]X',[]Y_1>),(sub <[b][]X,[]Y_1>)>) <= (sub <[a](letrec [f]<[b][(a b)]X',[(a b)]X>),[]Y_1>) => (letrec [f]<[b][(a b)]X',[(a b)]X>) >,
     c#X',c#X,a#Y_1,f#Y_1,b#X',b#X |- < (letrec [f]<[a](sub <[b][]X',[]Y_1>),(sub <[b][]X,[]Y_1>)>) <= (sub <[c](letrec [f]<[a][(b c)]X',[(b c)]X>),[]Y_1>) => (letrec [f]<[a][(b c)]X',[(b c)]X>) > }
(8 on 8(out)): 
   { f#Y_1,a#Y_1 |- < (letrec [f]<[a](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) <= (sub <[b](letrec [f]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[a](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     c#Y_1,a#X'_1,f#Y_1,a#Y_1 |- < (letrec [f]<[a](sub <[b][(a c)]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) <= (sub <[b](letrec [f]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[c](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#Y_1,f#X_1,f#Y_1 |- < (letrec [f]<[a](sub <[b][(a f)]X'_1,[]Y_1>),(sub <[b][(a f)]X_1,[]Y_1>)>) <= (sub <[b](letrec [a]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[f](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     a#Y_1,f#X'_1,f#X_1,f#Y_1,c#Y_1 |- < (letrec [f]<[a](sub <[b][(c f)]X'_1,[]Y_1>),(sub <[b][(c f)]X_1,[]Y_1>)>) <= (sub <[b](letrec [c]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[a](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     f#Y_1,f#X_1,a#Y_1,c#Y_1,a#X'_1 |- < (letrec [f]<[a](sub <[b][(f a)(a c)]X'_1,[]Y_1>),(sub <[b][(c f)]X_1,[]Y_1>)>) <= (sub <[b](letrec [c]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[f](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     f#X'_1,a#Y_1,f#Y_1,f#X_1,c#Y_1 |- < (letrec [f]<[a](sub <[b][(c a)(a f)]X'_1,[]Y_1>),(sub <[b][(a f)]X_1,[]Y_1>)>) <= (sub <[b](letrec [a]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[c](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     d#Y_1,f#X'_1,f#X_1,f#Y_1,a#Y_1,c#Y_1,a#X'_1 |- < (letrec [f]<[a](sub <[b][(c f)(a d)]X'_1,[]Y_1>),(sub <[b][(c f)]X_1,[]Y_1>)>) <= (sub <[b](letrec [c]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[d](sub <[b][]X'_1,[]Y_1>),(sub <[b][]X_1,[]Y_1>)>) >,
     b#Y_1,f#Y_1,a#Y_1 |- < (letrec [f]<[a](sub <[b][(b f)]X'_1,[]Y_1>),(sub <[b][(b f)]X_1,[]Y_1>)>) <= (sub <[f](letrec [b]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[a](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#Y_1,f#Y_1,b#X_1,b#Y_1 |- < (letrec [f]<[a](sub <[b][(a b)]X'_1,[]Y_1>),(sub <[b][(a b)]X_1,[]Y_1>)>) <= (sub <[a](letrec [f]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[b](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     a#Y_1,b#X'_1,b#X_1,f#Y_1 |- < (letrec [f]<[a](sub <[b][(b c)]X'_1,[]Y_1>),(sub <[b][(b c)]X_1,[]Y_1>)>) <= (sub <[c](letrec [f]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[a](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X'_1,b#Y_1,a#Y_1,f#Y_1,c#Y_1 |- < (letrec [f]<[a](sub <[b][(b f)(a c)]X'_1,[]Y_1>),(sub <[b][(b f)]X_1,[]Y_1>)>) <= (sub <[f](letrec [b]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[c](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     b#Y_1,b#X_1,f#Y_1,a#Y_1,a#X'_1 |- < (letrec [f]<[a](sub <[b][(b a)(a c)]X'_1,[]Y_1>),(sub <[b][(b c)]X_1,[]Y_1>)>) <= (sub <[c](letrec [f]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[b](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     b#X'_1,f#Y_1,a#Y_1,b#X_1,c#Y_1 |- < (letrec [f]<[a](sub <[b][(c a)(a b)]X'_1,[]Y_1>),(sub <[b][(a b)]X_1,[]Y_1>)>) <= (sub <[a](letrec [f]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[c](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     d#Y_1,b#X'_1,b#X_1,a#Y_1,f#Y_1,a#X'_1 |- < (letrec [f]<[a](sub <[b][(b c)(a d)]X'_1,[]Y_1>),(sub <[b][(b c)]X_1,[]Y_1>)>) <= (sub <[c](letrec [f]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [f]<[d](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     f#X_1,b#Y_1,a#Y_1,f#Y_1 |- < (letrec [f]<[a](sub <[b][(f a)(a b)]X'_1,[]Y_1>),(sub <[b][(f a)(a b)]X_1,[]Y_1>)>) <= (sub <[a](letrec [b]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[f](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     b#Y_1,f#Y_1,a#Y_1,b#X_1 |- < (letrec [f]<[a](sub <[b][(b a)(a f)]X'_1,[]Y_1>),(sub <[b][(b a)(a f)]X_1,[]Y_1>)>) <= (sub <[f](letrec [a]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[b](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     f#X_1,a#Y_1,f#Y_1,b#X_1,b#X'_1 |- < (letrec [f]<[a](sub <[b][(b c)(a f)]X'_1,[]Y_1>),(sub <[b][(b c)(a f)]X_1,[]Y_1>)>) <= (sub <[c](letrec [a]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[f](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#Y_1,f#Y_1,b#Y_1,f#X_1,f#X'_1 |- < (letrec [f]<[a](sub <[b][(c b)(b f)]X'_1,[]Y_1>),(sub <[b][(c b)(b f)]X_1,[]Y_1>)>) <= (sub <[c](letrec [b]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[a](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     f#X'_1,f#X_1,c#Y_1,a#Y_1,f#Y_1,b#X_1,b#Y_1 |- < (letrec [f]<[a](sub <[b][(c f)(a b)]X'_1,[]Y_1>),(sub <[b][(c f)(a b)]X_1,[]Y_1>)>) <= (sub <[a](letrec [c]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[b](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     b#X'_1,b#X_1,c#Y_1,a#Y_1,f#Y_1 |- < (letrec [f]<[a](sub <[b][(f b)(b c)]X'_1,[]Y_1>),(sub <[b][(f b)(b c)]X_1,[]Y_1>)>) <= (sub <[f](letrec [c]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[a](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     b#X'_1,b#X_1,f#Y_1,a#Y_1,d#Y_1,f#X_1,f#X'_1 |- < (letrec [f]<[a](sub <[b][(d f)(b c)]X'_1,[]Y_1>),(sub <[b][(d f)(b c)]X_1,[]Y_1>)>) <= (sub <[c](letrec [d]<[a][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[a](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X'_1,f#X_1,b#Y_1,a#Y_1,f#Y_1 |- < (letrec [f]<[a](sub <[b][(b f)(a c)]X'_1,[]Y_1>),(sub <[b][(c b)(b f)]X_1,[]Y_1>)>) <= (sub <[c](letrec [b]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[f](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     b#Y_1,b#X_1,f#Y_1,a#Y_1,c#Y_1,a#X'_1 |- < (letrec [f]<[a](sub <[b][(f b)(b a)(a c)]X'_1,[]Y_1>),(sub <[b][(f b)(b c)]X_1,[]Y_1>)>) <= (sub <[f](letrec [c]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[b](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     b#X'_1,f#X_1,c#Y_1,a#Y_1,f#Y_1,b#X_1 |- < (letrec [f]<[a](sub <[b][(c f)(a b)]X'_1,[]Y_1>),(sub <[b][(c f)(a b)]X_1,[]Y_1>)>) <= (sub <[a](letrec [c]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[f](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     b#X'_1,b#X_1,f#Y_1,a#Y_1,d#Y_1,f#X_1,a#X'_1 |- < (letrec [f]<[a](sub <[b][(f a)(b c)(a d)]X'_1,[]Y_1>),(sub <[b][(d f)(b c)]X_1,[]Y_1>)>) <= (sub <[c](letrec [d]<[f][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[f](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     f#X'_1,f#X_1,b#Y_1,a#Y_1,f#Y_1,c#Y_1 |- < (letrec [f]<[a](sub <[b][(f c)(c a)(a b)]X'_1,[]Y_1>),(sub <[b][(f a)(a b)]X_1,[]Y_1>)>) <= (sub <[a](letrec [b]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[c](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     d#Y_1,f#Y_1,a#Y_1,b#Y_1,f#X_1,f#X'_1,a#X'_1 |- < (letrec [f]<[a](sub <[b][(c b)(b f)(a d)]X'_1,[]Y_1>),(sub <[b][(c b)(b f)]X_1,[]Y_1>)>) <= (sub <[c](letrec [b]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [b]<[d](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     b#Y_1,b#X_1,f#Y_1,a#Y_1,f#X_1,f#X'_1 |- < (letrec [f]<[a](sub <[b][(c b)(b a)(a f)]X'_1,[]Y_1>),(sub <[b][(b c)(a f)]X_1,[]Y_1>)>) <= (sub <[c](letrec [a]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[b](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     a#X'_1,f#X'_1,f#X_1,c#Y_1,a#Y_1,f#Y_1,b#X_1,b#Y_1 |- < (letrec [f]<[a](sub <[b][(c f)(b a)(a d)]X'_1,[]Y_1>),(sub <[b][(c f)(b d)]X_1,[]Y_1>)>) <= (sub <[d](letrec [c]<[b][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[b](sub <[d][]X'_1,[]Y_1>),(sub <[d][]X_1,[]Y_1>)>) >,
     b#X'_1,b#X_1,a#Y_1,f#Y_1,c#Y_1 |- < (letrec [f]<[a](sub <[b][(b c)(a f)]X'_1,[]Y_1>),(sub <[b][(b a)(a f)]X_1,[]Y_1>)>) <= (sub <[f](letrec [a]<[c][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[c](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     d#Y_1,b#X'_1,b#X_1,f#Y_1,a#Y_1,f#X_1,f#X'_1 |- < (letrec [f]<[a](sub <[b][(d a)(b c)(a f)]X'_1,[]Y_1>),(sub <[b][(b c)(a f)]X_1,[]Y_1>)>) <= (sub <[c](letrec [a]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [a]<[d](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) >,
     d#Y_1,b#X_1,f#Y_1,a#Y_1,c#Y_1,f#X_1,f#X'_1,b#X'_1 |- < (letrec [f]<[a](sub <[b][(d a)(c f)(a b)]X'_1,[]Y_1>),(sub <[b][(c f)(a b)]X_1,[]Y_1>)>) <= (sub <[a](letrec [c]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[d](sub <[a][]X'_1,[]Y_1>),(sub <[a][]X_1,[]Y_1>)>) >,
     d#Y_1,f#Y_1,a#Y_1,c#Y_1,b#X_1,b#X'_1,a#X'_1 |- < (letrec [f]<[a](sub <[b][(f b)(b c)(a d)]X'_1,[]Y_1>),(sub <[b][(f b)(b c)]X_1,[]Y_1>)>) <= (sub <[f](letrec [c]<[d][]X'_1,[]X_1>),[]Y_1>) => (letrec [c]<[d](sub <[f][]X'_1,[]Y_1>),(sub <[f][]X_1,[]Y_1>)>) >,
     a#X'_1,f#X'_1,f#X_1,d#Y_1,a#Y_1,f#Y_1,b#X_1,b#X'_1,e#Y_1 |- < (letrec [f]<[a](sub <[b][(d f)(b c)(a e)]X'_1,[]Y_1>),(sub <[b][(d f)(b c)]X_1,[]Y_1>)>) <= (sub <[c](letrec [d]<[e][]X'_1,[]X_1>),[]Y_1>) => (letrec [d]<[e](sub <[c][]X'_1,[]Y_1>),(sub <[c][]X_1,[]Y_1>)>) > }
inBCP:  |- <  (sub <[a](sub <[a][]X,[]Y_1>),[]Z_1>),   (app <(sub <[a](lam [a][]X),[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>)  > is not closed
failed to show all BCPs are parallel closed
result: MAYBE
time: 1446 msec.