proposition: Lemma mm2_stop_terminates {P x} : mm2_stop P x -> P // x ↓.
proof: Proof. move=> ?. exists x. by split; [apply: rt_refl|]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun