proposition: Lemma step_progress (M : Cm1) (x: Config) : state x < length M -> 1 <= value x -> step M x = {| state := 1 + state x; value := value x |} \/ value x < value (step M x).
proof: Proof. move=> ? ?. rewrite /step. have ->: value x = S (value x - 1) by lia. move Ho: (nth_error M (state x)) => o. case: o Ho; first last. { move /nth_error_None. by lia. } move=> [j n] _. case H: (S (value x - 1) mod (n + 1)); last by left. right => /=. by apply: mod_frac_lt. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun