YES
Time: 0.033752
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())
    (mark# g X -> mark# X, mark# g X -> mark# X)
    (mark# g X -> mark# X, mark# f X -> a__f# X)}
   STATUS:
    arrows: 0.666667
    SCCS (1):
     Scc:
      {mark# g X -> mark# X}
     
     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