YES

Problem:
 active(f(x)) -> mark(x)
 top(active(c())) -> top(mark(c()))
 top(mark(x)) -> top(check(x))
 check(f(x)) -> f(check(x))
 check(x) -> start(match(f(X()),x))
 match(f(x),f(y)) -> f(match(x,y))
 match(X(),x) -> proper(x)
 proper(c()) -> ok(c())
 proper(f(x)) -> f(proper(x))
 f(ok(x)) -> ok(f(x))
 start(ok(x)) -> found(x)
 f(found(x)) -> found(f(x))
 top(found(x)) -> top(active(x))
 active(f(x)) -> f(active(x))
 f(mark(x)) -> mark(f(x))

Proof:
 DP Processor:
  DPs:
   top#(active(c())) -> top#(mark(c()))
   top#(mark(x)) -> check#(x)
   top#(mark(x)) -> top#(check(x))
   check#(f(x)) -> check#(x)
   check#(f(x)) -> f#(check(x))
   check#(x) -> f#(X())
   check#(x) -> match#(f(X()),x)
   check#(x) -> start#(match(f(X()),x))
   match#(f(x),f(y)) -> match#(x,y)
   match#(f(x),f(y)) -> f#(match(x,y))
   match#(X(),x) -> proper#(x)
   proper#(f(x)) -> proper#(x)
   proper#(f(x)) -> f#(proper(x))
   f#(ok(x)) -> f#(x)
   f#(found(x)) -> f#(x)
   top#(found(x)) -> active#(x)
   top#(found(x)) -> top#(active(x))
   active#(f(x)) -> active#(x)
   active#(f(x)) -> f#(active(x))
   f#(mark(x)) -> f#(x)
  TRS:
   active(f(x)) -> mark(x)
   top(active(c())) -> top(mark(c()))
   top(mark(x)) -> top(check(x))
   check(f(x)) -> f(check(x))
   check(x) -> start(match(f(X()),x))
   match(f(x),f(y)) -> f(match(x,y))
   match(X(),x) -> proper(x)
   proper(c()) -> ok(c())
   proper(f(x)) -> f(proper(x))
   f(ok(x)) -> ok(f(x))
   start(ok(x)) -> found(x)
   f(found(x)) -> found(f(x))
   top(found(x)) -> top(active(x))
   active(f(x)) -> f(active(x))
   f(mark(x)) -> mark(f(x))
  Usable Rule Processor:
   DPs:
    top#(active(c())) -> top#(mark(c()))
    top#(mark(x)) -> check#(x)
    top#(mark(x)) -> top#(check(x))
    check#(f(x)) -> check#(x)
    check#(f(x)) -> f#(check(x))
    check#(x) -> f#(X())
    check#(x) -> match#(f(X()),x)
    check#(x) -> start#(match(f(X()),x))
    match#(f(x),f(y)) -> match#(x,y)
    match#(f(x),f(y)) -> f#(match(x,y))
    match#(X(),x) -> proper#(x)
    proper#(f(x)) -> proper#(x)
    proper#(f(x)) -> f#(proper(x))
    f#(ok(x)) -> f#(x)
    f#(found(x)) -> f#(x)
    top#(found(x)) -> active#(x)
    top#(found(x)) -> top#(active(x))
    active#(f(x)) -> active#(x)
    active#(f(x)) -> f#(active(x))
    f#(mark(x)) -> f#(x)
   TRS:
    check(f(x)) -> f(check(x))
    check(x) -> start(match(f(X()),x))
    f(ok(x)) -> ok(f(x))
    f(found(x)) -> found(f(x))
    f(mark(x)) -> mark(f(x))
    start(ok(x)) -> found(x)
    match(f(x),f(y)) -> f(match(x,y))
    match(X(),x) -> proper(x)
    proper(c()) -> ok(c())
    proper(f(x)) -> f(proper(x))
    active(f(x)) -> mark(x)
    active(f(x)) -> f(active(x))
   Matrix Interpretation Processor: dim=2
    
    usable rules:
     check(f(x)) -> f(check(x))
     check(x) -> start(match(f(X()),x))
     f(ok(x)) -> ok(f(x))
     f(found(x)) -> found(f(x))
     f(mark(x)) -> mark(f(x))
     start(ok(x)) -> found(x)
     match(f(x),f(y)) -> f(match(x,y))
     match(X(),x) -> proper(x)
     proper(c()) -> ok(c())
     proper(f(x)) -> f(proper(x))
     active(f(x)) -> mark(x)
     active(f(x)) -> f(active(x))
    interpretation:
     [proper#](x0) = [3 0]x0,
     
     [start#](x0) = [0],
     
     [match#](x0, x1) = [3 0]x1 + [1],
     
     [f#](x0) = [2 0]x0,
     
     [check#](x0) = [3 0]x0 + [2],
     
     [top#](x0) = [1 1]x0 + [1],
     
     [active#](x0) = [2 0]x0 + [1],
     
                   [2 1]     [1]
     [found](x0) = [0 1]x0 + [0],
     
                [2 0]     [1]
     [ok](x0) = [0 1]x0 + [0],
     
                    [2 0]     [1]
     [proper](x0) = [0 0]x0 + [2],
     
                   [1 2]  
     [start](x0) = [0 1]x0,
     
                       [0 0]     [2 0]     [1]
     [match](x0, x1) = [0 2]x0 + [0 0]x1 + [0],
     
           [0]
     [X] = [2],
     
                   [2 0]     [1]
     [check](x0) = [0 0]x0 + [0],
     
           [0]
     [c] = [2],
     
                  [3 0]     [2]
     [mark](x0) = [0 0]x0 + [0],
     
                    [2 0]  
     [active](x0) = [0 2]x0,
     
               [2 0]     [1]
     [f](x0) = [0 0]x0 + [0]
    orientation:
     top#(active(c())) = 5 >= 3 = top#(mark(c()))
     
     top#(mark(x)) = [3 0]x + [3] >= [3 0]x + [2] = check#(x)
     
     top#(mark(x)) = [3 0]x + [3] >= [2 0]x + [2] = top#(check(x))
     
     check#(f(x)) = [6 0]x + [5] >= [3 0]x + [2] = check#(x)
     
     check#(f(x)) = [6 0]x + [5] >= [4 0]x + [2] = f#(check(x))
     
     check#(x) = [3 0]x + [2] >= [0] = f#(X())
     
     check#(x) = [3 0]x + [2] >= [3 0]x + [1] = match#(f(X()),x)
     
     check#(x) = [3 0]x + [2] >= [0] = start#(match(f(X()),x))
     
     match#(f(x),f(y)) = [6 0]y + [4] >= [3 0]y + [1] = match#(x,y)
     
     match#(f(x),f(y)) = [6 0]y + [4] >= [4 0]y + [2] = f#(match(x,y))
     
     match#(X(),x) = [3 0]x + [1] >= [3 0]x = proper#(x)
     
     proper#(f(x)) = [6 0]x + [3] >= [3 0]x = proper#(x)
     
     proper#(f(x)) = [6 0]x + [3] >= [4 0]x + [2] = f#(proper(x))
     
     f#(ok(x)) = [4 0]x + [2] >= [2 0]x = f#(x)
     
     f#(found(x)) = [4 2]x + [2] >= [2 0]x = f#(x)
     
     top#(found(x)) = [2 2]x + [2] >= [2 0]x + [1] = active#(x)
     
     top#(found(x)) = [2 2]x + [2] >= [2 2]x + [1] = top#(active(x))
     
     active#(f(x)) = [4 0]x + [3] >= [2 0]x + [1] = active#(x)
     
     active#(f(x)) = [4 0]x + [3] >= [4 0]x = f#(active(x))
     
     f#(mark(x)) = [6 0]x + [4] >= [2 0]x = f#(x)
     
                   [4 0]    [3]    [4 0]    [3]              
     check(f(x)) = [0 0]x + [0] >= [0 0]x + [0] = f(check(x))
     
                [2 0]    [1]    [2 0]    [1]                         
     check(x) = [0 0]x + [0] >= [0 0]x + [0] = start(match(f(X()),x))
     
                [4 0]    [3]    [4 0]    [3]           
     f(ok(x)) = [0 0]x + [0] >= [0 0]x + [0] = ok(f(x))
     
                   [4 2]    [3]    [4 0]    [3]              
     f(found(x)) = [0 0]x + [0] >= [0 0]x + [0] = found(f(x))
     
                  [6 0]    [5]    [6 0]    [5]             
     f(mark(x)) = [0 0]x + [0] >= [0 0]x + [0] = mark(f(x))
     
                    [2 2]    [1]    [2 1]    [1]           
     start(ok(x)) = [0 1]x + [0] >= [0 1]x + [0] = found(x)
     
                        [4 0]    [3]    [4 0]    [3]                
     match(f(x),f(y)) = [0 0]y + [0] >= [0 0]y + [0] = f(match(x,y))
     
                    [2 0]    [1]    [2 0]    [1]            
     match(X(),x) = [0 0]x + [4] >= [0 0]x + [2] = proper(x)
     
                   [1]    [1]          
     proper(c()) = [2] >= [2] = ok(c())
     
                    [4 0]    [3]    [4 0]    [3]               
     proper(f(x)) = [0 0]x + [2] >= [0 0]x + [0] = f(proper(x))
     
                    [4 0]    [2]    [3 0]    [2]          
     active(f(x)) = [0 0]x + [0] >= [0 0]x + [0] = mark(x)
     
                    [4 0]    [2]    [4 0]    [1]               
     active(f(x)) = [0 0]x + [0] >= [0 0]x + [0] = f(active(x))
    problem:
     DPs:
      
     TRS:
      check(f(x)) -> f(check(x))
      check(x) -> start(match(f(X()),x))
      f(ok(x)) -> ok(f(x))
      f(found(x)) -> found(f(x))
      f(mark(x)) -> mark(f(x))
      start(ok(x)) -> found(x)
      match(f(x),f(y)) -> f(match(x,y))
      match(X(),x) -> proper(x)
      proper(c()) -> ok(c())
      proper(f(x)) -> f(proper(x))
      active(f(x)) -> mark(x)
      active(f(x)) -> f(active(x))
    Qed