proposition: Lemma reaches'_Some_terminating x y z : reaches' x y -> step y z -> mm2_stop M z -> forall a b, (value1 x > 0 <-> a > 0) -> (value2 x > 0 <-> b > 0) -> terminating (index x, (a, b)).
proof: Proof. move=> Hx Hy Hz a b ? ?. move: Hx => /reaches'E [n] [m] /= [?] [?]. move=> /(_ a b ltac:(lia) ltac:(lia)) /reaches'_incl. move: Hy => /(mm2_step_parallel (index y, (a + n, b + m))) /= /(_ ltac:(lia)). move=> [[pz [az bz]]] /= [?] [?] ?. subst pz. move=> /mm2_steps_terminates_l. apply. apply: mm2_steps_terminates_l; first by (apply: rt_step; eassumption). eexists. split; [by apply: rt_refl|]. by apply: mm2_stop_index_eq; [eassumption|]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun