proposition: Theorem mm_fractran_not_zero n (P : list (mm_instr (pos n))) : { l | Forall (fun c => fst c <> 0 /\ snd c <> 0) l /\ forall v, (1,P) /MM/ (1,v) ↓ <-> l /F/ ps 1 * exp 1 v ↓ }.
proof: Proof. destruct mm_remove_self_loops with (P := P) as (Q & H1 & _ & H2). exists (encode_mm_instr 1 Q); split. + apply encode_mm_instr_regular. + intros x. rewrite H2, mm_fractran_simulation; auto. simpl exp; rewrite Nat.add_0_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)