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. 



   R
     ↳Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost. 


   R
     ↳OC
       →TRS2
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

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)
EQ(var(L), var(Lp)) -> EQ(L, Lp)
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(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)
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, apply(T, S)) -> REN(X, Y, T)
REN(X, Y, apply(T, S)) -> REN(X, Y, S)
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)

Furthermore, R contains two SCCs. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Usable Rules (Innermost)
           →DP Problem 2
             ↳Neg POLO


Dependency Pairs:

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


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)))


Strategy:

innermost




As we are in the innermost case, we can delete all 22 non-usable-rules.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
             ...
               →DP Problem 3
                 ↳Size-Change Principle
           →DP Problem 2
             ↳Neg POLO


Dependency Pairs:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(X, Xp)
  2. EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(T, Tp)
  3. EQ(apply(T, S), apply(Tp, Sp)) -> EQ(S, Sp)
  4. EQ(apply(T, S), apply(Tp, Sp)) -> EQ(T, Tp)
  5. EQ(var(L), var(Lp)) -> EQ(L, Lp)
  6. EQ(cons(T, L), cons(Tp, Lp)) -> EQ(L, Lp)
  7. EQ(cons(T, L), cons(Tp, Lp)) -> EQ(T, Tp)
and get the following Size-Change Graph(s):
{1, 2, 3, 4, 5, 6, 7} , {1, 2, 3, 4, 5, 6, 7}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1, 2, 3, 4, 5, 6, 7} , {1, 2, 3, 4, 5, 6, 7}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
apply(x1, x2) -> apply(x1, x2)
var(x1) -> var(x1)
cons(x1, x2) -> cons(x1, x2)
lambda(x1, x2) -> lambda(x1, x2)

We obtain no new DP problems. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳Negative Polynomial Order


Dependency Pairs:

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))
REN(X, Y, apply(T, S)) -> REN(X, Y, S)
REN(X, Y, apply(T, S)) -> REN(X, Y, T)


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)))


Strategy:

innermost




The following Dependency Pairs can be strictly oriented using the given order.

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))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

eq(var(L), lambda(X, T)) -> false
and(true, true) -> true
eq(apply(T, S), var(L)) -> false
ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp))
and(false, true) -> false
eq(apply(T, S), lambda(X, Tp)) -> false
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)))
eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp))
eq(lambda(X, T), var(L)) -> false
eq(cons(T, L), nil) -> false
ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S))
eq(nil, nil) -> true
eq(var(L), var(Lp)) -> eq(L, Lp)
eq(nil, cons(T, L)) -> false
eq(var(L), apply(T, S)) -> false
eq(lambda(X, T), apply(Tp, Sp)) -> false
eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp))
eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp))
and(true, false) -> false
if(false, var(K), var(L)) -> var(L)
if(true, var(K), var(L)) -> var(K)
and(false, false) -> false


Used ordering:
Polynomial Order with Interpretation:

POL( REN(x1, ..., x3) ) = x3

POL( lambda(x1, x2) ) = x2 + 1

POL( apply(x1, x2) ) = x1 + x2

POL( ren(x1, ..., x3) ) = x3

POL( eq(x1, x2) ) = 0

POL( false ) = 0

POL( and(x1, x2) ) = 0

POL( true ) = 0

POL( var(x1) ) = 0

POL( if(x1, ..., x3) ) = 0


This results in one new DP problem. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳Neg POLO
             ...
               →DP Problem 4
                 ↳Usable Rules (Innermost)


Dependency Pairs:

REN(X, Y, apply(T, S)) -> REN(X, Y, S)
REN(X, Y, apply(T, S)) -> REN(X, Y, T)


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)))


Strategy:

innermost




As we are in the innermost case, we can delete all 22 non-usable-rules.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳Neg POLO
             ...
               →DP Problem 5
                 ↳Size-Change Principle


Dependency Pairs:

REN(X, Y, apply(T, S)) -> REN(X, Y, S)
REN(X, Y, apply(T, S)) -> REN(X, Y, T)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. REN(X, Y, apply(T, S)) -> REN(X, Y, S)
  2. REN(X, Y, apply(T, S)) -> REN(X, Y, T)
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
1=1
2=2
3>3

which lead(s) to this/these maximal multigraph(s):
{1, 2} , {1, 2}
1=1
2=2
3>3

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
apply(x1, x2) -> apply(x1, x2)

We obtain no new DP problems.

Termination of R successfully shown.
Duration:
0:03 minutes