MAYBE

Problem:
 tower(x) -> f(a(),x,s(0()))
 f(a(),0(),y) -> y
 f(a(),s(x),y) -> f(b(),y,s(x))
 f(b(),y,x) -> f(a(),half(x),exp(y))
 exp(0()) -> s(0())
 exp(s(x)) -> double(exp(x))
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 half(0()) -> double(0())
 half(s(0())) -> half(0())
 half(s(s(x))) -> s(half(x))

Proof:
 RT Transformation Processor:
  strict:
   tower(x) -> f(a(),x,s(0()))
   f(a(),0(),y) -> y
   f(a(),s(x),y) -> f(b(),y,s(x))
   f(b(),y,x) -> f(a(),half(x),exp(y))
   exp(0()) -> s(0())
   exp(s(x)) -> double(exp(x))
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   half(0()) -> double(0())
   half(s(0())) -> half(0())
   half(s(s(x))) -> s(half(x))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [double](x0) = x0 + 4,
    
    [exp](x0) = x0 + 8,
    
    [half](x0) = x0 + 13,
    
    [b] = 17,
    
    [f](x0, x1, x2) = x0 + x1 + x2 + 18,
    
    [s](x0) = x0 + 1,
    
    [0] = 16,
    
    [a] = 8,
    
    [tower](x0) = x0
   orientation:
    tower(x) = x >= x + 43 = f(a(),x,s(0()))
    
    f(a(),0(),y) = y + 42 >= y = y
    
    f(a(),s(x),y) = x + y + 27 >= x + y + 36 = f(b(),y,s(x))
    
    f(b(),y,x) = x + y + 35 >= x + y + 47 = f(a(),half(x),exp(y))
    
    exp(0()) = 24 >= 17 = s(0())
    
    exp(s(x)) = x + 9 >= x + 12 = double(exp(x))
    
    double(0()) = 20 >= 16 = 0()
    
    double(s(x)) = x + 5 >= x + 6 = s(s(double(x)))
    
    half(0()) = 29 >= 20 = double(0())
    
    half(s(0())) = 30 >= 29 = half(0())
    
    half(s(s(x))) = x + 15 >= x + 14 = s(half(x))
   problem:
    strict:
     tower(x) -> f(a(),x,s(0()))
     f(a(),s(x),y) -> f(b(),y,s(x))
     f(b(),y,x) -> f(a(),half(x),exp(y))
     exp(s(x)) -> double(exp(x))
     double(s(x)) -> s(s(double(x)))
    weak:
     f(a(),0(),y) -> y
     exp(0()) -> s(0())
     double(0()) -> 0()
     half(0()) -> double(0())
     half(s(0())) -> half(0())
     half(s(s(x))) -> s(half(x))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [double](x0) = x0 + 12,
     
     [exp](x0) = x0 + 24,
     
     [half](x0) = x0 + 16,
     
     [b] = 1,
     
     [f](x0, x1, x2) = x0 + x1 + x2 + 8,
     
     [s](x0) = x0 + 20,
     
     [0] = 24,
     
     [a] = 0,
     
     [tower](x0) = x0
    orientation:
     tower(x) = x >= x + 52 = f(a(),x,s(0()))
     
     f(a(),s(x),y) = x + y + 28 >= x + y + 29 = f(b(),y,s(x))
     
     f(b(),y,x) = x + y + 9 >= x + y + 48 = f(a(),half(x),exp(y))
     
     exp(s(x)) = x + 44 >= x + 36 = double(exp(x))
     
     double(s(x)) = x + 32 >= x + 52 = s(s(double(x)))
     
     f(a(),0(),y) = y + 32 >= y = y
     
     exp(0()) = 48 >= 44 = s(0())
     
     double(0()) = 36 >= 24 = 0()
     
     half(0()) = 40 >= 36 = double(0())
     
     half(s(0())) = 60 >= 40 = half(0())
     
     half(s(s(x))) = x + 56 >= x + 36 = s(half(x))
    problem:
     strict:
      tower(x) -> f(a(),x,s(0()))
      f(a(),s(x),y) -> f(b(),y,s(x))
      f(b(),y,x) -> f(a(),half(x),exp(y))
      double(s(x)) -> s(s(double(x)))
     weak:
      exp(s(x)) -> double(exp(x))
      f(a(),0(),y) -> y
      exp(0()) -> s(0())
      double(0()) -> 0()
      half(0()) -> double(0())
      half(s(0())) -> half(0())
      half(s(s(x))) -> s(half(x))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [double](x0) = x0,
      
      [exp](x0) = x0,
      
      [half](x0) = x0 + 12,
      
      [b] = 0,
      
      [f](x0, x1, x2) = x0 + x1 + x2 + 4,
      
      [s](x0) = x0,
      
      [0] = 2,
      
      [a] = 16,
      
      [tower](x0) = x0
     orientation:
      tower(x) = x >= x + 22 = f(a(),x,s(0()))
      
      f(a(),s(x),y) = x + y + 20 >= x + y + 4 = f(b(),y,s(x))
      
      f(b(),y,x) = x + y + 4 >= x + y + 32 = f(a(),half(x),exp(y))
      
      double(s(x)) = x >= x = s(s(double(x)))
      
      exp(s(x)) = x >= x = double(exp(x))
      
      f(a(),0(),y) = y + 22 >= y = y
      
      exp(0()) = 2 >= 2 = s(0())
      
      double(0()) = 2 >= 2 = 0()
      
      half(0()) = 14 >= 2 = double(0())
      
      half(s(0())) = 14 >= 14 = half(0())
      
      half(s(s(x))) = x + 12 >= x + 12 = s(half(x))
     problem:
      strict:
       tower(x) -> f(a(),x,s(0()))
       f(b(),y,x) -> f(a(),half(x),exp(y))
       double(s(x)) -> s(s(double(x)))
      weak:
       f(a(),s(x),y) -> f(b(),y,s(x))
       exp(s(x)) -> double(exp(x))
       f(a(),0(),y) -> y
       exp(0()) -> s(0())
       double(0()) -> 0()
       half(0()) -> double(0())
       half(s(0())) -> half(0())
       half(s(s(x))) -> s(half(x))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [double](x0) = x0,
       
       [exp](x0) = x0,
       
       [half](x0) = x0,
       
       [b] = 0,
       
       [f](x0, x1, x2) = x0 + x1 + x2 + 3,
       
       [s](x0) = x0,
       
       [0] = 0,
       
       [a] = 0,
       
       [tower](x0) = x0 + 4
      orientation:
       tower(x) = x + 4 >= x + 3 = f(a(),x,s(0()))
       
       f(b(),y,x) = x + y + 3 >= x + y + 3 = f(a(),half(x),exp(y))
       
       double(s(x)) = x >= x = s(s(double(x)))
       
       f(a(),s(x),y) = x + y + 3 >= x + y + 3 = f(b(),y,s(x))
       
       exp(s(x)) = x >= x = double(exp(x))
       
       f(a(),0(),y) = y + 3 >= y = y
       
       exp(0()) = 0 >= 0 = s(0())
       
       double(0()) = 0 >= 0 = 0()
       
       half(0()) = 0 >= 0 = double(0())
       
       half(s(0())) = 0 >= 0 = half(0())
       
       half(s(s(x))) = x >= x = s(half(x))
      problem:
       strict:
        f(b(),y,x) -> f(a(),half(x),exp(y))
        double(s(x)) -> s(s(double(x)))
       weak:
        tower(x) -> f(a(),x,s(0()))
        f(a(),s(x),y) -> f(b(),y,s(x))
        exp(s(x)) -> double(exp(x))
        f(a(),0(),y) -> y
        exp(0()) -> s(0())
        double(0()) -> 0()
        half(0()) -> double(0())
        half(s(0())) -> half(0())
        half(s(s(x))) -> s(half(x))
      Open