Termination Proof using AProVE

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

Innermost Termination of R to be shown.

     ↳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.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

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

The following dependency pairs can be strictly oriented:

EQ(cons(T, L), cons(Tp, Lp)) -> EQ(L, Lp)
EQ(cons(T, L), cons(Tp, Lp)) -> EQ(T, Tp)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(apply(x₁, x₂)) = x₁ + x₂

POL(EQ(x₁, x₂)) = x₁ + x₂

POL(var(x₁)) = x₁

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

POL(lambda(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
cons(x₁, x₂) -> cons(x₁, x₂)
var(x₁) -> var(x₁)
lambda(x₁, x₂) -> lambda(x₁, x₂)
apply(x₁, x₂) -> apply(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

Dependency Pairs:

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 pair can be strictly oriented:

EQ(var(L), var(Lp)) -> EQ(L, Lp)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(apply(x₁, x₂)) = x₁ + x₂

POL(EQ(x₁, x₂)) = x₁ + x₂

POL(var(x₁)) = 1 + x₁

POL(lambda(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
var(x₁) -> var(x₁)
lambda(x₁, x₂) -> lambda(x₁, x₂)
apply(x₁, x₂) -> apply(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳AFS

...

               →DP Problem 4

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

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)

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:

EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(X, Xp)
EQ(lambda(X, T), lambda(Xp, Tp)) -> EQ(T, Tp)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(apply(x₁, x₂)) = x₁ + x₂

POL(EQ(x₁, x₂)) = x₁ + x₂

POL(lambda(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
lambda(x₁, x₂) -> lambda(x₁, x₂)
apply(x₁, x₂) -> apply(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳AFS

...

               →DP Problem 5

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

Dependency Pairs:

EQ(apply(T, S), apply(Tp, Sp)) -> EQ(S, Sp)
EQ(apply(T, S), apply(Tp, Sp)) -> 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

The following dependency pairs can be strictly oriented:

EQ(apply(T, S), apply(Tp, Sp)) -> EQ(S, Sp)
EQ(apply(T, S), apply(Tp, Sp)) -> EQ(T, Tp)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(apply(x₁, x₂)) = 1 + x₁ + x₂

POL(EQ(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
apply(x₁, x₂) -> apply(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳AFS

...

               →DP Problem 6

                 ↳Dependency Graph

       →DP Problem 2

         ↳AFS

Dependency Pair:

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

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

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:

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

The following usable rules for innermost can be oriented:

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)))
if(true, var(K), var(L)) -> var(K)
if(false, var(K), var(L)) -> var(L)
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))
and(false, false) -> false
and(true, false) -> false
and(false, true) -> false
and(true, true) -> true

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(REN(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(and(x₁, x₂)) = x₁ + x₂

POL(apply(x₁, x₂)) = 1 + x₁ + x₂

POL(if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(var) = 0

POL(eq) = 0

POL(false) = 0

POL(lambda(x₁, x₂)) = x₁ + x₂

POL(true) = 0

resulting in one new DP problem.
Used Argument Filtering System:

REN(x₁, x₂, x₃) -> REN(x₁, x₂, x₃)
apply(x₁, x₂) -> apply(x₁, x₂)
lambda(x₁, x₂) -> lambda(x₁, x₂)
var(x₁) -> var
ren(x₁, x₂, x₃) -> x₃
if(x₁, x₂, x₃) -> if(x₁, x₂, x₃)
eq(x₁, x₂) -> eq
and(x₁, x₂) -> and(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 7

             ↳Argument Filtering and Ordering

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

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:

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

The following usable rules for innermost can be oriented:

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)))
if(true, var(K), var(L)) -> var(K)
if(false, var(K), var(L)) -> var(L)
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))
and(false, false) -> false
and(true, false) -> false
and(false, true) -> false
and(true, true) -> true

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(REN(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

POL(and) = 0

POL(if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(var(x₁)) = x₁

POL(false) = 0

POL(lambda(x₁, x₂)) = 1 + x₁ + x₂

POL(nil) = 0

POL(true) = 0

POL(ren(x₁, x₂, x₃)) = x₁ + x₂ + x₃

resulting in one new DP problem.
Used Argument Filtering System:

REN(x₁, x₂, x₃) -> REN(x₁, x₂, x₃)
lambda(x₁, x₂) -> lambda(x₁, x₂)
var(x₁) -> var(x₁)
cons(x₁, x₂) -> x₂
ren(x₁, x₂, x₃) -> ren(x₁, x₂, x₃)
if(x₁, x₂, x₃) -> if(x₁, x₂, x₃)
eq(x₁, x₂) -> x₁
apply(x₁, x₂) -> x₁
and(x₁, x₂) -> and

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 7

             ↳AFS

...

               →DP Problem 8

                 ↳Dependency Graph

Dependency Pair:

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

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:05 minutes

POL(apply(x₁, x₂))	= x₁ + x₂
POL(EQ(x₁, x₂))	= x₁ + x₂
POL(var(x₁))	= x₁
POL(cons(x₁, x₂))	= 1 + x₁ + x₂
POL(lambda(x₁, x₂))	= x₁ + x₂

POL(REN(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(and(x₁, x₂))	= x₁ + x₂
POL(apply(x₁, x₂))	= 1 + x₁ + x₂
POL(if(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(var)	= 0
POL(eq)	= 0
POL(false)	= 0
POL(lambda(x₁, x₂))	= x₁ + x₂
POL(true)	= 0

POL(REN(x₁, x₂, x₃))	= 1 + x₁ + x₂ + x₃
POL(and)	= 0
POL(if(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(var(x₁))	= x₁
POL(false)	= 0
POL(lambda(x₁, x₂))	= 1 + x₁ + x₂
POL(nil)	= 0
POL(true)	= 0
POL(ren(x₁, x₂, x₃))	= x₁ + x₂ + x₃