proposition: Lemma not_transition_1_1_to_0_0 x : reaches' (1, (1, 1)) x -> not (step x (1, (0, 0))).
proof: Proof. move=> /reaches'E [n] [m] /= [H1x] [H2x] _. move Hy: (1, (0, 0)) => y [i] [+ Hxy]. case: Hxy Hy H1x H2x=> > /= []; lia. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun