proposition: Lemma mm2_terminates_Acc {P x y} : clos_refl_trans _ (mm2_step P) x y -> mm2_stop P y -> Acc (fun y' x' => mm2_step P x' y') x.
proof: Proof. move=> /clos_rt_rt1n_iff. elim. { move=> {}x Hx. by constructor => ? /Hx. } move=> {}x {}y z /mm2_step_det Hxy Hyz IH Hz. constructor. move=> y' /Hxy <-. by apply: IH. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun