Consider the TRS R consisting of the rewrite rules

1: and(true,y) -> y
2: and(false,y) -> false
3: eq(nil,nil) -> true
4: eq(cons(t,l),nil) -> false
5: eq(nil,cons(t,l)) -> false
6: eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
7: eq(var(l),var(l')) -> eq(l,l')
8: eq(var(l),apply(t,s)) -> false
9: eq(var(l),lambda(x,t)) -> false
10: eq(apply(t,s),var(l)) -> false
11: eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
12: eq(apply(t,s),lambda(x,t)) -> false
13: eq(lambda(x,t),var(l)) -> false
14: eq(lambda(x,t),apply(t,s)) -> false
15: eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
16: if(true,var(k),var(l')) -> var(k)
17: if(false,var(k),var(l')) -> var(l')
18: ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
19: ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
20: 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)))

There are 16 dependency pairs:

21: EQ(cons(t,l),cons(t',l')) -> AND(eq(t,t'),eq(l,l'))
22: EQ(cons(t,l),cons(t',l')) -> EQ(t,t')
23: EQ(cons(t,l),cons(t',l')) -> EQ(l,l')
24: EQ(var(l),var(l')) -> EQ(l,l')
25: EQ(apply(t,s),apply(t',s')) -> AND(eq(t,t'),eq(s,s'))
26: EQ(apply(t,s),apply(t',s')) -> EQ(t,t')
27: EQ(apply(t,s),apply(t',s')) -> EQ(s,s')
28: EQ(lambda(x,t),lambda(x',t')) -> AND(eq(x,x'),eq(t,t'))
29: EQ(lambda(x,t),lambda(x',t')) -> EQ(x,x')
30: EQ(lambda(x,t),lambda(x',t')) -> EQ(t,t')
31: REN(var(l),var(k),var(l')) -> IF(eq(l,l'),var(k),var(l'))
32: REN(var(l),var(k),var(l')) -> EQ(l,l')
33: REN(x,y,apply(t,s)) -> REN(x,y,t)
34: REN(x,y,apply(t,s)) -> REN(x,y,s)
35: REN(x,y,lambda(z,t)) -> REN(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t))
36: REN(x,y,lambda(z,t)) -> REN(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t)

The approximated dependency graph contains 2 SCCs:
{22-24,26,27,29,30}
and {33-36}.

- Consider the SCC {22-24,26,27,29,30}.
There are no usable rules.
By taking the polynomial interpretation
[var](x) = x + 1
and [apply](x,y) = [cons](x,y) = [EQ](x,y) = [lambda](x,y) = x + y + 1,
the rules in {22-24,26,27,29,30}
are strictly decreasing.

- Consider the SCC {33-36}.
By taking the polynomial interpretation
[false] = 0,
[eq](x,y) = [nil] = [true] = [var](x) = 1,
[apply](x,y) = [cons](x,y) = x + y + 1,
[and](x,y) = [if](x,y,z) = y,
[lambda](x,y) = y + 1,
[REN](x,y,z) = y + z + 1
and [ren](x,y,z) = z,
the rules in {1-3,6,7,11,15-20,36}
are weakly decreasing and
the rules in {4,5,8-10,12-14,33-35}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {36}.
There are no usable rules.
By taking the polynomial interpretation
[nil] = 1,
[cons](x,y) = [var](x) = x,
[lambda](x,y) = x + y + 1
and [REN](x,y,z) = x + y + z + 1,
rule 36
is strictly decreasing.


Hence the TRS is terminating.