YES

Problem:
 foldr_f[3](NilF()) -> 0()
 foldr_f[3](ConsF(plus_x(x2),x1)) -> comp_f_g[1](plus_x(x2),rec[foldr_0][3](x1))
 rec[foldr_0][3](NilF()) -> id()
 rec[foldr_0][3](ConsF(plus_x(x2),x1)) -> comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
 comp_f_g[1](plus_x(x3),comp_f_g(plus_x(x2),x1)) -> plus_x[1](x3,comp_f_g[1](plus_x(x2),x1))
 comp_f_g[1](plus_x(x7),id()) -> plus_x[1](x7,0())
 rec[mapF_0][2](Nil()) -> NilF()
 rec[mapF_0][2](Cons(x20,x14)) -> ConsF(plus_x(x20),rec[mapF_0][2](x14))
 plus_x[1](0(),x9) -> x9
 plus_x[1](S(x10),x4) -> S(plus_x[1](x10,x4))
 main(x7) -> foldr_f[3](rec[mapF_0][2](x7))

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [main](x0) = x0,
   
   [S](x0) = x0,
   
   [Cons](x0, x1) = x0 + x1 + 5,
   
   [rec[mapF_0][2]](x0) = x0,
   
   [Nil] = 0,
   
   [plus_x[1]](x0, x1) = x0 + x1 + 5,
   
   [comp_f_g](x0, x1) = x0 + x1 + 3,
   
   [id] = 3,
   
   [comp_f_g[1]](x0, x1) = x0 + x1,
   
   [rec[foldr_0][3]](x0) = x0 + 3,
   
   [ConsF](x0, x1) = x0 + x1 + 3,
   
   [plus_x](x0) = x0 + 2,
   
   [0] = 0,
   
   [foldr_f[3]](x0) = x0,
   
   [NilF] = 0
  orientation:
   foldr_f[3](NilF()) = 0 >= 0 = 0()
   
   foldr_f[3](ConsF(plus_x(x2),x1)) = x1 + x2 + 5 >= x1 + x2 + 5 = comp_f_g[1](plus_x(x2),rec[foldr_0][3](x1))
   
   rec[foldr_0][3](NilF()) = 3 >= 3 = id()
   
   rec[foldr_0][3](ConsF(plus_x(x2),x1)) = x1 + x2 + 8 >= x1 + x2 + 8 = comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
   
   comp_f_g[1](plus_x(x3),comp_f_g(plus_x(x2),x1)) = x1 + x2 + x3 + 7 >= x1 + x2 + x3 + 7 = plus_x[1](x3,comp_f_g[1](plus_x(x2),x1))
   
   comp_f_g[1](plus_x(x7),id()) = x7 + 5 >= x7 + 5 = plus_x[1](x7,0())
   
   rec[mapF_0][2](Nil()) = 0 >= 0 = NilF()
   
   rec[mapF_0][2](Cons(x20,x14)) = x14 + x20 + 5 >= x14 + x20 + 5 = ConsF(plus_x(x20),rec[mapF_0][2](x14))
   
   plus_x[1](0(),x9) = x9 + 5 >= x9 = x9
   
   plus_x[1](S(x10),x4) = x10 + x4 + 5 >= x10 + x4 + 5 = S(plus_x[1](x10,x4))
   
   main(x7) = x7 >= x7 = foldr_f[3](rec[mapF_0][2](x7))
  problem:
   foldr_f[3](NilF()) -> 0()
   foldr_f[3](ConsF(plus_x(x2),x1)) -> comp_f_g[1](plus_x(x2),rec[foldr_0][3](x1))
   rec[foldr_0][3](NilF()) -> id()
   rec[foldr_0][3](ConsF(plus_x(x2),x1)) -> comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
   comp_f_g[1](plus_x(x3),comp_f_g(plus_x(x2),x1)) -> plus_x[1](x3,comp_f_g[1](plus_x(x2),x1))
   comp_f_g[1](plus_x(x7),id()) -> plus_x[1](x7,0())
   rec[mapF_0][2](Nil()) -> NilF()
   rec[mapF_0][2](Cons(x20,x14)) -> ConsF(plus_x(x20),rec[mapF_0][2](x14))
   plus_x[1](S(x10),x4) -> S(plus_x[1](x10,x4))
   main(x7) -> foldr_f[3](rec[mapF_0][2](x7))
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [main](x0) = 4x0 + 7,
    
    [S](x0) = x0,
    
    [Cons](x0, x1) = x0 + 4x1 + 6,
    
    [rec[mapF_0][2]](x0) = x0,
    
    [Nil] = 0,
    
    [plus_x[1]](x0, x1) = x0 + x1 + 1,
    
    [comp_f_g](x0, x1) = x0 + x1,
    
    [id] = 0,
    
    [comp_f_g[1]](x0, x1) = 2x0 + 2x1 + 5,
    
    [rec[foldr_0][3]](x0) = x0 + 2,
    
    [ConsF](x0, x1) = x0 + x1,
    
    [plus_x](x0) = x0 + 1,
    
    [0] = 6,
    
    [foldr_f[3]](x0) = 4x0 + 7,
    
    [NilF] = 0
   orientation:
    foldr_f[3](NilF()) = 7 >= 6 = 0()
    
    foldr_f[3](ConsF(plus_x(x2),x1)) = 4x1 + 4x2 + 11 >= 2x1 + 2x2 + 11 = comp_f_g[1](plus_x(x2),rec[foldr_0][3](x1))
    
    rec[foldr_0][3](NilF()) = 2 >= 0 = id()
    
    rec[foldr_0][3](ConsF(plus_x(x2),x1)) = x1 + x2 + 3 >= x1 + x2 + 3 = comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
    
    comp_f_g[1](plus_x(x3),comp_f_g(plus_x(x2),x1)) = 2x1 + 2x2 + 2x3 + 9 >= 2x1 + 2x2 + x3 + 8 = plus_x[1](x3,comp_f_g[1](plus_x(x2),x1))
    
    comp_f_g[1](plus_x(x7),id()) = 2x7 + 7 >= x7 + 7 = plus_x[1](x7,0())
    
    rec[mapF_0][2](Nil()) = 0 >= 0 = NilF()
    
    rec[mapF_0][2](Cons(x20,x14)) = 4x14 + x20 + 6 >= x14 + x20 + 1 = ConsF(plus_x(x20),rec[mapF_0][2](x14))
    
    plus_x[1](S(x10),x4) = x10 + x4 + 1 >= x10 + x4 + 1 = S(plus_x[1](x10,x4))
    
    main(x7) = 4x7 + 7 >= 4x7 + 7 = foldr_f[3](rec[mapF_0][2](x7))
   problem:
    foldr_f[3](ConsF(plus_x(x2),x1)) -> comp_f_g[1](plus_x(x2),rec[foldr_0][3](x1))
    rec[foldr_0][3](ConsF(plus_x(x2),x1)) -> comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
    comp_f_g[1](plus_x(x7),id()) -> plus_x[1](x7,0())
    rec[mapF_0][2](Nil()) -> NilF()
    plus_x[1](S(x10),x4) -> S(plus_x[1](x10,x4))
    main(x7) -> foldr_f[3](rec[mapF_0][2](x7))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [main](x0) = x0 + 1,
     
     [S](x0) = x0,
     
     [rec[mapF_0][2]](x0) = x0,
     
     [Nil] = 0,
     
     [plus_x[1]](x0, x1) = x0 + x1 + 5,
     
     [comp_f_g](x0, x1) = x0 + x1 + 6,
     
     [id] = 0,
     
     [comp_f_g[1]](x0, x1) = x0 + x1 + 3,
     
     [rec[foldr_0][3]](x0) = x0 + 3,
     
     [ConsF](x0, x1) = x0 + x1 + 6,
     
     [plus_x](x0) = x0 + 6,
     
     [0] = 4,
     
     [foldr_f[3]](x0) = x0,
     
     [NilF] = 0
    orientation:
     foldr_f[3](ConsF(plus_x(x2),x1)) = x1 + x2 + 12 >= x1 + x2 + 12 = comp_f_g[1](plus_x(x2),rec[foldr_0][3](x1))
     
     rec[foldr_0][3](ConsF(plus_x(x2),x1)) = x1 + x2 + 15 >= x1 + x2 + 15 = comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
     
     comp_f_g[1](plus_x(x7),id()) = x7 + 9 >= x7 + 9 = plus_x[1](x7,0())
     
     rec[mapF_0][2](Nil()) = 0 >= 0 = NilF()
     
     plus_x[1](S(x10),x4) = x10 + x4 + 5 >= x10 + x4 + 5 = S(plus_x[1](x10,x4))
     
     main(x7) = x7 + 1 >= x7 = foldr_f[3](rec[mapF_0][2](x7))
    problem:
     foldr_f[3](ConsF(plus_x(x2),x1)) -> comp_f_g[1](plus_x(x2),rec[foldr_0][3](x1))
     rec[foldr_0][3](ConsF(plus_x(x2),x1)) -> comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
     comp_f_g[1](plus_x(x7),id()) -> plus_x[1](x7,0())
     rec[mapF_0][2](Nil()) -> NilF()
     plus_x[1](S(x10),x4) -> S(plus_x[1](x10,x4))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [S](x0) = x0,
      
      [rec[mapF_0][2]](x0) = x0 + 4,
      
      [Nil] = 1,
      
      [plus_x[1]](x0, x1) = 2x0 + x1 + 4,
      
      [comp_f_g](x0, x1) = 4x0 + 4x1,
      
      [id] = 0,
      
      [comp_f_g[1]](x0, x1) = 2x0 + 4x1 + 1,
      
      [rec[foldr_0][3]](x0) = 4x0 + 4,
      
      [ConsF](x0, x1) = x0 + 4x1 + 3,
      
      [plus_x](x0) = 2x0 + 2,
      
      [0] = 1,
      
      [foldr_f[3]](x0) = 4x0 + 4,
      
      [NilF] = 0
     orientation:
      foldr_f[3](ConsF(plus_x(x2),x1)) = 16x1 + 8x2 + 24 >= 16x1 + 4x2 + 21 = comp_f_g[1](plus_x(x2),rec[foldr_0][3](x1))
      
      rec[foldr_0][3](ConsF(plus_x(x2),x1)) = 16x1 + 8x2 + 24 >= 16x1 + 8x2 + 24 = comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
      
      comp_f_g[1](plus_x(x7),id()) = 4x7 + 5 >= 2x7 + 5 = plus_x[1](x7,0())
      
      rec[mapF_0][2](Nil()) = 5 >= 0 = NilF()
      
      plus_x[1](S(x10),x4) = 2x10 + x4 + 4 >= 2x10 + x4 + 4 = S(plus_x[1](x10,x4))
     problem:
      rec[foldr_0][3](ConsF(plus_x(x2),x1)) -> comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
      comp_f_g[1](plus_x(x7),id()) -> plus_x[1](x7,0())
      plus_x[1](S(x10),x4) -> S(plus_x[1](x10,x4))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [S](x0) = x0,
       
       [plus_x[1]](x0, x1) = 4x0 + x1,
       
       [comp_f_g](x0, x1) = x0 + 2x1,
       
       [id] = 5,
       
       [comp_f_g[1]](x0, x1) = x0 + x1 + 6,
       
       [rec[foldr_0][3]](x0) = x0 + 4,
       
       [ConsF](x0, x1) = 4x0 + 2x1 + 4,
       
       [plus_x](x0) = 5x0 + 5,
       
       [0] = 4
      orientation:
       rec[foldr_0][3](ConsF(plus_x(x2),x1)) = 2x1 + 20x2 + 28 >= 2x1 + 5x2 + 13 = comp_f_g(plus_x(x2),rec[foldr_0][3](x1))
       
       comp_f_g[1](plus_x(x7),id()) = 5x7 + 16 >= 4x7 + 4 = plus_x[1](x7,0())
       
       plus_x[1](S(x10),x4) = 4x10 + x4 >= 4x10 + x4 = S(plus_x[1](x10,x4))
      problem:
       plus_x[1](S(x10),x4) -> S(plus_x[1](x10,x4))
      Matrix Interpretation Processor: dim=3
       
       interpretation:
                       [0]
        [S](x0) = x0 + [1]
                       [1],
        
                              [1 1 0]     [1 0 0]  
        [plus_x[1]](x0, x1) = [1 0 1]x0 + [0 0 0]x1
                              [0 1 0]     [0 0 0]  
       orientation:
                               [1 1 0]      [1 0 0]     [1]    [1 1 0]      [1 0 0]     [0]                       
        plus_x[1](S(x10),x4) = [1 0 1]x10 + [0 0 0]x4 + [1] >= [1 0 1]x10 + [0 0 0]x4 + [1] = S(plus_x[1](x10,x4))
                               [0 1 0]      [0 0 0]     [1]    [0 1 0]      [0 0 0]     [1]                       
       problem:
        
       Qed