YES(?,O(n^1))
0.16/0.27	YES(?,O(n^1))
0.16/0.27	
0.16/0.27	Problem:
0.16/0.27	 f(a,empty()) -> g(a,empty())
0.16/0.27	 f(a,cons(x,k)) -> f(cons(x,a),k)
0.16/0.27	 g(empty(),d) -> d
0.16/0.27	 g(cons(x,k),d) -> g(k,cons(x,d))
0.16/0.27	
0.16/0.27	Proof:
0.16/0.27	 Bounds Processor:
0.16/0.27	  bound: 2
0.16/0.27	  enrichment: match
0.16/0.27	  automaton:
0.16/0.27	   final states: {4,3}
0.16/0.27	   transitions:
0.16/0.27	    g1(10,5) -> 3*
0.16/0.27	    g1(1,10) -> 4*
0.16/0.27	    g1(7,5) -> 3*
0.16/0.27	    g1(2,5) -> 3*
0.16/0.27	    g1(2,7) -> 4*
0.16/0.27	    g1(1,5) -> 3*
0.16/0.27	    g1(1,7) -> 4*
0.16/0.27	    g1(2,10) -> 4*
0.16/0.27	    cons1(2,12) -> 5*
0.16/0.27	    cons1(2,14) -> 5*
0.16/0.27	    cons1(1,2) -> 7*
0.16/0.27	    cons1(1,10) -> 7*
0.16/0.27	    cons1(1,12) -> 5*
0.16/0.27	    cons1(1,14) -> 5*
0.16/0.27	    cons1(2,1) -> 7*
0.16/0.27	    cons1(2,5) -> 5*
0.16/0.27	    cons1(2,7) -> 7*
0.16/0.27	    cons1(1,1) -> 7*
0.16/0.27	    cons1(1,5) -> 5*
0.16/0.27	    cons1(1,7) -> 7*
0.16/0.27	    cons1(2,2) -> 10*
0.16/0.27	    cons1(2,10) -> 7*
0.16/0.27	    f1(10,1) -> 3*
0.16/0.27	    f1(7,1) -> 3*
0.16/0.27	    f1(10,2) -> 3*
0.16/0.27	    f1(7,2) -> 3*
0.16/0.27	    empty1() -> 5*
0.16/0.27	    g2(7,12) -> 3*
0.16/0.27	    g2(2,12) -> 3*
0.16/0.27	    g2(7,14) -> 3*
0.16/0.27	    g2(2,14) -> 3*
0.16/0.27	    g2(1,12) -> 3*
0.16/0.27	    g2(1,14) -> 3*
0.16/0.27	    g2(10,12) -> 3*
0.16/0.27	    g2(10,14) -> 3*
0.16/0.27	    f0(1,2) -> 3*
0.16/0.27	    f0(2,1) -> 3*
0.16/0.27	    f0(1,1) -> 3*
0.16/0.27	    f0(2,2) -> 3*
0.16/0.27	    cons2(2,12) -> 12*
0.16/0.27	    cons2(2,14) -> 12*
0.16/0.27	    cons2(1,12) -> 12*
0.16/0.27	    cons2(1,14) -> 12*
0.16/0.27	    cons2(2,5) -> 14*
0.16/0.27	    cons2(1,5) -> 12*
0.16/0.27	    empty0() -> 1*
0.16/0.27	    g0(1,2) -> 4*
0.16/0.27	    g0(2,1) -> 4*
0.16/0.27	    g0(1,1) -> 4*
0.16/0.27	    g0(2,2) -> 4*
0.16/0.27	    cons0(1,2) -> 2*
0.16/0.27	    cons0(2,1) -> 2*
0.16/0.27	    cons0(1,1) -> 2*
0.16/0.27	    cons0(2,2) -> 2*
0.16/0.27	    1 -> 4*
0.16/0.27	    2 -> 4*
0.16/0.27	    5 -> 3*
0.16/0.27	    7 -> 4*
0.16/0.27	    10 -> 4*
0.16/0.27	    12 -> 3*
0.16/0.27	    14 -> 3*
0.16/0.27	  problem:
0.16/0.27	   
0.16/0.27	  Qed
0.16/0.28	EOF