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

         ↳Polynomial Ordering

       →DP Problem 2

         ↳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

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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(var(x₁)) = x₁

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 3

             ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

Dependency Pairs:

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(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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(var(x₁)) = x₁

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 3

             ↳Polo

...

               →DP Problem 4

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

Dependency Pairs:

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

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

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 3

             ↳Polo

...

               →DP Problem 5

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

Dependency Pairs:

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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 3

             ↳Polo

...

               →DP Problem 6

                 ↳Dependency Graph

       →DP Problem 2

         ↳Polo

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

         ↳Polo

       →DP Problem 2

         ↳Polynomial 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, 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))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS 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)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

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

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

POL(var(x₁)) = 0

POL(eq(x₁, x₂)) = 0

POL(cons(x₁, x₂)) = 0

POL(false) = 0

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

POL(nil) = 0

POL(true) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 7

             ↳Polynomial Ordering

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

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)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 7

             ↳Polo

...

               →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:04 minutes

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

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