YES
(VAR T L Tp Lp S X Sp Xp K Y Z)
(RULES 
and(false,false) -> false
and(true,false) -> false
and(false,true) -> false
and(true,true) -> true
eq(nil,nil) -> true
eq(cons(T,L),nil) -> false
eq(nil,cons(T,L)) -> false
eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
eq(var(L),var(Lp)) -> eq(L,Lp)
eq(var(L),apply(T,S)) -> false
eq(var(L),lambda(X,T)) -> false
eq(apply(T,S),var(L)) -> false
eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
eq(apply(T,S),lambda(X,Tp)) -> false
eq(lambda(X,T),var(L)) -> false
eq(lambda(X,T),apply(Tp,Sp)) -> false
eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
if(true,var(K),var(L)) -> var(K)
if(false,var(K),var(L)) -> var(L)
ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S))
ren(X,Y,lambda(Z,T)) -> lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)))
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for ma96:

-> Dependency pairs:
nF_eq(cons(T,L),cons(Tp,Lp)) -> nF_and(eq(T,Tp),eq(L,Lp))
nF_eq(cons(T,L),cons(Tp,Lp)) -> nF_eq(T,Tp)
nF_eq(cons(T,L),cons(Tp,Lp)) -> nF_eq(L,Lp)
nF_eq(var(L),var(Lp)) -> nF_eq(L,Lp)
nF_eq(apply(T,S),apply(Tp,Sp)) -> nF_and(eq(T,Tp),eq(S,Sp))
nF_eq(apply(T,S),apply(Tp,Sp)) -> nF_eq(T,Tp)
nF_eq(apply(T,S),apply(Tp,Sp)) -> nF_eq(S,Sp)
nF_eq(lambda(X,T),lambda(Xp,Tp)) -> nF_and(eq(T,Tp),eq(X,Xp))
nF_eq(lambda(X,T),lambda(Xp,Tp)) -> nF_eq(T,Tp)
nF_eq(lambda(X,T),lambda(Xp,Tp)) -> nF_eq(X,Xp)
nF_ren(var(L),var(K),var(Lp)) -> nF_if(eq(L,Lp),var(K),var(Lp))
nF_ren(var(L),var(K),var(Lp)) -> nF_eq(L,Lp)
nF_ren(X,Y,apply(T,S)) -> nF_ren(X,Y,T)
nF_ren(X,Y,apply(T,S)) -> nF_ren(X,Y,S)
nF_ren(X,Y,lambda(Z,T)) -> nF_ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))
nF_ren(X,Y,lambda(Z,T)) -> nF_ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)

-> Proof of termination for ma96_1_1:
-> -> Dependency pairs in cycle:
nF_ren(X,Y,apply(T,S)) -> nF_ren(X,Y,T)
nF_ren(X,Y,lambda(Z,T)) -> nF_ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)
nF_ren(X,Y,lambda(Z,T)) -> nF_ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))
nF_ren(X,Y,apply(T,S)) -> nF_ren(X,Y,S)

UsableRules:
and(false,false) -> false
and(true,false) -> false
and(false,true) -> false
and(true,true) -> true
eq(nil,nil) -> true
eq(cons(T,L),nil) -> false
eq(nil,cons(T,L)) -> false
eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
eq(var(L),var(Lp)) -> eq(L,Lp)
eq(var(L),apply(T,S)) -> false
eq(var(L),lambda(X,T)) -> false
eq(apply(T,S),var(L)) -> false
eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
eq(apply(T,S),lambda(X,Tp)) -> false
eq(lambda(X,T),var(L)) -> false
eq(lambda(X,T),apply(Tp,Sp)) -> false
eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
if(true,var(K),var(L)) -> var(K)
if(false,var(K),var(L)) -> var(L)
ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S))
ren(X,Y,lambda(Z,T)) -> lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)))

Polynomial Interpretation:

[and](X1,X2) = 0
[false] = 0
[true] = 0
[eq](X1,X2) = 0
[nil] = 0
[cons](X1,X2) = 0
[var](X) = 1
[apply](X1,X2) = X1 + X2 + 1
[lambda](X1,X2) = X2
[if](X1,X2,X3) = X3
[ren](X1,X2,X3) = X3
[nF_ren](X1,X2,X3) = X3

