YES

Problem:
 f(0()) -> true()
 f(1()) -> false()
 f(s(x)) -> f(x)
 if(true(),s(x),s(y)) -> s(x)
 if(false(),s(x),s(y)) -> s(y)
 g(x,c(y)) -> c(g(x,y))
 g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))

Proof:
 DP Processor:
  DPs:
   f#(s(x)) -> f#(x)
   g#(x,c(y)) -> g#(x,y)
   g#(x,c(y)) -> g#(s(x),y)
   g#(x,c(y)) -> f#(x)
   g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
   g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
  TRS:
   f(0()) -> true()
   f(1()) -> false()
   f(s(x)) -> f(x)
   if(true(),s(x),s(y)) -> s(x)
   if(false(),s(x),s(y)) -> s(y)
   g(x,c(y)) -> c(g(x,y))
   g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
  Usable Rule Processor:
   DPs:
    f#(s(x)) -> f#(x)
    g#(x,c(y)) -> g#(x,y)
    g#(x,c(y)) -> g#(s(x),y)
    g#(x,c(y)) -> f#(x)
    g#(x,c(y)) -> if#(f(x),c(g(s(x),y)),c(y))
    g#(x,c(y)) -> g#(x,if(f(x),c(g(s(x),y)),c(y)))
   TRS:
    g(x,c(y)) -> c(g(x,y))
    g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
    f(0()) -> true()
    f(1()) -> false()
    f(s(x)) -> f(x)
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     f(0()) -> true()
     f(1()) -> false()
     f(s(x)) -> f(x)
    interpretation:
     [g#](x0, x1) = 2x0 + 3x1,
     
     [if#](x0, x1, x2) = 2x0 + 2,
     
     [f#](x0) = 2x0,
     
     [g](x0, x1) = 2x0 + 6,
     
     [c](x0) = 2x0 + 3,
     
     [if](x0, x1, x2) = 0,
     
     [s](x0) = x0 + 1,
     
     [false] = 1,
     
     [1] = 1,
     
     [true] = 0,
     
     [f](x0) = x0,
     
     [0] = 1
    orientation:
     f#(s(x)) = 2x + 2 >= 2x = f#(x)
     
     g#(x,c(y)) = 2x + 6y + 9 >= 2x + 3y = g#(x,y)
     
     g#(x,c(y)) = 2x + 6y + 9 >= 2x + 3y + 2 = g#(s(x),y)
     
     g#(x,c(y)) = 2x + 6y + 9 >= 2x = f#(x)
     
     g#(x,c(y)) = 2x + 6y + 9 >= 2x + 2 = if#(f(x),c(g(s(x),y)),c(y))
     
     g#(x,c(y)) = 2x + 6y + 9 >= 2x = g#(x,if(f(x),c(g(s(x),y)),c(y)))
     
     g(x,c(y)) = 2x + 6 >= 4x + 15 = c(g(x,y))
     
     g(x,c(y)) = 2x + 6 >= 2x + 6 = g(x,if(f(x),c(g(s(x),y)),c(y)))
     
     f(0()) = 1 >= 0 = true()
     
     f(1()) = 1 >= 1 = false()
     
     f(s(x)) = x + 1 >= x = f(x)
    problem:
     DPs:
      
     TRS:
      g(x,c(y)) -> c(g(x,y))
      g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))
      f(0()) -> true()
      f(1()) -> false()
      f(s(x)) -> f(x)
    Qed