Internal Utility functions

def MUList.InternalUtils.alive_tids {α : Type} (s : State.ListST α) : List Tokens.Elem.TId

Definition of alive Token Ids

Equations

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

def MUList.InternalUtils.alive_keys {α : Type} (s : State.ListST α) : List State.Key

Get alive token keys

Equations

• MUList.InternalUtils.alive_keys s = List.filterMap (fun (x : Option (Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α))) => do let x ← x x.data.key) s

theorem MUList.InternalUtils.alive_keys_append {α : Type} {s s' : State.ListST α} : alive_keys (s ++ s') = alive_keys s ++ alive_keys s'

def MUList.InternalUtils.all_alive_tids {α : Type} (s : State.ListST α) (f : Tokens.Elem.TokenD (State.Elemt State.Key α) × Nat → Bool) (k : Nat := 0) : Bool

Forall alive tokens

Equations

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

def MUList.InternalUtils.all_alive_valid {α : Type} (ls : State.ListST α) : Bool

Equations

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

theorem MUList.InternalUtils.alive_after_burn {α : Type} {s s' : State.ListST α} {t : Tokens.Elem.TId} {k : State.Key} (Hs : Tokens.State.Tokens.burn t s = some s') (HKey : State.ListST.get_key t s = some k) : (alive_keys s).length = (alive_keys s').length.succ

All alive Invariant utils

def MUList.InternalUtils.find_token? {α : Type} (s : State.ListST α) (P : Tokens.Elem.TokenD (State.Elemt State.Key α) → Bool) : Option (Tokens.Elem.TokenD (State.Elemt State.Key α))

Finds first token holding P

Equations

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

theorem MUList.InternalUtils.find_token_eq_none {α : Type} {s : State.ListST α} {P : Tokens.Elem.TokenD (State.Elemt State.Key α) → Bool} : find_token? s P = none ↔ ∀ (p : Tokens.Elem.TId), match Tokens.State.Tokens.get p s with | some tkn => ¬P tkn = true | none => True

theorem MUList.InternalUtils.find_token_eq_some_iff {α : Type} {s : State.ListST α} {P : Tokens.Elem.TokenD (State.Elemt State.Key α) → Bool} {t : Tokens.Elem.TokenD (State.Elemt State.Key α)} : find_token? s P = some t ↔ ∃ (l₁ : State.ListST α), ∃ (l₂ : State.ListST α), s = l₁ ++ some t :: l₂ ∧ P t = true ∧ all_alive_tids l₁ (not ∘ P ∘ fun (x : Tokens.Elem.TokenD (State.Elemt State.Key α) × Nat) => x.fst) = true

def MUList.InternalUtils.find_tokenSome? {α β : Type} (s : State.ListST α) (P : Tokens.Elem.TokenD (State.Elemt State.Key α) → Option β) : Option β

Equations

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

def MUList.InternalUtils.find_key {α : Type} (s : State.ListST α) (k : State.Key) : Option (Tokens.Elem.TokenD (State.Elemt State.Key α))

Equations

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

theorem MUList.InternalUtils.find_key_update {α : Type} {s s' : State.ListST α} {tid : Tokens.Elem.TId} {d : α} (HStep : Relation.Rel s (State.Actions.ModifyData tid d) s') : alive_keys s = alive_keys s'

def MUList.InternalUtils.find_anchor {α : Type} (s : State.ListST α) (k : State.Key) : Option (Tokens.Elem.TokenD (State.Elemt State.Key α))

Equations

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

def MUList.InternalUtils.find_anchors {α : Type} (s : State.ListST α) (k : State.Key) : List (Tokens.Elem.TokenD (State.Elemt State.Key α))

Equations

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