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