Require Import List Arith Relations.
Set Implicit Arguments.
Section self_contained_mm2.
Inductive mm2_instr : Set :=
| mm2_inc_a : mm2_instr
| mm2_inc_b : mm2_instr
| mm2_dec_a : nat -> mm2_instr
| mm2_dec_b : nat -> mm2_instr.
Reserved Notation "i '//' r '⇢' s" (at level 70, no associativity).
Reserved Notation "P '//' r '→' s" (at level 70, no associativity).
Reserved Notation "P '//' r '↠' s" (at level 70, no associativity).
Reserved Notation "P '//' r ↓" (at level 70, no associativity).
Notation mm2_state := (nat*(nat*nat))%type.
Inductive mm2_atom : mm2_instr -> mm2_state -> mm2_state -> Prop :=
| in_mm2s_inc_a : forall i a b, mm2_inc_a // (i,( a, b)) ⇢ (1+i,(S a, b))
| in_mm2s_inc_b : forall i a b, mm2_inc_b // (i,( a, b)) ⇢ (1+i,( a,S b))
| in_mm2s_dec_aS : forall i j a b, mm2_dec_a j // (i,(S a, b)) ⇢ ( j,( a, b))
| in_mm2s_dec_bS : forall i j a b, mm2_dec_b j // (i,( a,S b)) ⇢ ( j,( a, b))
| in_mm2s_dec_a0 : forall i j b, mm2_dec_a j // (i,( 0, b)) ⇢ (1+i,( 0, b))
| in_mm2s_dec_b0 : forall i j a, mm2_dec_b j // (i,( a, 0)) ⇢ (1+i,( a, 0))
where "ρ // x ⇢ y" := (mm2_atom ρ x y).
Definition mm2_instr_at (ρ : mm2_instr) i P := exists l r, P = l++ρ::r /\ 1+length l = i.
Definition mm2_step P x y := exists ρ, mm2_instr_at ρ (fst x) P /\ ρ // x ⇢ y.
Notation "P // x → y" := (mm2_step P x y).
Definition mm2_stop P s := forall s', ~ P // s → s'.
Notation "P // x ↠ y" := (clos_refl_trans _ (mm2_step P) x y).
Definition mm2_terminates P s := exists s', P // s ↠ s' /\ mm2_stop P s'.
Notation "P // s ↓" := (mm2_terminates P s).
Definition MM2_PROBLEM := (list mm2_instr * nat * nat)%type.
Definition MM2_HALTING (P : MM2_PROBLEM) :=
match P with (P,a,b) => P // (1,(a,b)) ↓ end.
Definition MM2_HALTS_ON_ZERO (P : MM2_PROBLEM) :=
match P with (P,a,b) => P // (1,(a,b)) ↠ (0,(0,0)) end.
End self_contained_mm2.