proposition: Lemma steps_backward m i P i1 v1 k st : @mm_no_self_loops m (i, P) -> encode_mm_instr i P /F/ encode_state (i1,v1) -[k]-> st -> exists i2 v2, (i, P) /MM/ (i1, v1) -[k]-> (i2,v2) /\ st = encode_state (i2,v2).
proof: Proof. intros H1. revert i1 v1 st; induction k as [ | k IHk ]; intros i1 v1 st H; simpl in H. - subst; exists i1, v1; split; auto; constructor. - destruct H as (st1 & H2 & H3). destruct one_step_backward with (2 := H2) as (i2 & v2 & -> & H5); auto. destruct IHk with (1 := H3) as (i3 & v3 & ? & ->). exists i3, v3; split; auto. constructor 2 with (i2,v2); 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)