Transporting a subset's data along an equality

The interface recursion glues with Fragment.gluePair, which dispatches on whether the two glued flags already bound a common edge. Each branch identifies the glued fragment with the one the per-glue lemmas are stated for, and the subset, the transition system and the ledger's two counts have to be carried across that identification.

Nothing here is more than subst: the transports exist so the recursion can name them rather than unfold them.

def RS.EdgeSubset.relOfEq {β : Type} {V : Fragment β} {F F' : EdgeSubset V} (hF : F = F') (κ : F.RelTransitionSystem) : F'.RelTransitionSystem

Transport a transition system along an equality of subsets.

Equations

• RS.EdgeSubset.relOfEq hF κ = hF ▸ κ

def RS.EdgeSubset.orientOfEq {β : Type} {V : Fragment β} {F F' : EdgeSubset V} (hF : F = F') {κ : F.RelTransitionSystem} (o : κ.Orientation) : (relOfEq hF κ).Orientation

Transport an orientation along an equality of subsets.

Equations

• RS.EdgeSubset.orientOfEq hF o = hF ▸ o

theorem RS.EdgeSubset.openCircuitCount_relOfEq {β : Type} {V : Fragment β} {F F' : EdgeSubset V} (hF : F = F') (κ : F.RelTransitionSystem) : (relOfEq hF κ).openCircuitCount = κ.openCircuitCount

Transporting a system along an equality of subsets does not change its circuit count.

theorem RS.EdgeSubset.chordInv_relOfEq {β : Type} {V : Fragment β} {F F' : EdgeSubset V} (hF : F = F') (κ : F.RelTransitionSystem) (a : β) : F'.chordInv (relOfEq hF κ) a = F.chordInv κ a

Nor its boundary pairing.

theorem RS.EdgeSubset.swapPaired_of_eq {β : Type} {V : Fragment β} {F F' : EdgeSubset V} (hF : F = F') (ι : β → β) (h : F.SwapPaired ι) : F'.SwapPaired ι

Nor whether the subset uses interface pairs together.