proposition: Lemma shift_addr_outcode i : i < 1 \/ S (length P) <= i -> shift_addr i = S (length P).
proof: Proof. move: i => [|i] Hi /=; [done|]. case E: (S (length P) - i) => [|?]; [done|]. cbn in *. 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