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