Unsorted Key single linked list is relation Rel is computational.

theorem MUList.Computational.ComputationalRelation {α : Type} (s s' : State.ListST α) (a : State.Actions α) : Computation.next a s = ComputationResult.Success s' ↔ Relation.Rel s a s'

Unsorted key linked list Step Machine

def MUList.Computational.StepList {α : Type} (rinit : α) : StepMachines.StepMachine Unit (State.Actions α) (State.ListST α)

Equations

• MUList.Computational.StepList rinit = { init := (MUList.State.ListST.init rinit).fst, STS := fun (x : Unit) (a : MUList.State.Actions α) (s : MUList.State.ListST α) => MUList.Relation.Rel s a }

structure MUList.Computational.ReachableUList {α : Type} (s : State.ListST α) : Type

• init_val : α
• reachable : (StepList self.init_val).FromInit () s