YES(?,O(n^1))
0.16/0.80	YES(?,O(n^1))
0.16/0.81	
0.16/0.81	Problem:
0.16/0.81	 active(c()) -> mark(f(g(c())))
0.16/0.81	 active(f(g(X))) -> mark(g(X))
0.16/0.81	 proper(c()) -> ok(c())
0.16/0.81	 proper(f(X)) -> f(proper(X))
0.16/0.81	 proper(g(X)) -> g(proper(X))
0.16/0.81	 f(ok(X)) -> ok(f(X))
0.16/0.81	 g(ok(X)) -> ok(g(X))
0.16/0.81	 top(mark(X)) -> top(proper(X))
0.16/0.81	 top(ok(X)) -> top(active(X))
0.16/0.81	
0.16/0.81	Proof:
0.16/0.81	 Bounds Processor:
0.16/0.81	  bound: 6
0.16/0.81	  enrichment: match
0.16/0.81	  automaton:
0.16/0.81	   final states: {8,7,6,5,4}
0.16/0.81	   transitions:
0.16/0.81	    f3(137) -> 138*
0.16/0.81	    f3(119) -> 120*
0.16/0.81	    ok2(111) -> 112*
0.16/0.81	    ok3(131) -> 132*
0.16/0.81	    ok3(138) -> 139*
0.16/0.81	    ok3(135) -> 136*
0.16/0.81	    g3(122) -> 123*
0.16/0.81	    g3(130) -> 131*
0.16/0.81	    c3() -> 135*
0.16/0.81	    active3(149) -> 150*
0.16/0.81	    ok4(144) -> 145*
0.16/0.81	    ok4(201) -> 202*
0.16/0.81	    ok4(163) -> 164*
0.16/0.81	    g4(156) -> 157*
0.16/0.81	    g4(143) -> 144*
0.16/0.81	    f4(162) -> 163*
0.16/0.81	    active0(2) -> 4*
0.16/0.81	    active0(1) -> 4*
0.16/0.81	    active0(3) -> 4*
0.16/0.81	    mark4(157) -> 158*
0.16/0.81	    c0() -> 1*
0.16/0.81	    top4(169) -> 170*
0.16/0.81	    mark0(2) -> 2*
0.16/0.81	    mark0(1) -> 2*
0.16/0.81	    mark0(3) -> 2*
0.16/0.81	    active4(173) -> 174*
0.16/0.81	    f0(2) -> 6*
0.16/0.81	    f0(1) -> 6*
0.16/0.81	    f0(3) -> 6*
0.16/0.81	    proper4(168) -> 169*
0.16/0.81	    g0(2) -> 7*
0.16/0.81	    g0(1) -> 7*
0.16/0.81	    g0(3) -> 7*
0.16/0.81	    g5(182) -> 183*
0.16/0.81	    g5(210) -> 211*
0.16/0.81	    g5(175) -> 176*
0.16/0.81	    proper0(2) -> 5*
0.16/0.81	    proper0(1) -> 5*
0.16/0.81	    proper0(3) -> 5*
0.16/0.81	    proper5(187) -> 188*
0.16/0.81	    proper5(181) -> 182*
0.16/0.81	    ok0(2) -> 3*
0.16/0.81	    ok0(1) -> 3*
0.16/0.81	    ok0(3) -> 3*
0.16/0.81	    mark5(176) -> 177*
0.16/0.81	    top0(2) -> 8*
0.16/0.81	    top0(1) -> 8*
0.16/0.81	    top0(3) -> 8*
0.16/0.81	    top5(188) -> 189*
0.16/0.81	    top1(53) -> 54*
0.16/0.81	    g6(194) -> 195*
0.16/0.81	    active1(69) -> 70*
0.16/0.81	    active1(71) -> 72*
0.16/0.81	    active1(63) -> 64*
0.16/0.81	    proper6(193) -> 194*
0.16/0.81	    proper1(55) -> 56*
0.16/0.81	    proper1(52) -> 53*
0.16/0.81	    proper1(61) -> 62*
0.16/0.81	    active5(203) -> 204*
0.16/0.81	    ok1(25) -> 26*
0.16/0.81	    ok1(17) -> 18*
0.16/0.81	    ok1(36) -> 37*
0.16/0.81	    c4() -> 201*
0.16/0.81	    g1(45) -> 46*
0.16/0.81	    g1(35) -> 36*
0.16/0.81	    g1(43) -> 44*
0.16/0.81	    g1(13) -> 14*
0.16/0.81	    ok5(211) -> 212*
0.16/0.81	    f1(27) -> 28*
0.16/0.81	    f1(24) -> 25*
0.16/0.81	    f1(14) -> 15*
0.16/0.81	    f1(33) -> 34*
0.16/0.81	    top6(217) -> 218*
0.16/0.81	    c1() -> 13*
0.16/0.81	    active6(216) -> 217*
0.16/0.81	    mark1(15) -> 16*
0.16/0.81	    top2(79) -> 80*
0.16/0.81	    active2(83) -> 84*
0.16/0.81	    proper2(102) -> 103*
0.16/0.81	    proper2(93) -> 94*
0.16/0.81	    proper2(78) -> 79*
0.16/0.81	    f2(94) -> 95*
0.16/0.81	    f2(86) -> 87*
0.16/0.81	    mark2(87) -> 88*
0.16/0.81	    g2(85) -> 86*
0.16/0.81	    g2(103) -> 104*
0.16/0.81	    c2() -> 85*
0.16/0.81	    top3(106) -> 107*
0.16/0.81	    proper3(121) -> 122*
0.16/0.81	    proper3(118) -> 119*
0.16/0.81	    proper3(105) -> 106*
0.16/0.81	    1 -> 69,55,43,27
0.16/0.81	    2 -> 63,52,35,24
0.16/0.81	    3 -> 71,61,45,33
0.16/0.81	    13 -> 102,17
0.16/0.81	    14 -> 93*
0.16/0.81	    15 -> 78*
0.16/0.81	    16 -> 70,53,4
0.16/0.81	    17 -> 83*
0.16/0.81	    18 -> 56,53,5
0.16/0.81	    26 -> 34,25,6
0.16/0.81	    28 -> 25*
0.16/0.81	    34 -> 25*
0.16/0.81	    37 -> 46,36,7
0.16/0.81	    44 -> 36*
0.16/0.81	    46 -> 36*
0.16/0.81	    54 -> 8*
0.16/0.81	    56 -> 53*
0.16/0.81	    62 -> 53*
0.16/0.81	    64 -> 53*
0.16/0.81	    70 -> 53*
0.16/0.81	    72 -> 53*
0.16/0.81	    80 -> 54,8
0.16/0.81	    84 -> 79*
0.16/0.81	    85 -> 121,111
0.16/0.81	    86 -> 118*
0.16/0.81	    87 -> 105*
0.16/0.81	    88 -> 84,79
0.16/0.81	    95 -> 79*
0.16/0.81	    104 -> 94*
0.16/0.81	    107 -> 80,54
0.16/0.81	    111 -> 130*
0.16/0.81	    112 -> 103*
0.16/0.81	    120 -> 106*
0.16/0.81	    123 -> 119*
0.16/0.81	    130 -> 156*
0.16/0.81	    131 -> 137*
0.16/0.81	    132 -> 104,94
0.16/0.81	    135 -> 143*
0.16/0.81	    136 -> 182,122
0.16/0.81	    138 -> 149*
0.16/0.81	    139 -> 95,79
0.16/0.81	    143 -> 175*
0.16/0.81	    144 -> 203,162
0.16/0.81	    145 -> 183,169,123,119
0.16/0.81	    150 -> 106*
0.16/0.81	    156 -> 181*
0.16/0.81	    157 -> 168*
0.16/0.81	    158 -> 150,106
0.16/0.81	    163 -> 173*
0.16/0.81	    164 -> 120,106
0.16/0.81	    170 -> 107,80
0.16/0.81	    174 -> 169*
0.16/0.81	    175 -> 193*
0.16/0.81	    176 -> 187*
0.16/0.81	    177 -> 174,169
0.16/0.81	    183 -> 169*
0.16/0.81	    189 -> 170,107
0.16/0.81	    195 -> 188*
0.16/0.81	    201 -> 210*
0.16/0.81	    202 -> 194*
0.16/0.81	    204 -> 188*
0.16/0.81	    211 -> 216*
0.16/0.81	    212 -> 195,188
0.16/0.81	    218 -> 189,170
0.16/0.81	  problem:
0.16/0.81	   
0.16/0.81	  Qed
0.16/0.81	EOF