YES
TRS:
 {       f(mark(x)) -> mark(f(x)),
       f(active(x)) -> active(f(x)),
           f(no(x)) -> no(f(x)),
       active(f(x)) -> mark(f(f(x))),
      chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
       chk(no(c())) -> active(c()),
  mat(f(x), f(y())) -> f(mat(x, y())),
     mat(f(x), c()) -> no(c()),
        tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
 DP:
  Strict:
   {       f#(mark(x)) -> f#(x),
         f#(active(x)) -> f#(x),
         f#(active(x)) -> active#(f(x)),
             f#(no(x)) -> f#(x),
         active#(f(x)) -> f#(f(x)),
        chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))),
        chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))),
        chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))),
        chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))),
        chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))),
        chk#(no(f(x))) -> f#(f(f(f(f(X()))))),
        chk#(no(f(x))) -> f#(f(f(f(X())))),
        chk#(no(f(x))) -> f#(f(f(X()))),
        chk#(no(f(x))) -> f#(f(X())),
        chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
        chk#(no(f(x))) -> f#(X()),
        chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)),
        chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x),
         chk#(no(c())) -> active#(c()),
    mat#(f(x), f(y())) -> f#(mat(x, y())),
    mat#(f(x), f(y())) -> mat#(x, y()),
          tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))),
          tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))),
          tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))),
          tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))),
          tp#(mark(x)) -> f#(f(f(f(f(f(X())))))),
          tp#(mark(x)) -> f#(f(f(f(f(X()))))),
          tp#(mark(x)) -> f#(f(f(f(X())))),
          tp#(mark(x)) -> f#(f(f(X()))),
          tp#(mark(x)) -> f#(f(X())),
          tp#(mark(x)) -> f#(X()),
          tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)),
          tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x),
          tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
  Weak:
  {       f(mark(x)) -> mark(f(x)),
        f(active(x)) -> active(f(x)),
            f(no(x)) -> no(f(x)),
        active(f(x)) -> mark(f(f(x))),
       chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
        chk(no(c())) -> active(c()),
   mat(f(x), f(y())) -> f(mat(x, y())),
      mat(f(x), c()) -> no(c()),
         tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
  EDG:
   {(active#(f(x)) -> f#(f(x)), f#(no(x)) -> f#(x))
    (active#(f(x)) -> f#(f(x)), f#(active(x)) -> active#(f(x)))
    (active#(f(x)) -> f#(f(x)), f#(active(x)) -> f#(x))
    (active#(f(x)) -> f#(f(x)), f#(mark(x)) -> f#(x))
    (tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x), mat#(f(x), f(y())) -> mat#(x, y()))
    (tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x), mat#(f(x), f(y())) -> f#(mat(x, y())))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(X()))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(X())))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(X()))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(X())))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(X()))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(X())))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))))
    (f#(mark(x)) -> f#(x), f#(no(x)) -> f#(x))
    (f#(mark(x)) -> f#(x), f#(active(x)) -> active#(f(x)))
    (f#(mark(x)) -> f#(x), f#(active(x)) -> f#(x))
    (f#(mark(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (f#(no(x)) -> f#(x), f#(no(x)) -> f#(x))
    (f#(no(x)) -> f#(x), f#(active(x)) -> active#(f(x)))
    (f#(no(x)) -> f#(x), f#(active(x)) -> f#(x))
    (f#(no(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(c())) -> active#(c()))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(X()))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(X())))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(X()))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(X())))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(X()))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(X()))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(X())))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(X()))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(X())))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(X()))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(c())) -> active#(c()))
    (f#(active(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (f#(active(x)) -> f#(x), f#(active(x)) -> f#(x))
    (f#(active(x)) -> f#(x), f#(active(x)) -> active#(f(x)))
    (f#(active(x)) -> f#(x), f#(no(x)) -> f#(x))
    (chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), f#(mark(x)) -> f#(x))
    (chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), f#(active(x)) -> f#(x))
    (chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), f#(active(x)) -> active#(f(x)))
    (chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), f#(no(x)) -> f#(x))
    (chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x), mat#(f(x), f(y())) -> f#(mat(x, y())))
    (chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x), mat#(f(x), f(y())) -> mat#(x, y()))
    (f#(active(x)) -> active#(f(x)), active#(f(x)) -> f#(f(x)))}
   SCCS:
    Scc:
     {tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
    Scc:
     {chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))}
    Scc:
     {  f#(mark(x)) -> f#(x),
      f#(active(x)) -> f#(x),
      f#(active(x)) -> active#(f(x)),
          f#(no(x)) -> f#(x),
      active#(f(x)) -> f#(f(x))}
    SCC:
     Strict:
      {tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
     Weak:
     {       f(mark(x)) -> mark(f(x)),
           f(active(x)) -> active(f(x)),
               f(no(x)) -> no(f(x)),
           active(f(x)) -> mark(f(f(x))),
          chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
           chk(no(c())) -> active(c()),
      mat(f(x), f(y())) -> f(mat(x, y())),
         mat(f(x), c()) -> no(c()),
            tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 0
      Automaton:
       {        a_0() -> 13*
            tp#_0(15) -> 1*
                c_0() -> 16*
                y_0() -> 17*
             no_0(16) -> 14*
                X_0() -> 2*
        mat_0(12, 13) -> 14*
        mat_0(11, 17) -> 18*
            chk_0(14) -> 15*
         active_0(16) -> 15*
              f_0(18) -> 14*
              f_0(11) -> 12*
              f_0(10) -> 11*
               f_0(9) -> 10*
               f_0(8) -> 9*
               f_0(7) -> 8*
               f_0(6) -> 7*
               f_0(5) -> 6*
               f_0(4) -> 5*
               f_0(3) -> 4*
               f_0(2) -> 3*}
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))}
     Weak:
     {       f(mark(x)) -> mark(f(x)),
           f(active(x)) -> active(f(x)),
               f(no(x)) -> no(f(x)),
           active(f(x)) -> mark(f(f(x))),
          chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
           chk(no(c())) -> active(c()),
      mat(f(x), f(y())) -> f(mat(x, y())),
         mat(f(x), c()) -> no(c()),
            tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
     POLY:
      Argument Filtering:
       pi(tp) = [], pi(c) = [], pi(y) = [], pi(no) = 0, pi(X) = [], pi(mat) = 1, pi(chk#) = 0, pi(chk) = [], pi(active) = [], pi(f) = [0], pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [f](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {       f(mark(x)) -> mark(f(x)),
             f(active(x)) -> active(f(x)),
                 f(no(x)) -> no(f(x)),
             active(f(x)) -> mark(f(f(x))),
            chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
             chk(no(c())) -> active(c()),
        mat(f(x), f(y())) -> f(mat(x, y())),
           mat(f(x), c()) -> no(c()),
              tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
      Qed
    SCC:
     Strict:
      {  f#(mark(x)) -> f#(x),
       f#(active(x)) -> f#(x),
       f#(active(x)) -> active#(f(x)),
           f#(no(x)) -> f#(x),
       active#(f(x)) -> f#(f(x))}
     Weak:
     {       f(mark(x)) -> mark(f(x)),
           f(active(x)) -> active(f(x)),
               f(no(x)) -> no(f(x)),
           active(f(x)) -> mark(f(f(x))),
          chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
           chk(no(c())) -> active(c()),
      mat(f(x), f(y())) -> f(mat(x, y())),
         mat(f(x), c()) -> no(c()),
            tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
     POLY:
      Argument Filtering:
       pi(tp) = [], pi(c) = [], pi(y) = [], pi(no) = [0], pi(X) = [], pi(mat) = [], pi(chk) = [], pi(active#) = [0], pi(active) = [0], pi(f#) = [0], pi(f) = 0, pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [active#](x0) = x0 + 1,
       [f#](x0) = x0 + 1,
       [no](x0) = x0 + 1,
       [active](x0) = x0 + 1
      Strict:
       {  f#(mark(x)) -> f#(x),
        active#(f(x)) -> f#(f(x))}
      Weak:
       {       f(mark(x)) -> mark(f(x)),
             f(active(x)) -> active(f(x)),
                 f(no(x)) -> no(f(x)),
             active(f(x)) -> mark(f(f(x))),
            chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
             chk(no(c())) -> active(c()),
        mat(f(x), f(y())) -> f(mat(x, y())),
           mat(f(x), c()) -> no(c()),
              tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
      EDG:
       {(active#(f(x)) -> f#(f(x)), f#(mark(x)) -> f#(x))
        (f#(mark(x)) -> f#(x), f#(mark(x)) -> f#(x))}
       SCCS:
        Scc:
         {f#(mark(x)) -> f#(x)}
        SCC:
         Strict:
          {f#(mark(x)) -> f#(x)}
         Weak:
         {       f(mark(x)) -> mark(f(x)),
               f(active(x)) -> active(f(x)),
                   f(no(x)) -> no(f(x)),
               active(f(x)) -> mark(f(f(x))),
              chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
               chk(no(c())) -> active(c()),
          mat(f(x), f(y())) -> f(mat(x, y())),
             mat(f(x), c()) -> no(c()),
                tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed