YES(?,O(n^1))
0.17/0.43	YES(?,O(n^1))
0.17/0.43	
0.17/0.43	Problem:
0.17/0.43	 active(g(X)) -> mark(h(X))
0.17/0.43	 active(c()) -> mark(d())
0.17/0.43	 active(h(d())) -> mark(g(c()))
0.17/0.43	 proper(g(X)) -> g(proper(X))
0.17/0.43	 proper(h(X)) -> h(proper(X))
0.17/0.43	 proper(c()) -> ok(c())
0.17/0.43	 proper(d()) -> ok(d())
0.17/0.43	 g(ok(X)) -> ok(g(X))
0.17/0.43	 h(ok(X)) -> ok(h(X))
0.17/0.43	 top(mark(X)) -> top(proper(X))
0.17/0.43	 top(ok(X)) -> top(active(X))
0.17/0.43	
0.17/0.43	Proof:
0.17/0.43	 Bounds Processor:
0.17/0.43	  bound: 4
0.17/0.43	  enrichment: match
0.17/0.43	  automaton:
0.17/0.43	   final states: {9,8,7,6,5}
0.17/0.43	   transitions:
0.17/0.43	    ok3(124) -> 125*
0.17/0.43	    top1(62) -> 63*
0.17/0.43	    d3() -> 124*
0.17/0.43	    active1(80) -> 81*
0.17/0.43	    active1(86) -> 87*
0.17/0.43	    active1(88) -> 89*
0.17/0.43	    active1(78) -> 79*
0.17/0.43	    top4(132) -> 133*
0.17/0.43	    proper1(70) -> 71*
0.17/0.43	    proper1(72) -> 73*
0.17/0.43	    proper1(64) -> 65*
0.17/0.43	    proper1(61) -> 62*
0.17/0.43	    active4(131) -> 132*
0.17/0.43	    ok1(44) -> 45*
0.17/0.43	    ok1(26) -> 27*
0.17/0.43	    ok1(16) -> 17*
0.17/0.43	    ok1(18) -> 19*
0.17/0.43	    h1(52) -> 53*
0.17/0.43	    h1(54) -> 55*
0.17/0.43	    h1(46) -> 47*
0.17/0.43	    h1(43) -> 44*
0.17/0.43	    g1(25) -> 26*
0.17/0.43	    g1(34) -> 35*
0.17/0.43	    g1(36) -> 37*
0.17/0.43	    g1(28) -> 29*
0.17/0.43	    d1() -> 10*
0.17/0.43	    c1() -> 16*
0.17/0.43	    mark1(10) -> 11*
0.17/0.43	    top2(93) -> 94*
0.17/0.43	    active0(2) -> 5*
0.17/0.43	    active0(4) -> 5*
0.17/0.43	    active0(1) -> 5*
0.17/0.43	    active0(3) -> 5*
0.17/0.43	    active2(104) -> 105*
0.17/0.43	    active2(98) -> 99*
0.17/0.43	    g0(2) -> 7*
0.17/0.43	    g0(4) -> 7*
0.17/0.43	    g0(1) -> 7*
0.17/0.43	    g0(3) -> 7*
0.17/0.43	    proper2(92) -> 93*
0.17/0.43	    mark0(2) -> 1*
0.17/0.43	    mark0(4) -> 1*
0.17/0.43	    mark0(1) -> 1*
0.17/0.43	    mark0(3) -> 1*
0.17/0.43	    ok2(110) -> 111*
0.17/0.43	    h0(2) -> 8*
0.17/0.43	    h0(4) -> 8*
0.17/0.43	    h0(1) -> 8*
0.17/0.43	    h0(3) -> 8*
0.17/0.43	    d2() -> 106*
0.17/0.43	    c0() -> 2*
0.17/0.43	    mark2(106) -> 107*
0.17/0.43	    d0() -> 3*
0.17/0.43	    top3(118) -> 119*
0.17/0.43	    proper0(2) -> 6*
0.17/0.43	    proper0(4) -> 6*
0.17/0.43	    proper0(1) -> 6*
0.17/0.43	    proper0(3) -> 6*
0.17/0.43	    active3(122) -> 123*
0.17/0.43	    ok0(2) -> 4*
0.17/0.43	    ok0(4) -> 4*
0.17/0.43	    ok0(1) -> 4*
0.17/0.43	    ok0(3) -> 4*
0.17/0.43	    proper3(117) -> 118*
0.17/0.43	    top0(2) -> 9*
0.17/0.43	    top0(4) -> 9*
0.17/0.43	    top0(1) -> 9*
0.17/0.43	    top0(3) -> 9*
0.17/0.43	    1 -> 86,70,52,34
0.17/0.43	    2 -> 78,61,43,25
0.17/0.43	    3 -> 88,72,54,36
0.17/0.43	    4 -> 80,64,46,28
0.17/0.43	    10 -> 92,18
0.17/0.43	    11 -> 79,62,5
0.17/0.43	    16 -> 98*
0.17/0.43	    17 -> 62,6
0.17/0.43	    18 -> 104*
0.17/0.43	    19 -> 73,62,6
0.17/0.43	    27 -> 29,26,7
0.17/0.43	    29 -> 26*
0.17/0.43	    35 -> 26*
0.17/0.43	    37 -> 26*
0.17/0.43	    45 -> 47,44,8
0.17/0.43	    47 -> 44*
0.17/0.43	    53 -> 44*
0.17/0.43	    55 -> 44*
0.17/0.43	    63 -> 9*
0.17/0.43	    65 -> 62*
0.17/0.43	    71 -> 62*
0.17/0.43	    73 -> 62*
0.17/0.43	    79 -> 62*
0.17/0.43	    81 -> 62*
0.17/0.43	    87 -> 62*
0.17/0.43	    89 -> 62*
0.17/0.43	    94 -> 63,9
0.17/0.43	    99 -> 93*
0.17/0.43	    105 -> 93*
0.17/0.43	    106 -> 117,110
0.17/0.43	    107 -> 99,93
0.17/0.43	    110 -> 122*
0.17/0.43	    111 -> 93*
0.17/0.43	    119 -> 94,63
0.17/0.43	    123 -> 118*
0.17/0.43	    124 -> 131*
0.17/0.43	    125 -> 118*
0.17/0.43	    133 -> 119,94
0.17/0.43	  problem:
0.17/0.43	   
0.17/0.43	  Qed
0.17/0.43	EOF