proposition: Fact encode_mm_instr_in_inv n i P el c er : @encode_mm_instr n i P = el++c::er -> exists l rho r, P = l++rho::r /\ In c (encode_one_instr (length l+i) rho).
proof: Proof. revert i el c er; induction P as [ | rho P IHP ]; simpl; intros i el c er H. + destruct el; discriminate. + destruct list_app_cons_eq_inv with (1 := H) as [ (m & H1 & H2) | (m & H1 & H2) ]. * destruct IHP with (1 := H2) as (l & rho' & r & G1 & G2). exists (rho::l), rho', r; subst; split; auto. eq goal G2; do 2 f_equal; simpl; lia. * exists nil, rho, P; split; simpl; auto. rewrite <- H1; apply in_or_app; simpl; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs mm_no_self) Undecidability.FRACTRAN(FRACTRAN fractran_utils prime_seq FRACTRAN_sss)