YES(?,O(n^1)) 3.80/1.29 YES(?,O(n^1)) 4.19/1.30 4.19/1.30 Problem: 4.19/1.30 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1)))))))))) 4.19/1.30 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1))))))))))))) 4.19/1.30 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))) 4.19/1.30 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))) 4.19/1.30 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))) 4.19/1.30 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))) 4.19/1.30 0(1(2(1(x1)))) -> 4.19/1.30 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))) 4.19/1.30 0(1(2(1(x1)))) -> 4.19/1.30 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))) 4.19/1.30 4.19/1.30 Proof: 4.19/1.30 Bounds Processor: 4.19/1.30 bound: 3 4.19/1.30 enrichment: match 4.19/1.30 automaton: 4.19/1.30 final states: {4} 4.19/1.30 transitions: 4.19/1.30 13(107) -> 108* 4.19/1.30 13(102) -> 103* 4.19/1.30 13(136) -> 137* 4.19/1.30 13(138) -> 139* 4.19/1.30 13(133) -> 134* 4.19/1.30 13(108) -> 109* 4.19/1.30 13(135) -> 136* 4.19/1.30 13(130) -> 131* 4.19/1.30 13(110) -> 111* 4.19/1.30 13(105) -> 106* 4.19/1.30 11(25) -> 26* 4.19/1.30 11(20) -> 21* 4.19/1.30 11(22) -> 23* 4.19/1.30 11(17) -> 18* 4.19/1.30 11(23) -> 24* 4.19/1.30 23(157) -> 158* 4.19/1.30 23(137) -> 138* 4.19/1.30 23(132) -> 133* 4.19/1.30 23(127) -> 128* 4.19/1.30 23(112) -> 113* 4.19/1.30 23(144) -> 145* 4.19/1.30 23(129) -> 130* 4.19/1.30 23(109) -> 110* 4.19/1.30 23(104) -> 105* 4.19/1.30 23(101) -> 102* 4.19/1.30 21(35) -> 36* 4.19/1.30 21(27) -> 28* 4.19/1.30 21(24) -> 25* 4.19/1.30 21(19) -> 20* 4.19/1.30 21(16) -> 17* 4.19/1.30 21(33) -> 34* 4.19/1.30 03(134) -> 135* 4.19/1.30 03(131) -> 132* 4.19/1.30 03(106) -> 107* 4.19/1.30 03(103) -> 104* 4.19/1.30 01(21) -> 22* 4.19/1.30 01(18) -> 19* 4.19/1.30 12(65) -> 66* 4.19/1.30 12(60) -> 61* 4.19/1.30 12(50) -> 51* 4.19/1.30 12(45) -> 46* 4.19/1.30 12(62) -> 63* 4.19/1.30 12(57) -> 58* 4.19/1.30 12(47) -> 48* 4.19/1.30 12(42) -> 43* 4.19/1.30 12(63) -> 64* 4.19/1.30 12(48) -> 49* 4.19/1.30 00(4) -> 4* 4.19/1.30 22(97) -> 98* 4.19/1.30 22(64) -> 65* 4.19/1.30 22(59) -> 60* 4.19/1.30 22(54) -> 55* 4.19/1.30 22(49) -> 50* 4.19/1.30 22(44) -> 45* 4.19/1.30 22(56) -> 57* 4.19/1.30 22(41) -> 42* 4.19/1.30 22(95) -> 96* 4.19/1.30 22(80) -> 81* 4.19/1.30 10(4) -> 4* 4.19/1.30 02(61) -> 62* 4.19/1.30 02(46) -> 47* 4.19/1.30 02(58) -> 59* 4.19/1.30 02(43) -> 44* 4.19/1.30 20(4) -> 4* 4.19/1.30 4 -> 16* 4.19/1.30 22 -> 80,27 4.19/1.30 23 -> 33* 4.19/1.30 25 -> 41,35 4.19/1.30 26 -> 19,4 4.19/1.30 28 -> 20* 4.19/1.30 34 -> 17* 4.19/1.30 36 -> 17* 4.19/1.30 47 -> 54* 4.19/1.30 50 -> 112,56 4.19/1.30 51 -> 22,27,19 4.19/1.30 55 -> 45* 4.19/1.30 62 -> 95* 4.19/1.30 65 -> 101,97 4.19/1.30 66 -> 22,27 4.19/1.30 81 -> 42* 4.19/1.30 96 -> 45* 4.19/1.30 98 -> 42* 4.19/1.30 107 -> 127* 4.19/1.30 110 -> 129* 4.19/1.30 111 -> 44* 4.19/1.30 113 -> 102* 4.19/1.30 128 -> 105* 4.19/1.30 135 -> 144* 4.19/1.30 138 -> 157* 4.19/1.30 139 -> 47,54 4.19/1.30 145 -> 133* 4.19/1.30 158 -> 130* 4.19/1.30 problem: 4.19/1.30 4.19/1.30 Qed 4.19/1.30 EOF