proposition: Theorem mm_fractran n (P : list (mm_instr (pos (S n)))) : { l | forall x, (1,P) /MM/ (1,x##vec_zero) ↓ <-> l /F/ ps 1 * qs 1^x ↓ }.
proof: Proof. destruct mm_fractran_n with (P := P) as (l & _ & Hl). exists l; intros x; rewrite Hl; simpl. rewrite exp_zero, Nat.mul_1_r; tauto. 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)