fact: Definition decide : { P : list (nat * nat) | fractran_reversible P } * nat -> bool := fun '(exist _ P HP, x) => match Argument.decision P x HP with | inl _ => true | inr _ => false end.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils) Undecidability.Synthetic.Definitions