proposition: Lemma Hbound : { bound : nat | forall y, mm2_reaches c0 y -> (fst (snd y) + snd (snd y)) < bound }.
proof: Proof. Proof using Hc0c'0 Hc'0. move: (c'0) (Hc0c'0) (Hc'0) => z. move=> /mm2_terminates_Acc /[apply]. elim. move=> x _ IH. have [[y]|Hx] := mm2_sig_step_dec mm x. - move=> /[dup] /IH [bound Hbound] Hxy. exists (1 + bound + (fst (snd x)) + (snd (snd x))). move=> y' /clos_rt_rt1n_iff Hxy'. case: Hxy' Hxy; [lia|]. move=> > /mm2_step_det H + /H ?. subst y. move=> /clos_rt_rt1n_iff /Hbound. lia. - exists (1 + (fst (snd x)) + (snd (snd x))). move=> y /clos_rt_rt1n_iff Hxy. case: Hxy Hx; [lia|]. by move=> > + + H => /H. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun