proposition: Lemma transition_loop a b: (forall a' b', (a > 0 <-> a' > 0) -> (b > 0 <-> b' > 0) -> exists a'' b'', reaches_plus (1, (a', b')) (1, (a'', b'')) /\ (a' > 0 <-> a'' > 0) /\ (b' > 0 <-> b'' > 0)) -> non_terminating (1, (a, b)).
proof: Proof. move=> H. apply: (mm2_clos_trans_not_terminates (fun '(p', (a', b')) => p' = 1 /\ (a > 0 <-> a' > 0) /\ (b > 0 <-> b' > 0))); last by lia. move=> [px [ax bx]] [->] H'. move: (H') => [/H] {}H /H [ax'] [bx'] [? ?]. exists (1, (ax', bx')). split; [done|lia]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun