Inductive Relation

It is a restriction over the relation of Unsorted Linked Lists.

inductive MOList.Relation.Rel {α : Type} (s : MUList.State.ListST α) (a : State.Actions α) : MUList.State.ListST α → Prop

• ModifyData {α : Type} {s : MUList.State.ListST α} {a : State.Actions α} (tkn : Tokens.Elem.TId) (d : α) (s' : MUList.State.ListST α) : a = State.Actions.ModifyData tkn d → MUList.Relation.Rel s (MUList.State.Actions.ModifyData tkn d) s' → Rel s a s'
• SafeAppend {α : Type} {s : MUList.State.ListST α} {a : State.Actions α} (key : MUList.State.Key) (data : α) (last : Tokens.Elem.TId) (s' : MUList.State.ListST α) : a = State.Actions.SafeAppend key data last → MUList.Relation.Rel s (MUList.State.Actions.UnsafeAppend key data last) s' → Operations.is_non_member (some key) last s = true → Rel s a s'
• SafePrepend {α : Type} {s : MUList.State.ListST α} {a : State.Actions α} (key : MUList.State.Key) (data : α) (root : Tokens.Elem.TId) (s' : MUList.State.ListST α) : a = State.Actions.SafePrepend key data root → MUList.Relation.Rel s (MUList.State.Actions.UnsafePrepend key data root) s' → Operations.is_non_member (some key) root s = true → Rel s a s'
• Insert {α : Type} {s : MUList.State.ListST α} {a : State.Actions α} (key : MUList.State.Key) (data : α) (s' : MUList.State.ListST α) (anchor_tid : Tokens.Elem.TId) (anchor_nd : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α)) : a = State.Actions.Insert key data anchor_tid → Tokens.State.Tokens.get anchor_tid s = some anchor_nd → Operations.is_non_member (some key) anchor_tid s = true → some s' = MUList.State.ListST.upd_link anchor_tid (some key) (Tokens.State.Tokens.mint (MUList.State.serialize_key (some key)) { key := some key, link := anchor_nd.data.link, data := data } s) → Rel s a s'
• Remove {α : Type} {s : MUList.State.ListST α} {a : State.Actions α} (rem_tid anch_id : Tokens.Elem.TId) (s' : MUList.State.ListST α) : MUList.Relation.Rel s (MUList.State.Actions.Remove rem_tid anch_id) s' → a = State.Actions.Remove rem_tid anch_id → Rel s a s'

def MOList.Relation.StepListOrdered {α : Type} (rinit : α) : StepMachines.StepMachine Unit (State.Actions α) (MUList.State.ListST α)

Equations

• One or more equations did not get rendered due to their size.

def MOList.Notation.«term_=>⟨_⟩_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.