YES(?,O(n^1)) 0.16/0.36 YES(?,O(n^1)) 0.16/0.36 0.16/0.36 Problem: 0.16/0.36 b(a(b(a(a(x1))))) -> a(a(b(b(a(b(a(b(a(x1))))))))) 0.16/0.36 0.16/0.36 Proof: 0.16/0.36 Bounds Processor: 0.16/0.36 bound: 4 0.16/0.36 enrichment: match 0.16/0.36 automaton: 0.16/0.36 final states: {3} 0.16/0.36 transitions: 0.16/0.36 b3(142) -> 143* 0.16/0.36 b3(112) -> 113* 0.16/0.36 b3(102) -> 103* 0.16/0.36 b3(114) -> 115* 0.16/0.36 b3(104) -> 105* 0.16/0.36 b3(84) -> 85* 0.16/0.36 b3(79) -> 80* 0.16/0.36 b3(171) -> 172* 0.16/0.36 b3(166) -> 167* 0.16/0.36 b3(81) -> 82* 0.16/0.36 b3(168) -> 169* 0.16/0.36 b3(143) -> 144* 0.16/0.36 b3(138) -> 139* 0.16/0.36 b3(83) -> 84* 0.16/0.36 b3(170) -> 171* 0.16/0.36 b3(140) -> 141* 0.16/0.36 b3(115) -> 116* 0.16/0.36 b3(110) -> 111* 0.16/0.36 b3(105) -> 106* 0.16/0.36 b3(100) -> 101* 0.16/0.36 a4(212) -> 213* 0.16/0.36 a4(202) -> 203* 0.16/0.36 a4(204) -> 205* 0.16/0.36 a4(194) -> 195* 0.16/0.36 a4(164) -> 165* 0.16/0.36 a4(211) -> 212* 0.16/0.36 a4(206) -> 207* 0.16/0.36 a4(201) -> 202* 0.16/0.36 a4(196) -> 197* 0.16/0.36 a4(156) -> 157* 0.16/0.36 a4(208) -> 209* 0.16/0.36 a4(198) -> 199* 0.16/0.36 a4(163) -> 164* 0.16/0.36 a4(158) -> 159* 0.16/0.36 a4(160) -> 161* 0.16/0.36 b4(207) -> 208* 0.16/0.36 b4(197) -> 198* 0.16/0.36 b4(162) -> 163* 0.16/0.36 b4(157) -> 158* 0.16/0.36 b4(209) -> 210* 0.16/0.36 b4(199) -> 200* 0.16/0.36 b4(159) -> 160* 0.16/0.36 b4(161) -> 162* 0.16/0.36 b4(210) -> 211* 0.16/0.36 b4(205) -> 206* 0.16/0.36 b4(200) -> 201* 0.16/0.36 b4(195) -> 196* 0.16/0.36 b0(3) -> 3* 0.16/0.36 a0(3) -> 3* 0.16/0.36 a1(22) -> 23* 0.16/0.36 a1(14) -> 15* 0.16/0.36 a1(21) -> 22* 0.16/0.36 a1(16) -> 17* 0.16/0.36 a1(18) -> 19* 0.16/0.36 b1(50) -> 51* 0.16/0.36 b1(20) -> 21* 0.16/0.36 b1(15) -> 16* 0.16/0.36 b1(17) -> 18* 0.16/0.36 b1(19) -> 20* 0.16/0.36 b1(46) -> 47* 0.16/0.36 a2(65) -> 66* 0.16/0.36 a2(32) -> 33* 0.16/0.36 a2(64) -> 65* 0.16/0.36 a2(59) -> 60* 0.16/0.36 a2(54) -> 55* 0.16/0.36 a2(24) -> 25* 0.16/0.36 a2(61) -> 62* 0.16/0.36 a2(31) -> 32* 0.16/0.36 a2(26) -> 27* 0.16/0.36 a2(28) -> 29* 0.16/0.36 b2(60) -> 61* 0.16/0.36 b2(30) -> 31* 0.16/0.36 b2(25) -> 26* 0.16/0.36 b2(62) -> 63* 0.16/0.36 b2(27) -> 28* 0.16/0.36 b2(29) -> 30* 0.16/0.36 b2(76) -> 77* 0.16/0.36 b2(63) -> 64* 0.16/0.36 b2(58) -> 59* 0.16/0.36 a3(172) -> 173* 0.16/0.36 a3(167) -> 168* 0.16/0.36 a3(117) -> 118* 0.16/0.36 a3(107) -> 108* 0.16/0.36 a3(82) -> 83* 0.16/0.36 a3(169) -> 170* 0.16/0.36 a3(144) -> 145* 0.16/0.36 a3(139) -> 140* 0.16/0.36 a3(109) -> 110* 0.16/0.36 a3(141) -> 142* 0.16/0.36 a3(116) -> 117* 0.16/0.36 a3(111) -> 112* 0.16/0.36 a3(106) -> 107* 0.16/0.36 a3(101) -> 102* 0.16/0.36 a3(86) -> 87* 0.16/0.36 a3(173) -> 174* 0.16/0.36 a3(113) -> 114* 0.16/0.36 a3(103) -> 104* 0.16/0.36 a3(78) -> 79* 0.16/0.36 a3(145) -> 146* 0.16/0.36 a3(85) -> 86* 0.16/0.36 a3(80) -> 81* 0.16/0.36 3 -> 14* 0.16/0.36 21 -> 54* 0.16/0.36 22 -> 46,24 0.16/0.36 23 -> 16,50,18,3 0.16/0.36 32 -> 58* 0.16/0.36 33 -> 28,20,18 0.16/0.36 47 -> 16* 0.16/0.36 51 -> 16* 0.16/0.36 55 -> 25* 0.16/0.36 64 -> 109* 0.16/0.36 65 -> 78* 0.16/0.36 66 -> 76,26,47,16 0.16/0.36 77 -> 26* 0.16/0.36 86 -> 100* 0.16/0.36 87 -> 30* 0.16/0.36 106 -> 156* 0.16/0.36 108 -> 138,59 0.16/0.36 118 -> 82,28 0.16/0.36 145 -> 166* 0.16/0.36 146 -> 63* 0.16/0.36 165 -> 141* 0.16/0.36 172 -> 204* 0.16/0.36 173 -> 194* 0.16/0.36 174 -> 111* 0.16/0.36 203 -> 115* 0.16/0.36 213 -> 198* 0.16/0.36 problem: 0.16/0.36 0.16/0.36 Qed 0.16/0.37 EOF