MAYBE
ignored inputs:
(COMMENT a system of beta reduction for the lambda calculus via orthogonal explicit substitution calculus )

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):  |- (sub <[a]b,[]Y>) -> b,
     (4): b#Y |- (sub <[a](lam [b][]X),[]Y>) -> (lam [b](sub <[a][]X,[]Y>)) ]
Check confluence by orthogonality
abstract skeleton preserving
left-linear
check proper overlapping
a proper overlap exists
0-1
 |- < (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>)>) >
found proper overlaps
result: MAYBE
time: 4 msec.