YES(?,O(n^1))
3.39/1.15	YES(?,O(n^1))
3.39/1.15	
3.39/1.15	Problem:
3.39/1.15	 +(0(),y) -> y
3.39/1.15	 +(s(x),0()) -> s(x)
3.39/1.15	 +(s(x),s(y)) -> s(+(s(x),+(y,0())))
3.39/1.15	
3.39/1.15	Proof:
3.39/1.15	 Complexity Transformation Processor:
3.39/1.15	  strict:
3.39/1.15	   +(0(),y) -> y
3.39/1.15	   +(s(x),0()) -> s(x)
3.39/1.15	   +(s(x),s(y)) -> s(+(s(x),+(y,0())))
3.39/1.15	  weak:
3.39/1.15	   
3.39/1.15	  Matrix Interpretation Processor: dim=1
3.39/1.15	   
3.39/1.15	   max_matrix:
3.39/1.15	    1
3.39/1.15	   interpretation:
3.39/1.15	    [s](x0) = x0 + 1,
3.39/1.15	    
3.39/1.15	    [+](x0, x1) = x0 + x1,
3.39/1.15	    
3.39/1.15	    [0] = 13
3.39/1.15	   orientation:
3.39/1.15	    +(0(),y) = y + 13 >= y = y
3.39/1.15	    
3.39/1.15	    +(s(x),0()) = x + 14 >= x + 1 = s(x)
3.39/1.15	    
3.39/1.15	    +(s(x),s(y)) = x + y + 2 >= x + y + 15 = s(+(s(x),+(y,0())))
3.39/1.15	   problem:
3.39/1.15	    strict:
3.39/1.15	     +(s(x),s(y)) -> s(+(s(x),+(y,0())))
3.39/1.15	    weak:
3.39/1.15	     +(0(),y) -> y
3.39/1.15	     +(s(x),0()) -> s(x)
3.39/1.15	   Bounds Processor:
3.39/1.15	    bound: 2
3.39/1.15	    enrichment: match
3.39/1.15	    automaton:
3.39/1.15	     final states: {3}
3.39/1.15	     transitions:
3.39/1.15	      s1(7) -> 3*
3.39/1.15	      s1(2) -> 17,7,5,6
3.39/1.15	      s1(1) -> 17,7,5,6
3.39/1.15	      +1(1,4) -> 5*
3.39/1.15	      +1(6,5) -> 7*
3.39/1.15	      +1(2,4) -> 5*
3.39/1.15	      01() -> 4*
3.39/1.15	      s2(2) -> 19,18
3.39/1.15	      s2(19) -> 19,7
3.39/1.15	      s2(1) -> 19,18
3.39/1.15	      +0(1,2) -> 3*
3.39/1.15	      +0(2,1) -> 3*
3.39/1.15	      +0(1,1) -> 3*
3.39/1.15	      +0(2,2) -> 3*
3.39/1.15	      +2(2,16) -> 17*
3.39/1.15	      +2(18,17) -> 19*
3.39/1.15	      +2(1,16) -> 17*
3.39/1.15	      s0(2) -> 1*
3.39/1.15	      s0(1) -> 1*
3.39/1.15	      02() -> 16*
3.39/1.15	      00() -> 2*
3.39/1.15	      1 -> 3*
3.39/1.15	      2 -> 3*
3.39/1.15	      4 -> 5*
3.39/1.15	      16 -> 17*
3.39/1.15	    problem:
3.39/1.15	     strict:
3.39/1.15	      
3.39/1.15	     weak:
3.39/1.15	      +(s(x),s(y)) -> s(+(s(x),+(y,0())))
3.39/1.15	      +(0(),y) -> y
3.39/1.15	      +(s(x),0()) -> s(x)
3.39/1.15	    Qed
3.39/1.15	EOF