Require Import List Nat.

Definition State : Set := nat.
Record Config : Set := mkConfig { state : State; value : nat }.

Definition Instruction : Set := State * nat.

Definition Cm1 : Set := list Instruction.

Definition step (M: Cm1) (x: Config) : Config :=
  match (value x), (nth_error M (state x)) with
  | 0, _ => x
  | _, None => x
  | _, Some (p, n) =>
      match modulo (value x) (n+1) with
      | 0 => {| state := p; value := ((value x) * (n+2)) / (n+1) |}
      | _ => {| state := 1 + state x; value := value x |}
      end
  end.

Arguments step _ !x /.

Definition halting (M : Cm1) (x: Config) : Prop := step M x = x.

Definition CM1_HALT : { M : Cm1 | Forall (fun '(_, n) => n < 4) M } -> Prop :=
  fun '(exist _ M _) =>
    exists n, halting M (Nat.iter n (step M) {| state := 0; value := 1 |}).