Ordered actual-body boundary transport under port renaming

The same finite successor table certifies a body after an injection on its occurring and boundary names. This transports both actual-body and probe checks without permuting darts, reflecting argument scopes or introducing new relation symbols. Repeated boundary occurrences are retained. The map may behave arbitrarily on unused names.

theorem Cslib.Complexity.CSP.OrderedBoundary.probeBody_relabel {Rel V W : Type} (F : Logic.PL.CSP Rel V) (ports : List V) (f : V → W) : Logic.PL.CSP.relabel f (probeBody F ports) = probeBody (Logic.PL.CSP.relabel f F) (List.map f ports)

The structural probe follows the same pointwise port renaming as the actual body.

theorem Cslib.Complexity.CSP.OrderedBoundary.vars_probeBody {Rel V : Type} (F : Logic.PL.CSP Rel V) (ports : List V) : (probeBody F ports).vars = F.vars ++ ports.reverse

The augmented occurrence word is the old word followed by the reversed boundary word.

theorem Cslib.Complexity.CSP.OrderedBoundary.bodyCertificate_relabel {Rel V W : Type} (F : Logic.PL.CSP Rel V) (f : V → W) (c : Graph.RotationCertificate) : bodyCertificate (Logic.PL.CSP.relabel f F) c = bodyCertificate F c

Pointwise renaming retains the body-prefix restriction of every raw successor table.

def Cslib.Complexity.CSP.OrderedBoundary.Witness.relabel {Rel V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {ports : List V} (w : Witness F ports) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ F.vars ∨ v ∈ ports}) : Witness (Logic.PL.CSP.relabel f F) (List.map f ports)

Rename the actual body and all boundary positions using one injection on used names. The literal table is unchanged, including for nullaries, closed components and repeated visits.

theorem Cslib.Complexity.CSP.OrderedBoundary.Witness.relabel_certificate {Rel V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {ports : List V} (w : Witness F ports) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ F.vars ∨ v ∈ ports}) : (w.relabel f hf).certificate = w.certificate

Port renaming retains the literal successor table, including repeated boundary visits.