proposition: Lemma RZ_loop v : (forall ab, RZ v ab -> exists a'b', RZ v a'b' /\ reaches_plus (1, ab) (1, a'b')) -> forall ab, RZ v ab -> non_terminating (1, ab).
proof: Proof. move=> Hv ab Hab [z] [/mm2_terminates_Acc] /[apply] /Acc_clos_trans. move Ex: (1, ab) => x Hx. elim: Hx ab Ex Hab => {}x _ IH ab ? Hab. subst x. have [a'b' [Ha'b' /clos_trans_transp_permute Ha'b'ab]] := Hv ab Hab. by apply: (IH _ Ha'b'ab a'b'). Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun