import SovereignApollo.State

inductive CommsState where
  | Acquire | Lock | Data | Drop
  deriving DecidableEq, Repr

def commsTransition : CommsState → CommsState → Prop
  | .Acquire, .Lock => True
  | .Lock, .Data => True
  | .Data, .Drop => True
  | .Drop, .Acquire => True
  | s, t => s = t  -- stutter allowed

theorem comms_no_skip_acquire_to_data : ¬ commsTransition .Acquire .Data := by
  simp [commsTransition]

theorem comms_reflexive (s : CommsState) : commsTransition s s := by
  cases s <;> simp [commsTransition]