Term Rewriting System R:

   [y, t, l, t', l', s, x, s', x', k, z]
   and(true, y) -> y
   and(false, y) -> false
   eq(nil, nil) -> true
   eq(cons(t, l), nil) -> false
   eq(nil, cons(t, l)) -> false
   eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
   eq(var(l), var(l')) -> eq(l, l')
   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(t', s')) -> and(eq(t, t'), eq(s, s'))
   eq(apply(t, s), lambda(x, t)) -> false
   eq(lambda(x, t), var(l)) -> false
   eq(lambda(x, t), apply(t, s)) -> false
   eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
   if(true, var(k), var(l')) -> var(k)
   if(false, var(k), var(l')) -> var(l')
   ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))
   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 contains the following Dependency Pairs: 


   EQ(var(l), var(l')) -> EQ(l, l')
   EQ(apply(t, s), apply(t', s')) -> AND(eq(t, t'), eq(s, s'))
   EQ(apply(t, s), apply(t', s')) -> EQ(t, t')
   EQ(apply(t, s), apply(t', s')) -> EQ(s, s')
   EQ(lambda(x, t), lambda(x', t')) -> AND(eq(x, x'), eq(t, t'))
   EQ(lambda(x, t), lambda(x', t')) -> EQ(x, x')
   EQ(lambda(x, t), lambda(x', t')) -> EQ(t, t')
   EQ(cons(t, l), cons(t', l')) -> AND(eq(t, t'), eq(l, l'))
   EQ(cons(t, l), cons(t', l')) -> EQ(t, t')
   EQ(cons(t, l), cons(t', l')) -> EQ(l, l')
   REN(x, y, apply(t, s)) -> REN(x, y, t)
   REN(x, y, apply(t, s)) -> REN(x, y, s)
   REN(var(l), var(k), var(l')) -> IF(eq(l, l'), var(k), var(l'))
   REN(var(l), var(k), var(l')) -> EQ(l, l')
   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.


SCC1:

EQ(cons(t, l), cons(t', l')) -> EQ(l, l')
EQ(cons(t, l), cons(t', l')) -> EQ(t, t')
EQ(lambda(x, t), lambda(x', t')) -> EQ(t, t')
EQ(lambda(x, t), lambda(x', t')) -> EQ(x, x')
EQ(apply(t, s), apply(t', s')) -> EQ(s, s')
EQ(apply(t, s), apply(t', s')) -> EQ(t, t')
EQ(var(l), var(l')) -> EQ(l, l')

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(t', l')) -> EQ(l, l')
   EQ(cons(t, l), cons(t', l')) -> EQ(t, t')
   EQ(lambda(x, t), lambda(x', t')) -> EQ(t, t')
   EQ(lambda(x, t), lambda(x', t')) -> EQ(x, x')
   EQ(apply(t, s), apply(t', s')) -> EQ(s, s')
   EQ(apply(t, s), apply(t', s')) -> EQ(t, t')
   EQ(var(l), var(l')) -> EQ(l, l')



 This transformation is resulting in no new subcycles.


SCC2:

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)

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(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
   ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))
   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(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(apply(x_1, x_2)) = 1 + x_1 + x_2
POL(eq(x_1, x_2)) = 0
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.




Innermost Termination of R successfully shown.


Duration: 2.534 seconds.