YES(?,O(n^1))
0.16/1.09	YES(?,O(n^1))
0.16/1.10	
0.16/1.10	Problem:
0.16/1.10	 h(x,c(y,z)) -> h(c(s(y),x),z)
0.16/1.10	 h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z)))
0.16/1.10	
0.16/1.10	Proof:
0.16/1.10	 Bounds Processor:
0.16/1.10	  bound: 2
0.16/1.10	  enrichment: match
0.16/1.10	  automaton:
0.16/1.10	   final states: {4}
0.16/1.10	   transitions:
0.16/1.10	    h1(22,16) -> 4*
0.16/1.10	    h1(12,16) -> 4*
0.16/1.10	    h1(2,16) -> 4*
0.16/1.10	    h1(8,1) -> 4*
0.16/1.10	    h1(8,3) -> 4*
0.16/1.10	    h1(34,16) -> 4*
0.16/1.10	    h1(1,16) -> 4*
0.16/1.10	    h1(12,1) -> 4*
0.16/1.10	    h1(12,3) -> 4*
0.16/1.10	    h1(8,2) -> 4*
0.16/1.10	    h1(28,16) -> 4*
0.16/1.10	    h1(8,16) -> 4*
0.16/1.10	    h1(3,16) -> 4*
0.16/1.10	    h1(30,16) -> 4*
0.16/1.10	    h1(12,2) -> 4*
0.16/1.10	    c1(2,16) -> 13*
0.16/1.10	    c1(3,1) -> 13*
0.16/1.10	    c1(3,3) -> 13*
0.16/1.10	    c1(7,28) -> 8*
0.16/1.10	    c1(7,30) -> 8*
0.16/1.10	    c1(7,34) -> 8*
0.16/1.10	    c1(15,13) -> 16*
0.16/1.10	    c1(11,2) -> 8*
0.16/1.10	    c1(1,2) -> 13*
0.16/1.10	    c1(11,8) -> 8*
0.16/1.10	    c1(11,12) -> 8*
0.16/1.10	    c1(1,16) -> 13*
0.16/1.10	    c1(7,1) -> 8*
0.16/1.10	    c1(2,1) -> 13*
0.16/1.10	    c1(7,3) -> 8*
0.16/1.10	    c1(2,3) -> 13*
0.16/1.10	    c1(11,28) -> 8*
0.16/1.10	    c1(11,30) -> 8*
0.16/1.10	    c1(11,34) -> 8*
0.16/1.10	    c1(3,2) -> 13*
0.16/1.10	    c1(3,16) -> 13*
0.16/1.10	    c1(15,16) -> 16*
0.16/1.10	    c1(11,1) -> 12*
0.16/1.10	    c1(1,1) -> 13*
0.16/1.10	    c1(11,3) -> 8*
0.16/1.10	    c1(1,3) -> 13*
0.16/1.10	    c1(7,2) -> 8*
0.16/1.10	    c1(2,2) -> 13*
0.16/1.10	    c1(7,8) -> 8*
0.16/1.10	    c1(7,12) -> 8*
0.16/1.10	    s1(2) -> 7*
0.16/1.10	    s1(14) -> 15*
0.16/1.10	    s1(1) -> 11*
0.16/1.10	    s1(3) -> 7*
0.16/1.10	    01() -> 14*
0.16/1.10	    h2(22,16) -> 4*
0.16/1.10	    h2(28,1) -> 4*
0.16/1.10	    h2(28,3) -> 4*
0.16/1.10	    h2(34,2) -> 4*
0.16/1.10	    h2(34,16) -> 4*
0.16/1.10	    h2(30,1) -> 4*
0.16/1.10	    h2(30,3) -> 4*
0.16/1.10	    h2(22,13) -> 4*
0.16/1.10	    h2(28,2) -> 4*
0.16/1.10	    h2(28,16) -> 4*
0.16/1.10	    h2(34,1) -> 4*
0.16/1.10	    h2(34,3) -> 4*
0.16/1.10	    h2(30,2) -> 4*
0.16/1.10	    h2(30,16) -> 4*
0.16/1.10	    h0(3,1) -> 4*
0.16/1.10	    h0(3,3) -> 4*
0.16/1.10	    h0(1,2) -> 4*
0.16/1.10	    h0(2,1) -> 4*
0.16/1.10	    h0(2,3) -> 4*
0.16/1.10	    h0(3,2) -> 4*
0.16/1.10	    h0(1,1) -> 4*
0.16/1.10	    h0(1,3) -> 4*
0.16/1.10	    h0(2,2) -> 4*
0.16/1.10	    c2(27,22) -> 28*
0.16/1.10	    c2(29,22) -> 30*
0.16/1.10	    c2(21,2) -> 22*
0.16/1.10	    c2(21,8) -> 22*
0.16/1.10	    c2(21,12) -> 22*
0.16/1.10	    c2(21,22) -> 22*
0.16/1.10	    c2(21,28) -> 22*
0.16/1.10	    c2(21,30) -> 22*
0.16/1.10	    c2(21,34) -> 22*
0.16/1.10	    c2(33,22) -> 34*
0.16/1.10	    c2(21,1) -> 22*
0.16/1.10	    c2(21,3) -> 22*
0.16/1.10	    c0(3,1) -> 1*
0.16/1.10	    c0(3,3) -> 1*
0.16/1.10	    c0(1,2) -> 1*
0.16/1.10	    c0(2,1) -> 1*
0.16/1.10	    c0(2,3) -> 1*
0.16/1.10	    c0(3,2) -> 1*
0.16/1.10	    c0(1,1) -> 1*
0.16/1.10	    c0(1,3) -> 1*
0.16/1.10	    c0(2,2) -> 1*
0.16/1.10	    s2(15) -> 21*
0.16/1.10	    s2(2) -> 27*
0.16/1.10	    s2(1) -> 33*
0.16/1.10	    s2(3) -> 29*
0.16/1.10	    s0(2) -> 2*
0.16/1.10	    s0(1) -> 2*
0.16/1.10	    s0(3) -> 2*
0.16/1.10	    00() -> 3*
0.16/1.10	  problem:
0.16/1.10	   
0.16/1.10	  Qed
0.16/1.10	EOF