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))
  Matrix Interpretation Processor: dim=2
   
   interpretation:
    [proper#](x0) = [0 3]x0,
    
    [start#](x0) = [0],
    
    [match#](x0, x1) = [0 3]x1 + [1],
    
    [f#](x0) = [0 2]x0,
    
    [check#](x0) = [0 3]x0 + [2],
    
    [top#](x0) = [2 1]x0 + [1],
    
    [active#](x0) = [0 2]x0 + [1],
    
                  [1 0]     [0]
    [found](x0) = [2 2]x0 + [1],
    
               [1 0]     [0]
    [ok](x0) = [0 2]x0 + [1],
    
                   [0 0]     [1]
    [proper](x0) = [0 2]x0 + [1],
    
                  [1 0]  
    [start](x0) = [2 1]x0,
    
                      [2 0]     [0 0]     [0]
    [match](x0, x1) = [0 0]x0 + [0 2]x1 + [1],
    
          [2]
    [X] = [0],
    
                  [0 0]     [0]
    [check](x0) = [0 2]x0 + [1],
    
                [1 1]     [2]
    [top](x0) = [0 0]x0 + [1],
    
          [1]
    [c] = [0],
    
                 [0 0]     [0]
    [mark](x0) = [0 3]x0 + [2],
    
                   [2 0]  
    [active](x0) = [0 2]x0,
    
              [0 0]     [0]
    [f](x0) = [0 2]x0 + [1]
   orientation:
    top#(active(c())) = 5 >= 3 = top#(mark(c()))
    
    top#(mark(x)) = [0 3]x + [3] >= [0 3]x + [2] = check#(x)
    
    top#(mark(x)) = [0 3]x + [3] >= [0 2]x + [2] = top#(check(x))
    
    check#(f(x)) = [0 6]x + [5] >= [0 3]x + [2] = check#(x)
    
    check#(f(x)) = [0 6]x + [5] >= [0 4]x + [2] = f#(check(x))
    
    check#(x) = [0 3]x + [2] >= [0] = f#(X())
    
    check#(x) = [0 3]x + [2] >= [0 3]x + [1] = match#(f(X()),x)
    
    check#(x) = [0 3]x + [2] >= [0] = start#(match(f(X()),x))
    
    match#(f(x),f(y)) = [0 6]y + [4] >= [0 3]y + [1] = match#(x,y)
    
    match#(f(x),f(y)) = [0 6]y + [4] >= [0 4]y + [2] = f#(match(x,y))
    
    match#(X(),x) = [0 3]x + [1] >= [0 3]x = proper#(x)
    
    proper#(f(x)) = [0 6]x + [3] >= [0 3]x = proper#(x)
    
    proper#(f(x)) = [0 6]x + [3] >= [0 4]x + [2] = f#(proper(x))
    
    f#(ok(x)) = [0 4]x + [2] >= [0 2]x = f#(x)
    
    f#(found(x)) = [4 4]x + [2] >= [0 2]x = f#(x)
    
    top#(found(x)) = [4 2]x + [2] >= [0 2]x + [1] = active#(x)
    
    top#(found(x)) = [4 2]x + [2] >= [4 2]x + [1] = top#(active(x))
    
    active#(f(x)) = [0 4]x + [3] >= [0 2]x + [1] = active#(x)
    
    active#(f(x)) = [0 4]x + [3] >= [0 4]x = f#(active(x))
    
    f#(mark(x)) = [0 6]x + [4] >= [0 2]x = f#(x)
    
                   [0 0]    [0]    [0 0]    [0]          
    active(f(x)) = [0 4]x + [2] >= [0 3]x + [2] = mark(x)
    
                       [4]    [4]                 
    top(active(c())) = [1] >= [1] = top(mark(c()))
    
                   [0 3]    [4]    [0 2]    [3]                
    top(mark(x)) = [0 0]x + [1] >= [0 0]x + [1] = top(check(x))
    
                  [0 0]    [0]    [0 0]    [0]              
    check(f(x)) = [0 4]x + [3] >= [0 4]x + [3] = f(check(x))
    
               [0 0]    [0]    [0 0]    [0]                         
    check(x) = [0 2]x + [1] >= [0 2]x + [1] = start(match(f(X()),x))
    
                       [0 0]    [0]    [0 0]    [0]                
    match(f(x),f(y)) = [0 4]y + [3] >= [0 4]y + [3] = f(match(x,y))
    
                   [0 0]    [4]    [0 0]    [1]            
    match(X(),x) = [0 2]x + [1] >= [0 2]x + [1] = proper(x)
    
                  [1]    [1]          
    proper(c()) = [1] >= [1] = ok(c())
    
                   [0 0]    [1]    [0 0]    [0]               
    proper(f(x)) = [0 4]x + [3] >= [0 4]x + [3] = f(proper(x))
    
               [0 0]    [0]    [0 0]    [0]           
    f(ok(x)) = [0 4]x + [3] >= [0 4]x + [3] = ok(f(x))
    
                   [1 0]    [0]    [1 0]    [0]           
    start(ok(x)) = [2 2]x + [1] >= [2 2]x + [1] = found(x)
    
                  [0 0]    [0]    [0 0]    [0]              
    f(found(x)) = [4 4]x + [3] >= [0 4]x + [3] = found(f(x))
    
                    [3 2]    [3]    [2 2]    [2]                 
    top(found(x)) = [0 0]x + [1] >= [0 0]x + [1] = top(active(x))
    
                   [0 0]    [0]    [0 0]    [0]               
    active(f(x)) = [0 4]x + [2] >= [0 4]x + [1] = f(active(x))
    
                 [0 0]    [0]    [0 0]    [0]             
    f(mark(x)) = [0 6]x + [5] >= [0 6]x + [5] = mark(f(x))
   problem:
    DPs:
     
    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))
   Qed