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)))
  Matrix Interpretation Processor: dim=2
   
   interpretation:
    [g#](x0, x1) = [1 1]x0 + [2 0]x1,
    
    [if#](x0, x1, x2) = [1 0]x0 + [1 0]x1,
    
    [f#](x0) = [0 1]x0 + [2],
    
                  [0 0]     [1 0]  
    [g](x0, x1) = [0 1]x0 + [0 0]x1,
    
              [2 0]     [2]
    [c](x0) = [0 0]x0 + [0],
    
                       [0 0]     [0 2]     [0 1]  
    [if](x0, x1, x2) = [0 1]x0 + [3 1]x1 + [0 2]x2,
    
              [0 0]     [0]
    [s](x0) = [1 1]x0 + [2],
    
              [0]
    [false] = [0],
    
          [2]
    [1] = [2],
    
             [0]
    [true] = [1],
    
              [1 1]     [1]
    [f](x0) = [0 0]x0 + [1],
    
          [3]
    [0] = [1]
   orientation:
    f#(s(x)) = [1 1]x + [4] >= [0 1]x + [2] = f#(x)
    
    g#(x,c(y)) = [1 1]x + [4 0]y + [4] >= [1 1]x + [2 0]y = g#(x,y)
    
    g#(x,c(y)) = [1 1]x + [4 0]y + [4] >= [1 1]x + [2 0]y + [2] = g#(s(x),y)
    
    g#(x,c(y)) = [1 1]x + [4 0]y + [4] >= [0 1]x + [2] = f#(x)
    
    g#(x,c(y)) = [1 1]x + [4 0]y + [4] >= [1 1]x + [2 0]y + [3] = if#(f(x),c(g(s(x),y)),c(y))
    
    g#(x,c(y)) = [1 1]x + [4 0]y + [4] >= [1 1]x = g#(x,if(f(x),c(g(s(x),y)),c(y)))
    
             [5]    [0]         
    f(0()) = [1] >= [1] = true()
    
             [5]    [0]          
    f(1()) = [1] >= [0] = false()
    
              [1 1]    [3]    [1 1]    [1]       
    f(s(x)) = [0 0]x + [1] >= [0 0]x + [1] = f(x)
    
                           [2 2]    [1 1]    [6]    [0 0]    [0]       
    if(true(),s(x),s(y)) = [1 1]x + [2 2]y + [7] >= [1 1]x + [2] = s(x)
    
                            [2 2]    [1 1]    [6]    [0 0]    [0]       
    if(false(),s(x),s(y)) = [1 1]x + [2 2]y + [6] >= [1 1]y + [2] = s(y)
    
                [0 0]    [2 0]    [2]    [2 0]    [2]            
    g(x,c(y)) = [0 1]x + [0 0]y + [0] >= [0 0]y + [0] = c(g(x,y))
    
                [0 0]    [2 0]    [2]    [0 0]                                   
    g(x,c(y)) = [0 1]x + [0 0]y + [0] >= [0 1]x = g(x,if(f(x),c(g(s(x),y)),c(y)))
   problem:
    DPs:
     
    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)))
   Qed