MAYBE

Problem:
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 -(x,0()) -> x
 -(s(x),s(y)) -> -(x,y)
 if(0(),y,z) -> y
 if(s(x),y,z) -> z
 half(double(x)) -> x

Proof:
 RT Transformation Processor:
  strict:
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
   -(x,0()) -> x
   -(s(x),s(y)) -> -(x,y)
   if(0(),y,z) -> y
   if(s(x),y,z) -> z
   half(double(x)) -> x
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [if](x0, x1, x2) = x0 + x1 + x2,
    
    [-](x0, x1) = x0 + x1 + 15,
    
    [half](x0) = x0 + 23,
    
    [s](x0) = x0 + 17,
    
    [double](x0) = x0 + 18,
    
    [0] = 21
   orientation:
    double(0()) = 39 >= 21 = 0()
    
    double(s(x)) = x + 35 >= x + 52 = s(s(double(x)))
    
    half(0()) = 44 >= 21 = 0()
    
    half(s(0())) = 61 >= 21 = 0()
    
    half(s(s(x))) = x + 57 >= x + 40 = s(half(x))
    
    -(x,0()) = x + 36 >= x = x
    
    -(s(x),s(y)) = x + y + 49 >= x + y + 15 = -(x,y)
    
    if(0(),y,z) = y + z + 21 >= y = y
    
    if(s(x),y,z) = x + y + z + 17 >= z = z
    
    half(double(x)) = x + 41 >= x = x
   problem:
    strict:
     double(s(x)) -> s(s(double(x)))
    weak:
     double(0()) -> 0()
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     if(0(),y,z) -> y
     if(s(x),y,z) -> z
     half(double(x)) -> x
   Open