YES(?,O(n^1)) 0.16/0.42 YES(?,O(n^1)) 0.16/0.43 0.16/0.43 Problem: 0.16/0.43 a__f(f(X)) -> a__c(f(g(f(X)))) 0.16/0.43 a__c(X) -> d(X) 0.16/0.43 a__h(X) -> a__c(d(X)) 0.16/0.43 mark(f(X)) -> a__f(mark(X)) 0.16/0.43 mark(c(X)) -> a__c(X) 0.16/0.43 mark(h(X)) -> a__h(mark(X)) 0.16/0.43 mark(g(X)) -> g(X) 0.16/0.43 mark(d(X)) -> d(X) 0.16/0.43 a__f(X) -> f(X) 0.16/0.43 a__c(X) -> c(X) 0.16/0.43 a__h(X) -> h(X) 0.16/0.43 0.16/0.43 Proof: 0.16/0.43 Bounds Processor: 0.16/0.43 bound: 3 0.16/0.43 enrichment: match 0.16/0.43 automaton: 0.16/0.43 final states: {9,8,7,6} 0.16/0.43 transitions: 0.16/0.43 h1(172) -> 173* 0.16/0.43 h1(174) -> 175* 0.16/0.43 h1(164) -> 165* 0.16/0.43 h1(166) -> 167* 0.16/0.43 h1(180) -> 181* 0.16/0.43 c1(142) -> 143* 0.16/0.43 c1(156) -> 157* 0.16/0.43 c1(158) -> 159* 0.16/0.43 c1(148) -> 149* 0.16/0.43 c1(150) -> 151* 0.16/0.43 f1(20) -> 21* 0.16/0.43 f1(15) -> 16* 0.16/0.43 f1(17) -> 18* 0.16/0.43 f1(34) -> 35* 0.16/0.43 f1(26) -> 27* 0.16/0.43 f1(28) -> 29* 0.16/0.43 d1(50) -> 51* 0.16/0.43 d1(52) -> 53* 0.16/0.43 d1(42) -> 43* 0.16/0.43 d1(44) -> 45* 0.16/0.43 d1(36) -> 37* 0.16/0.43 g1(132) -> 133* 0.16/0.43 g1(134) -> 135* 0.16/0.43 g1(124) -> 125* 0.16/0.43 g1(126) -> 127* 0.16/0.43 g1(16) -> 17* 0.16/0.43 g1(140) -> 141* 0.16/0.43 a__h1(118) -> 119* 0.16/0.43 mark1(92) -> 93* 0.16/0.43 mark1(94) -> 95* 0.16/0.43 mark1(84) -> 85* 0.16/0.43 mark1(86) -> 87* 0.16/0.43 mark1(76) -> 77* 0.16/0.43 a__c1(60) -> 61* 0.16/0.43 a__c1(102) -> 103* 0.16/0.43 a__c1(74) -> 75* 0.16/0.43 a__c1(116) -> 117* 0.16/0.43 a__c1(66) -> 67* 0.16/0.43 a__c1(108) -> 109* 0.16/0.43 a__c1(68) -> 69* 0.16/0.43 a__c1(58) -> 59* 0.16/0.43 a__c1(18) -> 19* 0.16/0.43 a__c1(110) -> 111* 0.16/0.43 a__c1(100) -> 101* 0.16/0.43 a__f1(77) -> 78* 0.16/0.43 h2(280) -> 281* 0.16/0.43 a__f0(5) -> 6* 0.16/0.43 a__f0(2) -> 6* 0.16/0.43 a__f0(4) -> 6* 0.16/0.43 a__f0(1) -> 6* 0.16/0.43 a__f0(3) -> 6* 0.16/0.43 c2(262) -> 263* 0.16/0.43 c2(254) -> 255* 0.16/0.43 c2(234) -> 235* 0.16/0.43 c2(276) -> 277* 0.16/0.43 c2(256) -> 257* 0.16/0.43 c2(246) -> 247* 0.16/0.43 c2(268) -> 269* 0.16/0.43 c2(248) -> 249* 0.16/0.43 c2(238) -> 239* 0.16/0.43 c2(270) -> 271* 0.16/0.43 c2(240) -> 241* 0.16/0.43 f0(5) -> 1* 0.16/0.43 f0(2) -> 1* 0.16/0.43 f0(4) -> 1* 0.16/0.43 f0(1) -> 1* 0.16/0.43 f0(3) -> 1* 0.16/0.43 f2(232) -> 233* 0.16/0.43 f2(283) -> 284* 0.16/0.43 a__c0(5) -> 7* 0.16/0.43 a__c0(2) -> 7* 0.16/0.43 a__c0(4) -> 7* 0.16/0.43 a__c0(1) -> 7* 0.16/0.43 a__c0(3) -> 7* 0.16/0.43 a__c2(227) -> 228* 0.16/0.43 g0(5) -> 2* 0.16/0.43 g0(2) -> 2* 0.16/0.43 g0(4) -> 2* 0.16/0.43 g0(1) -> 2* 0.16/0.43 g0(3) -> 2* 0.16/0.43 d2(212) -> 213* 0.16/0.43 d2(182) -> 183* 0.16/0.43 d2(224) -> 225* 0.16/0.43 d2(204) -> 205* 0.16/0.43 d2(226) -> 227* 0.16/0.43 d2(206) -> 207* 0.16/0.43 d2(196) -> 197* 0.16/0.43 d2(218) -> 219* 0.16/0.43 d2(198) -> 199* 0.16/0.43 d2(188) -> 189* 0.16/0.43 d2(220) -> 221* 0.16/0.43 d2(190) -> 191* 0.16/0.43 d0(5) -> 3* 0.16/0.43 d0(2) -> 3* 0.16/0.43 d0(4) -> 3* 0.16/0.43 d0(1) -> 3* 0.16/0.43 d0(3) -> 3* 0.16/0.43 c3(292) -> 293* 0.16/0.43 a__h0(5) -> 8* 0.16/0.43 a__h0(2) -> 8* 0.16/0.43 a__h0(4) -> 8* 0.16/0.43 a__h0(1) -> 8* 0.16/0.43 a__h0(3) -> 8* 0.16/0.43 d3(287) -> 288* 0.16/0.43 mark0(5) -> 9* 0.16/0.43 mark0(2) -> 9* 0.16/0.43 mark0(4) -> 9* 0.16/0.43 mark0(1) -> 9* 0.16/0.43 mark0(3) -> 9* 0.16/0.43 g2(282) -> 283* 0.16/0.43 c0(5) -> 4* 0.16/0.43 c0(2) -> 4* 0.16/0.43 c0(4) -> 4* 0.16/0.43 c0(1) -> 4* 0.16/0.43 c0(3) -> 4* 0.16/0.43 h0(5) -> 5* 0.16/0.43 h0(2) -> 5* 0.16/0.43 h0(4) -> 5* 0.16/0.43 h0(1) -> 5* 0.16/0.43 h0(3) -> 5* 0.16/0.43 1 -> 166,148,134,110,92,42,28 0.16/0.43 2 -> 174,156,126,102,84,50,20 0.16/0.43 3 -> 164,142,140,116,94,36,34 0.16/0.43 4 -> 172,150,132,108,86,44,26 0.16/0.43 5 -> 180,158,124,100,76,52,15 0.16/0.43 16 -> 6* 0.16/0.43 18 -> 248,198 0.16/0.43 19 -> 6* 0.16/0.43 21 -> 6,16 0.16/0.43 27 -> 6,16 0.16/0.43 29 -> 6,16 0.16/0.43 35 -> 6,16 0.16/0.43 37 -> 95,77,118,9,58,7 0.16/0.43 43 -> 95,77,118,9,60,7 0.16/0.43 45 -> 95,77,118,9,66,7 0.16/0.43 51 -> 95,77,118,9,68,7 0.16/0.43 53 -> 95,77,118,9,74,7 0.16/0.43 58 -> 246,196 0.16/0.43 59 -> 8* 0.16/0.43 60 -> 276,224 0.16/0.43 61 -> 8* 0.16/0.43 66 -> 268,218 0.16/0.43 67 -> 8* 0.16/0.43 68 -> 262,212 0.16/0.43 69 -> 8* 0.16/0.43 74 -> 270,220 0.16/0.43 75 -> 8* 0.16/0.43 77 -> 232,118 0.16/0.43 78 -> 93,77,118,9 0.16/0.43 85 -> 77* 0.16/0.43 87 -> 77* 0.16/0.43 93 -> 77* 0.16/0.43 95 -> 77* 0.16/0.43 100 -> 256,206 0.16/0.43 101 -> 87,77,118,9 0.16/0.43 102 -> 234,182 0.16/0.43 103 -> 87,77,118,9 0.16/0.43 108 -> 240,190 0.16/0.43 109 -> 87,77,118,9 0.16/0.43 110 -> 254,204 0.16/0.43 111 -> 87,77,118,9 0.16/0.43 116 -> 238,188 0.16/0.43 117 -> 87,77,118,9 0.16/0.43 118 -> 280,226 0.16/0.43 119 -> 77,118,9 0.16/0.43 125 -> 85,77,118,9 0.16/0.43 127 -> 85,77,118,9 0.16/0.43 133 -> 85,77,118,9 0.16/0.43 135 -> 85,77,118,9 0.16/0.43 141 -> 85,77,118,9 0.16/0.43 143 -> 7* 0.16/0.43 149 -> 7* 0.16/0.43 151 -> 7* 0.16/0.43 157 -> 7* 0.16/0.43 159 -> 7* 0.16/0.43 165 -> 8* 0.16/0.43 167 -> 8* 0.16/0.43 173 -> 8* 0.16/0.43 175 -> 8* 0.16/0.43 181 -> 8* 0.16/0.43 183 -> 103* 0.16/0.43 189 -> 117* 0.16/0.43 191 -> 109* 0.16/0.43 197 -> 59* 0.16/0.43 199 -> 19* 0.16/0.43 205 -> 111* 0.16/0.43 207 -> 101,9 0.16/0.43 213 -> 69,8 0.16/0.43 219 -> 67,8 0.16/0.43 221 -> 75,8 0.16/0.43 225 -> 61,8 0.16/0.43 227 -> 292,287 0.16/0.43 228 -> 78,93,119,9 0.16/0.43 233 -> 282,78,9 0.16/0.43 235 -> 103* 0.16/0.43 239 -> 117* 0.16/0.43 241 -> 109* 0.16/0.43 247 -> 59* 0.16/0.43 249 -> 19* 0.16/0.43 255 -> 111* 0.16/0.43 257 -> 101,9 0.16/0.43 263 -> 69,8 0.16/0.43 269 -> 67,8 0.16/0.43 271 -> 75,8 0.16/0.43 277 -> 61,8 0.16/0.43 281 -> 119,9 0.16/0.43 284 -> 227* 0.16/0.43 288 -> 228,119 0.16/0.43 293 -> 228,119 0.16/0.43 problem: 0.16/0.43 0.16/0.43 Qed 0.16/0.43 EOF