MAYBE
MAYBE
TRS:
 {
       sent(up(x)) -> up(sent(x)),
      rec(sent(x)) -> sent(rec(x)),
       rec(rec(x)) -> sent(rec(x)),
        rec(no(x)) -> sent(rec(x)),
        rec(up(x)) -> up(rec(x)),
        rec(bot()) -> up(sent(bot())),
         no(up(x)) -> up(no(x)),
  top(sent(up(x))) -> top(check(rec(x))),
   top(rec(up(x))) -> top(check(rec(x))),
    top(no(up(x))) -> top(check(rec(x))),
    check(sent(x)) -> sent(check(x)),
     check(rec(x)) -> rec(check(x)),
      check(no(x)) -> no(x),
      check(no(x)) -> no(check(x)),
      check(up(x)) -> up(check(x))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
         sent(up(x)) -> up(sent(x)),
        rec(sent(x)) -> sent(rec(x)),
         rec(rec(x)) -> sent(rec(x)),
          rec(no(x)) -> sent(rec(x)),
          rec(up(x)) -> up(rec(x)),
          rec(bot()) -> up(sent(bot())),
           no(up(x)) -> up(no(x)),
    top(sent(up(x))) -> top(check(rec(x))),
     top(rec(up(x))) -> top(check(rec(x))),
      top(no(up(x))) -> top(check(rec(x))),
      check(sent(x)) -> sent(check(x)),
       check(rec(x)) -> rec(check(x)),
        check(no(x)) -> no(x),
        check(no(x)) -> no(check(x)),
        check(up(x)) -> up(check(x))
   }
  Fail