proposition: Lemma skip_steps m k l r k' (v v' : vec _ m) : @mm_no_self_loops m (k, l ++ r) -> encode_mm_instr (k + length l) r /F/ encode_state (k + length l,v) → encode_state (k',v') -> encode_mm_instr k (l ++ r) /F/ encode_state (k + length l,v) → encode_state (k',v').
proof: Proof. Proof with eauto; try lia. revert k. induction l; cbn - [subcode] in *; intros. - revert H0. ring_simplify (k + 0). eauto. - revert H0. ring_simplify (k + S (length l)). intros H1. destruct a. + econstructor 2. intros [[|] % divides_mult_inv | ] % divides_mult_inv; eauto. * eapply primestream_divides in H0; lia. * now eapply ps_qs_div in H0. * eapply divides_encode_state in H0; lia. * specialize IHl with (k := S k). revert IHl. cbn - [subcode]. ring_simplify (S (k + length l)). intros IHl. eapply IHl. 2:exact H1. intros ? ? ?. eapply H. eapply subcode_cons. eassumption. + repeat econstructor 2. 2:unfold encode_dec2. 2,3: cbn- [subcode]. 1: intros [] % divides_mult_inv_l. 2: intros [ | ] % divides_mult_inv... * eapply divides_mult_inv in H0 as [? | ?]... eapply primestream_divides in H0... eapply divides_encode_state in H0... * eapply primestream_divides in H0... subst. eapply (H n t). eauto. * eapply divides_encode_state in H0... * specialize (IHl (S k)). revert IHl. cbn - [subcode]. ring_simplify (S (k + length l)). intros IHl. eapply IHl. 2:exact H1. intros ? ? ?. eapply H. eapply subcode_cons. eassumption. 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)