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