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))}
 DP:
  Strict:
   {     sent#(up(x)) -> sent#(x),
        rec#(sent(x)) -> sent#(rec(x)),
        rec#(sent(x)) -> rec#(x),
         rec#(rec(x)) -> sent#(rec(x)),
          rec#(no(x)) -> sent#(rec(x)),
          rec#(no(x)) -> rec#(x),
          rec#(up(x)) -> rec#(x),
          rec#(bot()) -> sent#(bot()),
           no#(up(x)) -> no#(x),
    top#(sent(up(x))) -> rec#(x),
    top#(sent(up(x))) -> top#(check(rec(x))),
    top#(sent(up(x))) -> check#(rec(x)),
     top#(rec(up(x))) -> rec#(x),
     top#(rec(up(x))) -> top#(check(rec(x))),
     top#(rec(up(x))) -> check#(rec(x)),
      top#(no(up(x))) -> rec#(x),
      top#(no(up(x))) -> top#(check(rec(x))),
      top#(no(up(x))) -> check#(rec(x)),
      check#(sent(x)) -> sent#(check(x)),
      check#(sent(x)) -> check#(x),
       check#(rec(x)) -> rec#(check(x)),
       check#(rec(x)) -> check#(x),
        check#(no(x)) -> no#(check(x)),
        check#(no(x)) -> check#(x),
        check#(up(x)) -> check#(x)}
  Weak:
  {     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))}
  EDG:
   {(rec#(sent(x)) -> rec#(x), rec#(bot()) -> sent#(bot()))
    (rec#(sent(x)) -> rec#(x), rec#(up(x)) -> rec#(x))
    (rec#(sent(x)) -> rec#(x), rec#(no(x)) -> rec#(x))
    (rec#(sent(x)) -> rec#(x), rec#(no(x)) -> sent#(rec(x)))
    (rec#(sent(x)) -> rec#(x), rec#(rec(x)) -> sent#(rec(x)))
    (rec#(sent(x)) -> rec#(x), rec#(sent(x)) -> rec#(x))
    (rec#(sent(x)) -> rec#(x), rec#(sent(x)) -> sent#(rec(x)))
    (rec#(up(x)) -> rec#(x), rec#(bot()) -> sent#(bot()))
    (rec#(up(x)) -> rec#(x), rec#(up(x)) -> rec#(x))
    (rec#(up(x)) -> rec#(x), rec#(no(x)) -> rec#(x))
    (rec#(up(x)) -> rec#(x), rec#(no(x)) -> sent#(rec(x)))
    (rec#(up(x)) -> rec#(x), rec#(rec(x)) -> sent#(rec(x)))
    (rec#(up(x)) -> rec#(x), rec#(sent(x)) -> rec#(x))
    (rec#(up(x)) -> rec#(x), rec#(sent(x)) -> sent#(rec(x)))
    (top#(sent(up(x))) -> rec#(x), rec#(bot()) -> sent#(bot()))
    (top#(sent(up(x))) -> rec#(x), rec#(up(x)) -> rec#(x))
    (top#(sent(up(x))) -> rec#(x), rec#(no(x)) -> rec#(x))
    (top#(sent(up(x))) -> rec#(x), rec#(no(x)) -> sent#(rec(x)))
    (top#(sent(up(x))) -> rec#(x), rec#(rec(x)) -> sent#(rec(x)))
    (top#(sent(up(x))) -> rec#(x), rec#(sent(x)) -> rec#(x))
    (top#(sent(up(x))) -> rec#(x), rec#(sent(x)) -> sent#(rec(x)))
    (top#(no(up(x))) -> rec#(x), rec#(bot()) -> sent#(bot()))
    (top#(no(up(x))) -> rec#(x), rec#(up(x)) -> rec#(x))
    (top#(no(up(x))) -> rec#(x), rec#(no(x)) -> rec#(x))
    (top#(no(up(x))) -> rec#(x), rec#(no(x)) -> sent#(rec(x)))
    (top#(no(up(x))) -> rec#(x), rec#(rec(x)) -> sent#(rec(x)))
    (top#(no(up(x))) -> rec#(x), rec#(sent(x)) -> rec#(x))
    (top#(no(up(x))) -> rec#(x), rec#(sent(x)) -> sent#(rec(x)))
    (check#(rec(x)) -> check#(x), check#(up(x)) -> check#(x))
    (check#(rec(x)) -> check#(x), check#(no(x)) -> check#(x))
    (check#(rec(x)) -> check#(x), check#(no(x)) -> no#(check(x)))
    (check#(rec(x)) -> check#(x), check#(rec(x)) -> check#(x))
    (check#(rec(x)) -> check#(x), check#(rec(x)) -> rec#(check(x)))
    (check#(rec(x)) -> check#(x), check#(sent(x)) -> check#(x))
    (check#(rec(x)) -> check#(x), check#(sent(x)) -> sent#(check(x)))
    (check#(up(x)) -> check#(x), check#(up(x)) -> check#(x))
    (check#(up(x)) -> check#(x), check#(no(x)) -> check#(x))
    (check#(up(x)) -> check#(x), check#(no(x)) -> no#(check(x)))
    (check#(up(x)) -> check#(x), check#(rec(x)) -> check#(x))
    (check#(up(x)) -> check#(x), check#(rec(x)) -> rec#(check(x)))
    (check#(up(x)) -> check#(x), check#(sent(x)) -> check#(x))
    (check#(up(x)) -> check#(x), check#(sent(x)) -> sent#(check(x)))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> check#(rec(x)))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> top#(check(rec(x))))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> rec#(x))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> check#(rec(x)))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> top#(check(rec(x))))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> rec#(x))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> check#(rec(x)))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> top#(check(rec(x))))
    (top#(sent(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> rec#(x))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> check#(rec(x)))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> top#(check(rec(x))))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> rec#(x))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> check#(rec(x)))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> top#(check(rec(x))))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> rec#(x))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> check#(rec(x)))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> top#(check(rec(x))))
    (top#(no(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> rec#(x))
    (rec#(rec(x)) -> sent#(rec(x)), sent#(up(x)) -> sent#(x))
    (top#(sent(up(x))) -> check#(rec(x)), check#(up(x)) -> check#(x))
    (top#(sent(up(x))) -> check#(rec(x)), check#(no(x)) -> check#(x))
    (top#(sent(up(x))) -> check#(rec(x)), check#(no(x)) -> no#(check(x)))
    (top#(sent(up(x))) -> check#(rec(x)), check#(rec(x)) -> check#(x))
    (top#(sent(up(x))) -> check#(rec(x)), check#(rec(x)) -> rec#(check(x)))
    (top#(sent(up(x))) -> check#(rec(x)), check#(sent(x)) -> check#(x))
    (top#(sent(up(x))) -> check#(rec(x)), check#(sent(x)) -> sent#(check(x)))
    (top#(no(up(x))) -> check#(rec(x)), check#(up(x)) -> check#(x))
    (top#(no(up(x))) -> check#(rec(x)), check#(no(x)) -> check#(x))
    (top#(no(up(x))) -> check#(rec(x)), check#(no(x)) -> no#(check(x)))
    (top#(no(up(x))) -> check#(rec(x)), check#(rec(x)) -> check#(x))
    (top#(no(up(x))) -> check#(rec(x)), check#(rec(x)) -> rec#(check(x)))
    (top#(no(up(x))) -> check#(rec(x)), check#(sent(x)) -> check#(x))
    (top#(no(up(x))) -> check#(rec(x)), check#(sent(x)) -> sent#(check(x)))
    (check#(rec(x)) -> rec#(check(x)), rec#(up(x)) -> rec#(x))
    (check#(rec(x)) -> rec#(check(x)), rec#(no(x)) -> rec#(x))
    (check#(rec(x)) -> rec#(check(x)), rec#(no(x)) -> sent#(rec(x)))
    (check#(rec(x)) -> rec#(check(x)), rec#(rec(x)) -> sent#(rec(x)))
    (check#(rec(x)) -> rec#(check(x)), rec#(sent(x)) -> rec#(x))
    (check#(rec(x)) -> rec#(check(x)), rec#(sent(x)) -> sent#(rec(x)))
    (check#(no(x)) -> no#(check(x)), no#(up(x)) -> no#(x))
    (check#(sent(x)) -> sent#(check(x)), sent#(up(x)) -> sent#(x))
    (top#(rec(up(x))) -> check#(rec(x)), check#(sent(x)) -> sent#(check(x)))
    (top#(rec(up(x))) -> check#(rec(x)), check#(sent(x)) -> check#(x))
    (top#(rec(up(x))) -> check#(rec(x)), check#(rec(x)) -> rec#(check(x)))
    (top#(rec(up(x))) -> check#(rec(x)), check#(rec(x)) -> check#(x))
    (top#(rec(up(x))) -> check#(rec(x)), check#(no(x)) -> no#(check(x)))
    (top#(rec(up(x))) -> check#(rec(x)), check#(no(x)) -> check#(x))
    (top#(rec(up(x))) -> check#(rec(x)), check#(up(x)) -> check#(x))
    (rec#(no(x)) -> sent#(rec(x)), sent#(up(x)) -> sent#(x))
    (rec#(sent(x)) -> sent#(rec(x)), sent#(up(x)) -> sent#(x))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> rec#(x))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> top#(check(rec(x))))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> check#(rec(x)))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> rec#(x))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> top#(check(rec(x))))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> check#(rec(x)))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> rec#(x))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> top#(check(rec(x))))
    (top#(rec(up(x))) -> top#(check(rec(x))), top#(no(up(x))) -> check#(rec(x)))
    (check#(no(x)) -> check#(x), check#(sent(x)) -> sent#(check(x)))
    (check#(no(x)) -> check#(x), check#(sent(x)) -> check#(x))
    (check#(no(x)) -> check#(x), check#(rec(x)) -> rec#(check(x)))
    (check#(no(x)) -> check#(x), check#(rec(x)) -> check#(x))
    (check#(no(x)) -> check#(x), check#(no(x)) -> no#(check(x)))
    (check#(no(x)) -> check#(x), check#(no(x)) -> check#(x))
    (check#(no(x)) -> check#(x), check#(up(x)) -> check#(x))
    (check#(sent(x)) -> check#(x), check#(sent(x)) -> sent#(check(x)))
    (check#(sent(x)) -> check#(x), check#(sent(x)) -> check#(x))
    (check#(sent(x)) -> check#(x), check#(rec(x)) -> rec#(check(x)))
    (check#(sent(x)) -> check#(x), check#(rec(x)) -> check#(x))
    (check#(sent(x)) -> check#(x), check#(no(x)) -> no#(check(x)))
    (check#(sent(x)) -> check#(x), check#(no(x)) -> check#(x))
    (check#(sent(x)) -> check#(x), check#(up(x)) -> check#(x))
    (top#(rec(up(x))) -> rec#(x), rec#(sent(x)) -> sent#(rec(x)))
    (top#(rec(up(x))) -> rec#(x), rec#(sent(x)) -> rec#(x))
    (top#(rec(up(x))) -> rec#(x), rec#(rec(x)) -> sent#(rec(x)))
    (top#(rec(up(x))) -> rec#(x), rec#(no(x)) -> sent#(rec(x)))
    (top#(rec(up(x))) -> rec#(x), rec#(no(x)) -> rec#(x))
    (top#(rec(up(x))) -> rec#(x), rec#(up(x)) -> rec#(x))
    (top#(rec(up(x))) -> rec#(x), rec#(bot()) -> sent#(bot()))
    (no#(up(x)) -> no#(x), no#(up(x)) -> no#(x))
    (rec#(no(x)) -> rec#(x), rec#(sent(x)) -> sent#(rec(x)))
    (rec#(no(x)) -> rec#(x), rec#(sent(x)) -> rec#(x))
    (rec#(no(x)) -> rec#(x), rec#(rec(x)) -> sent#(rec(x)))
    (rec#(no(x)) -> rec#(x), rec#(no(x)) -> sent#(rec(x)))
    (rec#(no(x)) -> rec#(x), rec#(no(x)) -> rec#(x))
    (rec#(no(x)) -> rec#(x), rec#(up(x)) -> rec#(x))
    (rec#(no(x)) -> rec#(x), rec#(bot()) -> sent#(bot()))
    (sent#(up(x)) -> sent#(x), sent#(up(x)) -> sent#(x))}
   SCCS:
    Scc:
     {check#(sent(x)) -> check#(x),
       check#(rec(x)) -> check#(x),
        check#(no(x)) -> check#(x),
        check#(up(x)) -> check#(x)}
    Scc:
     {top#(sent(up(x))) -> top#(check(rec(x))),
       top#(rec(up(x))) -> top#(check(rec(x))),
        top#(no(up(x))) -> top#(check(rec(x)))}
    Scc:
     {no#(up(x)) -> no#(x)}
    Scc:
     {rec#(sent(x)) -> rec#(x),
        rec#(no(x)) -> rec#(x),
        rec#(up(x)) -> rec#(x)}
    Scc:
     {sent#(up(x)) -> sent#(x)}
    SCC:
     Strict:
      {check#(sent(x)) -> check#(x),
        check#(rec(x)) -> check#(x),
         check#(no(x)) -> check#(x),
         check#(up(x)) -> check#(x)}
     Weak:
     {     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))}
     SPSC:
      Simple Projection:
       pi(check#) = 0
      Strict:
       {check#(sent(x)) -> check#(x),
         check#(rec(x)) -> check#(x),
          check#(up(x)) -> check#(x)}
      EDG:
       {(check#(rec(x)) -> check#(x), check#(up(x)) -> check#(x))
        (check#(rec(x)) -> check#(x), check#(rec(x)) -> check#(x))
        (check#(rec(x)) -> check#(x), check#(sent(x)) -> check#(x))
        (check#(up(x)) -> check#(x), check#(sent(x)) -> check#(x))
        (check#(up(x)) -> check#(x), check#(rec(x)) -> check#(x))
        (check#(up(x)) -> check#(x), check#(up(x)) -> check#(x))
        (check#(sent(x)) -> check#(x), check#(sent(x)) -> check#(x))
        (check#(sent(x)) -> check#(x), check#(rec(x)) -> check#(x))
        (check#(sent(x)) -> check#(x), check#(up(x)) -> check#(x))}
       SCCS:
        Scc:
         {check#(sent(x)) -> check#(x),
           check#(rec(x)) -> check#(x),
            check#(up(x)) -> check#(x)}
        SCC:
         Strict:
          {check#(sent(x)) -> check#(x),
            check#(rec(x)) -> check#(x),
             check#(up(x)) -> check#(x)}
         Weak:
         {     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))}
         SPSC:
          Simple Projection:
           pi(check#) = 0
          Strict:
           {check#(sent(x)) -> check#(x),
              check#(up(x)) -> check#(x)}
          EDG:
           {(check#(up(x)) -> check#(x), check#(up(x)) -> check#(x))
            (check#(up(x)) -> check#(x), check#(sent(x)) -> check#(x))
            (check#(sent(x)) -> check#(x), check#(sent(x)) -> check#(x))
            (check#(sent(x)) -> check#(x), check#(up(x)) -> check#(x))}
           SCCS:
            Scc:
             {check#(sent(x)) -> check#(x),
                check#(up(x)) -> check#(x)}
            SCC:
             Strict:
              {check#(sent(x)) -> check#(x),
                 check#(up(x)) -> check#(x)}
             Weak:
             {     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))}
             SPSC:
              Simple Projection:
               pi(check#) = 0
              Strict:
               {check#(up(x)) -> check#(x)}
              EDG:
               {(check#(up(x)) -> check#(x), check#(up(x)) -> check#(x))}
               SCCS:
                Scc:
                 {check#(up(x)) -> check#(x)}
                SCC:
                 Strict:
                  {check#(up(x)) -> check#(x)}
                 Weak:
                 {     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))}
                 SPSC:
                  Simple Projection:
                   pi(check#) = 0
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {top#(sent(up(x))) -> top#(check(rec(x))),
        top#(rec(up(x))) -> top#(check(rec(x))),
         top#(no(up(x))) -> top#(check(rec(x)))}
     Weak:
     {     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))}
     POLY:
      Argument Filtering:
       pi(check) = 0, pi(top#) = 0, pi(top) = [], pi(bot) = [], pi(up) = [], pi(no) = [], pi(rec) = [], pi(sent) = []
      Usable Rules:
       {}
      Interpretation:
       [no] = 1,
       [rec] = 0,
       [sent] = 0
      Strict:
       {top#(sent(up(x))) -> top#(check(rec(x))),
         top#(rec(up(x))) -> top#(check(rec(x)))}
      Weak:
       {     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))}
      EDG:
       {(top#(rec(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> top#(check(rec(x))))
        (top#(rec(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> top#(check(rec(x))))
        (top#(sent(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> top#(check(rec(x))))
        (top#(sent(up(x))) -> top#(check(rec(x))), top#(rec(up(x))) -> top#(check(rec(x))))}
       SCCS:
        Scc:
         {top#(sent(up(x))) -> top#(check(rec(x))),
           top#(rec(up(x))) -> top#(check(rec(x)))}
        SCC:
         Strict:
          {top#(sent(up(x))) -> top#(check(rec(x))),
            top#(rec(up(x))) -> top#(check(rec(x)))}
         Weak:
         {     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))}
         POLY:
          Argument Filtering:
           pi(check) = 0, pi(top#) = 0, pi(top) = [], pi(bot) = [], pi(up) = [0], pi(no) = 0, pi(rec) = [0], pi(sent) = 0
          Usable Rules:
           {}
          Interpretation:
           [up](x0) = x0 + 1,
           [rec](x0) = x0 + 1
          Strict:
           {top#(sent(up(x))) -> top#(check(rec(x)))}
          Weak:
           {     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))}
          EDG:
           {(top#(sent(up(x))) -> top#(check(rec(x))), top#(sent(up(x))) -> top#(check(rec(x))))}
           SCCS:
            Scc:
             {top#(sent(up(x))) -> top#(check(rec(x)))}
            SCC:
             Strict:
              {top#(sent(up(x))) -> top#(check(rec(x)))}
             Weak:
             {     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
    SCC:
     Strict:
      {no#(up(x)) -> no#(x)}
     Weak:
     {     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))}
     SPSC:
      Simple Projection:
       pi(no#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {rec#(sent(x)) -> rec#(x),
         rec#(no(x)) -> rec#(x),
         rec#(up(x)) -> rec#(x)}
     Weak:
     {     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))}
     SPSC:
      Simple Projection:
       pi(rec#) = 0
      Strict:
       {rec#(sent(x)) -> rec#(x),
          rec#(up(x)) -> rec#(x)}
      EDG:
       {(rec#(up(x)) -> rec#(x), rec#(up(x)) -> rec#(x))
        (rec#(up(x)) -> rec#(x), rec#(sent(x)) -> rec#(x))
        (rec#(sent(x)) -> rec#(x), rec#(sent(x)) -> rec#(x))
        (rec#(sent(x)) -> rec#(x), rec#(up(x)) -> rec#(x))}
       SCCS:
        Scc:
         {rec#(sent(x)) -> rec#(x),
            rec#(up(x)) -> rec#(x)}
        SCC:
         Strict:
          {rec#(sent(x)) -> rec#(x),
             rec#(up(x)) -> rec#(x)}
         Weak:
         {     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))}
         SPSC:
          Simple Projection:
           pi(rec#) = 0
          Strict:
           {rec#(up(x)) -> rec#(x)}
          EDG:
           {(rec#(up(x)) -> rec#(x), rec#(up(x)) -> rec#(x))}
           SCCS:
            Scc:
             {rec#(up(x)) -> rec#(x)}
            SCC:
             Strict:
              {rec#(up(x)) -> rec#(x)}
             Weak:
             {     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))}
             SPSC:
              Simple Projection:
               pi(rec#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {sent#(up(x)) -> sent#(x)}
     Weak:
     {     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))}
     SPSC:
      Simple Projection:
       pi(sent#) = 0
      Strict:
       {}
      Qed