proposition: Lemma one_step_forward m i P i1 v1 i2 v2 : @mm_no_self_loops m (i,P) -> (i, P) /MM/ (i1, v1) → (i2,v2) -> encode_mm_instr i P /F/ encode_state (i1,v1) → encode_state (i2,v2).
proof: Proof. Proof with eauto; try lia. intros HP (k & l & [ u | u j ] & r & v & ? & ? & ?); inversion H; subst; clear H. - inversion H0; inversion H1; subst; clear H0 H1. eapply skip_steps... econstructor. cbn. ring_simplify. replace (1 + (k + length l)) with (k + length l + 1) by lia. unfold encode_state, fst, snd. rewrite vec_prod_mult. rewrite Nat.add_0_r; ring. - inversion H0; inversion H1; subst; clear H0 H1. all:eapply skip_steps... + cbn. econstructor 2. intros [] % divides_mult_inv_l... eapply divides_mult_inv in H0 as [ | ]... * now eapply qs_ps_div in H0. * eapply qs_encode_state in H0. lia. * unfold encode_dec2. econstructor. unfold encode_state, fst, snd. ring. + econstructor. cbn. unfold encode_state, fst, snd. ring_simplify. replace (1 + (k + length l)) with (k + length l + 1) by lia. erewrite <- (vec_prod_div _ _ _ H4). rewrite Nat.add_0_r; ring. 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)