proposition: Fact mm2_linstr_enc_In i P c : In c (mm2_linstr_enc i P) -> exists l r ρ, P = l++ρ::r /\ In c (mm2_instr_enc (length l+i) ρ).
proof: Proof. revert i; induction P as [ | ρ P IH ]; intros i. + intros []. + simpl; rewrite in_app_iff; intros [ H | H ]. * exists nil, P, ρ; split; auto. * destruct (IH (1+i)) as (l & r & ρ' & H1 & H2); auto. exists (ρ::l), r, ρ'; split; auto. - simpl; f_equal; auto. - eq goal H2; do 2 f_equal; simpl; lia. Qed.
imports: List Arith Lia Relations Undecidability.MinskyMachines(MM2 ndMM2) Undecidability.Shared.Libs.DLW(utils) Undecidability.Synthetic(Definitions ReducibilityFacts)