proposition: Lemma subcode_nth_compose i j codes offset : j = length (compose (firstn i codes) offset) -> subcode.subcode (j + offset, nth i codes (fun=> []) (j + offset)) (offset, compose codes offset).
proof: Proof. move=> -> /=. elim: codes i offset => /=. { rewrite /compose. by move=> [|i] /=; exists nil, nil; rewrite /= Nat.add_0_r. } move=> code codes IH [|i] offset /=. - eexists nil, _. by rewrite /= Nat.add_0_r. - have [l [r [-> Hl]]] := IH i (length (code offset) + offset). eexists (code offset ++ l), _. rewrite !app_length. split; [|lia]. rewrite -!app_assoc. do 3 congr app. congr (nth i codes). lia. 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