proposition: Fact mma2_linstr_enc_In i P c : c ∊ ⟪i,P⟫ₗ -> exists L ρ R, P = L++ρ::R /\ c ∊ ⟨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(MMA mma_defs ndMM2) Undecidability.Shared.Libs.DLW(utils Vec.pos Vec.vec Code.subcode Code.sss) Undecidability.Synthetic(Definitions ReducibilityFacts)