fact: Fixpoint mma_fractran_step Q i { struct Q } := match Q with | nil => nil | (p,q)::Q => let P := FRAC_ONEₐ p q j i in P ++ mma_fractran_step Q (length P+i) end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils) Undecidability.FRACTRAN(FRACTRAN fractran_utils)