The two flag enumerations

The Definition 5 pair enumeration and the block-slot enumeration are duplicate-free lists of the participating flags at a vertex: the raw material for the canonical index permutation between them.

theorem RS.mem_pairBase {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} {o : κ.Orientation} {v : W.Vertex} {f : ↥F.flags} (hf : f ∈ (F.inFlagsAt o v).attachWith (fun (x : W.Flag) => x ∈ F.flags) ⋯) : ↑f ∈ F.inFlagsAt o v

Members of the pair base are incoming flags.

theorem RS.attach_of_mem_inFlagsAt {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} {o : κ.Orientation} {v : W.Vertex} {f : W.Flag} (hf : f ∈ F.inFlagsAt o v) : W.attach f = Sum.inl v

Incoming flags attach to their vertex.

theorem RS.pairFlagList_nodup {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} (o : κ.Orientation) (v : W.Vertex) : (pairFlagList o v).Nodup

The pair enumeration is duplicate-free.

theorem RS.mem_pairFlagList {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} (o : κ.Orientation) (v : W.Vertex) (x : ↥F.flags) : x ∈ pairFlagList o v ↔ W.attach ↑x = Sum.inl v

Membership in the pair enumeration is attachment at the vertex.

noncomputable def RS.blockOddFlagList (W : ClosedFragment) (F : EdgeSubset W) (v : Fin (ds W).length) : List ↥F.flags

The block-slot enumeration: the participating slots of a block in slot order, as flags.

Equations

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

theorem RS.blockOddFlagList_nodup (W : ClosedFragment) (F : EdgeSubset W) (v : Fin (ds W).length) : (blockOddFlagList W F v).Nodup

The block-slot enumeration is duplicate-free.

theorem RS.mem_blockOddFlagList (W : ClosedFragment) (F : EdgeSubset W) (v : Fin (ds W).length) (x : ↥F.flags) : x ∈ blockOddFlagList W F v ↔ W.attach ↑x = Sum.inl (blockVertex W v)

Membership in the block-slot enumeration is attachment at the block's vertex.

theorem RS.mem_blockOddFlagList_iff_pairFlagList (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (v : Fin (ds W).length) (x : ↥F.flags) : x ∈ blockOddFlagList W F v ↔ x ∈ pairFlagList o (blockVertex W v)

The two enumerations list the same flags.