YES(?,O(n^1))
0.16/0.27	YES(?,O(n^1))
0.16/0.28	
0.16/0.28	Problem:
0.16/0.28	 h(x,c(y,z)) -> h(c(s(y),x),z)
0.16/0.28	 h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z)))
0.16/0.28	
0.16/0.28	Proof:
0.16/0.28	 Bounds Processor:
0.16/0.28	  bound: 2
0.16/0.28	  enrichment: match
0.16/0.28	  automaton:
0.16/0.28	   final states: {5}
0.16/0.28	   transitions:
0.16/0.28	    h1(5,13) -> 5*
0.16/0.28	    h1(17,13) -> 5*
0.16/0.28	    h1(9,5) -> 5*
0.16/0.28	    h1(19,13) -> 5*
0.16/0.28	    h1(9,13) -> 5*
0.16/0.28	    c1(8,5) -> 9*
0.16/0.28	    c1(8,9) -> 9*
0.16/0.28	    c1(8,17) -> 9*
0.16/0.28	    c1(8,19) -> 9*
0.16/0.28	    c1(5,5) -> 10*
0.16/0.28	    c1(5,13) -> 10*
0.16/0.28	    c1(12,5) -> 10*
0.16/0.28	    c1(12,13) -> 13*
0.16/0.28	    c1(5,10) -> 10*
0.16/0.28	    c1(12,10) -> 13*
0.16/0.28	    s1(5) -> 8*
0.16/0.28	    s1(11) -> 12*
0.16/0.28	    01() -> 11*
0.16/0.28	    h2(19,10) -> 5*
0.16/0.28	    h2(17,5) -> 5*
0.16/0.28	    h2(17,13) -> 5*
0.16/0.28	    h2(19,5) -> 5*
0.16/0.28	    h2(19,13) -> 5*
0.16/0.28	    h2(17,10) -> 5*
0.16/0.28	    h0(5,5) -> 5*
0.16/0.28	    c2(18,17) -> 19*
0.16/0.28	    c2(18,19) -> 17*
0.16/0.28	    c2(16,5) -> 17*
0.16/0.28	    c2(16,9) -> 19*
0.16/0.28	    c2(16,17) -> 17*
0.16/0.28	    c2(16,19) -> 17*
0.16/0.28	    c0(5,5) -> 5*
0.16/0.28	    s2(5) -> 18*
0.16/0.28	    s2(12) -> 16*
0.16/0.28	    s0(5) -> 5*
0.16/0.28	    00() -> 5*
0.16/0.28	  problem:
0.16/0.28	   
0.16/0.28	  Qed
0.16/0.28	EOF