MAYBE
MAYBE
TRS:
 {
  top2(x, free(y)) -> top1(x, check(new(y))),
  top2(x, free(y)) -> top1(check(x), new(y)),
  top2(x, free(y)) -> top1(check(new(x)), y),
  top2(x, free(y)) -> top1(new(x), check(y)),
     check(new(x)) -> new(check(x)),
    check(free(x)) -> free(check(x)),
     check(old(x)) -> old(x),
     check(old(x)) -> old(check(x)),
      new(free(x)) -> free(new(x)),
      new(serve()) -> free(serve()),
  top1(free(x), y) -> top2(x, check(new(y))),
  top1(free(x), y) -> top2(check(x), new(y)),
  top1(free(x), y) -> top2(check(new(x)), y),
  top1(free(x), y) -> top2(new(x), check(y)),
      old(free(x)) -> free(old(x)),
      old(serve()) -> free(serve())
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
    top2(x, free(y)) -> top1(x, check(new(y))),
    top2(x, free(y)) -> top1(check(x), new(y)),
    top2(x, free(y)) -> top1(check(new(x)), y),
    top2(x, free(y)) -> top1(new(x), check(y)),
       check(new(x)) -> new(check(x)),
      check(free(x)) -> free(check(x)),
       check(old(x)) -> old(x),
       check(old(x)) -> old(check(x)),
        new(free(x)) -> free(new(x)),
        new(serve()) -> free(serve()),
    top1(free(x), y) -> top2(x, check(new(y))),
    top1(free(x), y) -> top2(check(x), new(y)),
    top1(free(x), y) -> top2(check(new(x)), y),
    top1(free(x), y) -> top2(new(x), check(y)),
        old(free(x)) -> free(old(x)),
        old(serve()) -> free(serve())
   }
  Fail