YES(?,O(n^1))
0.16/0.22	YES(?,O(n^1))
0.16/0.23	
0.16/0.23	Problem:
0.16/0.23	 fst(0(),Z) -> nil()
0.16/0.23	 fst(s(),cons(Y)) -> cons(Y)
0.16/0.23	 from(X) -> cons(X)
0.16/0.23	 add(0(),X) -> X
0.16/0.23	 add(s(),Y) -> s()
0.16/0.23	 len(nil()) -> 0()
0.16/0.23	 len(cons(X)) -> s()
0.16/0.23	
0.16/0.23	Proof:
0.16/0.23	 Bounds Processor:
0.16/0.23	  bound: 1
0.16/0.23	  enrichment: match
0.16/0.23	  automaton:
0.16/0.23	   final states: {9}
0.16/0.23	   transitions:
0.16/0.23	    s1() -> 9*
0.16/0.23	    01() -> 9*
0.16/0.23	    cons1(9) -> 9*
0.16/0.23	    nil1() -> 9*
0.16/0.23	    fst0(9,9) -> 9*
0.16/0.23	    00() -> 9*
0.16/0.23	    nil0() -> 9*
0.16/0.23	    s0() -> 9*
0.16/0.23	    cons0(9) -> 9*
0.16/0.23	    from0(9) -> 9*
0.16/0.23	    add0(9,9) -> 9*
0.16/0.23	    len0(9) -> 9*
0.16/0.23	  problem:
0.16/0.23	   
0.16/0.23	  Qed
0.16/0.23	EOF