YES
Time: 0.014456
TRS:
 {            f 0() -> true(),
              f 1() -> false(),
              f s x -> f x,
   if(true(), x, y) -> x,
  if(false(), x, y) -> y,
          g(x, c y) -> g(x, g(s c y, y)),
        g(s x, s y) -> if(f x, s x, s y)}
 DP:
  DP:
   {      f# s x -> f# x,
      g#(x, c y) -> g#(x, g(s c y, y)),
      g#(x, c y) -> g#(s c y, y),
    g#(s x, s y) -> f# x,
    g#(s x, s y) -> if#(f x, s x, s y)}
  TRS:
  {            f 0() -> true(),
               f 1() -> false(),
               f s x -> f x,
    if(true(), x, y) -> x,
   if(false(), x, y) -> y,
           g(x, c y) -> g(x, g(s c y, y)),
         g(s x, s y) -> if(f x, s x, s y)}
  UR:
   {            f 0() -> true(),
                f 1() -> false(),
                f s x -> f x,
     if(true(), x, y) -> x,
    if(false(), x, y) -> y,
            g(x, c y) -> g(x, g(s c y, y)),
          g(s x, s y) -> if(f x, s x, s y)}
   EDG:
    {(g#(x, c y) -> g#(s c y, y), g#(s x, s y) -> if#(f x, s x, s y))
     (g#(x, c y) -> g#(s c y, y), g#(s x, s y) -> f# x)
     (g#(x, c y) -> g#(s c y, y), g#(x, c y) -> g#(s c y, y))
     (g#(x, c y) -> g#(s c y, y), g#(x, c y) -> g#(x, g(s c y, y)))
     (f# s x -> f# x, f# s x -> f# x)
     (g#(s x, s y) -> f# x, f# s x -> f# x)
     (g#(x, c y) -> g#(x, g(s c y, y)), g#(x, c y) -> g#(x, g(s c y, y)))
     (g#(x, c y) -> g#(x, g(s c y, y)), g#(x, c y) -> g#(s c y, y))
     (g#(x, c y) -> g#(x, g(s c y, y)), g#(s x, s y) -> f# x)
     (g#(x, c y) -> g#(x, g(s c y, y)), g#(s x, s y) -> if#(f x, s x, s y))}
    STATUS:
     arrows: 0.600000
     SCCS (2):
      Scc:
       {g#(x, c y) -> g#(x, g(s c y, y)),
        g#(x, c y) -> g#(s c y, y)}
      Scc:
       {f# s x -> f# x}
      
      SCC (2):
       Strict:
        {g#(x, c y) -> g#(x, g(s c y, y)),
         g#(x, c y) -> g#(s c y, y)}
       Weak:
       {            f 0() -> true(),
                    f 1() -> false(),
                    f s x -> f x,
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
                g(x, c y) -> g(x, g(s c y, y)),
              g(s x, s y) -> if(f x, s x, s y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2) = x0 + x1,
         
         [g](x0, x1) = 0,
         
         [f](x0) = 0,
         
         [s](x0) = 0,
         
         [c](x0) = x0 + 1,
         
         [true] = 0,
         
         [0] = 0,
         
         [false] = 0,
         
         [1] = 0,
         
         [g#](x0, x1) = x0
        Strict:
         g#(x, c y) -> g#(s c y, y)
         1 + 0x + 1y >= 0 + 1y
         g#(x, c y) -> g#(x, g(s c y, y))
         1 + 0x + 1y >= 0 + 0x + 0y
        Weak:
         g(s x, s y) -> if(f x, s x, s y)
         0 + 0x + 0y >= 0 + 0x + 0y
         g(x, c y) -> g(x, g(s c y, y))
         0 + 0x + 0y >= 0 + 0x + 0y
         if(false(), x, y) -> y
         0 + 1x + 1y >= 1y
         if(true(), x, y) -> x
         0 + 1x + 1y >= 1x
         f s x -> f x
         0 + 0x >= 0 + 0x
         f 1() -> false()
         0 >= 0
         f 0() -> true()
         0 >= 0
       Qed
     
     
     SCC (1):
      Strict:
       {f# s x -> f# x}
      Weak:
      {            f 0() -> true(),
                   f 1() -> false(),
                   f s x -> f x,
        if(true(), x, y) -> x,
       if(false(), x, y) -> y,
               g(x, c y) -> g(x, g(s c y, y)),
             g(s x, s y) -> if(f x, s x, s y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2) = x0 + x1 + 1,
        
        [g](x0, x1) = x0 + 1,
        
        [f](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [c](x0) = 1,
        
        [true] = 1,
        
        [0] = 0,
        
        [false] = 1,
        
        [1] = 0,
        
        [f#](x0) = x0
       Strict:
        f# s x -> f# x
        1 + 1x >= 0 + 1x
       Weak:
        g(s x, s y) -> if(f x, s x, s y)
        2 + 1x + 0y >= 2 + 1x + 0y
        g(x, c y) -> g(x, g(s c y, y))
        1 + 1x + 0y >= 1 + 1x + 0y
        if(false(), x, y) -> y
        2 + 1x + 0y >= 1y
        if(true(), x, y) -> x
        2 + 1x + 0y >= 1x
        f s x -> f x
        0 + 0x >= 0 + 0x
        f 1() -> false()
        0 >= 1
        f 0() -> true()
        0 >= 1
      Qed