YES(?,O(n^1))
0.17/0.53	YES(?,O(n^1))
0.17/0.53	
0.17/0.53	Problem:
0.17/0.53	 f(f(X)) -> c(n__f(n__g(n__f(X))))
0.17/0.53	 c(X) -> d(activate(X))
0.17/0.53	 h(X) -> c(n__d(X))
0.17/0.53	 f(X) -> n__f(X)
0.17/0.53	 g(X) -> n__g(X)
0.17/0.53	 d(X) -> n__d(X)
0.17/0.53	 activate(n__f(X)) -> f(activate(X))
0.17/0.53	 activate(n__g(X)) -> g(X)
0.17/0.53	 activate(n__d(X)) -> d(X)
0.17/0.53	 activate(X) -> X
0.17/0.53	
0.17/0.53	Proof:
0.17/0.53	 Bounds Processor:
0.17/0.53	  bound: 4
0.17/0.53	  enrichment: match
0.17/0.53	  automaton:
0.17/0.53	   final states: {9,8,7,6,5,4}
0.17/0.53	   transitions:
0.17/0.53	    n__d4(194) -> 195*
0.17/0.53	    d1(96) -> 97*
0.17/0.53	    d1(11) -> 12*
0.17/0.53	    d1(88) -> 89*
0.17/0.53	    d1(90) -> 91*
0.17/0.53	    g3(216) -> 217*
0.17/0.53	    g3(208) -> 209*
0.17/0.53	    g3(210) -> 211*
0.17/0.53	    g1(80) -> 81*
0.17/0.53	    g1(82) -> 83*
0.17/0.53	    g1(74) -> 75*
0.17/0.53	    n__f4(204) -> 205*
0.17/0.53	    f1(72) -> 73*
0.17/0.53	    f1(64) -> 65*
0.17/0.53	    f1(66) -> 67*
0.17/0.53	    n__g4(222) -> 223*
0.17/0.53	    n__g4(228) -> 229*
0.17/0.53	    n__g4(220) -> 221*
0.17/0.53	    activate1(20) -> 21*
0.17/0.53	    activate1(10) -> 11*
0.17/0.53	    activate1(18) -> 19*
0.17/0.53	    n__d1(30) -> 31*
0.17/0.53	    n__d1(27) -> 28*
0.17/0.53	    n__d1(36) -> 37*
0.17/0.53	    n__g1(60) -> 61*
0.17/0.53	    n__g1(52) -> 53*
0.17/0.53	    n__g1(54) -> 55*
0.17/0.53	    n__f1(44) -> 45*
0.17/0.53	    n__f1(46) -> 47*
0.17/0.53	    n__f1(38) -> 39*
0.17/0.53	    c1(28) -> 29*
0.17/0.53	    n__d2(132) -> 133*
0.17/0.53	    n__d2(138) -> 139*
0.17/0.53	    n__d2(140) -> 141*
0.17/0.53	    n__d2(130) -> 131*
0.17/0.53	    n__g2(122) -> 123*
0.17/0.53	    n__g2(144) -> 145*
0.17/0.53	    n__g2(124) -> 125*
0.17/0.53	    n__g2(156) -> 157*
0.17/0.53	    n__g2(116) -> 117*
0.17/0.53	    n__g2(148) -> 149*
0.17/0.53	    f0(2) -> 4*
0.17/0.53	    f0(1) -> 4*
0.17/0.53	    f0(3) -> 4*
0.17/0.53	    n__f2(114) -> 115*
0.17/0.53	    n__f2(106) -> 107*
0.17/0.53	    n__f2(108) -> 109*
0.17/0.53	    n__f2(145) -> 146*
0.17/0.53	    c0(2) -> 5*
0.17/0.53	    c0(1) -> 5*
0.17/0.53	    c0(3) -> 5*
0.17/0.53	    d2(172) -> 173*
0.17/0.53	    d2(102) -> 103*
0.17/0.53	    d2(164) -> 165*
0.17/0.53	    d2(166) -> 167*
0.17/0.53	    n__f0(2) -> 1*
0.17/0.53	    n__f0(1) -> 1*
0.17/0.53	    n__f0(3) -> 1*
0.17/0.53	    activate2(101) -> 102*
0.17/0.53	    n__g0(2) -> 2*
0.17/0.53	    n__g0(1) -> 2*
0.17/0.53	    n__g0(3) -> 2*
0.17/0.53	    n__d3(182) -> 183*
0.17/0.53	    n__d3(186) -> 187*
0.17/0.53	    n__d3(188) -> 189*
0.17/0.53	    n__d3(160) -> 161*
0.17/0.53	    d0(2) -> 8*
0.17/0.53	    d0(1) -> 8*
0.17/0.53	    d0(3) -> 8*
0.17/0.53	    c2(146) -> 147*
0.17/0.53	    activate0(2) -> 9*
0.17/0.53	    activate0(1) -> 9*
0.17/0.53	    activate0(3) -> 9*
0.17/0.53	    d3(177) -> 178*
0.17/0.53	    h0(2) -> 6*
0.17/0.53	    h0(1) -> 6*
0.17/0.53	    h0(3) -> 6*
0.17/0.53	    activate3(176) -> 177*
0.17/0.53	    activate3(198) -> 199*
0.17/0.53	    n__d0(2) -> 3*
0.17/0.53	    n__d0(1) -> 3*
0.17/0.53	    n__d0(3) -> 3*
0.17/0.53	    f3(199) -> 200*
0.17/0.53	    g0(2) -> 7*
0.17/0.53	    g0(1) -> 7*
0.17/0.53	    g0(3) -> 7*
0.17/0.53	    1 -> 9,90,80,54,44,30,18
0.17/0.53	    2 -> 9,88,74,60,46,36,20
0.17/0.53	    3 -> 9,96,82,52,38,27,10
0.17/0.53	    10 -> 11,72
0.17/0.53	    11 -> 130,72
0.17/0.53	    12 -> 5*
0.17/0.53	    18 -> 19,66,11,72
0.17/0.53	    19 -> 66,11
0.17/0.53	    20 -> 21,11,72,64
0.17/0.53	    21 -> 64,11
0.17/0.53	    27 -> 166*
0.17/0.53	    28 -> 101,8
0.17/0.53	    29 -> 6*
0.17/0.53	    30 -> 164*
0.17/0.53	    31 -> 28*
0.17/0.53	    36 -> 172*
0.17/0.53	    37 -> 28*
0.17/0.53	    39 -> 4*
0.17/0.53	    45 -> 4*
0.17/0.53	    47 -> 4*
0.17/0.53	    53 -> 7*
0.17/0.53	    55 -> 7*
0.17/0.53	    61 -> 7*
0.17/0.53	    64 -> 106*
0.17/0.53	    65 -> 19,66,11,72,9
0.17/0.53	    66 -> 108*
0.17/0.53	    67 -> 19,66,11,72,9
0.17/0.53	    72 -> 114*
0.17/0.53	    73 -> 19,66,11,72,9
0.17/0.53	    74 -> 122*
0.17/0.53	    75 -> 21,64,11,72,9
0.17/0.53	    80 -> 124*
0.17/0.53	    81 -> 21,64,11,72,9
0.17/0.53	    82 -> 116*
0.17/0.53	    83 -> 21,64,11,72,9
0.17/0.53	    88 -> 132*
0.17/0.53	    89 -> 11,72,9
0.17/0.53	    90 -> 138*
0.17/0.53	    91 -> 11,72,9
0.17/0.53	    96 -> 140*
0.17/0.53	    97 -> 11,72,9
0.17/0.53	    101 -> 102*
0.17/0.53	    102 -> 160*
0.17/0.53	    103 -> 29,6
0.17/0.53	    107 -> 148,65
0.17/0.53	    109 -> 156,67,9
0.17/0.53	    115 -> 144,73,9
0.17/0.53	    117 -> 83*
0.17/0.53	    123 -> 75,9
0.17/0.53	    125 -> 81,9
0.17/0.53	    131 -> 12*
0.17/0.53	    133 -> 89*
0.17/0.53	    139 -> 91,9
0.17/0.53	    141 -> 97,9
0.17/0.53	    144 -> 208*
0.17/0.53	    145 -> 198*
0.17/0.53	    146 -> 176*
0.17/0.53	    147 -> 73,67
0.17/0.53	    148 -> 216*
0.17/0.53	    149 -> 145*
0.17/0.53	    156 -> 210*
0.17/0.53	    157 -> 145*
0.17/0.53	    161 -> 103,29
0.17/0.53	    164 -> 182*
0.17/0.53	    165 -> 102*
0.17/0.53	    166 -> 186*
0.17/0.53	    167 -> 102*
0.17/0.53	    172 -> 188*
0.17/0.53	    173 -> 102*
0.17/0.53	    176 -> 177*
0.17/0.53	    177 -> 194*
0.17/0.53	    178 -> 147,67,73,72,66,108,114
0.17/0.53	    183 -> 165*
0.17/0.53	    187 -> 167,102,160
0.17/0.53	    189 -> 173,102,160
0.17/0.53	    195 -> 178,147,73,67,19
0.17/0.53	    198 -> 199*
0.17/0.53	    199 -> 204*
0.17/0.53	    200 -> 177*
0.17/0.53	    205 -> 200,177,194
0.17/0.53	    208 -> 220*
0.17/0.53	    209 -> 199*
0.17/0.53	    210 -> 222*
0.17/0.53	    211 -> 199*
0.17/0.53	    216 -> 228*
0.17/0.53	    217 -> 199*
0.17/0.53	    221 -> 209*
0.17/0.53	    223 -> 211,199,204
0.17/0.53	    229 -> 217,199,204
0.17/0.53	  problem:
0.17/0.53	   
0.17/0.53	  Qed
0.17/0.54	EOF