YES(?,O(n^1))
0.16/0.25	YES(?,O(n^1))
0.16/0.26	
0.16/0.26	Problem:
0.16/0.26	 *(i(x),x) -> 1()
0.16/0.26	 *(1(),y) -> y
0.16/0.26	 *(x,0()) -> 0()
0.16/0.26	 *(*(x,y),z) -> *(x,*(y,z))
0.16/0.26	
0.16/0.26	Proof:
0.16/0.26	 Bounds Processor:
0.16/0.26	  bound: 1
0.16/0.26	  enrichment: match
0.16/0.26	  automaton:
0.16/0.26	   final states: {7,6,5,4}
0.16/0.26	   transitions:
0.16/0.26	    01() -> 6*,3,4
0.16/0.26	    11() -> 7*,2,4
0.16/0.26	    *0(3,1) -> 4*
0.16/0.26	    *0(3,3) -> 4*
0.16/0.26	    *0(3,5) -> 4*
0.16/0.26	    *0(3,7) -> 4*
0.16/0.26	    *0(5,1) -> 4*
0.16/0.26	    *0(5,3) -> 4*
0.16/0.26	    *0(5,5) -> 4*
0.16/0.26	    *0(5,7) -> 4*
0.16/0.26	    *0(6,2) -> 4*
0.16/0.26	    *0(1,2) -> 4*
0.16/0.26	    *0(6,6) -> 4*
0.16/0.26	    *0(1,6) -> 4*
0.16/0.26	    *0(7,1) -> 4*
0.16/0.26	    *0(2,1) -> 4*
0.16/0.26	    *0(7,3) -> 4*
0.16/0.26	    *0(2,3) -> 4*
0.16/0.26	    *0(7,5) -> 4*
0.16/0.26	    *0(2,5) -> 4*
0.16/0.26	    *0(7,7) -> 4*
0.16/0.26	    *0(2,7) -> 4*
0.16/0.26	    *0(3,2) -> 4*
0.16/0.26	    *0(3,6) -> 4*
0.16/0.26	    *0(5,2) -> 4*
0.16/0.26	    *0(5,6) -> 4*
0.16/0.26	    *0(6,1) -> 4*
0.16/0.26	    *0(1,1) -> 4*
0.16/0.26	    *0(6,3) -> 4*
0.16/0.26	    *0(1,3) -> 4*
0.16/0.26	    *0(6,5) -> 4*
0.16/0.26	    *0(1,5) -> 4*
0.16/0.26	    *0(6,7) -> 4*
0.16/0.26	    *0(1,7) -> 4*
0.16/0.26	    *0(7,2) -> 4*
0.16/0.26	    *0(2,2) -> 4*
0.16/0.26	    *0(7,6) -> 4*
0.16/0.26	    *0(2,6) -> 4*
0.16/0.26	    i0(5) -> 4,5*
0.16/0.26	    i0(7) -> 4,5*
0.16/0.26	    i0(2) -> 5*,4,1
0.16/0.26	    i0(6) -> 4,5*
0.16/0.26	    i0(1) -> 5*,4,1
0.16/0.26	    i0(3) -> 5*,4,1
0.16/0.26	    1 -> 4*
0.16/0.26	    2 -> 4*
0.16/0.26	    3 -> 4*
0.16/0.26	    5 -> 4*
0.16/0.26	    6 -> 4*
0.16/0.26	    7 -> 4*
0.16/0.26	  problem:
0.16/0.26	   
0.16/0.26	  Qed
0.16/0.26	EOF