proposition: Lemma qs_encode_state i n (u : pos n) (v : vec nat n) : divides (qs u) (encode_state (i,v)) <-> v #> u > 0.
proof: Proof. rewrite qs_exp. enough (forall i, divides (qs (i + u)) (exp i v) <-> v #> u > 0). eapply H. intros j. induction v. - inversion u. - revert u. eapply pos.pos_S_invert. + cbn; rewrite pos2nat_fst, Nat.add_0_r. split. * intros [ | ] % divides_mult_inv; eauto. -- destruct h; try lia. cbn in H. apply divides_1_inv in H. generalize (str_prime qs j); rewrite H. intros [ [] _ ]; auto. -- eapply qs_exp_div in H; now eauto. * intros. destruct h. inv H. exists (qs j ^ h * exp (S j) v). cbn. ring. + cbn. intros. rewrite <- IHv, pos2nat_nxt. rewrite qs_shift with (m := 1). simpl. replace (j+S (pos2nat p)) with (S (j+p)); try tauto. 2: rewrite (Nat.add_comm _ (S _)); simpl; rewrite Nat.add_comm; auto. split; intros H. * eapply divides_mult_inv in H as [ | ]; eauto. eapply divides_pow in H; auto. eapply primestream_divides in H. lia. * eapply divides_mult. revert H; cbn; rewrite plus_n_Sm; eauto. 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)