YES(?,O(n^1))
0.16/0.27	YES(?,O(n^1))
0.16/0.27	
0.16/0.27	Problem:
0.16/0.27	 active(f(X)) -> mark(g(h(f(X))))
0.16/0.27	 active(f(X)) -> f(active(X))
0.16/0.27	 active(h(X)) -> h(active(X))
0.16/0.27	 f(mark(X)) -> mark(f(X))
0.16/0.27	 h(mark(X)) -> mark(h(X))
0.16/0.27	 proper(f(X)) -> f(proper(X))
0.16/0.27	 proper(g(X)) -> g(proper(X))
0.16/0.27	 proper(h(X)) -> h(proper(X))
0.16/0.27	 f(ok(X)) -> ok(f(X))
0.16/0.27	 g(ok(X)) -> ok(g(X))
0.16/0.27	 h(ok(X)) -> ok(h(X))
0.16/0.27	 top(mark(X)) -> top(proper(X))
0.16/0.27	 top(ok(X)) -> top(active(X))
0.16/0.27	
0.16/0.27	Proof:
0.16/0.27	 Bounds Processor:
0.16/0.27	  bound: 1
0.16/0.27	  enrichment: match
0.16/0.27	  automaton:
0.16/0.27	   final states: {8,7,6,5,4,3}
0.16/0.27	   transitions:
0.16/0.27	    top1(48) -> 49*
0.16/0.27	    active1(57) -> 58*
0.16/0.27	    active1(63) -> 64*
0.16/0.27	    proper1(55) -> 56*
0.16/0.27	    proper1(47) -> 48*
0.16/0.27	    ok1(45) -> 46*
0.16/0.27	    ok1(37) -> 38*
0.16/0.27	    ok1(29) -> 30*
0.16/0.27	    h1(27) -> 28*
0.16/0.27	    h1(19) -> 20*
0.16/0.27	    g1(39) -> 40*
0.16/0.27	    g1(36) -> 37*
0.16/0.27	    f1(17) -> 18*
0.16/0.27	    f1(9) -> 10*
0.16/0.27	    mark1(20) -> 21*
0.16/0.27	    mark1(10) -> 11*
0.16/0.27	    active0(2) -> 3*
0.16/0.27	    active0(1) -> 3*
0.16/0.27	    f0(2) -> 4*
0.16/0.27	    f0(1) -> 4*
0.16/0.27	    mark0(2) -> 1*
0.16/0.27	    mark0(1) -> 1*
0.16/0.27	    g0(2) -> 7*
0.16/0.27	    g0(1) -> 7*
0.16/0.27	    h0(2) -> 5*
0.16/0.27	    h0(1) -> 5*
0.16/0.27	    proper0(2) -> 6*
0.16/0.27	    proper0(1) -> 6*
0.16/0.27	    ok0(2) -> 2*
0.16/0.27	    ok0(1) -> 2*
0.16/0.27	    top0(2) -> 8*
0.16/0.27	    top0(1) -> 8*
0.16/0.27	    1 -> 63,55,39,27,17
0.16/0.27	    2 -> 57,47,36,19,9
0.16/0.27	    10 -> 29*
0.16/0.27	    11 -> 18,10,29,4
0.16/0.27	    18 -> 10*
0.16/0.27	    20 -> 45*
0.16/0.27	    21 -> 28,20,45,5
0.16/0.27	    28 -> 20*
0.16/0.27	    30 -> 10,29,4
0.16/0.27	    38 -> 37,7
0.16/0.27	    40 -> 37*
0.16/0.27	    46 -> 20,45,5
0.16/0.27	    49 -> 8*
0.16/0.27	    56 -> 48*
0.16/0.27	    58 -> 48*
0.16/0.27	    64 -> 48*
0.16/0.27	  problem:
0.16/0.27	   
0.16/0.27	  Qed
0.16/0.28	EOF