proposition: Fact encode_mm_instr_regular n i l : Forall (fun c => fst c <> 0 /\ snd c <> 0) (@encode_mm_instr n i l).
proof: Proof. revert i; induction l as [ | [ u | u j ] l IHl ]; intros i; simpl. + constructor. + constructor; auto; unfold encode_inc; simpl; split; [ apply Nat.neq_mul_0; split | ]; apply prime_neq_0; apply nthprime_prime. + constructor; [ | constructor ]; auto; split; unfold encode_dec, encode_dec2; simpl. 2: apply Nat.neq_mul_0; split. all: apply prime_neq_0; apply nthprime_prime. 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)