proposition: Lemma steps_forward m i P i1 v1 i2 v2 k : @mm_no_self_loops m (i, P) -> (i, P) /MM/ (i1, v1) -[k]-> (i2,v2) -> encode_mm_instr i P /F/ encode_state (i1,v1) -[k]-> encode_state (i2,v2).
proof: Proof. intros HP H. revert v1 i1 i2 H. induction k; intros v1 i1 i2 H; inversion H; subst; clear H; cbn. - reflexivity. - destruct st2. eapply one_step_forward in H1; eauto. 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)