MAYBE
ignored inputs:
(COMMENT a system of beta eta 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>)),
     (5): a#X |- (lam [a](app <[]X,a>)) -> []X ]
Check confluence by Knuth-Bendix criterion
uniform

writing to temporary file...
./run_snprover.sh ./SMLNJ-UPeWAC.trs
NO

Problem:
 app(pair_2(lam(lambda(X)),Y)) -> sub(pair_2(lambda(X),Y))
 sub(pair_2(lambda(app(pair_2(X,Y))),Z)) ->
 app(pair_2(sub(pair_2(lambda(X),Z)),sub(pair_2(lambda(Y),Z))))
 sub(pair_2(lambda(diamond()),X)) -> X
 sub(pair_2(lambda(diamond()),Y)) -> diamond()
 sub(pair_2(lambda(lam(lambda(X))),Y)) -> lam(lambda(sub(pair_2(lambda(X),Y))))
 lam(lambda(app(pair_2(X,diamond())))) -> X

Proof:
 Unfolding Processor:
  loop length: 4
  terms:
   app(pair_2(lam(lambda(app(pair_2(diamond(),diamond())))),lam(lambda
                                                                (app(pair_2(diamond(),diamond()))))))
   sub(pair_2(lambda(app(pair_2(diamond(),diamond()))),lam(lambda(app(pair_2(diamond(),diamond()))))))
   app(pair_2(sub(pair_2(lambda(diamond()),lam(lambda(app(pair_2(diamond(),diamond())))))),
              sub(pair_2(lambda(diamond()),lam(lambda(app(pair_2(diamond(),diamond()))))))))
   app(pair_2(lam(lambda(app(pair_2(diamond(),diamond())))),sub(pair_2
                                                                (lambda(diamond()),
                                                                 lam(
                                                                    lambda
                                                                    (
                                                                    app
                                                                    (
                                                                    pair_2(diamond(),diamond()))))))))
  context: []
  substitution:
   
  Qed
termination proof failed
result: MAYBE
time: 4 msec.