1068 where |
1068 where |
1069 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] " |
1069 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] " |
1070 |
1070 |
1071 (* invariants of dither *) |
1071 (* invariants of dither *) |
1072 abbreviation |
1072 abbreviation |
1073 "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]" |
1073 "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]" |
1074 |
1074 |
1075 abbreviation |
1075 abbreviation |
1076 "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1076 "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]" |
1077 |
1077 |
1078 lemma dither_unhalt_state: |
1078 lemma dither_unhalt_state: |
1079 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> |
1079 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> |
1080 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))" |
1080 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))" |
1081 apply(induct stp) |
1081 apply(induct stp) |