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())}
 DP:
  Strict:
   {top2#(x, free(y)) -> check#(x),
    top2#(x, free(y)) -> check#(y),
    top2#(x, free(y)) -> check#(new(x)),
    top2#(x, free(y)) -> check#(new(y)),
    top2#(x, free(y)) -> new#(x),
    top2#(x, free(y)) -> new#(y),
    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)) -> check#(x),
       check#(new(x)) -> new#(check(x)),
      check#(free(x)) -> check#(x),
       check#(old(x)) -> check#(x),
       check#(old(x)) -> old#(check(x)),
        new#(free(x)) -> new#(x),
    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)),
    top1#(free(x), y) -> check#(x),
    top1#(free(x), y) -> check#(y),
    top1#(free(x), y) -> check#(new(x)),
    top1#(free(x), y) -> check#(new(y)),
    top1#(free(x), y) -> new#(x),
    top1#(free(x), y) -> new#(y),
        old#(free(x)) -> old#(x)}
  Weak:
  {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())}
  EDG:
   {
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> top1#(new(x), check(y)))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> top1#(check(new(x)), y))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> top1#(check(x), new(y)))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> top1#(x, check(new(y))))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> new#(y))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> new#(x))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> check#(new(y)))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> check#(new(x)))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> check#(y))
    (top1#(free(x), y) -> top2#(x, check(new(y))), top2#(x, free(y)) -> check#(x))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> new#(y))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> new#(x))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> check#(new(y)))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> check#(new(x)))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> check#(y))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> check#(x))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> top2#(new(x), check(y)))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> top2#(check(new(x)), y))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> top2#(check(x), new(y)))
    (top2#(x, free(y)) -> top1#(new(x), check(y)), top1#(free(x), y) -> top2#(x, check(new(y))))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> top1#(new(x), check(y)))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> top1#(check(new(x)), y))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> top1#(check(x), new(y)))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> top1#(x, check(new(y))))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> new#(y))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> new#(x))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> check#(new(y)))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> check#(new(x)))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> check#(y))
    (top1#(free(x), y) -> top2#(new(x), check(y)), top2#(x, free(y)) -> check#(x))
    (top2#(x, free(y)) -> new#(y), new#(free(x)) -> new#(x))
    (top1#(free(x), y) -> new#(y), new#(free(x)) -> new#(x))
    (top1#(free(x), y) -> check#(new(y)), check#(old(x)) -> old#(check(x)))
    (top1#(free(x), y) -> check#(new(y)), check#(old(x)) -> check#(x))
    (top1#(free(x), y) -> check#(new(y)), check#(free(x)) -> check#(x))
    (top1#(free(x), y) -> check#(new(y)), check#(new(x)) -> new#(check(x)))
    (top1#(free(x), y) -> check#(new(y)), check#(new(x)) -> check#(x))
    (check#(new(x)) -> new#(check(x)), new#(free(x)) -> new#(x))
    (top1#(free(x), y) -> check#(new(x)), check#(old(x)) -> old#(check(x)))
    (top1#(free(x), y) -> check#(new(x)), check#(old(x)) -> check#(x))
    (top1#(free(x), y) -> check#(new(x)), check#(free(x)) -> check#(x))
    (top1#(free(x), y) -> check#(new(x)), check#(new(x)) -> new#(check(x)))
    (top1#(free(x), y) -> check#(new(x)), check#(new(x)) -> check#(x))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> top1#(new(x), check(y)))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> top1#(check(new(x)), y))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> top1#(check(x), new(y)))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> top1#(x, check(new(y))))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> new#(y))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> new#(x))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> check#(new(y)))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> check#(new(x)))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> check#(y))
    (top1#(free(x), y) -> top2#(check(new(x)), y), top2#(x, free(y)) -> check#(x))
    (top2#(x, free(y)) -> new#(x), new#(free(x)) -> new#(x))
    (check#(free(x)) -> check#(x), check#(old(x)) -> old#(check(x)))
    (check#(free(x)) -> check#(x), check#(old(x)) -> check#(x))
    (check#(free(x)) -> check#(x), check#(free(x)) -> check#(x))
    (check#(free(x)) -> check#(x), check#(new(x)) -> new#(check(x)))
    (check#(free(x)) -> check#(x), check#(new(x)) -> check#(x))
    (new#(free(x)) -> new#(x), new#(free(x)) -> new#(x))
    (top1#(free(x), y) -> new#(x), new#(free(x)) -> new#(x))
    (old#(free(x)) -> old#(x), old#(free(x)) -> old#(x))
    (top1#(free(x), y) -> check#(x), check#(new(x)) -> check#(x))
    (top1#(free(x), y) -> check#(x), check#(new(x)) -> new#(check(x)))
    (top1#(free(x), y) -> check#(x), check#(free(x)) -> check#(x))
    (top1#(free(x), y) -> check#(x), check#(old(x)) -> check#(x))
    (top1#(free(x), y) -> check#(x), check#(old(x)) -> old#(check(x)))
    (check#(old(x)) -> check#(x), check#(new(x)) -> check#(x))
    (check#(old(x)) -> check#(x), check#(new(x)) -> new#(check(x)))
    (check#(old(x)) -> check#(x), check#(free(x)) -> check#(x))
    (check#(old(x)) -> check#(x), check#(old(x)) -> check#(x))
    (check#(old(x)) -> check#(x), check#(old(x)) -> old#(check(x)))
    (check#(new(x)) -> check#(x), check#(new(x)) -> check#(x))
    (check#(new(x)) -> check#(x), check#(new(x)) -> new#(check(x)))
    (check#(new(x)) -> check#(x), check#(free(x)) -> check#(x))
    (check#(new(x)) -> check#(x), check#(old(x)) -> check#(x))
    (check#(new(x)) -> check#(x), check#(old(x)) -> old#(check(x)))
    (top2#(x, free(y)) -> check#(x), check#(new(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(x), check#(new(x)) -> new#(check(x)))
    (top2#(x, free(y)) -> check#(x), check#(free(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(x), check#(old(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(x), check#(old(x)) -> old#(check(x)))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> top2#(x, check(new(y))))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> top2#(check(x), new(y)))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> top2#(check(new(x)), y))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> top2#(new(x), check(y)))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> check#(x))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> check#(y))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> check#(new(x)))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> check#(new(y)))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> new#(x))
    (top2#(x, free(y)) -> top1#(check(new(x)), y), top1#(free(x), y) -> new#(y))
    (check#(old(x)) -> old#(check(x)), old#(free(x)) -> old#(x))
    (top2#(x, free(y)) -> check#(new(x)), check#(new(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(new(x)), check#(new(x)) -> new#(check(x)))
    (top2#(x, free(y)) -> check#(new(x)), check#(free(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(new(x)), check#(old(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(new(x)), check#(old(x)) -> old#(check(x)))
    (top2#(x, free(y)) -> check#(new(y)), check#(new(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(new(y)), check#(new(x)) -> new#(check(x)))
    (top2#(x, free(y)) -> check#(new(y)), check#(free(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(new(y)), check#(old(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(new(y)), check#(old(x)) -> old#(check(x)))
    (top1#(free(x), y) -> check#(y), check#(new(x)) -> check#(x))
    (top1#(free(x), y) -> check#(y), check#(new(x)) -> new#(check(x)))
    (top1#(free(x), y) -> check#(y), check#(free(x)) -> check#(x))
    (top1#(free(x), y) -> check#(y), check#(old(x)) -> check#(x))
    (top1#(free(x), y) -> check#(y), check#(old(x)) -> old#(check(x)))
    (top2#(x, free(y)) -> check#(y), check#(new(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(y), check#(new(x)) -> new#(check(x)))
    (top2#(x, free(y)) -> check#(y), check#(free(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(y), check#(old(x)) -> check#(x))
    (top2#(x, free(y)) -> check#(y), check#(old(x)) -> old#(check(x)))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> check#(x))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> check#(y))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> check#(new(x)))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> check#(new(y)))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> new#(x))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> new#(y))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> top1#(x, check(new(y))))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> top1#(check(x), new(y)))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> top1#(check(new(x)), y))
    (top1#(free(x), y) -> top2#(check(x), new(y)), top2#(x, free(y)) -> top1#(new(x), check(y)))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> top2#(x, check(new(y))))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> top2#(check(x), new(y)))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> top2#(check(new(x)), y))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> top2#(new(x), check(y)))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> check#(x))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> check#(y))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> check#(new(x)))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> check#(new(y)))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> new#(x))
    (top2#(x, free(y)) -> top1#(check(x), new(y)), top1#(free(x), y) -> new#(y))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> top2#(x, check(new(y))))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> top2#(check(x), new(y)))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> top2#(check(new(x)), y))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> top2#(new(x), check(y)))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> check#(x))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> check#(y))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> check#(new(x)))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> check#(new(y)))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> new#(x))
    (top2#(x, free(y)) -> top1#(x, check(new(y))), top1#(free(x), y) -> new#(y))
   }
   SCCS:
    Scc:
     {old#(free(x)) -> old#(x)}
    Scc:
     {new#(free(x)) -> new#(x)}
    Scc:
     { check#(new(x)) -> check#(x),
      check#(free(x)) -> check#(x),
       check#(old(x)) -> check#(x)}
    Scc:
     {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)),
      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))}
    SCC:
     Strict:
      {old#(free(x)) -> old#(x)}
     Weak:
     {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())}
     SPSC:
      Simple Projection:
       pi(old#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {new#(free(x)) -> new#(x)}
     Weak:
     {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())}
     SPSC:
      Simple Projection:
       pi(new#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      { check#(new(x)) -> check#(x),
       check#(free(x)) -> check#(x),
        check#(old(x)) -> check#(x)}
     Weak:
     {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())}
     SPSC:
      Simple Projection:
       pi(check#) = 0
      Strict:
       {check#(new(x)) -> check#(x),
        check#(old(x)) -> check#(x)}
      EDG:
       {(check#(old(x)) -> check#(x), check#(old(x)) -> check#(x))
        (check#(old(x)) -> check#(x), check#(new(x)) -> check#(x))
        (check#(new(x)) -> check#(x), check#(new(x)) -> check#(x))
        (check#(new(x)) -> check#(x), check#(old(x)) -> check#(x))}
       SCCS:
        Scc:
         {check#(new(x)) -> check#(x),
          check#(old(x)) -> check#(x)}
        SCC:
         Strict:
          {check#(new(x)) -> check#(x),
           check#(old(x)) -> check#(x)}
         Weak:
         {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())}
         SPSC:
          Simple Projection:
           pi(check#) = 0
          Strict:
           {check#(old(x)) -> check#(x)}
          EDG:
           {(check#(old(x)) -> check#(x), check#(old(x)) -> check#(x))}
           SCCS:
            Scc:
             {check#(old(x)) -> check#(x)}
            SCC:
             Strict:
              {check#(old(x)) -> check#(x)}
             Weak:
             {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())}
             SPSC:
              Simple Projection:
               pi(check#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {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)),
       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))}
     Weak:
     {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