def Paths.Traversals.Traversal {α : Type} (ls : List Tokens.Elem.TId) (s : MUList.State.ListST α) : Prop

Equations

• Paths.Traversals.Traversal ls s = (Paths.Definitions.isPath ls s ∧ Paths.Utils.fromRootToLast ls s)

def Paths.Traversals.TraversalB {α : Type} (ls : List Tokens.Elem.TId) (s : MUList.State.ListST α) : Bool

Equations

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

theorem Paths.Traversals.travPath {α : Type} (ls : List Tokens.Elem.TId) (s : MUList.State.ListST α) (HT : Traversal ls s) : Definitions.isPath ls s

def Paths.Traversals.CompleteTraversal {α : Type} (ls : List Tokens.Elem.TId) (s : MUList.State.ListST α) : Bool

Equations

• Paths.Traversals.CompleteTraversal ls s = (((MUList.InternalUtils.alive_tids s).all fun (t : Tokens.Elem.TId) => ls.contains t) && Paths.Traversals.TraversalB ls s)

def Paths.Traversals.AllNodesInTrav {α : Type} (ls : List Tokens.Elem.TId) (s : MUList.State.ListST α) : Bool

Equations

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