YES(?,O(n^2))
29.51/12.53	YES(?,O(n^2))
29.51/12.54	
29.51/12.54	Problem:
29.51/12.54	 a(b(x1)) -> b(a(x1))
29.51/12.54	 b(a(x1)) -> a(a(c(b(x1))))
29.51/12.54	
29.51/12.54	Proof:
29.51/12.54	 Complexity Transformation Processor:
29.51/12.54	  strict:
29.51/12.54	   a(b(x1)) -> b(a(x1))
29.51/12.54	   b(a(x1)) -> a(a(c(b(x1))))
29.51/12.54	  weak:
29.51/12.54	   
29.51/12.54	  Splitting Processor:
29.51/12.54	   strict:
29.51/12.54	    b(a(x1)) -> a(a(c(b(x1))))
29.51/12.54	   weak:
29.51/12.54	    a(b(x1)) -> b(a(x1))
29.51/12.54	   Bounds Processor:
29.51/12.54	    bound: 2
29.51/12.54	    enrichment: match
29.51/12.54	    automaton:
29.51/12.54	     final states: {4}
29.51/12.54	     transitions:
29.51/12.54	      a1(12) -> 13*
29.51/12.54	      a1(13) -> 14*
29.51/12.54	      c1(11) -> 12*
29.51/12.54	      b1(15) -> 16*
29.51/12.54	      b1(10) -> 11*
29.51/12.54	      a2(35) -> 36*
29.51/12.54	      a2(24) -> 25*
29.51/12.54	      a2(36) -> 37*
29.51/12.54	      a2(23) -> 24*
29.51/12.54	      b0(4) -> 4*
29.51/12.54	      c2(22) -> 23*
29.51/12.54	      c2(34) -> 35*
29.51/12.54	      a0(4) -> 4*
29.51/12.54	      b2(21) -> 22*
29.51/12.54	      b2(33) -> 34*
29.51/12.54	      c0(4) -> 4*
29.51/12.54	      4 -> 10*
29.51/12.54	      12 -> 33*
29.51/12.54	      13 -> 21,15
29.51/12.54	      14 -> 11,4
29.51/12.54	      16 -> 11*
29.51/12.54	      25 -> 11*
29.51/12.54	      37 -> 22,16
29.51/12.54	    problem:
29.51/12.54	     strict:
29.51/12.54	      
29.51/12.54	     weak:
29.51/12.54	      b(a(x1)) -> a(a(c(b(x1))))
29.51/12.54	      a(b(x1)) -> b(a(x1))
29.51/12.54	    Qed
29.51/12.54	   
29.51/12.54	   strict:
29.51/12.54	    a(b(x1)) -> b(a(x1))
29.51/12.54	   weak:
29.51/12.54	    b(a(x1)) -> a(a(c(b(x1))))
29.51/12.54	   Matrix Interpretation Processor: dim=2
29.51/12.54	    
29.51/12.54	    max_matrix:
29.51/12.54	     [1 1]
29.51/12.54	     [0 1]
29.51/12.54	    interpretation:
29.51/12.54	               [1 0]  
29.51/12.54	     [c](x0) = [0 0]x0,
29.51/12.54	     
29.51/12.54	               [1 1]  
29.51/12.54	     [a](x0) = [0 1]x0,
29.51/12.54	     
29.51/12.54	               [1 1]     [6]
29.51/12.54	     [b](x0) = [0 1]x0 + [1]
29.51/12.54	    orientation:
29.51/12.54	                [1 2]     [7]    [1 2]     [6]           
29.51/12.54	     a(b(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = b(a(x1))
29.51/12.54	     
29.51/12.54	                [1 2]     [6]    [1 1]     [6]                 
29.51/12.54	     b(a(x1)) = [0 1]x1 + [1] >= [0 0]x1 + [0] = a(a(c(b(x1))))
29.51/12.54	    problem:
29.51/12.54	     strict:
29.51/12.54	      
29.51/12.54	     weak:
29.51/12.54	      a(b(x1)) -> b(a(x1))
29.51/12.54	      b(a(x1)) -> a(a(c(b(x1))))
29.51/12.54	    Qed
29.51/12.54	EOF