proposition: Lemma terminating_reaches_iff {M : Cm1} {k x y} : (Nat.iter k (CM1.step M) x = y -> ((exists m, CM1.halting M (Nat.iter m (CM1.step M) y))) <-> (exists n, CM1.halting M (Nat.iter n (CM1.step M) x))).
proof: Proof. move=> Hxy. split. - move=> [m Hm]. exists (k+m). by rewrite iter_plus Hxy. - move=> [n] /(halting_monotone (m := k+n)) => /(_ ltac:(lia)). rewrite iter_plus Hxy => ?. by exists n. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun