YES
TRS:
 {     active(f(x)) -> mark(x),
       active(f(x)) -> f(active(x)),
         f(mark(x)) -> mark(f(x)),
           f(ok(x)) -> ok(f(x)),
        f(found(x)) -> found(f(x)),
       top(mark(x)) -> top(check(x)),
   top(active(c())) -> top(mark(c())),
      top(found(x)) -> top(active(x)),
           check(x) -> start(match(f(X()), x)),
        check(f(x)) -> f(check(x)),
       start(ok(x)) -> found(x),
  match(f(x), f(y)) -> f(match(x, y)),
      match(X(), x) -> proper(x),
       proper(f(x)) -> f(proper(x)),
        proper(c()) -> ok(c())}
 DP:
  Strict:
   {     active#(f(x)) -> active#(x),
         active#(f(x)) -> f#(active(x)),
           f#(mark(x)) -> f#(x),
             f#(ok(x)) -> f#(x),
          f#(found(x)) -> f#(x),
         top#(mark(x)) -> top#(check(x)),
         top#(mark(x)) -> check#(x),
     top#(active(c())) -> top#(mark(c())),
        top#(found(x)) -> active#(x),
        top#(found(x)) -> top#(active(x)),
             check#(x) -> f#(X()),
             check#(x) -> start#(match(f(X()), x)),
             check#(x) -> match#(f(X()), x),
          check#(f(x)) -> f#(check(x)),
          check#(f(x)) -> check#(x),
    match#(f(x), f(y)) -> f#(match(x, y)),
    match#(f(x), f(y)) -> match#(x, y),
        match#(X(), x) -> proper#(x),
         proper#(f(x)) -> f#(proper(x)),
         proper#(f(x)) -> proper#(x)}
  Weak:
  {     active(f(x)) -> mark(x),
        active(f(x)) -> f(active(x)),
          f(mark(x)) -> mark(f(x)),
            f(ok(x)) -> ok(f(x)),
         f(found(x)) -> found(f(x)),
        top(mark(x)) -> top(check(x)),
    top(active(c())) -> top(mark(c())),
       top(found(x)) -> top(active(x)),
            check(x) -> start(match(f(X()), x)),
         check(f(x)) -> f(check(x)),
        start(ok(x)) -> found(x),
   match(f(x), f(y)) -> f(match(x, y)),
       match(X(), x) -> proper(x),
        proper(f(x)) -> f(proper(x)),
         proper(c()) -> ok(c())}
  EDG:
   {(top#(mark(x)) -> top#(check(x)), top#(found(x)) -> top#(active(x)))
    (top#(mark(x)) -> top#(check(x)), top#(found(x)) -> active#(x))
    (top#(mark(x)) -> top#(check(x)), top#(mark(x)) -> check#(x))
    (top#(mark(x)) -> top#(check(x)), top#(mark(x)) -> top#(check(x)))
    (check#(f(x)) -> f#(check(x)), f#(found(x)) -> f#(x))
    (check#(f(x)) -> f#(check(x)), f#(ok(x)) -> f#(x))
    (check#(f(x)) -> f#(check(x)), f#(mark(x)) -> f#(x))
    (top#(active(c())) -> top#(mark(c())), top#(mark(x)) -> check#(x))
    (top#(active(c())) -> top#(mark(c())), top#(mark(x)) -> top#(check(x)))
    (active#(f(x)) -> active#(x), active#(f(x)) -> f#(active(x)))
    (active#(f(x)) -> active#(x), active#(f(x)) -> active#(x))
    (f#(ok(x)) -> f#(x), f#(found(x)) -> f#(x))
    (f#(ok(x)) -> f#(x), f#(ok(x)) -> f#(x))
    (f#(ok(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (top#(mark(x)) -> check#(x), check#(f(x)) -> check#(x))
    (top#(mark(x)) -> check#(x), check#(f(x)) -> f#(check(x)))
    (top#(mark(x)) -> check#(x), check#(x) -> match#(f(X()), x))
    (top#(mark(x)) -> check#(x), check#(x) -> start#(match(f(X()), x)))
    (top#(mark(x)) -> check#(x), check#(x) -> f#(X()))
    (check#(f(x)) -> check#(x), check#(f(x)) -> check#(x))
    (check#(f(x)) -> check#(x), check#(f(x)) -> f#(check(x)))
    (check#(f(x)) -> check#(x), check#(x) -> match#(f(X()), x))
    (check#(f(x)) -> check#(x), check#(x) -> start#(match(f(X()), x)))
    (check#(f(x)) -> check#(x), check#(x) -> f#(X()))
    (proper#(f(x)) -> proper#(x), proper#(f(x)) -> proper#(x))
    (proper#(f(x)) -> proper#(x), proper#(f(x)) -> f#(proper(x)))
    (match#(f(x), f(y)) -> match#(x, y), match#(f(x), f(y)) -> f#(match(x, y)))
    (match#(f(x), f(y)) -> match#(x, y), match#(f(x), f(y)) -> match#(x, y))
    (match#(f(x), f(y)) -> match#(x, y), match#(X(), x) -> proper#(x))
    (match#(X(), x) -> proper#(x), proper#(f(x)) -> f#(proper(x)))
    (match#(X(), x) -> proper#(x), proper#(f(x)) -> proper#(x))
    (top#(found(x)) -> active#(x), active#(f(x)) -> active#(x))
    (top#(found(x)) -> active#(x), active#(f(x)) -> f#(active(x)))
    (f#(found(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (f#(found(x)) -> f#(x), f#(ok(x)) -> f#(x))
    (f#(found(x)) -> f#(x), f#(found(x)) -> f#(x))
    (f#(mark(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (f#(mark(x)) -> f#(x), f#(ok(x)) -> f#(x))
    (f#(mark(x)) -> f#(x), f#(found(x)) -> f#(x))
    (match#(f(x), f(y)) -> f#(match(x, y)), f#(mark(x)) -> f#(x))
    (match#(f(x), f(y)) -> f#(match(x, y)), f#(ok(x)) -> f#(x))
    (match#(f(x), f(y)) -> f#(match(x, y)), f#(found(x)) -> f#(x))
    (check#(x) -> match#(f(X()), x), match#(f(x), f(y)) -> f#(match(x, y)))
    (check#(x) -> match#(f(X()), x), match#(f(x), f(y)) -> match#(x, y))
    (proper#(f(x)) -> f#(proper(x)), f#(mark(x)) -> f#(x))
    (proper#(f(x)) -> f#(proper(x)), f#(ok(x)) -> f#(x))
    (proper#(f(x)) -> f#(proper(x)), f#(found(x)) -> f#(x))
    (top#(found(x)) -> top#(active(x)), top#(mark(x)) -> top#(check(x)))
    (top#(found(x)) -> top#(active(x)), top#(mark(x)) -> check#(x))
    (top#(found(x)) -> top#(active(x)), top#(active(c())) -> top#(mark(c())))
    (top#(found(x)) -> top#(active(x)), top#(found(x)) -> active#(x))
    (top#(found(x)) -> top#(active(x)), top#(found(x)) -> top#(active(x)))
    (active#(f(x)) -> f#(active(x)), f#(mark(x)) -> f#(x))
    (active#(f(x)) -> f#(active(x)), f#(ok(x)) -> f#(x))
    (active#(f(x)) -> f#(active(x)), f#(found(x)) -> f#(x))}
   SCCS:
    Scc:
     {proper#(f(x)) -> proper#(x)}
    Scc:
     {match#(f(x), f(y)) -> match#(x, y)}
    Scc:
     {check#(f(x)) -> check#(x)}
    Scc:
     {    top#(mark(x)) -> top#(check(x)),
      top#(active(c())) -> top#(mark(c())),
         top#(found(x)) -> top#(active(x))}
    Scc:
     { f#(mark(x)) -> f#(x),
         f#(ok(x)) -> f#(x),
      f#(found(x)) -> f#(x)}
    Scc:
     {active#(f(x)) -> active#(x)}
    SCC:
     Strict:
      {proper#(f(x)) -> proper#(x)}
     Weak:
     {     active(f(x)) -> mark(x),
           active(f(x)) -> f(active(x)),
             f(mark(x)) -> mark(f(x)),
               f(ok(x)) -> ok(f(x)),
            f(found(x)) -> found(f(x)),
           top(mark(x)) -> top(check(x)),
       top(active(c())) -> top(mark(c())),
          top(found(x)) -> top(active(x)),
               check(x) -> start(match(f(X()), x)),
            check(f(x)) -> f(check(x)),
           start(ok(x)) -> found(x),
      match(f(x), f(y)) -> f(match(x, y)),
          match(X(), x) -> proper(x),
           proper(f(x)) -> f(proper(x)),
            proper(c()) -> ok(c())}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {match#(f(x), f(y)) -> match#(x, y)}
     Weak:
     {     active(f(x)) -> mark(x),
           active(f(x)) -> f(active(x)),
             f(mark(x)) -> mark(f(x)),
               f(ok(x)) -> ok(f(x)),
            f(found(x)) -> found(f(x)),
           top(mark(x)) -> top(check(x)),
       top(active(c())) -> top(mark(c())),
          top(found(x)) -> top(active(x)),
               check(x) -> start(match(f(X()), x)),
            check(f(x)) -> f(check(x)),
           start(ok(x)) -> found(x),
      match(f(x), f(y)) -> f(match(x, y)),
          match(X(), x) -> proper(x),
           proper(f(x)) -> f(proper(x)),
            proper(c()) -> ok(c())}
     SPSC:
      Simple Projection:
       pi(match#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {check#(f(x)) -> check#(x)}
     Weak:
     {     active(f(x)) -> mark(x),
           active(f(x)) -> f(active(x)),
             f(mark(x)) -> mark(f(x)),
               f(ok(x)) -> ok(f(x)),
            f(found(x)) -> found(f(x)),
           top(mark(x)) -> top(check(x)),
       top(active(c())) -> top(mark(c())),
          top(found(x)) -> top(active(x)),
               check(x) -> start(match(f(X()), x)),
            check(f(x)) -> f(check(x)),
           start(ok(x)) -> found(x),
      match(f(x), f(y)) -> f(match(x, y)),
          match(X(), x) -> proper(x),
           proper(f(x)) -> f(proper(x)),
            proper(c()) -> ok(c())}
     SPSC:
      Simple Projection:
       pi(check#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {    top#(mark(x)) -> top#(check(x)),
       top#(active(c())) -> top#(mark(c())),
          top#(found(x)) -> top#(active(x))}
     Weak:
     {     active(f(x)) -> mark(x),
           active(f(x)) -> f(active(x)),
             f(mark(x)) -> mark(f(x)),
               f(ok(x)) -> ok(f(x)),
            f(found(x)) -> found(f(x)),
           top(mark(x)) -> top(check(x)),
       top(active(c())) -> top(mark(c())),
          top(found(x)) -> top(active(x)),
               check(x) -> start(match(f(X()), x)),
            check(f(x)) -> f(check(x)),
           start(ok(x)) -> found(x),
      match(f(x), f(y)) -> f(match(x, y)),
          match(X(), x) -> proper(x),
           proper(f(x)) -> f(proper(x)),
            proper(c()) -> ok(c())}
     POLY:
      Argument Filtering:
       pi(found) = 0, pi(ok) = 0, pi(proper) = [], pi(X) = [], pi(match) = 0, pi(start) = 0, pi(check) = [], pi(c) = [], pi(top#) = 0, pi(top) = [], pi(f) = [], pi(active) = 0, pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [check] = 0,
       [mark] = 0,
       [c] = 1
      Strict:
       { top#(mark(x)) -> top#(check(x)),
        top#(found(x)) -> top#(active(x))}
      Weak:
       {     active(f(x)) -> mark(x),
             active(f(x)) -> f(active(x)),
               f(mark(x)) -> mark(f(x)),
                 f(ok(x)) -> ok(f(x)),
              f(found(x)) -> found(f(x)),
             top(mark(x)) -> top(check(x)),
         top(active(c())) -> top(mark(c())),
            top(found(x)) -> top(active(x)),
                 check(x) -> start(match(f(X()), x)),
              check(f(x)) -> f(check(x)),
             start(ok(x)) -> found(x),
        match(f(x), f(y)) -> f(match(x, y)),
            match(X(), x) -> proper(x),
             proper(f(x)) -> f(proper(x)),
              proper(c()) -> ok(c())}
      EDG:
       {(top#(found(x)) -> top#(active(x)), top#(found(x)) -> top#(active(x)))
        (top#(found(x)) -> top#(active(x)), top#(mark(x)) -> top#(check(x)))
        (top#(mark(x)) -> top#(check(x)), top#(mark(x)) -> top#(check(x)))
        (top#(mark(x)) -> top#(check(x)), top#(found(x)) -> top#(active(x)))}
       SCCS:
        Scc:
         { top#(mark(x)) -> top#(check(x)),
          top#(found(x)) -> top#(active(x))}
        SCC:
         Strict:
          { top#(mark(x)) -> top#(check(x)),
           top#(found(x)) -> top#(active(x))}
         Weak:
         {     active(f(x)) -> mark(x),
               active(f(x)) -> f(active(x)),
                 f(mark(x)) -> mark(f(x)),
                   f(ok(x)) -> ok(f(x)),
                f(found(x)) -> found(f(x)),
               top(mark(x)) -> top(check(x)),
           top(active(c())) -> top(mark(c())),
              top(found(x)) -> top(active(x)),
                   check(x) -> start(match(f(X()), x)),
                check(f(x)) -> f(check(x)),
               start(ok(x)) -> found(x),
          match(f(x), f(y)) -> f(match(x, y)),
              match(X(), x) -> proper(x),
               proper(f(x)) -> f(proper(x)),
                proper(c()) -> ok(c())}
         POLY:
          Argument Filtering:
           pi(found) = 0, pi(ok) = 0, pi(proper) = 0, pi(X) = [], pi(match) = 1, pi(start) = 0, pi(check) = 0, pi(c) = [], pi(top#) = 0, pi(top) = [], pi(f) = [0], pi(active) = 0, pi(mark) = [0]
          Usable Rules:
           {}
          Interpretation:
           [mark](x0) = x0 + 1
          Strict:
           {top#(found(x)) -> top#(active(x))}
          Weak:
           {     active(f(x)) -> mark(x),
                 active(f(x)) -> f(active(x)),
                   f(mark(x)) -> mark(f(x)),
                     f(ok(x)) -> ok(f(x)),
                  f(found(x)) -> found(f(x)),
                 top(mark(x)) -> top(check(x)),
             top(active(c())) -> top(mark(c())),
                top(found(x)) -> top(active(x)),
                     check(x) -> start(match(f(X()), x)),
                  check(f(x)) -> f(check(x)),
                 start(ok(x)) -> found(x),
            match(f(x), f(y)) -> f(match(x, y)),
                match(X(), x) -> proper(x),
                 proper(f(x)) -> f(proper(x)),
                  proper(c()) -> ok(c())}
          EDG:
           {(top#(found(x)) -> top#(active(x)), top#(found(x)) -> top#(active(x)))}
           SCCS:
            Scc:
             {top#(found(x)) -> top#(active(x))}
            SCC:
             Strict:
              {top#(found(x)) -> top#(active(x))}
             Weak:
             {     active(f(x)) -> mark(x),
                   active(f(x)) -> f(active(x)),
                     f(mark(x)) -> mark(f(x)),
                       f(ok(x)) -> ok(f(x)),
                    f(found(x)) -> found(f(x)),
                   top(mark(x)) -> top(check(x)),
               top(active(c())) -> top(mark(c())),
                  top(found(x)) -> top(active(x)),
                       check(x) -> start(match(f(X()), x)),
                    check(f(x)) -> f(check(x)),
                   start(ok(x)) -> found(x),
              match(f(x), f(y)) -> f(match(x, y)),
                  match(X(), x) -> proper(x),
                   proper(f(x)) -> f(proper(x)),
                    proper(c()) -> ok(c())}
             POLY:
              Argument Filtering:
               pi(found) = [], pi(ok) = [], pi(proper) = [], pi(X) = [], pi(match) = [], pi(start) = [], pi(check) = [], pi(c) = [], pi(top#) = 0, pi(top) = [], pi(f) = 0, pi(active) = [], pi(mark) = []
              Usable Rules:
               {}
              Interpretation:
               [found] = 1,
               [active] = 0
              Strict:
               {}
              Weak:
               {     active(f(x)) -> mark(x),
                     active(f(x)) -> f(active(x)),
                       f(mark(x)) -> mark(f(x)),
                         f(ok(x)) -> ok(f(x)),
                      f(found(x)) -> found(f(x)),
                     top(mark(x)) -> top(check(x)),
                 top(active(c())) -> top(mark(c())),
                    top(found(x)) -> top(active(x)),
                         check(x) -> start(match(f(X()), x)),
                      check(f(x)) -> f(check(x)),
                     start(ok(x)) -> found(x),
                match(f(x), f(y)) -> f(match(x, y)),
                    match(X(), x) -> proper(x),
                     proper(f(x)) -> f(proper(x)),
                      proper(c()) -> ok(c())}
              Qed
    SCC:
     Strict:
      { f#(mark(x)) -> f#(x),
          f#(ok(x)) -> f#(x),
       f#(found(x)) -> f#(x)}
     Weak:
     {     active(f(x)) -> mark(x),
           active(f(x)) -> f(active(x)),
             f(mark(x)) -> mark(f(x)),
               f(ok(x)) -> ok(f(x)),
            f(found(x)) -> found(f(x)),
           top(mark(x)) -> top(check(x)),
       top(active(c())) -> top(mark(c())),
          top(found(x)) -> top(active(x)),
               check(x) -> start(match(f(X()), x)),
            check(f(x)) -> f(check(x)),
           start(ok(x)) -> found(x),
      match(f(x), f(y)) -> f(match(x, y)),
          match(X(), x) -> proper(x),
           proper(f(x)) -> f(proper(x)),
            proper(c()) -> ok(c())}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(mark(x)) -> f#(x),
          f#(ok(x)) -> f#(x)}
      EDG:
       {(f#(ok(x)) -> f#(x), f#(ok(x)) -> f#(x))
        (f#(ok(x)) -> f#(x), f#(mark(x)) -> f#(x))
        (f#(mark(x)) -> f#(x), f#(mark(x)) -> f#(x))
        (f#(mark(x)) -> f#(x), f#(ok(x)) -> f#(x))}
       SCCS:
        Scc:
         {f#(mark(x)) -> f#(x),
            f#(ok(x)) -> f#(x)}
        SCC:
         Strict:
          {f#(mark(x)) -> f#(x),
             f#(ok(x)) -> f#(x)}
         Weak:
         {     active(f(x)) -> mark(x),
               active(f(x)) -> f(active(x)),
                 f(mark(x)) -> mark(f(x)),
                   f(ok(x)) -> ok(f(x)),
                f(found(x)) -> found(f(x)),
               top(mark(x)) -> top(check(x)),
           top(active(c())) -> top(mark(c())),
              top(found(x)) -> top(active(x)),
                   check(x) -> start(match(f(X()), x)),
                check(f(x)) -> f(check(x)),
               start(ok(x)) -> found(x),
          match(f(x), f(y)) -> f(match(x, y)),
              match(X(), x) -> proper(x),
               proper(f(x)) -> f(proper(x)),
                proper(c()) -> ok(c())}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {f#(ok(x)) -> f#(x)}
          EDG:
           {(f#(ok(x)) -> f#(x), f#(ok(x)) -> f#(x))}
           SCCS:
            Scc:
             {f#(ok(x)) -> f#(x)}
            SCC:
             Strict:
              {f#(ok(x)) -> f#(x)}
             Weak:
             {     active(f(x)) -> mark(x),
                   active(f(x)) -> f(active(x)),
                     f(mark(x)) -> mark(f(x)),
                       f(ok(x)) -> ok(f(x)),
                    f(found(x)) -> found(f(x)),
                   top(mark(x)) -> top(check(x)),
               top(active(c())) -> top(mark(c())),
                  top(found(x)) -> top(active(x)),
                       check(x) -> start(match(f(X()), x)),
                    check(f(x)) -> f(check(x)),
                   start(ok(x)) -> found(x),
              match(f(x), f(y)) -> f(match(x, y)),
                  match(X(), x) -> proper(x),
                   proper(f(x)) -> f(proper(x)),
                    proper(c()) -> ok(c())}
             SPSC:
              Simple Projection:
               pi(f#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {active#(f(x)) -> active#(x)}
     Weak:
     {     active(f(x)) -> mark(x),
           active(f(x)) -> f(active(x)),
             f(mark(x)) -> mark(f(x)),
               f(ok(x)) -> ok(f(x)),
            f(found(x)) -> found(f(x)),
           top(mark(x)) -> top(check(x)),
       top(active(c())) -> top(mark(c())),
          top(found(x)) -> top(active(x)),
               check(x) -> start(match(f(X()), x)),
            check(f(x)) -> f(check(x)),
           start(ok(x)) -> found(x),
      match(f(x), f(y)) -> f(match(x, y)),
          match(X(), x) -> proper(x),
           proper(f(x)) -> f(proper(x)),
            proper(c()) -> ok(c())}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {}
      Qed