YES
TRS:
 {         f(ok(X)) -> ok(f(X)),
         g(mark(X)) -> mark(g(X)),
           g(ok(X)) -> ok(g(X)),
  active(f(f(a()))) -> mark(f(g(f(a())))),
       active(g(X)) -> g(active(X)),
       proper(f(X)) -> f(proper(X)),
       proper(g(X)) -> g(proper(X)),
        proper(a()) -> ok(a()),
       top(mark(X)) -> top(proper(X)),
         top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {         f#(ok(X)) -> f#(X),
           g#(mark(X)) -> g#(X),
             g#(ok(X)) -> g#(X),
    active#(f(f(a()))) -> f#(g(f(a()))),
    active#(f(f(a()))) -> g#(f(a())),
         active#(g(X)) -> g#(active(X)),
         active#(g(X)) -> active#(X),
         proper#(f(X)) -> f#(proper(X)),
         proper#(f(X)) -> proper#(X),
         proper#(g(X)) -> g#(proper(X)),
         proper#(g(X)) -> proper#(X),
         top#(mark(X)) -> proper#(X),
         top#(mark(X)) -> top#(proper(X)),
           top#(ok(X)) -> active#(X),
           top#(ok(X)) -> top#(active(X))}
  Weak:
  {         f(ok(X)) -> ok(f(X)),
          g(mark(X)) -> mark(g(X)),
            g(ok(X)) -> ok(g(X)),
   active(f(f(a()))) -> mark(f(g(f(a())))),
        active(g(X)) -> g(active(X)),
        proper(f(X)) -> f(proper(X)),
        proper(g(X)) -> g(proper(X)),
         proper(a()) -> ok(a()),
        top(mark(X)) -> top(proper(X)),
          top(ok(X)) -> top(active(X))}
  EDG:
   {(g#(mark(X)) -> g#(X), g#(ok(X)) -> g#(X))
    (g#(mark(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (active#(g(X)) -> active#(X), active#(g(X)) -> active#(X))
    (active#(g(X)) -> active#(X), active#(g(X)) -> g#(active(X)))
    (active#(g(X)) -> active#(X), active#(f(f(a()))) -> g#(f(a())))
    (active#(g(X)) -> active#(X), active#(f(f(a()))) -> f#(g(f(a()))))
    (proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
    (proper#(g(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
    (proper#(g(X)) -> proper#(X), proper#(f(X)) -> proper#(X))
    (proper#(g(X)) -> proper#(X), proper#(f(X)) -> f#(proper(X)))
    (top#(ok(X)) -> active#(X), active#(g(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(g(X)) -> g#(active(X)))
    (top#(ok(X)) -> active#(X), active#(f(f(a()))) -> g#(f(a())))
    (top#(ok(X)) -> active#(X), active#(f(f(a()))) -> f#(g(f(a()))))
    (proper#(f(X)) -> f#(proper(X)), f#(ok(X)) -> f#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
    (proper#(g(X)) -> g#(proper(X)), g#(mark(X)) -> g#(X))
    (proper#(g(X)) -> g#(proper(X)), g#(ok(X)) -> g#(X))
    (active#(g(X)) -> g#(active(X)), g#(mark(X)) -> g#(X))
    (active#(g(X)) -> g#(active(X)), g#(ok(X)) -> g#(X))
    (top#(mark(X)) -> proper#(X), proper#(f(X)) -> f#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(f(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
    (proper#(f(X)) -> proper#(X), proper#(f(X)) -> f#(proper(X)))
    (proper#(f(X)) -> proper#(X), proper#(f(X)) -> proper#(X))
    (proper#(f(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
    (proper#(f(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
    (g#(ok(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (g#(ok(X)) -> g#(X), g#(ok(X)) -> g#(X))
    (f#(ok(X)) -> f#(X), f#(ok(X)) -> f#(X))}
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {proper#(f(X)) -> proper#(X),
      proper#(g(X)) -> proper#(X)}
    Scc:
     {active#(g(X)) -> active#(X)}
    Scc:
     {g#(mark(X)) -> g#(X),
        g#(ok(X)) -> g#(X)}
    Scc:
     {f#(ok(X)) -> f#(X)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {         f(ok(X)) -> ok(f(X)),
             g(mark(X)) -> mark(g(X)),
               g(ok(X)) -> ok(g(X)),
      active(f(f(a()))) -> mark(f(g(f(a())))),
           active(g(X)) -> g(active(X)),
           proper(f(X)) -> f(proper(X)),
           proper(g(X)) -> g(proper(X)),
            proper(a()) -> ok(a()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 2
      Automaton:
       {  top#_2(80) -> 81*
          top#_1(24) -> 25*
          top#_0(21) -> 22*
          top#_0(20) -> 10*
           top_0(20) -> 18*
           top_0(19) -> 18*
           top_0(18) -> 18*
           top_0(17) -> 18*
           top_0(16) -> 18*
           top_0(14) -> 18*
           top_0(13) -> 18*
           top_0(12) -> 18*
            ok_1(83) -> 84*
            ok_1(77) -> 78*
            ok_1(74) -> 75*
            ok_1(71) -> 72*
            ok_1(68) -> 69*
            ok_0(20) -> 17*
            ok_0(19) -> 17*
            ok_0(18) -> 17*
            ok_0(17) -> 17*
            ok_0(16) -> 17*
            ok_0(14) -> 17*
            ok_0(13) -> 17*
            ok_0(12) -> 17*
        proper_1(66) -> 67*
        proper_1(63) -> 64*
        proper_1(60) -> 61*
        proper_1(57) -> 58*
        proper_1(52) -> 53*
        proper_1(50) -> 51*
        proper_1(45) -> 46*
        proper_0(20) -> 16*
        proper_0(19) -> 16*
        proper_0(18) -> 16*
        proper_0(17) -> 16*
        proper_0(16) -> 16*
        proper_0(14) -> 16*
        proper_0(13) -> 16*
        proper_0(12) -> 16*
        active_2(92) -> 93*
        active_2(89) -> 90*
        active_2(85) -> 86*
        active_2(79) -> 80*
        active_1(36) -> 37*
        active_1(34) -> 35*
        active_1(32) -> 33*
        active_1(30) -> 31*
        active_1(28) -> 29*
        active_1(26) -> 27*
        active_1(23) -> 24*
        active_0(20) -> 20*
        active_0(19) -> 20*
        active_0(18) -> 20*
        active_0(17) -> 20*
        active_0(16) -> 20*
        active_0(14) -> 20*
        active_0(13) -> 20*
        active_0(12) -> 20*
               a_1() -> 40*
               a_0() -> 19*
             g_2(90) -> 91*
             g_1(87) -> 88*
             g_1(82) -> 83*
             g_1(73) -> 74*
             g_1(61) -> 62*
             g_1(58) -> 59*
             g_1(55) -> 56*
             g_1(47) -> 48*
             g_1(41) -> 42*
             g_1(38) -> 39*
             g_0(20) -> 14*
             g_0(19) -> 14*
             g_0(18) -> 14*
             g_0(17) -> 14*
             g_0(16) -> 14*
             g_0(14) -> 14*
             g_0(13) -> 14*
             g_0(12) -> 14*
             f_1(76) -> 77*
             f_1(70) -> 71*
             f_1(64) -> 65*
             f_1(53) -> 54*
             f_1(42) -> 43*
             f_1(40) -> 41*
             f_0(20) -> 13*
             f_0(19) -> 13*
             f_0(18) -> 13*
             f_0(17) -> 13*
             f_0(16) -> 13*
             f_0(14) -> 13*
             f_0(13) -> 13*
             f_0(12) -> 13*
          mark_1(48) -> 49*
          mark_1(43) -> 44*
          mark_0(20) -> 12*
          mark_0(19) -> 12*
          mark_0(18) -> 12*
          mark_0(17) -> 12*
          mark_0(16) -> 12*
          mark_0(14) -> 12*
          mark_0(13) -> 12*
          mark_0(12) -> 12*
                  93 -> 90*
                  91 -> 93 | 86
                  88 -> 83*
                  87 -> 92*
                  86 -> 80*
                  84 -> 62 | 39
                  83 -> 87 | 85
                  82 -> 89*
                  81 -> 25*
                  78 -> 54*
                  77 -> 82 | 79
                  75 -> 59*
                  74 -> 76*
                  72 -> 65*
                  71 -> 73*
                  69 -> 64*
                  68 -> 70*
                  67 -> 61*
                  65 -> 58*
                  62 -> 67 | 51
                  59 -> 53*
                  56 -> 48*
                  55 -> 66*
                  54 -> 61 | 46
                  51 -> 24*
                  49 -> 39*
                  48 -> 55 | 50
                  47 -> 60*
                  46 -> 24*
                  44 -> 31 | 27
                  43 -> 47 | 45
                  42 -> 52*
                  41 -> 57*
                  40 -> 68 | 63
                  39 -> 37 | 31 | 29
                  37 -> 24*
                  35 -> 24*
                  33 -> 24*
                  31 -> 24*
                  29 -> 24*
                  27 -> 24*
                  25 -> 22*
                  24 -> 38*
                  22 -> 10*
                  20 -> 36*
                  19 -> 34*
                  18 -> 32*
                  17 -> 16 | 14 | 13
                  16 -> 30 | 21
                  14 -> 28 | 20 | 16
                  13 -> 26 | 16
                  12 -> 23 | 14}
      Strict:
       {top#(mark(X)) -> top#(proper(X))}
      EDG:
       {(top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))}
       SCCS:
        Scc:
         {top#(mark(X)) -> top#(proper(X))}
        SCC:
         Strict:
          {top#(mark(X)) -> top#(proper(X))}
         Weak:
         {         f(ok(X)) -> ok(f(X)),
                 g(mark(X)) -> mark(g(X)),
                   g(ok(X)) -> ok(g(X)),
          active(f(f(a()))) -> mark(f(g(f(a())))),
               active(g(X)) -> g(active(X)),
               proper(f(X)) -> f(proper(X)),
               proper(g(X)) -> g(proper(X)),
                proper(a()) -> ok(a()),
               top(mark(X)) -> top(proper(X)),
                 top(ok(X)) -> top(active(X))}
         POLY:
          Argument Filtering:
           pi(top#) = 0, pi(top) = [], pi(ok) = 0, pi(proper) = 0, pi(active) = [], pi(a) = [], pi(g) = [0], pi(f) = [], pi(mark) = [0]
          Usable Rules:
           {}
          Interpretation:
           [mark](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {         f(ok(X)) -> ok(f(X)),
                   g(mark(X)) -> mark(g(X)),
                     g(ok(X)) -> ok(g(X)),
            active(f(f(a()))) -> mark(f(g(f(a())))),
                 active(g(X)) -> g(active(X)),
                 proper(f(X)) -> f(proper(X)),
                 proper(g(X)) -> g(proper(X)),
                  proper(a()) -> ok(a()),
                 top(mark(X)) -> top(proper(X)),
                   top(ok(X)) -> top(active(X))}
          Qed
    SCC:
     Strict:
      {proper#(f(X)) -> proper#(X),
       proper#(g(X)) -> proper#(X)}
     Weak:
     {         f(ok(X)) -> ok(f(X)),
             g(mark(X)) -> mark(g(X)),
               g(ok(X)) -> ok(g(X)),
      active(f(f(a()))) -> mark(f(g(f(a())))),
           active(g(X)) -> g(active(X)),
           proper(f(X)) -> f(proper(X)),
           proper(g(X)) -> g(proper(X)),
            proper(a()) -> ok(a()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {proper#(g(X)) -> proper#(X)}
      EDG:
       {(proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))}
       SCCS:
        Scc:
         {proper#(g(X)) -> proper#(X)}
        SCC:
         Strict:
          {proper#(g(X)) -> proper#(X)}
         Weak:
         {         f(ok(X)) -> ok(f(X)),
                 g(mark(X)) -> mark(g(X)),
                   g(ok(X)) -> ok(g(X)),
          active(f(f(a()))) -> mark(f(g(f(a())))),
               active(g(X)) -> g(active(X)),
               proper(f(X)) -> f(proper(X)),
               proper(g(X)) -> g(proper(X)),
                proper(a()) -> ok(a()),
               top(mark(X)) -> top(proper(X)),
                 top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {active#(g(X)) -> active#(X)}
     Weak:
     {         f(ok(X)) -> ok(f(X)),
             g(mark(X)) -> mark(g(X)),
               g(ok(X)) -> ok(g(X)),
      active(f(f(a()))) -> mark(f(g(f(a())))),
           active(g(X)) -> g(active(X)),
           proper(f(X)) -> f(proper(X)),
           proper(g(X)) -> g(proper(X)),
            proper(a()) -> ok(a()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {g#(mark(X)) -> g#(X),
         g#(ok(X)) -> g#(X)}
     Weak:
     {         f(ok(X)) -> ok(f(X)),
             g(mark(X)) -> mark(g(X)),
               g(ok(X)) -> ok(g(X)),
      active(f(f(a()))) -> mark(f(g(f(a())))),
           active(g(X)) -> g(active(X)),
           proper(f(X)) -> f(proper(X)),
           proper(g(X)) -> g(proper(X)),
            proper(a()) -> ok(a()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {g#(ok(X)) -> g#(X)}
      EDG:
       {(g#(ok(X)) -> g#(X), g#(ok(X)) -> g#(X))}
       SCCS:
        Scc:
         {g#(ok(X)) -> g#(X)}
        SCC:
         Strict:
          {g#(ok(X)) -> g#(X)}
         Weak:
         {         f(ok(X)) -> ok(f(X)),
                 g(mark(X)) -> mark(g(X)),
                   g(ok(X)) -> ok(g(X)),
          active(f(f(a()))) -> mark(f(g(f(a())))),
               active(g(X)) -> g(active(X)),
               proper(f(X)) -> f(proper(X)),
               proper(g(X)) -> g(proper(X)),
                proper(a()) -> ok(a()),
               top(mark(X)) -> top(proper(X)),
                 top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {f#(ok(X)) -> f#(X)}
     Weak:
     {         f(ok(X)) -> ok(f(X)),
             g(mark(X)) -> mark(g(X)),
               g(ok(X)) -> ok(g(X)),
      active(f(f(a()))) -> mark(f(g(f(a())))),
           active(g(X)) -> g(active(X)),
           proper(f(X)) -> f(proper(X)),
           proper(g(X)) -> g(proper(X)),
            proper(a()) -> ok(a()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {}
      Qed