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))
  TDG 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)) -> f#(proper(x))
    proper#(f(x)) -> proper#(x) -> proper#(f(x)) -> proper#(x)
    proper#(f(x)) -> f#(proper(x)) -> f#(mark(x)) -> f#(x)
    proper#(f(x)) -> f#(proper(x)) -> f#(found(x)) -> f#(x)
    proper#(f(x)) -> f#(proper(x)) -> f#(ok(x)) -> f#(x)
    match#(X(),x) -> proper#(x) -> proper#(f(x)) -> f#(proper(x))
    match#(X(),x) -> proper#(x) -> proper#(f(x)) -> proper#(x)
    match#(f(x),f(y)) -> match#(x,y) -> match#(X(),x) -> proper#(x)
    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#(f(x),f(y)) -> match#(x,y)
    match#(f(x),f(y)) -> f#(match(x,y)) -> f#(mark(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#(ok(x)) -> f#(x)
    f#(found(x)) -> f#(x) -> f#(mark(x)) -> f#(x)
    f#(found(x)) -> f#(x) -> f#(found(x)) -> f#(x)
    f#(found(x)) -> f#(x) -> f#(ok(x)) -> f#(x)
    f#(ok(x)) -> f#(x) -> f#(mark(x)) -> f#(x)
    f#(ok(x)) -> f#(x) -> f#(found(x)) -> f#(x)
    f#(ok(x)) -> f#(x) -> f#(ok(x)) -> f#(x)
    f#(mark(x)) -> f#(x) -> f#(mark(x)) -> f#(x)
    f#(mark(x)) -> f#(x) -> f#(found(x)) -> f#(x)
    f#(mark(x)) -> f#(x) -> f#(ok(x)) -> f#(x)
    check#(f(x)) -> f#(check(x)) -> f#(mark(x)) -> f#(x)
    check#(f(x)) -> f#(check(x)) -> f#(found(x)) -> f#(x)
    check#(f(x)) -> f#(check(x)) -> f#(ok(x)) -> f#(x)
    check#(f(x)) -> check#(x) -> check#(x) -> start#(match(f(X()),x))
    check#(f(x)) -> check#(x) -> check#(x) -> match#(f(X()),x)
    check#(f(x)) -> check#(x) -> check#(x) -> f#(X())
    check#(f(x)) -> check#(x) -> check#(f(x)) -> f#(check(x))
    check#(f(x)) -> check#(x) -> check#(f(x)) -> check#(x)
    check#(x) -> match#(f(X()),x) -> match#(X(),x) -> proper#(x)
    check#(x) -> match#(f(X()),x) ->
    match#(f(x),f(y)) -> f#(match(x,y))
    check#(x) -> match#(f(X()),x) -> match#(f(x),f(y)) -> match#(x,y)
    check#(x) -> f#(X()) -> f#(mark(x)) -> f#(x)
    check#(x) -> f#(X()) -> f#(found(x)) -> f#(x)
    check#(x) -> f#(X()) -> f#(ok(x)) -> f#(x)
    top#(found(x)) -> top#(active(x)) ->
    top#(found(x)) -> top#(active(x))
    top#(found(x)) -> top#(active(x)) ->
    top#(found(x)) -> active#(x)
    top#(found(x)) -> top#(active(x)) ->
    top#(mark(x)) -> top#(check(x))
    top#(found(x)) -> top#(active(x)) ->
    top#(mark(x)) -> check#(x)
    top#(found(x)) -> top#(active(x)) ->
    top#(active(c())) -> top#(mark(c()))
    top#(found(x)) -> active#(x) -> active#(f(x)) -> f#(active(x))
    top#(found(x)) -> active#(x) -> active#(f(x)) -> active#(x)
    top#(mark(x)) -> check#(x) -> check#(x) -> start#(match(f(X()),x))
    top#(mark(x)) -> check#(x) -> check#(x) -> match#(f(X()),x)
    top#(mark(x)) -> check#(x) -> check#(x) -> f#(X())
    top#(mark(x)) -> check#(x) -> check#(f(x)) -> f#(check(x))
    top#(mark(x)) -> check#(x) -> check#(f(x)) -> check#(x)
    top#(mark(x)) -> top#(check(x)) ->
    top#(found(x)) -> top#(active(x))
    top#(mark(x)) -> top#(check(x)) -> top#(found(x)) -> active#(x)
    top#(mark(x)) -> top#(check(x)) ->
    top#(mark(x)) -> top#(check(x))
    top#(mark(x)) -> top#(check(x)) -> top#(mark(x)) -> check#(x)
    top#(mark(x)) -> top#(check(x)) ->
    top#(active(c())) -> top#(mark(c()))
    top#(active(c())) -> top#(mark(c())) ->
    top#(found(x)) -> top#(active(x))
    top#(active(c())) -> top#(mark(c())) ->
    top#(found(x)) -> active#(x)
    top#(active(c())) -> top#(mark(c())) ->
    top#(mark(x)) -> top#(check(x))
    top#(active(c())) -> top#(mark(c())) ->
    top#(mark(x)) -> check#(x)
    top#(active(c())) -> top#(mark(c())) ->
    top#(active(c())) -> top#(mark(c()))
    active#(f(x)) -> f#(active(x)) -> f#(mark(x)) -> f#(x)
    active#(f(x)) -> f#(active(x)) -> f#(found(x)) -> f#(x)
    active#(f(x)) -> f#(active(x)) -> f#(ok(x)) -> f#(x)
    active#(f(x)) -> active#(x) -> active#(f(x)) -> f#(active(x))
    active#(f(x)) -> active#(x) -> active#(f(x)) -> active#(x)
   SCC Processor:
    #sccs: 6
    #rules: 10
    #arcs: 63/400
    DPs:
     top#(found(x)) -> top#(active(x))
     top#(active(c())) -> top#(mark(c()))
     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))
    EDG Processor:
     DPs:
      top#(found(x)) -> top#(active(x))
      top#(active(c())) -> top#(mark(c()))
      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))
     graph:
      top#(found(x)) -> top#(active(x)) ->
      top#(active(c())) -> top#(mark(c()))
      top#(found(x)) -> top#(active(x)) ->
      top#(mark(x)) -> top#(check(x))
      top#(found(x)) -> top#(active(x)) ->
      top#(found(x)) -> top#(active(x))
      top#(mark(x)) -> top#(check(x)) ->
      top#(mark(x)) -> top#(check(x))
      top#(mark(x)) -> top#(check(x)) ->
      top#(found(x)) -> top#(active(x))
      top#(active(c())) -> top#(mark(c())) -> top#(mark(x)) -> top#(check(x))
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [top#](x0) = x0 + 1,
       
       [found](x0) = x0 + 0,
       
       [ok](x0) = x0 + 0,
       
       [proper](x0) = 5,
       
       [start](x0) = x0 + 0,
       
       [match](x0, x1) = x0 + 0,
       
       [X] = 5,
       
       [check](x0) = 4,
       
       [top](x0) = x0 + 0,
       
       [c] = 5,
       
       [mark](x0) = 4,
       
       [active](x0) = x0 + 0,
       
       [f](x0) = 4
      orientation:
       top#(found(x)) = x + 1 >= x + 1 = top#(active(x))
       
       top#(active(c())) = 5 >= 4 = top#(mark(c()))
       
       top#(mark(x)) = 4 >= 4 = top#(check(x))
       
       active(f(x)) = 4 >= 4 = mark(x)
       
       top(active(c())) = 5 >= 4 = top(mark(c()))
       
       top(mark(x)) = 4 >= 4 = top(check(x))
       
       check(f(x)) = 4 >= 4 = f(check(x))
       
       check(x) = 4 >= 4 = start(match(f(X()),x))
       
       match(f(x),f(y)) = 4 >= 4 = f(match(x,y))
       
       match(X(),x) = 5 >= 5 = proper(x)
       
       proper(c()) = 5 >= 5 = ok(c())
       
       proper(f(x)) = 5 >= 4 = f(proper(x))
       
       f(ok(x)) = 4 >= 4 = ok(f(x))
       
       start(ok(x)) = x + 0 >= x + 0 = found(x)
       
       f(found(x)) = 4 >= 4 = found(f(x))
       
       top(found(x)) = x + 0 >= x + 0 = top(active(x))
       
       active(f(x)) = 4 >= 4 = f(active(x))
       
       f(mark(x)) = 4 >= 4 = 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))
      KBO Processor:
       argument filtering:
        pi(f) = [0]
        pi(active) = 0
        pi(mark) = [0]
        pi(c) = []
        pi(top) = []
        pi(check) = [0]
        pi(X) = []
        pi(match) = 1
        pi(start) = 0
        pi(proper) = 0
        pi(ok) = 0
        pi(found) = 0
        pi(top#) = 0
       weight function:
        w0 = 1
        w(top#) = w(proper) = w(X) = w(top) = w(c) = w(mark) = w(f) = 1
        w(found) = w(ok) = w(start) = w(match) = w(check) = w(active) = 0
       precedence:
        X ~ check ~ top ~ c > f > top# ~ found ~ ok ~ proper ~ start ~ match ~ mark ~ active
       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))
       KBO Processor:
        argument filtering:
         pi(f) = 0
         pi(active) = 0
         pi(mark) = 0
         pi(c) = []
         pi(top) = []
         pi(check) = [0]
         pi(X) = []
         pi(match) = 1
         pi(start) = [0]
         pi(proper) = 0
         pi(ok) = 0
         pi(found) = [0]
         pi(top#) = 0
        weight function:
         w0 = 1
         w(top#) = w(start) = w(match) = w(X) = w(check) = w(top) = w(
         c) = w(active) = w(f) = 1
         w(found) = w(ok) = w(proper) = w(mark) = 0
        precedence:
         mark ~ f > found ~ top ~ c > check > top# ~ ok ~ proper ~ start ~ match ~ X ~ active
        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#(ok(x)) -> f#(x)
     f#(found(x)) -> f#(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))
    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