proposition: Lemma mortal_steps_iff k x : mortal k x <-> steps (S k) x = None.
proof: Proof. elim: k x. { move=> x /=. split. - case: (mm2_sig_step_dec M x) => [[y Hxy]|]; last done. move=> /(_ [y]) /= H. suff : 1 <= 0 by lia. by apply: H. - case: (mm2_sig_step_dec M x) => [[y Hxy]|Hx]; first done. move=> _ [|??]; first done. by move=> [/Hx]. } move=> k IH x /=. split. - case: (mm2_sig_step_dec M x) => [[y Hxy]|]; last done. move=> Hx. apply /IH. move=> L HyL. move: (Hx (y::L)) => /= H. suff: S (length L) <= S k by lia. by apply: H. - case: (mm2_sig_step_dec M x) => [[y Hxy]|Hx]. + move=> /IH Hy [|??] /=; [lia|]. move: Hxy => /mm2_step_det + [] => /[apply] <-. move=> /Hy. lia. + move=> _ [|??] /=; [lia|]. by move=> [/Hx]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties ConstructiveEpsilon Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Deciders.MM2_UBOUNDED_dec Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun