proposition: Theorem decision (P : list (nat * nat)) (n: nat) : fractran_reversible P -> (P /F/ n ↓) + (not (P /F/ n ↓)).
proof: Proof. induction P as [P IH] using (induction_ltof1 _ (fun P => length P)); unfold ltof in IH. destruct P as [|(a,b) [|(c,d) P]]. - intros _. left. now apply fractran_empty_decision. - intros _. now apply fractran_singleton_decision. - destruct a as [|a]; simpl. { intros _. right. now intros H%fractran_nstop_zero_num_1. } destruct c as [|c]; simpl. { intros _. right. now apply fractran_nstop_cons, fractran_nstop_zero_num_1. } intros HP. enough (H'P : forall s t, ((S a, b) :: P) /F/ s ≻ t <-> ((S a, b) :: (S c, d) :: P) /F/ s ≻ t). { apply (fractran_step_iff_decide H'P). apply IH; simpl; [lia|]. intros n1 n2 m Hn1%H'P Hn2%H'P. eapply HP; eassumption. } intros s t. now apply fractran_reversible_shorten. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)