YES(?,O(n^1))
0.15/0.36	YES(?,O(n^1))
0.15/0.36	
0.15/0.36	Problem:
0.15/0.36	 a(a(x1)) -> b(b(b(x1)))
0.15/0.36	 b(b(x1)) -> c(c(c(x1)))
0.15/0.36	 c(c(x1)) -> d(d(d(x1)))
0.15/0.36	 b(x1) -> d(d(x1))
0.15/0.36	 c(d(d(x1))) -> a(x1)
0.15/0.36	
0.15/0.36	Proof:
0.15/0.36	 Complexity Transformation Processor:
0.15/0.36	  strict:
0.15/0.36	   a(a(x1)) -> b(b(b(x1)))
0.15/0.36	   b(b(x1)) -> c(c(c(x1)))
0.15/0.36	   c(c(x1)) -> d(d(d(x1)))
0.15/0.36	   b(x1) -> d(d(x1))
0.15/0.36	   c(d(d(x1))) -> a(x1)
0.15/0.36	  weak:
0.15/0.36	   
0.15/0.36	  Matrix Interpretation Processor: dim=1
0.15/0.36	   
0.15/0.36	   max_matrix:
0.15/0.36	    1
0.15/0.36	   interpretation:
0.15/0.36	    [d](x0) = x0 + 42,
0.15/0.36	    
0.15/0.36	    [c](x0) = x0 + 1,
0.15/0.36	    
0.15/0.36	    [b](x0) = x0 + 33,
0.15/0.36	    
0.15/0.36	    [a](x0) = x0
0.15/0.36	   orientation:
0.15/0.36	    a(a(x1)) = x1 >= x1 + 99 = b(b(b(x1)))
0.15/0.36	    
0.15/0.36	    b(b(x1)) = x1 + 66 >= x1 + 3 = c(c(c(x1)))
0.15/0.36	    
0.15/0.36	    c(c(x1)) = x1 + 2 >= x1 + 126 = d(d(d(x1)))
0.15/0.36	    
0.15/0.36	    b(x1) = x1 + 33 >= x1 + 84 = d(d(x1))
0.15/0.36	    
0.15/0.36	    c(d(d(x1))) = x1 + 85 >= x1 = a(x1)
0.15/0.36	   problem:
0.15/0.36	    strict:
0.15/0.36	     a(a(x1)) -> b(b(b(x1)))
0.15/0.36	     c(c(x1)) -> d(d(d(x1)))
0.15/0.36	     b(x1) -> d(d(x1))
0.15/0.36	    weak:
0.15/0.36	     b(b(x1)) -> c(c(c(x1)))
0.15/0.36	     c(d(d(x1))) -> a(x1)
0.15/0.36	   Matrix Interpretation Processor: dim=1
0.15/0.36	    
0.15/0.36	    max_matrix:
0.15/0.36	     1
0.15/0.36	    interpretation:
0.15/0.36	     [d](x0) = x0,
0.15/0.36	     
0.15/0.36	     [c](x0) = x0 + 17,
0.15/0.36	     
0.15/0.36	     [b](x0) = x0 + 94,
0.15/0.36	     
0.15/0.36	     [a](x0) = x0 + 17
0.15/0.36	    orientation:
0.15/0.36	     a(a(x1)) = x1 + 34 >= x1 + 282 = b(b(b(x1)))
0.15/0.36	     
0.15/0.36	     c(c(x1)) = x1 + 34 >= x1 = d(d(d(x1)))
0.15/0.36	     
0.15/0.36	     b(x1) = x1 + 94 >= x1 = d(d(x1))
0.15/0.36	     
0.15/0.36	     b(b(x1)) = x1 + 188 >= x1 + 51 = c(c(c(x1)))
0.15/0.36	     
0.15/0.36	     c(d(d(x1))) = x1 + 17 >= x1 + 17 = a(x1)
0.15/0.36	    problem:
0.15/0.36	     strict:
0.15/0.36	      a(a(x1)) -> b(b(b(x1)))
0.15/0.36	     weak:
0.15/0.36	      c(c(x1)) -> d(d(d(x1)))
0.15/0.36	      b(x1) -> d(d(x1))
0.15/0.36	      b(b(x1)) -> c(c(c(x1)))
0.15/0.36	      c(d(d(x1))) -> a(x1)
0.15/0.36	    Matrix Interpretation Processor: dim=1
0.15/0.36	     
0.15/0.36	     max_matrix:
0.15/0.36	      1
0.15/0.36	     interpretation:
0.15/0.36	      [d](x0) = x0 + 4,
0.15/0.36	      
0.15/0.36	      [c](x0) = x0 + 6,
0.15/0.36	      
0.15/0.36	      [b](x0) = x0 + 9,
0.15/0.36	      
0.15/0.36	      [a](x0) = x0 + 14
0.15/0.36	     orientation:
0.15/0.36	      a(a(x1)) = x1 + 28 >= x1 + 27 = b(b(b(x1)))
0.15/0.36	      
0.15/0.36	      c(c(x1)) = x1 + 12 >= x1 + 12 = d(d(d(x1)))
0.15/0.36	      
0.15/0.36	      b(x1) = x1 + 9 >= x1 + 8 = d(d(x1))
0.15/0.36	      
0.15/0.36	      b(b(x1)) = x1 + 18 >= x1 + 18 = c(c(c(x1)))
0.15/0.36	      
0.15/0.36	      c(d(d(x1))) = x1 + 14 >= x1 + 14 = a(x1)
0.15/0.36	     problem:
0.15/0.36	      strict:
0.15/0.36	       
0.15/0.36	      weak:
0.15/0.36	       a(a(x1)) -> b(b(b(x1)))
0.15/0.36	       c(c(x1)) -> d(d(d(x1)))
0.15/0.36	       b(x1) -> d(d(x1))
0.15/0.36	       b(b(x1)) -> c(c(c(x1)))
0.15/0.36	       c(d(d(x1))) -> a(x1)
0.15/0.36	     Qed
0.15/0.36	EOF