YES(?,O(n^1))
0.15/0.23	YES(?,O(n^1))
0.15/0.23	
0.15/0.23	Problem:
0.15/0.23	 app(nil(),YS) -> YS
0.15/0.23	 app(cons(X),YS) -> cons(X)
0.15/0.23	 from(X) -> cons(X)
0.15/0.23	 zWadr(nil(),YS) -> nil()
0.15/0.23	 zWadr(XS,nil()) -> nil()
0.15/0.23	 zWadr(cons(X),cons(Y)) -> cons(app(Y,cons(X)))
0.15/0.23	 prefix(L) -> cons(nil())
0.15/0.23	
0.15/0.23	Proof:
0.15/0.23	 Bounds Processor:
0.15/0.23	  bound: 1
0.15/0.23	  enrichment: match
0.15/0.23	  automaton:
0.15/0.23	   final states: {6,5,4,3}
0.15/0.23	   transitions:
0.15/0.23	    cons1(5) -> 6*
0.15/0.23	    cons1(2) -> 4,3
0.15/0.23	    cons1(1) -> 4,3
0.15/0.23	    cons1(8) -> 5*
0.15/0.23	    nil1() -> 5*
0.15/0.23	    app1(2,3) -> 8*
0.15/0.23	    app1(1,3) -> 8*
0.15/0.23	    app0(1,2) -> 3*
0.15/0.23	    app0(2,1) -> 3*
0.15/0.23	    app0(1,1) -> 3*
0.15/0.23	    app0(2,2) -> 3*
0.15/0.23	    nil0() -> 1*
0.15/0.23	    cons0(2) -> 2*
0.15/0.23	    cons0(1) -> 2*
0.15/0.23	    from0(2) -> 4*
0.15/0.23	    from0(1) -> 4*
0.15/0.23	    zWadr0(1,2) -> 5*
0.15/0.23	    zWadr0(2,1) -> 5*
0.15/0.23	    zWadr0(1,1) -> 5*
0.15/0.23	    zWadr0(2,2) -> 5*
0.15/0.23	    prefix0(2) -> 6*
0.15/0.23	    prefix0(1) -> 6*
0.15/0.23	    1 -> 3*
0.15/0.23	    2 -> 3*
0.15/0.23	    3 -> 8*
0.15/0.23	  problem:
0.15/0.23	   
0.15/0.23	  Qed
0.15/0.23	EOF