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