Term Rewriting System R:

   [T, L, Tp, Lp, S, X, Sp, Xp, K, Y, Z]
   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)))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   EQ(apply(T, S), apply(Tp, Sp)) -> AND(eq(T, Tp), eq(S, Sp))
   EQ(apply(T, S), apply(Tp, Sp)) -> EQ(T, Tp)
   EQ(apply(T, S), apply(Tp, Sp)) -> EQ(S, Sp)
   EQ(var(L), var(Lp)) -> EQ(L, Lp)
   EQ(lambda(X, T), lambda(Xp, Tp)) -> AND(eq(T, Tp), eq(X, Xp))
   EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(T, Tp)
   EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(X, Xp)
   EQ(cons(T, L), cons(Tp, Lp)) -> AND(eq(T, Tp), eq(L, Lp))
   EQ(cons(T, L), cons(Tp, Lp)) -> EQ(T, Tp)
   EQ(cons(T, L), cons(Tp, Lp)) -> EQ(L, Lp)
   REN(var(L), var(K), var(Lp)) -> IF(eq(L, Lp), var(K), var(Lp))
   REN(var(L), var(K), var(Lp)) -> EQ(L, Lp)
   REN(X, Y, lambda(Z, T)) -> REN(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T))
   REN(X, Y, lambda(Z, T)) -> REN(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)
   REN(X, Y, apply(T, S)) -> REN(X, Y, T)
   REN(X, Y, apply(T, S)) -> REN(X, Y, S)

Furthermore, R contains two SCCs.


SCC1:

EQ(cons(T, L), cons(Tp, Lp)) -> EQ(L, Lp)
EQ(cons(T, L), cons(Tp, Lp)) -> EQ(T, Tp)
EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(X, Xp)
EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(T, Tp)
EQ(var(L), var(Lp)) -> EQ(L, Lp)
EQ(apply(T, S), apply(Tp, Sp)) -> EQ(S, Sp)
EQ(apply(T, S), apply(Tp, Sp)) -> EQ(T, Tp)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(lambda(x_1, x_2)) = 1 + x_1 + x_2
POL(EQ(x_1, x_2)) = 1 + x_1 + x_2
POL(apply(x_1, x_2)) = 1 + x_1 + x_2
POL(var(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   EQ(cons(T, L), cons(Tp, Lp)) -> EQ(L, Lp)
   EQ(cons(T, L), cons(Tp, Lp)) -> EQ(T, Tp)
   EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(X, Xp)
   EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(T, Tp)
   EQ(var(L), var(Lp)) -> EQ(L, Lp)
   EQ(apply(T, S), apply(Tp, Sp)) -> EQ(S, Sp)
   EQ(apply(T, S), apply(Tp, Sp)) -> EQ(T, Tp)



 This transformation is resulting in no new subcycles.


SCC2:

REN(X, Y, apply(T, S)) -> REN(X, Y, S)
REN(X, Y, apply(T, S)) -> REN(X, Y, T)
REN(X, Y, lambda(Z, T)) -> REN(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)
REN(X, Y, lambda(Z, T)) -> REN(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp))
   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)))
   ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S))
   if(false, var(K), var(L)) -> var(L)
   if(true, var(K), var(L)) -> var(K)


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(lambda(x_1, x_2)) = 1 + x_2
POL(ren(x_1, x_2, x_3)) = x_3
POL(eq(x_1, x_2)) = 0
POL(apply(x_1, x_2)) = 1 + x_1 + x_2
POL(REN(x_1, x_2, x_3)) = x_3
POL(and(x_1, x_2)) = 0
POL(true) = 0
POL(var(x_1)) = 0
POL(if(x_1, x_2, x_3)) = 0
POL(false) = 0
POL(cons(x_1, x_2)) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 2.636 seconds.