proposition: Fact linker_out_err j : err = lsum (snd P) + i -> out_code j P -> linker j = err.
proof: Proof. intros H1 H2. destruct (eq_nat_dec j (code_end P)) as [ H | H ]. + rewrite H1, H; unfold code_end. rewrite Nat.add_comm, linker_app with (mm := nil); auto. rewrite app_nil_r; auto. + apply linker_err_code; red in H2; unfold code_end, code_start in *; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)