YES(?,O(n^1))
3.25/1.51	YES(?,O(n^1))
3.25/1.52	
3.25/1.52	Problem:
3.25/1.52	 f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x))))
3.25/1.52	 f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x))
3.25/1.52	
3.25/1.52	Proof:
3.25/1.52	 Uncurry Processor:
3.25/1.52	  a1(b1(a1(x))) -> a1(b1(b1(a1(x))))
3.25/1.52	  b1(b1(b1(x))) -> b1(b1(x))
3.25/1.52	  f(a(),x1) -> a1(x1)
3.25/1.52	  f(b(),x1) -> b1(x1)
3.25/1.52	  Complexity Transformation Processor:
3.25/1.52	   strict:
3.25/1.52	    a1(b1(a1(x))) -> a1(b1(b1(a1(x))))
3.25/1.52	    b1(b1(b1(x))) -> b1(b1(x))
3.25/1.52	    f(a(),x1) -> a1(x1)
3.25/1.52	    f(b(),x1) -> b1(x1)
3.25/1.52	   weak:
3.25/1.52	    
3.25/1.52	   Matrix Interpretation Processor: dim=1
3.25/1.52	    
3.25/1.52	    max_matrix:
3.25/1.52	     1
3.25/1.52	    interpretation:
3.25/1.52	     [b1](x0) = x0,
3.25/1.52	     
3.25/1.52	     [a1](x0) = x0,
3.25/1.52	     
3.25/1.52	     [f](x0, x1) = x0 + x1 + 13,
3.25/1.52	     
3.25/1.52	     [b] = 6,
3.25/1.52	     
3.25/1.52	     [a] = 6
3.25/1.52	    orientation:
3.25/1.52	     a1(b1(a1(x))) = x >= x = a1(b1(b1(a1(x))))
3.25/1.52	     
3.25/1.52	     b1(b1(b1(x))) = x >= x = b1(b1(x))
3.25/1.52	     
3.25/1.52	     f(a(),x1) = x1 + 19 >= x1 = a1(x1)
3.25/1.52	     
3.25/1.52	     f(b(),x1) = x1 + 19 >= x1 = b1(x1)
3.25/1.52	    problem:
3.25/1.52	     strict:
3.25/1.52	      a1(b1(a1(x))) -> a1(b1(b1(a1(x))))
3.25/1.52	      b1(b1(b1(x))) -> b1(b1(x))
3.25/1.52	     weak:
3.25/1.52	      f(a(),x1) -> a1(x1)
3.25/1.52	      f(b(),x1) -> b1(x1)
3.25/1.52	    Matrix Interpretation Processor: dim=1
3.25/1.52	     
3.25/1.52	     max_matrix:
3.25/1.52	      1
3.25/1.52	     interpretation:
3.25/1.52	      [b1](x0) = x0 + 33,
3.25/1.52	      
3.25/1.52	      [a1](x0) = x0 + 142,
3.25/1.52	      
3.25/1.52	      [f](x0, x1) = x0 + x1 + 31,
3.25/1.52	      
3.25/1.52	      [b] = 2,
3.25/1.52	      
3.25/1.52	      [a] = 111
3.25/1.52	     orientation:
3.25/1.52	      a1(b1(a1(x))) = x + 317 >= x + 350 = a1(b1(b1(a1(x))))
3.25/1.52	      
3.25/1.52	      b1(b1(b1(x))) = x + 99 >= x + 66 = b1(b1(x))
3.25/1.52	      
3.25/1.52	      f(a(),x1) = x1 + 142 >= x1 + 142 = a1(x1)
3.25/1.52	      
3.25/1.52	      f(b(),x1) = x1 + 33 >= x1 + 33 = b1(x1)
3.25/1.52	     problem:
3.25/1.52	      strict:
3.25/1.52	       a1(b1(a1(x))) -> a1(b1(b1(a1(x))))
3.25/1.52	      weak:
3.25/1.52	       b1(b1(b1(x))) -> b1(b1(x))
3.25/1.52	       f(a(),x1) -> a1(x1)
3.25/1.52	       f(b(),x1) -> b1(x1)
3.25/1.52	     Matrix Interpretation Processor: dim=5
3.25/1.52	      
3.25/1.52	      max_matrix:
3.25/1.52	       [1 1 1 0 0]
3.25/1.52	       [0 0 1 0 1]
3.25/1.52	       [0 0 0 0 0]
3.25/1.52	       [0 0 0 0 0]
3.25/1.52	       [0 0 0 0 0]
3.25/1.52	      interpretation:
3.25/1.52	                  [1 0 1 0 0]  
3.25/1.52	                  [0 0 0 0 1]  
3.25/1.52	       [b1](x0) = [0 0 0 0 0]x0
3.25/1.52	                  [0 0 0 0 0]  
3.25/1.52	                  [0 0 0 0 0]  ,
3.25/1.52	       
3.25/1.52	                  [1 1 1 0 0]     [0]
3.25/1.52	                  [0 0 1 0 1]     [0]
3.25/1.52	       [a1](x0) = [0 0 0 0 0]x0 + [0]
3.25/1.52	                  [0 0 0 0 0]     [0]
3.25/1.52	                  [0 0 0 0 0]     [1],
3.25/1.52	       
3.25/1.52	                     [1 1 1 0 0]     [1 1 1 0 0]     [0]
3.25/1.52	                     [0 0 1 0 1]     [0 0 1 0 1]     [0]
3.25/1.52	       [f](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [0]
3.25/1.52	                     [0 0 0 0 0]     [0 0 0 0 0]     [0]
3.25/1.52	                     [0 0 0 0 0]     [0 0 0 0 0]     [1],
3.25/1.52	       
3.25/1.52	             [0]
3.25/1.52	             [0]
3.25/1.52	       [b] = [0]
3.25/1.52	             [0]
3.25/1.52	             [0],
3.25/1.52	       
3.25/1.52	             [0]
3.25/1.52	             [0]
3.25/1.52	       [a] = [0]
3.25/1.52	             [0]
3.25/1.52	             [0]
3.25/1.52	      orientation:
3.25/1.52	                       [1 1 1 0 0]    [1]    [1 1 1 0 0]    [0]                    
3.25/1.52	                       [0 0 0 0 0]    [0]    [0 0 0 0 0]    [0]                    
3.25/1.52	       a1(b1(a1(x))) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x + [0] = a1(b1(b1(a1(x))))
3.25/1.52	                       [0 0 0 0 0]    [0]    [0 0 0 0 0]    [0]                    
3.25/1.52	                       [0 0 0 0 0]    [1]    [0 0 0 0 0]    [1]                    
3.25/1.52	       
3.25/1.52	                       [1 0 1 0 0]     [1 0 1 0 0]             
3.25/1.52	                       [0 0 0 0 0]     [0 0 0 0 0]             
3.25/1.52	       b1(b1(b1(x))) = [0 0 0 0 0]x >= [0 0 0 0 0]x = b1(b1(x))
3.25/1.52	                       [0 0 0 0 0]     [0 0 0 0 0]             
3.25/1.52	                       [0 0 0 0 0]     [0 0 0 0 0]             
3.25/1.52	       
3.25/1.52	                   [1 1 1 0 0]     [0]    [1 1 1 0 0]     [0]         
3.25/1.52	                   [0 0 1 0 1]     [0]    [0 0 1 0 1]     [0]         
3.25/1.52	       f(a(),x1) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = a1(x1)
3.25/1.52	                   [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]         
3.25/1.52	                   [0 0 0 0 0]     [1]    [0 0 0 0 0]     [1]         
3.25/1.52	       
3.25/1.52	                   [1 1 1 0 0]     [0]    [1 0 1 0 0]           
3.25/1.52	                   [0 0 1 0 1]     [0]    [0 0 0 0 1]           
3.25/1.52	       f(b(),x1) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = b1(x1)
3.25/1.52	                   [0 0 0 0 0]     [0]    [0 0 0 0 0]           
3.25/1.52	                   [0 0 0 0 0]     [1]    [0 0 0 0 0]           
3.25/1.52	      problem:
3.25/1.52	       strict:
3.25/1.52	        
3.25/1.52	       weak:
3.25/1.52	        a1(b1(a1(x))) -> a1(b1(b1(a1(x))))
3.25/1.52	        b1(b1(b1(x))) -> b1(b1(x))
3.25/1.52	        f(a(),x1) -> a1(x1)
3.25/1.52	        f(b(),x1) -> b1(x1)
3.25/1.52	      Qed
3.25/1.53	EOF