Require Import List.
Definition State : Set := nat.
Record Config : Set := mkConfig { state : State; value1 : nat; value2 : nat }.
Inductive Instruction : Set :=
| inc : bool -> Instruction
| dec : bool -> State -> Instruction.
Definition Cm2 : Set := list Instruction.
Definition step (M: Cm2) (x: Config) : Config :=
match nth_error M (state x) with
| None => x
| Some (inc b) =>
{| state := 1 + (state x);
value1 := (if b then 0 else 1) + (value1 x);
value2 := (if b then 1 else 0) + (value2 x) |}
| Some (dec b y) =>
if b then
match value2 x with
| 0 => {| state := 1 + (state x); value1 := value1 x; value2 := 0 |}
| S n => {| state := y; value1 := value1 x; value2 := n |}
end
else
match value1 x with
| 0 => {| state := 1 + (state x); value1 := 0; value2 := value2 x |}
| S n => {| state := y; value1 := n; value2 := value2 x |}
end
end.
Arguments step _ !x /.
Definition halting (M : Cm2) (x: Config) : Prop := step M x = x.
Definition CM2_HALT : Cm2 -> Prop :=
fun M => exists (n: nat),
halting M (Nat.iter n (step M) {| state := 0; value1 := 0; value2 := 0 |}).