YES(?,O(n^3))
156.43/76.06	YES(?,O(n^3))
156.43/76.07	
156.43/76.07	Problem:
156.43/76.07	 b(x,y) -> c(a(c(y),a(0(),x)))
156.43/76.07	 a(y,x) -> y
156.43/76.07	 a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
156.43/76.07	
156.43/76.07	Proof:
156.43/76.07	 Complexity Transformation Processor:
156.43/76.07	  strict:
156.43/76.07	   b(x,y) -> c(a(c(y),a(0(),x)))
156.43/76.07	   a(y,x) -> y
156.43/76.07	   a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
156.43/76.07	  weak:
156.43/76.07	   
156.43/76.07	  Matrix Interpretation Processor: dim=1
156.43/76.07	   
156.43/76.07	   max_matrix:
156.43/76.07	    1
156.43/76.07	   interpretation:
156.43/76.07	    [a](x0, x1) = x0 + x1 + 3,
156.43/76.07	    
156.43/76.07	    [0] = 0,
156.43/76.07	    
156.43/76.07	    [c](x0) = x0 + 5,
156.43/76.07	    
156.43/76.07	    [b](x0, x1) = x0 + x1
156.43/76.07	   orientation:
156.43/76.07	    b(x,y) = x + y >= x + y + 16 = c(a(c(y),a(0(),x)))
156.43/76.07	    
156.43/76.07	    a(y,x) = x + y + 3 >= y = y
156.43/76.07	    
156.43/76.07	    a(y,c(b(a(0(),x),0()))) = x + y + 11 >= x + y + 8 = b(a(c(b(0(),y)),x),0())
156.43/76.07	   problem:
156.43/76.07	    strict:
156.43/76.07	     b(x,y) -> c(a(c(y),a(0(),x)))
156.43/76.07	    weak:
156.43/76.07	     a(y,x) -> y
156.43/76.07	     a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
156.43/76.07	   Matrix Interpretation Processor: dim=3
156.43/76.07	    
156.43/76.07	    max_matrix:
156.43/76.07	     [1 1 0]
156.43/76.07	     [0 1 1]
156.43/76.07	     [0 0 1]
156.43/76.07	    interpretation:
156.43/76.07	                   [1 1 0]     [1 0 0]     [0]
156.43/76.07	     [a](x0, x1) = [0 1 1]x0 + [0 0 0]x1 + [0]
156.43/76.07	                   [0 0 1]     [0 0 1]     [2],
156.43/76.07	     
156.43/76.07	           [0]
156.43/76.07	     [0] = [0]
156.43/76.07	           [2],
156.43/76.07	     
156.43/76.07	               [1 1 0]  
156.43/76.07	     [c](x0) = [0 0 0]x0
156.43/76.07	               [0 0 0]  ,
156.43/76.07	     
156.43/76.07	                   [1 0 0]     [1 1 0]     [1]
156.43/76.07	     [b](x0, x1) = [0 1 0]x0 + [0 0 0]x1 + [0]
156.43/76.07	                   [0 0 0]     [0 0 0]     [2]
156.43/76.07	    orientation:
156.43/76.07	              [1 0 0]    [1 1 0]    [1]    [1 0 0]    [1 1 0]                       
156.43/76.07	     b(x,y) = [0 1 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y = c(a(c(y),a(0(),x)))
156.43/76.07	              [0 0 0]    [0 0 0]    [2]    [0 0 0]    [0 0 0]                       
156.43/76.07	     
156.43/76.07	              [1 0 0]    [1 1 0]    [0]         
156.43/76.07	     a(y,x) = [0 0 0]x + [0 1 1]y + [0] >= y = y
156.43/76.07	              [0 0 1]    [0 0 1]    [2]         
156.43/76.07	     
156.43/76.07	                               [1 0 0]    [1 1 0]    [3]    [1 0 0]    [1 1 0]    [2]                          
156.43/76.07	     a(y,c(b(a(0(),x),0()))) = [0 0 0]x + [0 1 1]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = b(a(c(b(0(),y)),x),0())
156.43/76.07	                               [0 0 0]    [0 0 1]    [2]    [0 0 0]    [0 0 0]    [2]                          
156.43/76.07	    problem:
156.43/76.07	     strict:
156.43/76.07	      
156.43/76.07	     weak:
156.43/76.07	      b(x,y) -> c(a(c(y),a(0(),x)))
156.43/76.07	      a(y,x) -> y
156.43/76.07	      a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
156.43/76.07	    Qed
156.43/76.07	EOF