Transporting actual incidence walks

Port transport between positional CSP lists retains the original variable names. Linkage, endpoint and nonreuse proofs require preservation only at the actual used ports. This permits total executable lookup maps with an irrelevant fallback outside their certified domain.

def Cslib.Logic.PL.CSP.Walk.mapPorts {Rel : Type u_1} {Rel' : Type u_2} {V : Type u_3} {F : CSP Rel V} {G : CSP Rel' V} (port : F.Occurrence → G.Occurrence) (w : F.Walk) : G.Walk

Map actual incidence pairs, retaining the original starting variable.

theorem Cslib.Logic.PL.CSP.Walk.edges_mapPorts {Rel : Type u_1} {Rel' : Type u_2} {V : Type u_3} {F : CSP Rel V} {G : CSP Rel' V} (port : F.Occurrence → G.Occurrence) (w : F.Walk) : (mapPorts port w).edges = List.map port w.edges

The transported incidence list is the original finite incidence list mapped portwise.

theorem Cslib.Logic.PL.CSP.Walk.mapPorts_take {Rel : Type u_1} {Rel' : Type u_2} {V : Type u_3} {F : CSP Rel V} {G : CSP Rel' V} (port : F.Occurrence → G.Occurrence) (w : F.Walk) (n : ℕ) : mapPorts port (w.take n) = (mapPorts port w).take n

Actual-port transport commutes with every variable-ended prefix.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.mapPorts {Rel : Type u_1} {Rel' : Type u_2} {V : Type u_3} {F : CSP Rel V} {G : CSP Rel' V} (port : F.Occurrence → G.Occurrence) {w : F.Walk} (hw : w.IsWalk) (hv : ∀ o ∈ w.edges, (port o).var = o.var) (hc : ∀ s ∈ w.steps, match s with | (input, output) => (port input).fst = (port output).fst) (hi : ∀ o ∈ w.edges, ∀ p ∈ w.edges, port o = port p → o = p) : (Walk.mapPorts port w).IsWalk

Preserving used variable names and step constraints, with injectivity on used ports, transports a genuine incidence trail between the original positional CSP list models.

theorem Cslib.Logic.PL.CSP.Walk.finish_mapPorts {Rel : Type u_1} {Rel' : Type u_2} {V : Type u_3} {F : CSP Rel V} {G : CSP Rel' V} (port : F.Occurrence → G.Occurrence) (w : F.Walk) (hv : ∀ o ∈ w.edges, (port o).var = o.var) : (mapPorts port w).finish = w.finish

Used-variable preservation retains the actual final variable, also for the empty walk.

theorem Cslib.Logic.PL.CSP.Walk.InternallyConsistent.mapPorts {Rel : Type u_1} {Rel' : Type u_2} {V : Type u_3} {F : CSP Rel V} {G : CSP Rel' V} (port : F.Occurrence → G.Occurrence) {f : F.OccurrenceLabeling Bool} {g : G.OccurrenceLabeling Bool} {ss : List (F.Occurrence × F.Occurrence)} (hi : InternallyConsistent f ss) (hd : ∀ o ∈ edgesOf ss, Inconsistent g (port o).var ↔ Inconsistent f o.var) : InternallyConsistent g (List.map (fun (x : F.Occurrence × F.Occurrence) => match x with | (input, output) => (port input, port output)) ss)

Internal consistency transports when defect status agrees at each actual used port.