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