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