YES(?,O(n^1))
0.16/0.26	YES(?,O(n^1))
0.16/0.26	
0.16/0.26	Problem:
0.16/0.26	 f(nil()) -> nil()
0.16/0.26	 f(.(nil(),y)) -> .(nil(),f(y))
0.16/0.26	 f(.(.(x,y),z)) -> f(.(x,.(y,z)))
0.16/0.26	 g(nil()) -> nil()
0.16/0.26	 g(.(x,nil())) -> .(g(x),nil())
0.16/0.26	 g(.(x,.(y,z))) -> g(.(.(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: {4,3}
0.16/0.26	   transitions:
0.16/0.26	    g1(12) -> 14*
0.16/0.26	    g1(7) -> 14*
0.16/0.26	    g1(2) -> 14*
0.16/0.26	    g1(16) -> 14,4
0.16/0.26	    g1(1) -> 14*
0.16/0.26	    .1(2,12) -> 8*
0.16/0.26	    .1(3,5) -> 5,3
0.16/0.26	    .1(16,2) -> 16*
0.16/0.26	    .1(1,2) -> 7*
0.16/0.26	    .1(1,8) -> 8*
0.16/0.26	    .1(1,12) -> 8*
0.16/0.26	    .1(12,1) -> 16*
0.16/0.26	    .1(7,1) -> 16*
0.16/0.26	    .1(2,1) -> 7*
0.16/0.26	    .1(2,7) -> 8*
0.16/0.26	    .1(14,3) -> 14,4
0.16/0.26	    .1(16,1) -> 16*
0.16/0.26	    .1(1,1) -> 12*
0.16/0.26	    .1(1,7) -> 8*
0.16/0.26	    .1(12,2) -> 16*
0.16/0.26	    .1(7,2) -> 16*
0.16/0.26	    .1(2,2) -> 7*
0.16/0.26	    .1(2,8) -> 8*
0.16/0.26	    nil1() -> 14,5,4,3
0.16/0.26	    f1(12) -> 5*
0.16/0.26	    f1(7) -> 5*
0.16/0.26	    f1(2) -> 5*
0.16/0.26	    f1(1) -> 5*
0.16/0.26	    f1(8) -> 5,3
0.16/0.26	    f0(2) -> 3*
0.16/0.26	    f0(1) -> 3*
0.16/0.26	    nil0() -> 1*
0.16/0.26	    .0(1,2) -> 2*
0.16/0.26	    .0(2,1) -> 2*
0.16/0.26	    .0(1,1) -> 2*
0.16/0.26	    .0(2,2) -> 2*
0.16/0.26	    g0(2) -> 4*
0.16/0.26	    g0(1) -> 4*
0.16/0.26	  problem:
0.16/0.26	   
0.16/0.26	  Qed
0.16/0.26	EOF