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))
  EDG 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))
   graph:
    proper#(f(x)) -> proper#(x) -> proper#(f(x)) -> proper#(x)
    proper#(f(x)) -> proper#(x) -> proper#(f(x)) -> f#(proper(x))
    proper#(f(x)) -> f#(proper(x)) -> f#(ok(x)) -> f#(x)
    proper#(f(x)) -> f#(proper(x)) -> f#(found(x)) -> f#(x)
    proper#(f(x)) -> f#(proper(x)) -> f#(mark(x)) -> f#(x)
    match#(X(),x) -> proper#(x) -> proper#(f(x)) -> proper#(x)
    match#(X(),x) -> proper#(x) -> proper#(f(x)) -> f#(proper(x))
    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#(f(x),f(y)) -> f#(match(x,y))
    match#(f(x),f(y)) -> match#(x,y) ->
    match#(X(),x) -> proper#(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)
    match#(f(x),f(y)) -> f#(match(x,y)) -> 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#(found(x)) -> f#(x) -> f#(mark(x)) -> f#(x)
    f#(ok(x)) -> f#(x) -> f#(ok(x)) -> f#(x)
    f#(ok(x)) -> f#(x) -> f#(found(x)) -> f#(x)
    f#(ok(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)
    f#(mark(x)) -> f#(x) -> f#(mark(x)) -> f#(x)
    check#(f(x)) -> f#(check(x)) -> f#(ok(x)) -> f#(x)
    check#(f(x)) -> f#(check(x)) -> f#(found(x)) -> f#(x)
    check#(f(x)) -> f#(check(x)) -> f#(mark(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) -> f#(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#(x) -> match#(f(X()),x) -> match#(f(x),f(y)) -> match#(x,y)
    check#(x) -> match#(f(X()),x) ->
    match#(f(x),f(y)) -> f#(match(x,y))
    top#(found(x)) -> top#(active(x)) ->
    top#(active(c())) -> top#(mark(c()))
    top#(found(x)) -> top#(active(x)) ->
    top#(mark(x)) -> check#(x)
    top#(found(x)) -> top#(active(x)) ->
    top#(mark(x)) -> top#(check(x))
    top#(found(x)) -> top#(active(x)) ->
    top#(found(x)) -> active#(x)
    top#(found(x)) -> top#(active(x)) ->
    top#(found(x)) -> top#(active(x))
    top#(found(x)) -> active#(x) -> active#(f(x)) -> active#(x)
    top#(found(x)) -> active#(x) -> active#(f(x)) -> f#(active(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) -> f#(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)) -> top#(check(x)) -> top#(mark(x)) -> check#(x)
    top#(mark(x)) -> top#(check(x)) ->
    top#(mark(x)) -> top#(check(x))
    top#(mark(x)) -> top#(check(x)) -> top#(found(x)) -> active#(x)
    top#(mark(x)) -> top#(check(x)) ->
    top#(found(x)) -> top#(active(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)) -> f#(active(x)) -> f#(ok(x)) -> f#(x)
    active#(f(x)) -> f#(active(x)) -> f#(found(x)) -> f#(x)
    active#(f(x)) -> f#(active(x)) -> f#(mark(x)) -> f#(x)
    active#(f(x)) -> active#(x) -> active#(f(x)) -> active#(x)
    active#(f(x)) -> active#(x) -> active#(f(x)) -> f#(active(x))
   SCC Processor:
    #sccs: 6
    #rules: 10
    #arcs: 55/400
    DPs:
     top#(found(x)) -> top#(active(x))
     top#(mark(x)) -> top#(check(x))
     top#(active(c())) -> top#(mark(c()))
    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:
     dimension: 1
     interpretation:
      [top#](x0) = x0,
      
      [found](x0) = x0,
      
      [ok](x0) = x0,
      
      [proper](x0) = 1,
      
      [start](x0) = x0,
      
      [match](x0, x1) = x0,
      
      [X] = 1,
      
      [check](x0) = 0,
      
      [top](x0) = 1,
      
      [c] = 1,
      
      [mark](x0) = 0,
      
      [active](x0) = x0,
      
      [f](x0) = 0
     orientation:
      top#(found(x)) = x >= x = top#(active(x))
      
      top#(mark(x)) = 0 >= 0 = top#(check(x))
      
      top#(active(c())) = 1 >= 0 = top#(mark(c()))
      
      active(f(x)) = 0 >= 0 = mark(x)
      
      top(active(c())) = 1 >= 1 = top(mark(c()))
      
      top(mark(x)) = 1 >= 1 = top(check(x))
      
      check(f(x)) = 0 >= 0 = f(check(x))
      
      check(x) = 0 >= 0 = start(match(f(X()),x))
      
      match(f(x),f(y)) = 0 >= 0 = f(match(x,y))
      
      match(X(),x) = 1 >= 1 = proper(x)
      
      proper(c()) = 1 >= 1 = ok(c())
      
      proper(f(x)) = 1 >= 0 = f(proper(x))
      
      f(ok(x)) = 0 >= 0 = ok(f(x))
      
      start(ok(x)) = x >= x = found(x)
      
      f(found(x)) = 0 >= 0 = found(f(x))
      
      top(found(x)) = 1 >= 1 = top(active(x))
      
      active(f(x)) = 0 >= 0 = f(active(x))
      
      f(mark(x)) = 0 >= 0 = mark(f(x))
     problem:
      DPs:
       top#(found(x)) -> top#(active(x))
       top#(mark(x)) -> top#(check(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:
      dimension: 1
      interpretation:
       [top#](x0) = x0,
       
       [found](x0) = x0,
       
       [ok](x0) = x0,
       
       [proper](x0) = x0,
       
       [start](x0) = x0,
       
       [match](x0, x1) = x1,
       
       [X] = 0,
       
       [check](x0) = x0,
       
       [top](x0) = 0,
       
       [c] = 1,
       
       [mark](x0) = x0 + 1,
       
       [active](x0) = x0,
       
       [f](x0) = x0 + 1
      orientation:
       top#(found(x)) = x >= x = top#(active(x))
       
       top#(mark(x)) = x + 1 >= x = top#(check(x))
       
       active(f(x)) = x + 1 >= x + 1 = mark(x)
       
       top(active(c())) = 0 >= 0 = top(mark(c()))
       
       top(mark(x)) = 0 >= 0 = top(check(x))
       
       check(f(x)) = x + 1 >= x + 1 = f(check(x))
       
       check(x) = x >= x = start(match(f(X()),x))
       
       match(f(x),f(y)) = y + 1 >= y + 1 = f(match(x,y))
       
       match(X(),x) = x >= x = proper(x)
       
       proper(c()) = 1 >= 1 = ok(c())
       
       proper(f(x)) = x + 1 >= x + 1 = f(proper(x))
       
       f(ok(x)) = x + 1 >= x + 1 = ok(f(x))
       
       start(ok(x)) = x >= x = found(x)
       
       f(found(x)) = x + 1 >= x + 1 = found(f(x))
       
       top(found(x)) = 0 >= 0 = top(active(x))
       
       active(f(x)) = x + 1 >= x + 1 = f(active(x))
       
       f(mark(x)) = x + 2 >= x + 2 = mark(f(x))
      problem:
       DPs:
        top#(found(x)) -> top#(active(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:
       dimension: 1
       interpretation:
        [top#](x0) = x0,
        
        [found](x0) = 1,
        
        [ok](x0) = 0,
        
        [proper](x0) = 0,
        
        [start](x0) = 1,
        
        [match](x0, x1) = 0,
        
        [X] = 0,
        
        [check](x0) = 1,
        
        [top](x0) = 0,
        
        [c] = 0,
        
        [mark](x0) = 0,
        
        [active](x0) = 0,
        
        [f](x0) = x0
       orientation:
        top#(found(x)) = 1 >= 0 = top#(active(x))
        
        active(f(x)) = 0 >= 0 = mark(x)
        
        top(active(c())) = 0 >= 0 = top(mark(c()))
        
        top(mark(x)) = 0 >= 0 = top(check(x))
        
        check(f(x)) = 1 >= 1 = f(check(x))
        
        check(x) = 1 >= 1 = start(match(f(X()),x))
        
        match(f(x),f(y)) = 0 >= 0 = f(match(x,y))
        
        match(X(),x) = 0 >= 0 = proper(x)
        
        proper(c()) = 0 >= 0 = ok(c())
        
        proper(f(x)) = 0 >= 0 = f(proper(x))
        
        f(ok(x)) = 0 >= 0 = ok(f(x))
        
        start(ok(x)) = 1 >= 1 = found(x)
        
        f(found(x)) = 1 >= 1 = found(f(x))
        
        top(found(x)) = 0 >= 0 = top(active(x))
        
        active(f(x)) = 0 >= 0 = f(active(x))
        
        f(mark(x)) = 0 >= 0 = 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
    
    DPs:
     active#(f(x)) -> active#(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))
    Subterm Criterion Processor:
     simple projection:
      pi(active#) = 0
     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
    
    DPs:
     check#(f(x)) -> check#(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))
    Subterm Criterion Processor:
     simple projection:
      pi(check#) = 0
     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
    
    DPs:
     match#(f(x),f(y)) -> match#(x,y)
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(match#) = 1
     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
    
    DPs:
     proper#(f(x)) -> proper#(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))
    Subterm Criterion Processor:
     simple projection:
      pi(proper#) = 0
     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
    
    DPs:
     f#(mark(x)) -> f#(x)
     f#(found(x)) -> f#(x)
     f#(ok(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))
    Subterm Criterion Processor:
     simple projection:
      pi(f#) = 0
     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