proposition: Lemma mm2_clos_trans_not_terminates {P} (R : mm2_state -> Prop) : (forall x, R x -> exists y, (clos_trans _ (mm2_step P) x y) /\ R y) -> forall x, R x -> not (P // x ↓).
proof: Proof. move=> H x Hx [?] [/mm2_terminates_Acc] /[apply] /Acc_clos_trans H'x. elim: H'x Hx => {}x _ IH Hx. have [y [Hxy Hy]] := H x Hx. apply: (IH y _ Hy). move: Hxy. elim; by eauto using clos_trans with nocore. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun