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