proposition: Lemma compose_sss_compute_trans {codes : list (nat -> list mm_instr)} {offset} (i : nat) {v st st'} : let j := length (compose (firstn i codes) offset) in (j + offset, (nth i codes (fun _ => [])) (j+offset)) // (j + offset, v) ->> st' -> (offset, compose codes offset) // st' ->> st -> (offset, compose codes offset) // (j + offset, v) ->> st.
proof: Proof. move=> j H. apply: sss_compute_trans. move: H. apply: subcode_sss_compute. by apply: subcode_nth_compose. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun