YES

Problem:
 f(X) -> if(X,c(),n__f(true()))
 if(true(),X,Y) -> X
 if(false(),X,Y) -> activate(Y)
 f(X) -> n__f(X)
 activate(n__f(X)) -> f(X)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   f#(X) -> if#(X,c(),n__f(true()))
   if#(false(),X,Y) -> activate#(Y)
   activate#(n__f(X)) -> f#(X)
  TRS:
   f(X) -> if(X,c(),n__f(true()))
   if(true(),X,Y) -> X
   if(false(),X,Y) -> activate(Y)
   f(X) -> n__f(X)
   activate(n__f(X)) -> f(X)
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    f#(X) -> if#(X,c(),n__f(true()))
    if#(false(),X,Y) -> activate#(Y)
    activate#(n__f(X)) -> f#(X)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [activate#](x0) = x0 + 5,
     
     [if#](x0, x1, x2) = -6x0 + -8x1 + 1x2 + 0,
     
     [f#](x0) = -4x0 + 4,
     
     [false] = 12,
     
     [n__f](x0) = -3x0 + 0,
     
     [true] = 0,
     
     [c] = 8
    orientation:
     f#(X) = -4X + 4 >= -6X + 1 = if#(X,c(),n__f(true()))
     
     if#(false(),X,Y) = -8X + 1Y + 6 >= Y + 5 = activate#(Y)
     
     activate#(n__f(X)) = -3X + 5 >= -4X + 4 = f#(X)
    problem:
     DPs:
      
     TRS:
      
    Qed