One-port attachments of actual ordered bodies

Two source bodies with disjoint variable supports meet at exactly one selected boundary label. Actual probe corners derive the join and cofaciality conditions internally. The body is the literal append followed by the one-name update; the boundary inserts the remaining external ports in the selected position. This is not all-port conjunction.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.attachAt {Rel V W : Type} [DecidableEq V] [DecidableEq W] {F H : Logic.PL.CSP Rel V} {left right extra : List V} {x y : V} (w : Witness F (left ++ x :: right)) (v : Witness H (extra ++ [y])) (f : V → W) (hd : (F.vars ++ (left ++ x :: right)).Disjoint (H.vars ++ (extra ++ [y]))) (hn : (left ++ x :: right ++ (extra ++ [y])).Nodup) (hk : ∀ a ∈ F.vars ++ (left ++ x :: right) ++ (H.vars ++ (extra ++ [y])), ∀ b ∈ F.vars ++ (left ++ x :: right) ++ (H.vars ++ (extra ++ [y])), f a = f b ↔ Function.update id x y a = Function.update id x y b) (ht : (List.map f (left ++ extra ++ y :: right)).Nodup) : Witness (Logic.PL.CSP.relabel f (F ++ H)) (List.map f (left ++ extra ++ y :: right))

Attach the final port of the external boundary at the selected body port. The original selected name is replaced by the external name everywhere in the actual appended body. All other external ports are inserted immediately before the shared boundary marker.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.attachDisjoint {Rel W : Type} [DecidableEq W] {A B : Type} [DecidableEq A] [DecidableEq B] {F : Logic.PL.CSP Rel A} {H : Logic.PL.CSP Rel B} {left right : List A} {extra : List B} {x : A} {y : B} (w : Witness F (left ++ x :: right)) (v : Witness H (extra ++ [y])) (f : A ⊕ B → W) (hnF : (left ++ x :: right).Nodup) (hnH : (extra ++ [y]).Nodup) (hk : ∀ (a b : A ⊕ B), f a = f b ↔ Function.update id (Sum.inl x) (Sum.inr y) a = Function.update id (Sum.inl x) (Sum.inr y) b) (ht : (List.map f (List.map Sum.inl left ++ List.map Sum.inr extra ++ Sum.inr y :: List.map Sum.inl right)).Nodup) : Witness (Logic.PL.CSP.relabel f (Logic.PL.CSP.relabel Sum.inl F ++ Logic.PL.CSP.relabel Sum.inr H)) (List.map f (List.map Sum.inl left ++ List.map Sum.inr extra ++ Sum.inr y :: List.map Sum.inl right))

Attach disjoint tagged copies of two actual source bodies at one selected port. The separate tags derive support disjointness, including unused boundary labels.