proposition: Theorem Halt_REV_FRACTRAN_dec : decidable Halt_REV_FRACTRAN.
proof: Proof. exists Halt_REV_FRACTRAN_dec.decide. exact Halt_REV_FRACTRAN_dec.decide_spec. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.FRACTRAN.FRACTRAN