proposition: Corollary mm2_loop_not_terminates {P x} : (clos_trans _ (mm2_step P) x x) -> not (P // x ↓).
proof: Proof. move=> ?. apply: (mm2_clos_trans_not_terminates (fun y => y = x)); last done. move=> y ->. by exists x. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun