(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
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))
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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(cons(lift, s), cons(lift, t)) → CIRC(s, t)
CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
CIRC(circ(s, t), u) → CIRC(t, u)
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)
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
MSUBST(msubst(a, s), t) → CIRC(s, t)
The TRS R consists of the following rules:
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))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.