proposition: Lemma config_weight_step_monotone {M: Cm1} {x: Config} : not (halting M x) -> config_weight M x < config_weight M (step M x).
proof: Proof. move=> Hx. suff: not (config_weight M (step M x) <= config_weight M x) by lia. move: x Hx => [p v]. rewrite /config_weight /=. case: v => [|v]. { move=> + /ltac:(exfalso). by apply. } move Ho: (nth_error M p) => o. case: o Ho; first last. { move=> Hp + /ltac:(exfalso). apply. move=> /=. by rewrite Hp. } move=> [j n] Hp ?. case Hr: (S v mod (n + 1)); last by lia. have := mod_frac_lt Hr. have : p < length M. { apply /nth_error_Some. by rewrite Hp. } by nia. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun