proposition: Lemma reaches_bounded {K k x y} : steps k x = Some y -> bounded K y -> bounded (k+K) x.
proof: Proof. elim: k x. { by move=> x /= [<-]. } move=> k IH x /=. case: (mm2_sig_step_dec M x) => [[z /mm2_step_det Hxz]|]; last done. move=> /IH /[apply] => - [L] [H1L H2L]. exists (x::L) => /=. split; [lia|]. move=> z' /clos_rt_rt1n_iff Hxz'. case: Hxz' Hxz. - move=> *. by left. - move=> > + /clos_rt_rt1n_iff + Hxz => /Hxz <- /H2L ?. by right. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun