Require Import List.
Set Implicit Arguments.
Section Non_deterministic_Minsky_Machines.
Variables loc : Set.
Inductive ndmm2_instr : Set :=
| ndmm2_stop : loc -> ndmm2_instr
| ndmm2_inc : bool -> loc -> loc -> ndmm2_instr
| ndmm2_dec : bool -> loc -> loc -> ndmm2_instr
| ndmm2_zero : bool -> loc -> loc -> ndmm2_instr.
Notation α := true.
Notation β := false.
Notation STOP := ndmm2_stop.
Notation INC := ndmm2_inc.
Notation DEC := ndmm2_dec.
Notation ZERO := ndmm2_zero.
Infix "∊" := In (at level 70).
Reserved Notation "Σ // a ⊕ b ⊦ u" (at level 70, no associativity).
Inductive ndmm2_accept (Σ : list ndmm2_instr) : nat -> nat -> loc -> Prop :=
| in_ndmm2a_stop : forall p, STOP p ∊ Σ -> Σ // 0 ⊕ 0 ⊦ p
| in_ndmm2a_inc_1 : forall a b p q, INC α p q ∊ Σ -> Σ // 1+a ⊕ b ⊦ q
-> Σ // a ⊕ b ⊦ p
| in_ndmm2a_inc_0 : forall a b p q, INC β p q ∊ Σ -> Σ // a ⊕ 1+b ⊦ q
-> Σ // a ⊕ b ⊦ p
| in_ndmm2a_dec_1 : forall a b p q, DEC α p q ∊ Σ -> Σ // a ⊕ b ⊦ q
-> Σ // 1+a ⊕ b ⊦ p
| in_ndmm2a_dec_0 : forall a b p q, DEC β p q ∊ Σ -> Σ // a ⊕ b ⊦ q
-> Σ // a ⊕ 1+b ⊦ p
| in_ndmm2a_zero_1 : forall b p q, ZERO α p q ∊ Σ -> Σ // 0 ⊕ b ⊦ q
-> Σ // 0 ⊕ b ⊦ p
| in_ndmm2a_zero_0 : forall a p q, ZERO β p q ∊ Σ -> Σ // a ⊕ 0 ⊦ q
-> Σ // a ⊕ 0 ⊦ p
where "Σ // a ⊕ b ⊦ u" := (ndmm2_accept Σ a b u).
Definition ndMM2_problem := { Σ : list ndmm2_instr & loc * (nat * nat) }%type.
Definition ndMM2_ACCEPT (i : ndMM2_problem) : Prop :=
match i with existT _ Σ (u,(a,b)) => Σ // a ⊕ b ⊦ u end.
End Non_deterministic_Minsky_Machines.