proposition: Lemma compose_sss_compute_length_trans (i : nat) {codes : list (nat -> list mm_instr)} {lengths} {offset} {v st st'} : Forall2 (fun c l => forall j, length (c j) = l) codes lengths -> let j := list_sum (firstn i lengths) 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=> Hcl. suff -> : list_sum (firstn i lengths) = length (compose (firstn i codes) offset) by apply: compose_sss_compute_trans. elim: Hcl i offset. { by case. } move=> c l {}codes {}lengths Hcl _ IH [|i] offset. { done. } by rewrite /= app_length -IH Hcl. 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