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.



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


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
trivial

resulting in one new DP problem.
Used Argument Filtering System:
EQ(x1, x2) -> EQ(x1, x2)
cons(x1, x2) -> cons(x1, x2)
var(x1) -> var(x1)
lambda(x1, x2) -> lambda(x1, x2)
apply(x1, x2) -> apply(x1, x2)


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 3
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.


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


The following usable rules for innermost w.r.t. to the 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)
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: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
nil > {var, eq, true, false}
and > {var, eq, true, false}
cons > {var, eq, true, false}
lambda > REN > {var, eq, true, false}
ren > {var, eq, true, false}
if > {var, eq, true, false}
apply > {var, eq, true, false}

resulting in one new DP problem.
Used Argument Filtering System:
REN(x1, x2, x3) -> REN(x1, x2, x3)
apply(x1, x2) -> apply(x1, x2)
lambda(x1, x2) -> lambda(x1, x2)
var(x1) -> var
ren(x1, x2, x3) -> x3
if(x1, x2, x3) -> x1
eq(x1, x2) -> eq
and(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
           →DP Problem 4
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:17 minutes