proposition: Lemma read_current_char {m} {cs : vec nat m} {ts i k} : encodes_counters cs ts -> vec_pos cs i = k -> match k with | 0 => vec_pos (TM_facts.current_chars ts) i = Some true | S _ => vec_pos (TM_facts.current_chars ts) i = Some false \/ vec_pos (TM_facts.current_chars ts) i = None end.
proof: Proof. move=> H. elim: H i. { move=> i. by case: (pos_O_inv i). } move=> {}m c t {}cs {}ts Hct Hcsts IH i. have [->|[i' ->]] := pos_S_inv i. - case: Hct => /= *; subst k; by intuition done. - by apply: IH. Qed.
imports: Undecidability.MinskyMachines(MM MMA.mma_defs) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL.EqDec List Vector Lia PeanoNat Compare_dec ssreflect ssrbool ssrfun