proposition: Lemma divides_encode_state i k n v : divides (ps i) (@encode_state n (k,v)) -> i = k.
proof: Proof. unfold encode_state. intros. induction v. - cbn in H. replace (ps k * 1) with (ps k) in H by lia. now eapply primestream_divides in H. - cbn in H. eapply divides_mult_inv in H as [ | [ | ] % divides_mult_inv ]; eauto. + now eapply primestream_divides in H. + eapply divides_pow in H; eauto. now eapply ps_qs_div in H. + now eapply ps_exp in H. 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)