YES

Problem:
 a__f(X) -> a__if(mark(X),c(),f(true()))
 a__if(true(),X,Y) -> mark(X)
 a__if(false(),X,Y) -> mark(Y)
 mark(f(X)) -> a__f(mark(X))
 mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
 mark(c()) -> c()
 mark(true()) -> true()
 mark(false()) -> false()
 a__f(X) -> f(X)
 a__if(X1,X2,X3) -> if(X1,X2,X3)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [if](x0, x1, x2) = x0 + 2x1 + x2,
   
   [false] = 4,
   
   [a__if](x0, x1, x2) = x0 + 2x1 + x2,
   
   [f](x0) = 4x0,
   
   [true] = 0,
   
   [c] = 0,
   
   [mark](x0) = x0,
   
   [a__f](x0) = 4x0
  orientation:
   a__f(X) = 4X >= X = a__if(mark(X),c(),f(true()))
   
   a__if(true(),X,Y) = 2X + Y >= X = mark(X)
   
   a__if(false(),X,Y) = 2X + Y + 4 >= Y = mark(Y)
   
   mark(f(X)) = 4X >= 4X = a__f(mark(X))
   
   mark(if(X1,X2,X3)) = X1 + 2X2 + X3 >= X1 + 2X2 + X3 = a__if(mark(X1),mark(X2),X3)
   
   mark(c()) = 0 >= 0 = c()
   
   mark(true()) = 0 >= 0 = true()
   
   mark(false()) = 4 >= 4 = false()
   
   a__f(X) = 4X >= 4X = f(X)
   
   a__if(X1,X2,X3) = X1 + 2X2 + X3 >= X1 + 2X2 + X3 = if(X1,X2,X3)
  problem:
   a__f(X) -> a__if(mark(X),c(),f(true()))
   a__if(true(),X,Y) -> mark(X)
   mark(f(X)) -> a__f(mark(X))
   mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
   mark(c()) -> c()
   mark(true()) -> true()
   mark(false()) -> false()
   a__f(X) -> f(X)
   a__if(X1,X2,X3) -> if(X1,X2,X3)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [if](x0, x1, x2) = x0 + 3x1 + 2x2,
    
    [false] = 1,
    
    [a__if](x0, x1, x2) = x0 + 3x1 + 4x2,
    
    [f](x0) = 2x0,
    
    [true] = 0,
    
    [c] = 0,
    
    [mark](x0) = 2x0,
    
    [a__f](x0) = 2x0
   orientation:
    a__f(X) = 2X >= 2X = a__if(mark(X),c(),f(true()))
    
    a__if(true(),X,Y) = 3X + 4Y >= 2X = mark(X)
    
    mark(f(X)) = 4X >= 4X = a__f(mark(X))
    
    mark(if(X1,X2,X3)) = 2X1 + 6X2 + 4X3 >= 2X1 + 6X2 + 4X3 = a__if(mark(X1),mark(X2),X3)
    
    mark(c()) = 0 >= 0 = c()
    
    mark(true()) = 0 >= 0 = true()
    
    mark(false()) = 2 >= 1 = false()
    
    a__f(X) = 2X >= 2X = f(X)
    
    a__if(X1,X2,X3) = X1 + 3X2 + 4X3 >= X1 + 3X2 + 2X3 = if(X1,X2,X3)
   problem:
    a__f(X) -> a__if(mark(X),c(),f(true()))
    a__if(true(),X,Y) -> mark(X)
    mark(f(X)) -> a__f(mark(X))
    mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
    mark(c()) -> c()
    mark(true()) -> true()
    a__f(X) -> f(X)
    a__if(X1,X2,X3) -> if(X1,X2,X3)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [if](x0, x1, x2) = x0 + 4x1 + x2,
     
     [a__if](x0, x1, x2) = x0 + 4x1 + x2,
     
     [f](x0) = 3x0 + 1,
     
     [true] = 0,
     
     [c] = 0,
     
     [mark](x0) = 2x0,
     
     [a__f](x0) = 3x0 + 1
    orientation:
     a__f(X) = 3X + 1 >= 2X + 1 = a__if(mark(X),c(),f(true()))
     
     a__if(true(),X,Y) = 4X + Y >= 2X = mark(X)
     
     mark(f(X)) = 6X + 2 >= 6X + 1 = a__f(mark(X))
     
     mark(if(X1,X2,X3)) = 2X1 + 8X2 + 2X3 >= 2X1 + 8X2 + X3 = a__if(mark(X1),mark(X2),X3)
     
     mark(c()) = 0 >= 0 = c()
     
     mark(true()) = 0 >= 0 = true()
     
     a__f(X) = 3X + 1 >= 3X + 1 = f(X)
     
     a__if(X1,X2,X3) = X1 + 4X2 + X3 >= X1 + 4X2 + X3 = if(X1,X2,X3)
    problem:
     a__f(X) -> a__if(mark(X),c(),f(true()))
     a__if(true(),X,Y) -> mark(X)
     mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
     mark(c()) -> c()
     mark(true()) -> true()
     a__f(X) -> f(X)
     a__if(X1,X2,X3) -> if(X1,X2,X3)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [if](x0, x1, x2) = x0 + 4x1 + x2 + 1,
      
      [a__if](x0, x1, x2) = x0 + 4x1 + x2 + 2,
      
      [f](x0) = x0 + 1,
      
      [true] = 4,
      
      [c] = 0,
      
      [mark](x0) = 2x0,
      
      [a__f](x0) = 2x0 + 7
     orientation:
      a__f(X) = 2X + 7 >= 2X + 7 = a__if(mark(X),c(),f(true()))
      
      a__if(true(),X,Y) = 4X + Y + 6 >= 2X = mark(X)
      
      mark(if(X1,X2,X3)) = 2X1 + 8X2 + 2X3 + 2 >= 2X1 + 8X2 + X3 + 2 = a__if(mark(X1),mark(X2),X3)
      
      mark(c()) = 0 >= 0 = c()
      
      mark(true()) = 8 >= 4 = true()
      
      a__f(X) = 2X + 7 >= X + 1 = f(X)
      
      a__if(X1,X2,X3) = X1 + 4X2 + X3 + 2 >= X1 + 4X2 + X3 + 1 = if(X1,X2,X3)
     problem:
      a__f(X) -> a__if(mark(X),c(),f(true()))
      mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
      mark(c()) -> c()
     Matrix Interpretation Processor: dim=3
      
      interpretation:
                          [1 0 1]     [1 0 1]     [1 0 0]     [1]
       [if](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
                          [0 0 0]     [0 0 0]     [0 0 0]     [0],
       
                             [1 0 1]     [1 0 1]     [1 0 0]  
       [a__if](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
                             [0 0 0]     [0 0 0]     [0 0 0]  ,
       
                 [1 0 0]     [0]
       [f](x0) = [0 0 0]x0 + [1]
                 [0 0 0]     [0],
       
                [0]
       [true] = [0]
                [0],
       
             [0]
       [c] = [0]
             [0],
       
                    [1 0 0]  
       [mark](x0) = [0 0 0]x0
                    [0 0 1]  ,
       
                    [1 0 1]     [1]
       [a__f](x0) = [1 0 1]x0 + [0]
                    [0 0 0]     [0]
      orientation:
                 [1 0 1]    [1]    [1 0 1]                                
       a__f(X) = [1 0 1]X + [0] >= [0 0 0]X = a__if(mark(X),c(),f(true()))
                 [0 0 0]    [0]    [0 0 0]                                
       
                            [1 0 1]     [1 0 1]     [1 0 0]     [1]    [1 0 1]     [1 0 1]     [1 0 0]                                
       mark(if(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = a__if(mark(X1),mark(X2),X3)
                            [0 0 0]     [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0 0 0]                                
       
                   [0]    [0]      
       mark(c()) = [0] >= [0] = c()
                   [0]    [0]      
      problem:
       mark(c()) -> c()
      Matrix Interpretation Processor: dim=3
       
       interpretation:
              [0]
        [c] = [0]
              [0],
        
                     [1 0 0]     [1]
        [mark](x0) = [0 0 0]x0 + [0]
                     [0 0 0]     [0]
       orientation:
                    [1]    [0]      
        mark(c()) = [0] >= [0] = c()
                    [0]    [0]      
       problem:
        
       Qed