Term Rewriting System R:

   [a, s, t, u]
   circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t))
   circ(cons(lift, s), cons(a, t)) -> cons(a, circ(s, t))
   circ(cons(lift, s), cons(lift, t)) -> cons(lift, circ(s, t))
   circ(circ(s, t), u) -> circ(s, circ(t, u))
   circ(s, id) -> s
   circ(id, s) -> s
   circ(cons(lift, s), circ(cons(lift, t), u)) -> circ(cons(lift, circ(s, t)), u)
   subst(a, id) -> a
   msubst(a, id) -> a
   msubst(msubst(a, s), t) -> msubst(a, circ(s, t))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   CIRC(cons(lift, s), circ(cons(lift, t), u)) -> CIRC(cons(lift, circ(s, t)), u)
   CIRC(cons(lift, s), circ(cons(lift, t), u)) -> CIRC(s, t)
   CIRC(cons(lift, s), cons(lift, t)) -> CIRC(s, t)
   CIRC(cons(a, s), t) -> MSUBST(a, t)
   CIRC(cons(a, s), t) -> CIRC(s, t)
   CIRC(cons(lift, s), cons(a, t)) -> CIRC(s, t)
   CIRC(circ(s, t), u) -> CIRC(s, circ(t, u))
   CIRC(circ(s, t), u) -> CIRC(t, u)
   MSUBST(msubst(a, s), t) -> MSUBST(a, circ(s, t))
   MSUBST(msubst(a, s), t) -> CIRC(s, t)

Furthermore, R contains one SCC.


SCC1:

CIRC(circ(s, t), u) -> CIRC(t, u)
CIRC(circ(s, t), u) -> CIRC(s, circ(t, u))
CIRC(cons(lift, s), cons(a, t)) -> CIRC(s, t)
CIRC(cons(a, s), t) -> CIRC(s, t)
MSUBST(msubst(a, s), t) -> CIRC(s, t)
MSUBST(msubst(a, s), t) -> MSUBST(a, circ(s, t))
CIRC(cons(a, s), t) -> MSUBST(a, t)
CIRC(cons(lift, s), cons(lift, t)) -> CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) -> CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) -> CIRC(cons(lift, circ(s, t)), u)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   circ(cons(lift, s), circ(cons(lift, t), u)) -> circ(cons(lift, circ(s, t)), u)
   circ(id, s) -> s
   circ(cons(lift, s), cons(lift, t)) -> cons(lift, circ(s, t))
   circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t))
   circ(s, id) -> s
   circ(cons(lift, s), cons(a, t)) -> cons(a, circ(s, t))
   circ(circ(s, t), u) -> circ(s, circ(t, u))
   msubst(msubst(a, s), t) -> msubst(a, circ(s, t))
   msubst(a, id) -> a


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(circ(x_1, x_2)) = x_1 + x_1*x_2 + x_2
POL(id) = 0
POL(CIRC(x_1, x_2)) = x_1 + x_1*x_2
POL(lift) = 0
POL(MSUBST(x_1, x_2)) = x_1 + x_1*x_2
POL(msubst(x_1, x_2)) = x_1 + x_1*x_2 + x_2
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

 resulting in two subcycles.


SCC1.Polo1:

CIRC(circ(s, t), u) -> CIRC(s, circ(t, u))
CIRC(circ(s, t), u) -> CIRC(t, u)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(circ(x_1, x_2)) = 1 + x_1 + x_2
POL(id) = 0
POL(CIRC(x_1, x_2)) = x_1
POL(lift) = 0
POL(msubst(x_1, x_2)) = 0
POL(cons(x_1, x_2)) = 0

 resulting in no subcycles.


SCC1.Polo2:

MSUBST(msubst(a, s), t) -> MSUBST(a, circ(s, t))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(circ(x_1, x_2)) = 0
POL(id) = 0
POL(lift) = 0
POL(MSUBST(x_1, x_2)) = x_1
POL(msubst(x_1, x_2)) = 1 + x_1
POL(cons(x_1, x_2)) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 15.995 seconds.