proposition: Lemma in_code_step {n s P} : subcode.in_code (fst s) P -> exists t, sss_step (@mma_sss n) P s t.
proof: Proof. move: s P => [i v] [offset P] /= ?. case E: (nth_error P (i - offset)) => [instr|]; first last. { move=> /nth_error_None in E. cbn in *. lia. } have [t Ht] := mma_sss_total_ni instr (i, v). move: E => /(nth_error_split P) [?] [?] [->] Hi. eexists t, offset, _, instr, _, v. split; [done|split; [|eassumption]]. congr pair. lia. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect