proposition: Lemma reaches'_None_terminating x y : reaches' x y -> mm2_stop M y -> forall a b, (a > 0 -> value1 x > 0) -> (b > 0 -> value2 x > 0) -> terminating (index x, (a, b)).
proof: Proof. move=> Hx Hy a b ? ?. move: Hx => /reaches'E [n] [m] /= [?] [?]. move=> /(_ a b ltac:(lia) ltac:(lia)) /reaches'_incl. move=> /mm2_steps_terminates_l. apply. apply: mm2_stop_terminates. by apply: (mm2_stop_index_eq Hy). Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun