MAYBE
MAYBE
TRS:
 {
                                  msubst(a, id()) -> a,
                          msubst(msubst(a, s), t) -> msubst(a, circ(s, t)),
                                    circ(s, id()) -> s,
                              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(cons(lift(), s), circ(cons(lift(), t), u)) ->
  circ(cons(lift(), circ(s, t)), u),
                              circ(circ(s, t), u) -> circ(s, circ(t, u)),
                                    circ(id(), s) -> s,
                                   subst(a, id()) -> a
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                                    msubst(a, id()) -> a,
                            msubst(msubst(a, s), t) -> msubst(a, circ(s, t)),
                                      circ(s, id()) -> s,
                                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(cons(lift(), s), circ(cons(lift(), t), u)) ->
    circ(cons(lift(), circ(s, t)), u),
                                circ(circ(s, t), u) -> circ(s, circ(t, u)),
                                      circ(id(), s) -> s,
                                     subst(a, id()) -> a
   }
  Fail