proposition: Lemma haltingP {M : Cm1} {x: Config}: halting M x <-> (length M <= state x \/ value x = 0).
proof: Proof. move: x => [p c] /=. constructor; first last. { case; rewrite /halting /=; last by move=> ->. move: c => [|c]; first done. by move=> /nth_error_None ->. } have [* | /nth_error_Some] : length M <= p \/ p < length M by lia. { by left. } rewrite /halting /=. move: c => [|c]; first by (move=> *; right). case: (nth_error M p); last done. move=> [q n] _. move Hr: (S c mod (n + 1)) => r. move: r Hr => [/mod_frac_lt |r _ [?]]; last by lia. move: (S c) => ? ? []. lia. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun