YES
Time: 0.010189
TRS:
 {            f X -> g n__h n__f X,
              f X -> n__f X,
              h X -> n__h X,
       activate X -> X,
  activate n__h X -> h activate X,
  activate n__f X -> f activate X}
 DP:
  DP:
   {activate# n__h X -> h# activate X,
    activate# n__h X -> activate# X,
    activate# n__f X -> f# activate X,
    activate# n__f X -> activate# X}
  TRS:
  {            f X -> g n__h n__f X,
               f X -> n__f X,
               h X -> n__h X,
        activate X -> X,
   activate n__h X -> h activate X,
   activate n__f X -> f activate X}
  UR:
   {            f X -> g n__h n__f X,
                f X -> n__f X,
                h X -> n__h X,
         activate X -> X,
    activate n__h X -> h activate X,
    activate n__f X -> f activate X}
   EDG:
    {(activate# n__f X -> activate# X, activate# n__f X -> activate# X)
     (activate# n__f X -> activate# X, activate# n__f X -> f# activate X)
     (activate# n__f X -> activate# X, activate# n__h X -> activate# X)
     (activate# n__f X -> activate# X, activate# n__h X -> h# activate X)
     (activate# n__h X -> activate# X, activate# n__h X -> h# activate X)
     (activate# n__h X -> activate# X, activate# n__h X -> activate# X)
     (activate# n__h X -> activate# X, activate# n__f X -> f# activate X)
     (activate# n__h X -> activate# X, activate# n__f X -> activate# X)}
    STATUS:
     arrows: 0.500000
     SCCS (1):
      Scc:
       {activate# n__h X -> activate# X,
        activate# n__f X -> activate# X}
      
      SCC (2):
       Strict:
        {activate# n__h X -> activate# X,
         activate# n__f X -> activate# X}
       Weak:
       {            f X -> g n__h n__f X,
                    f X -> n__f X,
                    h X -> n__h X,
             activate X -> X,
        activate n__h X -> h activate X,
        activate n__f X -> f activate X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [g](x0) = 0,
         
         [n__h](x0) = x0 + 1,
         
         [n__f](x0) = x0 + 1,
         
         [f](x0) = 0,
         
         [h](x0) = 0,
         
         [activate](x0) = x0 + 1,
         
         [activate#](x0) = x0 + 1
        Strict:
         activate# n__f X -> activate# X
         2 + 1X >= 1 + 1X
         activate# n__h X -> activate# X
         2 + 1X >= 1 + 1X
        Weak:
         activate n__f X -> f activate X
         2 + 1X >= 0 + 0X
         activate n__h X -> h activate X
         2 + 1X >= 0 + 0X
         activate X -> X
         1 + 1X >= 1X
         h X -> n__h X
         0 + 0X >= 1 + 1X
         f X -> n__f X
         0 + 0X >= 1 + 1X
         f X -> g n__h n__f X
         0 + 0X >= 0 + 0X
       Qed