proposition: Theorem mm_fractran_n n (P : list (mm_instr (pos n))) : { l | Forall (fun c => snd c <> 0) l /\ forall v, (1,P) /MM/ (1,v) ↓ <-> l /F/ ps 1 * exp 1 v ↓ }.
proof: Proof. destruct (mm_fractran_not_zero P) as (l & H1 & H2). exists l; split; auto. revert H1; apply Forall_impl; intros; 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)