YES
Time: 0.014970
TRS:
 {    a__f X -> f X,
  a__f f a() -> a__f g f a(),
    mark g X -> g mark X,
    mark f X -> a__f X,
    mark a() -> a()}
 DP:
  DP:
   {a__f# f a() -> a__f# g f a(),
      mark# g X -> mark# X,
      mark# f X -> a__f# X}
  TRS:
  {    a__f X -> f X,
   a__f f a() -> a__f g f a(),
     mark g X -> g mark X,
     mark f X -> a__f X,
     mark a() -> a()}
  EDG:
   {(mark# f X -> a__f# X, a__f# f a() -> a__f# g f a())
    (a__f# f a() -> a__f# g f a(), a__f# f a() -> a__f# g f a())
    (mark# g X -> mark# X, mark# g X -> mark# X)
    (mark# g X -> mark# X, mark# f X -> a__f# X)}
   STATUS:
    arrows: 0.555556
    SCCS (2):
     Scc:
      {mark# g X -> mark# X}
     Scc:
      {a__f# f a() -> a__f# g f a()}
     
     SCC (1):
      Strict:
       {mark# g X -> mark# X}
      Weak:
      {    a__f X -> f X,
       a__f f a() -> a__f g f a(),
         mark g X -> g mark X,
         mark f X -> a__f X,
         mark a() -> a()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [a__f](x0) = 0,
        
        [g](x0) = x0 + 1,
        
        [f](x0) = 0,
        
        [mark](x0) = x0 + 1,
        
        [a] = 0,
        
        [mark#](x0) = x0 + 1
       Strict:
        mark# g X -> mark# X
        2 + 1X >= 1 + 1X
       Weak:
        mark a() -> a()
        1 >= 0
        mark f X -> a__f X
        1 + 0X >= 0 + 0X
        mark g X -> g mark X
        2 + 1X >= 2 + 1X
        a__f f a() -> a__f g f a()
        0 >= 0
        a__f X -> f X
        0 + 0X >= 0 + 0X
      Qed
    
    SCC (1):
     Strict:
      {a__f# f a() -> a__f# g f a()}
     Weak:
     {    a__f X -> f X,
      a__f f a() -> a__f g f a(),
        mark g X -> g mark X,
        mark f X -> a__f X,
        mark a() -> a()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [a__f](x0) = x0 + 1,
       
       [g](x0) = 0,
       
       [f](x0) = x0,
       
       [mark](x0) = 0,
       
       [a] = 1,
       
       [a__f#](x0) = x0 + 1
      Strict:
       a__f# f a() -> a__f# g f a()
       2 >= 1
      Weak:
       mark a() -> a()
       0 >= 1
       mark f X -> a__f X
       0 + 0X >= 1 + 1X
       mark g X -> g mark X
       0 + 0X >= 0 + 0X
       a__f f a() -> a__f g f a()
       2 >= 1
       a__f X -> f X
       1 + 1X >= 0 + 1X
     Qed