YES(?,O(n^1))
0.16/0.39	YES(?,O(n^1))
0.95/0.40	
0.95/0.40	Problem:
0.95/0.40	 a__f(0()) -> cons(0(),f(s(0())))
0.95/0.40	 a__f(s(0())) -> a__f(a__p(s(0())))
0.95/0.40	 a__p(s(0())) -> 0()
0.95/0.40	 mark(f(X)) -> a__f(mark(X))
0.95/0.40	 mark(p(X)) -> a__p(mark(X))
0.95/0.40	 mark(0()) -> 0()
0.95/0.40	 mark(cons(X1,X2)) -> cons(mark(X1),X2)
0.95/0.40	 mark(s(X)) -> s(mark(X))
0.95/0.40	 a__f(X) -> f(X)
0.95/0.40	 a__p(X) -> p(X)
0.95/0.40	
0.95/0.40	Proof:
0.95/0.40	 Bounds Processor:
0.95/0.40	  bound: 3
0.95/0.40	  enrichment: match
0.95/0.40	  automaton:
0.95/0.40	   final states: {8,7,6}
0.95/0.40	   transitions:
0.95/0.40	    f3(27) -> 28*
0.95/0.40	    f3(24) -> 18,8
0.95/0.40	    p1(5) -> 7*
0.95/0.40	    p1(2) -> 7*
0.95/0.40	    p1(4) -> 7*
0.95/0.40	    p1(1) -> 7*
0.95/0.40	    p1(3) -> 7*
0.95/0.40	    03() -> 24*
0.95/0.40	    f1(10) -> 11*
0.95/0.40	    f1(5) -> 6*
0.95/0.40	    f1(2) -> 6*
0.95/0.40	    f1(4) -> 6*
0.95/0.40	    f1(1) -> 6*
0.95/0.40	    f1(3) -> 6*
0.95/0.40	    cons3(24,28) -> 18,8
0.95/0.40	    s1(9) -> 10*
0.95/0.40	    s1(18) -> 18,8
0.95/0.40	    s3(24) -> 27*
0.95/0.40	    mark1(5) -> 18*
0.95/0.40	    mark1(2) -> 18*
0.95/0.40	    mark1(4) -> 18*
0.95/0.40	    mark1(1) -> 18*
0.95/0.40	    mark1(3) -> 18*
0.95/0.40	    cons1(18,1) -> 18,8
0.95/0.40	    cons1(18,3) -> 18,8
0.95/0.40	    cons1(18,5) -> 18,8
0.95/0.40	    cons1(18,2) -> 18,8
0.95/0.40	    cons1(18,4) -> 18,8
0.95/0.40	    cons1(9,11) -> 6*
0.95/0.40	    01() -> 18,8,7,9
0.95/0.40	    a__p1(10) -> 16*
0.95/0.40	    a__p1(18) -> 18,8
0.95/0.40	    a__f1(16) -> 6*
0.95/0.40	    a__f1(18) -> 18,8
0.95/0.40	    p2(10) -> 16*
0.95/0.40	    p2(18) -> 18,8
0.95/0.40	    a__f0(5) -> 6*
0.95/0.40	    a__f0(2) -> 6*
0.95/0.40	    a__f0(4) -> 6*
0.95/0.40	    a__f0(1) -> 6*
0.95/0.40	    a__f0(3) -> 6*
0.95/0.40	    f2(19) -> 20*
0.95/0.40	    f2(16) -> 6*
0.95/0.40	    f2(18) -> 18,8
0.95/0.40	    00() -> 1*
0.95/0.40	    02() -> 8,18,16
0.95/0.40	    cons0(3,1) -> 2*
0.95/0.40	    cons0(3,3) -> 2*
0.95/0.40	    cons0(3,5) -> 2*
0.95/0.40	    cons0(4,2) -> 2*
0.95/0.40	    cons0(4,4) -> 2*
0.95/0.40	    cons0(5,1) -> 2*
0.95/0.40	    cons0(5,3) -> 2*
0.95/0.40	    cons0(5,5) -> 2*
0.95/0.40	    cons0(1,2) -> 2*
0.95/0.40	    cons0(1,4) -> 2*
0.95/0.40	    cons0(2,1) -> 2*
0.95/0.40	    cons0(2,3) -> 2*
0.95/0.40	    cons0(2,5) -> 2*
0.95/0.40	    cons0(3,2) -> 2*
0.95/0.40	    cons0(3,4) -> 2*
0.95/0.40	    cons0(4,1) -> 2*
0.95/0.40	    cons0(4,3) -> 2*
0.95/0.40	    cons0(4,5) -> 2*
0.95/0.40	    cons0(5,2) -> 2*
0.95/0.40	    cons0(5,4) -> 2*
0.95/0.40	    cons0(1,1) -> 2*
0.95/0.40	    cons0(1,3) -> 2*
0.95/0.40	    cons0(1,5) -> 2*
0.95/0.40	    cons0(2,2) -> 2*
0.95/0.40	    cons0(2,4) -> 2*
0.95/0.40	    a__f2(24) -> 8,18
0.95/0.40	    f0(5) -> 3*
0.95/0.40	    f0(2) -> 3*
0.95/0.40	    f0(4) -> 3*
0.95/0.40	    f0(1) -> 3*
0.95/0.40	    f0(3) -> 3*
0.95/0.40	    a__p2(19) -> 24*
0.95/0.40	    s0(5) -> 4*
0.95/0.40	    s0(2) -> 4*
0.95/0.40	    s0(4) -> 4*
0.95/0.40	    s0(1) -> 4*
0.95/0.40	    s0(3) -> 4*
0.95/0.40	    s2(16) -> 19*
0.95/0.40	    a__p0(5) -> 7*
0.95/0.40	    a__p0(2) -> 7*
0.95/0.40	    a__p0(4) -> 7*
0.95/0.40	    a__p0(1) -> 7*
0.95/0.40	    a__p0(3) -> 7*
0.95/0.40	    cons2(16,20) -> 6,18,8
0.95/0.40	    mark0(5) -> 8*
0.95/0.40	    mark0(2) -> 8*
0.95/0.40	    mark0(4) -> 8*
0.95/0.40	    mark0(1) -> 8*
0.95/0.40	    mark0(3) -> 8*
0.95/0.40	    p3(19) -> 24*
0.95/0.40	    p0(5) -> 5*
0.95/0.40	    p0(2) -> 5*
0.95/0.40	    p0(4) -> 5*
0.95/0.40	    p0(1) -> 5*
0.95/0.40	    p0(3) -> 5*
0.95/0.40	  problem:
0.95/0.40	   
0.95/0.40	  Qed
0.95/0.40	EOF