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.