YES(?,O(n^1))
0.17/0.24	YES(?,O(n^1))
0.17/0.24	
0.17/0.24	Problem:
0.17/0.24	 flatten(nil()) -> nil()
0.17/0.24	 flatten(unit(x)) -> flatten(x)
0.17/0.24	 flatten(++(x,y)) -> ++(flatten(x),flatten(y))
0.17/0.24	 flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
0.17/0.24	 flatten(flatten(x)) -> flatten(x)
0.17/0.24	 rev(nil()) -> nil()
0.17/0.24	 rev(unit(x)) -> unit(x)
0.17/0.24	 rev(++(x,y)) -> ++(rev(y),rev(x))
0.17/0.24	 rev(rev(x)) -> x
0.17/0.24	 ++(x,nil()) -> x
0.17/0.24	 ++(nil(),y) -> y
0.17/0.24	 ++(++(x,y),z) -> ++(x,++(y,z))
0.17/0.24	
0.17/0.24	Proof:
0.17/0.24	 Bounds Processor:
0.17/0.24	  bound: 1
0.17/0.24	  enrichment: match
0.17/0.24	  automaton:
0.17/0.24	   final states: {5,4,3}
0.17/0.24	   transitions:
0.17/0.24	    unit1(2) -> 4*
0.17/0.24	    unit1(1) -> 4*
0.17/0.24	    nil1() -> 4,3
0.17/0.24	    flatten1(2) -> 3*
0.17/0.24	    flatten1(1) -> 3*
0.17/0.24	    flatten0(2) -> 3*
0.17/0.24	    flatten0(1) -> 3*
0.17/0.24	    nil0() -> 1*
0.17/0.24	    unit0(2) -> 2*
0.17/0.24	    unit0(1) -> 2*
0.17/0.24	    ++0(1,2) -> 5*
0.17/0.24	    ++0(2,1) -> 5*
0.17/0.24	    ++0(1,1) -> 5*
0.17/0.24	    ++0(2,2) -> 5*
0.17/0.24	    rev0(2) -> 4*
0.17/0.24	    rev0(1) -> 4*
0.17/0.24	    1 -> 5*
0.17/0.24	    2 -> 5*
0.17/0.24	  problem:
0.17/0.24	   
0.17/0.24	  Qed
0.17/0.24	EOF