YES(?,O(n^1))
0.16/0.30	YES(?,O(n^1))
0.16/0.30	
0.16/0.30	Problem:
0.16/0.30	 a(a(a(x1))) -> b(b(x1))
0.16/0.30	 b(b(b(x1))) -> c(x1)
0.16/0.30	 c(x1) -> d(d(x1))
0.16/0.30	 d(x1) -> a(a(x1))
0.16/0.30	
0.16/0.30	Proof:
0.16/0.30	 Complexity Transformation Processor:
0.16/0.30	  strict:
0.16/0.30	   a(a(a(x1))) -> b(b(x1))
0.16/0.30	   b(b(b(x1))) -> c(x1)
0.16/0.30	   c(x1) -> d(d(x1))
0.16/0.30	   d(x1) -> a(a(x1))
0.16/0.30	  weak:
0.16/0.30	   
0.16/0.30	  Matrix Interpretation Processor: dim=1
0.16/0.30	   
0.16/0.30	   max_matrix:
0.16/0.30	    1
0.16/0.30	   interpretation:
0.16/0.30	    [d](x0) = x0 + 128,
0.16/0.30	    
0.16/0.30	    [c](x0) = x0,
0.16/0.30	    
0.16/0.30	    [b](x0) = x0 + 162,
0.16/0.30	    
0.16/0.30	    [a](x0) = x0
0.16/0.30	   orientation:
0.16/0.30	    a(a(a(x1))) = x1 >= x1 + 324 = b(b(x1))
0.16/0.30	    
0.16/0.30	    b(b(b(x1))) = x1 + 486 >= x1 = c(x1)
0.16/0.30	    
0.16/0.30	    c(x1) = x1 >= x1 + 256 = d(d(x1))
0.16/0.30	    
0.16/0.30	    d(x1) = x1 + 128 >= x1 = a(a(x1))
0.16/0.30	   problem:
0.16/0.30	    strict:
0.16/0.30	     a(a(a(x1))) -> b(b(x1))
0.16/0.30	     c(x1) -> d(d(x1))
0.16/0.30	    weak:
0.16/0.30	     b(b(b(x1))) -> c(x1)
0.16/0.30	     d(x1) -> a(a(x1))
0.16/0.30	   Matrix Interpretation Processor: dim=1
0.16/0.30	    
0.16/0.30	    max_matrix:
0.16/0.30	     1
0.16/0.30	    interpretation:
0.16/0.30	     [d](x0) = x0 + 76,
0.16/0.30	     
0.16/0.30	     [c](x0) = x0 + 153,
0.16/0.30	     
0.16/0.30	     [b](x0) = x0 + 129,
0.16/0.30	     
0.16/0.30	     [a](x0) = x0 + 38
0.16/0.30	    orientation:
0.16/0.30	     a(a(a(x1))) = x1 + 114 >= x1 + 258 = b(b(x1))
0.16/0.30	     
0.16/0.30	     c(x1) = x1 + 153 >= x1 + 152 = d(d(x1))
0.16/0.30	     
0.16/0.30	     b(b(b(x1))) = x1 + 387 >= x1 + 153 = c(x1)
0.16/0.30	     
0.16/0.30	     d(x1) = x1 + 76 >= x1 + 76 = a(a(x1))
0.16/0.30	    problem:
0.16/0.30	     strict:
0.16/0.30	      a(a(a(x1))) -> b(b(x1))
0.16/0.30	     weak:
0.16/0.30	      c(x1) -> d(d(x1))
0.16/0.30	      b(b(b(x1))) -> c(x1)
0.16/0.30	      d(x1) -> a(a(x1))
0.16/0.30	    Matrix Interpretation Processor: dim=1
0.16/0.30	     
0.16/0.30	     max_matrix:
0.16/0.30	      1
0.16/0.30	     interpretation:
0.16/0.30	      [d](x0) = x0 + 15,
0.16/0.30	      
0.16/0.30	      [c](x0) = x0 + 30,
0.16/0.30	      
0.16/0.30	      [b](x0) = x0 + 10,
0.16/0.30	      
0.16/0.30	      [a](x0) = x0 + 7
0.16/0.30	     orientation:
0.16/0.30	      a(a(a(x1))) = x1 + 21 >= x1 + 20 = b(b(x1))
0.16/0.30	      
0.16/0.30	      c(x1) = x1 + 30 >= x1 + 30 = d(d(x1))
0.16/0.30	      
0.16/0.30	      b(b(b(x1))) = x1 + 30 >= x1 + 30 = c(x1)
0.16/0.30	      
0.16/0.30	      d(x1) = x1 + 15 >= x1 + 14 = a(a(x1))
0.16/0.30	     problem:
0.16/0.30	      strict:
0.16/0.30	       
0.16/0.30	      weak:
0.16/0.30	       a(a(a(x1))) -> b(b(x1))
0.16/0.30	       c(x1) -> d(d(x1))
0.16/0.30	       b(b(b(x1))) -> c(x1)
0.16/0.30	       d(x1) -> a(a(x1))
0.16/0.30	     Qed
0.16/0.31	EOF