TIME: 7.1081e-2

-> -> Dependency pairs in cycle:
nF_ren(X,Y,apply(T,S)) -> nF_ren(X,Y,T)
nF_ren(X,Y,lambda(Z,T)) -> nF_ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))
nF_ren(X,Y,lambda(Z,T)) -> nF_ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)

UsableRules:
and(false,false) -> false
and(true,false) -> false
and(false,true) -> false
and(true,true) -> true
eq(nil,nil) -> true
eq(cons(T,L),nil) -> false
eq(nil,cons(T,L)) -> false
eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
eq(var(L),var(Lp)) -> eq(L,Lp)
eq(var(L),apply(T,S)) -> false
eq(var(L),lambda(X,T)) -> false
eq(apply(T,S),var(L)) -> false
eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
eq(apply(T,S),lambda(X,Tp)) -> false
eq(lambda(X,T),var(L)) -> false
eq(lambda(X,T),apply(Tp,Sp)) -> false
eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
if(true,var(K),var(L)) -> var(K)
if(false,var(K),var(L)) -> var(L)
ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S))
ren(X,Y,lambda(Z,T)) -> lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)))

Polynomial Interpretation:

[and](X1,X2) = 0
[false] = 0
[true] = 0
[eq](X1,X2) = 0
[nil] = 0
[cons](X1,X2) = 0
[var](X) = X
[apply](X1,X2) = X1 + 1
[lambda](X1,X2) = X2 + 1
[if](X1,X2,X3) = X2 + X3
[ren](X1,X2,X3) = X2 + X3
[nF_ren](X1,X2,X3) = X3

TIME: 6.6514e-2

-> -> Dependency pairs in cycle:
nF_ren(X,Y,apply(T,S)) -> nF_ren(X,Y,T)
nF_ren(X,Y,lambda(Z,T)) -> nF_ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))

UsableRules:
and(false,false) -> false
and(true,false) -> false
and(false,true) -> false
and(true,true) -> true
eq(nil,nil) -> true
eq(cons(T,L),nil) -> false
eq(nil,cons(T,L)) -> false
eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
eq(var(L),var(Lp)) -> eq(L,Lp)
eq(var(L),apply(T,S)) -> false
eq(var(L),lambda(X,T)) -> false
eq(apply(T,S),var(L)) -> false
eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
eq(apply(T,S),lambda(X,Tp)) -> false
eq(lambda(X,T),var(L)) -> false
eq(lambda(X,T),apply(Tp,Sp)) -> false
eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
if(true,var(K),var(L)) -> var(K)
if(false,var(K),var(L)) -> var(L)
ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S))
ren(X,Y,lambda(Z,T)) -> lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)))

Polynomial Interpretation:

[and](X1,X2) = X1
[false] = 1
[true] = 1
[eq](X1,X2) = 1
[nil] = 0
[cons](X1,X2) = 0
[var](X) = 0
[apply](X1,X2) = X1
[lambda](X1,X2) = X2 + 1
[if](X1,X2,X3) = 0
[ren](X1,X2,X3) = X3
[nF_ren](X1,X2,X3) = X3

TIME: 6.8011e-2

-> -> Dependency pairs in cycle:
nF_ren(X,Y,apply(T,S)) -> nF_ren(X,Y,T)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for ma96_1_2:
-> -> Dependency pairs in cycle:
nF_eq(cons(T,L),cons(Tp,Lp)) -> nF_eq(T,Tp)
nF_eq(lambda(X,T),lambda(Xp,Tp)) -> nF_eq(X,Xp)
nF_eq(lambda(X,T),lambda(Xp,Tp)) -> nF_eq(T,Tp)
nF_eq(apply(T,S),apply(Tp,Sp)) -> nF_eq(S,Sp)
nF_eq(apply(T,S),apply(Tp,Sp)) -> nF_eq(T,Tp)
nF_eq(var(L),var(Lp)) -> nF_eq(L,Lp)
nF_eq(cons(T,L),cons(Tp,Lp)) -> nF_eq(L,Lp)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.