proposition: Lemma encode_state_inj n st1 st2 : @encode_state n st1 = @encode_state n st2 -> st1 = st2.
proof: Proof. intros H. destruct st1 as (i1, v1), st2 as (i2, v2). assert (i1 = i2); subst. - eapply divides_encode_state. rewrite <- H. unfold encode_state. cbn. rewrite Nat.mul_comm. eapply divides_mult, divides_refl. - f_equal. unfold encode_state in H. cbn in H. replace (ps i2) with (ps i2 ^ 1) in H by (cbn; lia). eapply power_factor_uniq in H as [_ H]. + eapply exp_inj. eauto. + pose proof (ps_prime i2) as ? % prime_ge_2. lia. + eapply ps_exp. + eapply ps_exp. 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)