YES(?,O(n^1))
0.17/0.34	YES(?,O(n^1))
0.17/0.35	
0.17/0.35	Problem:
0.17/0.35	 active(f(x)) -> mark(f(f(x)))
0.17/0.35	 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
0.17/0.35	 mat(f(x),f(y())) -> f(mat(x,y()))
0.17/0.35	 chk(no(c())) -> active(c())
0.17/0.35	 mat(f(x),c()) -> no(c())
0.17/0.35	 f(active(x)) -> active(f(x))
0.17/0.35	 f(no(x)) -> no(f(x))
0.17/0.35	 f(mark(x)) -> mark(f(x))
0.17/0.35	 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
0.17/0.35	
0.17/0.35	Proof:
0.17/0.35	 Bounds Processor:
0.17/0.35	  bound: 2
0.17/0.35	  enrichment: match
0.17/0.35	  automaton:
0.17/0.35	   final states: {10,9,8,7,6}
0.17/0.35	   transitions:
0.17/0.35	    tp1(27) -> 10*
0.17/0.35	    chk1(26) -> 27*
0.17/0.35	    mat1(25,1) -> 26*
0.17/0.35	    mat1(25,3) -> 26*
0.17/0.35	    mat1(25,5) -> 26*
0.17/0.35	    mat1(25,2) -> 26*
0.17/0.35	    mat1(25,4) -> 26*
0.17/0.35	    f1(20) -> 21*
0.17/0.35	    f1(15) -> 16*
0.17/0.35	    f1(5) -> 13*
0.17/0.35	    f1(22) -> 23*
0.17/0.35	    f1(17) -> 18*
0.17/0.35	    f1(2) -> 13*
0.17/0.35	    f1(24) -> 25*
0.17/0.35	    f1(19) -> 20*
0.17/0.35	    f1(4) -> 13*
0.17/0.35	    f1(21) -> 22*
0.17/0.35	    f1(16) -> 17*
0.17/0.35	    f1(1) -> 13*
0.17/0.35	    f1(23) -> 24*
0.17/0.35	    f1(18) -> 19*
0.17/0.35	    f1(3) -> 13*
0.17/0.35	    X1() -> 15*
0.17/0.35	    mark1(13) -> 13,9
0.17/0.35	    no1(12) -> 26*
0.17/0.35	    no1(13) -> 13,9
0.17/0.35	    active1(12) -> 7*
0.17/0.35	    c1() -> 12*
0.17/0.35	    active2(41) -> 27*
0.17/0.35	    c2() -> 41*
0.17/0.35	    active0(5) -> 6*
0.17/0.35	    active0(2) -> 6*
0.17/0.35	    active0(4) -> 6*
0.17/0.35	    active0(1) -> 6*
0.17/0.35	    active0(3) -> 6*
0.17/0.35	    f0(5) -> 9*
0.17/0.35	    f0(2) -> 9*
0.17/0.35	    f0(4) -> 9*
0.17/0.35	    f0(1) -> 9*
0.17/0.35	    f0(3) -> 9*
0.17/0.35	    mark0(5) -> 1*
0.17/0.35	    mark0(2) -> 1*
0.17/0.35	    mark0(4) -> 1*
0.17/0.35	    mark0(1) -> 1*
0.17/0.35	    mark0(3) -> 1*
0.17/0.35	    chk0(5) -> 7*
0.17/0.35	    chk0(2) -> 7*
0.17/0.35	    chk0(4) -> 7*
0.17/0.35	    chk0(1) -> 7*
0.17/0.35	    chk0(3) -> 7*
0.17/0.35	    no0(5) -> 2*
0.17/0.35	    no0(2) -> 2*
0.17/0.35	    no0(4) -> 2*
0.17/0.35	    no0(1) -> 2*
0.17/0.35	    no0(3) -> 2*
0.17/0.35	    mat0(3,1) -> 8*
0.17/0.35	    mat0(3,3) -> 8*
0.17/0.35	    mat0(3,5) -> 8*
0.17/0.35	    mat0(4,2) -> 8*
0.17/0.35	    mat0(4,4) -> 8*
0.17/0.35	    mat0(5,1) -> 8*
0.17/0.35	    mat0(5,3) -> 8*
0.17/0.35	    mat0(5,5) -> 8*
0.17/0.35	    mat0(1,2) -> 8*
0.17/0.35	    mat0(1,4) -> 8*
0.17/0.35	    mat0(2,1) -> 8*
0.17/0.35	    mat0(2,3) -> 8*
0.17/0.35	    mat0(2,5) -> 8*
0.17/0.35	    mat0(3,2) -> 8*
0.17/0.35	    mat0(3,4) -> 8*
0.17/0.35	    mat0(4,1) -> 8*
0.17/0.35	    mat0(4,3) -> 8*
0.17/0.35	    mat0(4,5) -> 8*
0.17/0.35	    mat0(5,2) -> 8*
0.17/0.35	    mat0(5,4) -> 8*
0.17/0.35	    mat0(1,1) -> 8*
0.17/0.35	    mat0(1,3) -> 8*
0.17/0.35	    mat0(1,5) -> 8*
0.17/0.35	    mat0(2,2) -> 8*
0.17/0.35	    mat0(2,4) -> 8*
0.17/0.35	    X0() -> 3*
0.17/0.35	    y0() -> 4*
0.17/0.35	    c0() -> 5*
0.17/0.35	    tp0(5) -> 10*
0.17/0.35	    tp0(2) -> 10*
0.17/0.35	    tp0(4) -> 10*
0.17/0.35	    tp0(1) -> 10*
0.17/0.35	    tp0(3) -> 10*
0.17/0.35	  problem:
0.17/0.35	   
0.17/0.35	  Qed
0.17/0.35	EOF