Appending disjoint ordered gadget boundaries

The two nonempty structural probes provide actual corners, even when their free labels do not occur in the bodies. Joining the probe centers yields the concatenated boundary word with its inherited orientation. The body is the literal left-then-right append. All closed and nullary components survive. This joins disjoint variable supports only.

theorem Cslib.Complexity.CSP.OrderedBoundary.Witness.nonempty_appendOfFn {Rel V : Type} [DecidableEq V] {F H : Logic.PL.CSP Rel V} {m n : ℕ} {p : Fin (m + 1) → V} {q : Fin (n + 1) → V} (w : Witness F (List.ofFn p)) (v : Witness H (List.ofFn q)) (hd : (F.vars ++ List.ofFn p).Disjoint (H.vars ++ List.ofFn q)) (hn : (List.ofFn p ++ List.ofFn q).Nodup) : Nonempty (Witness (F ++ H) (List.ofFn p ++ List.ofFn q))

Concatenate two distinct ordered boundary words on disjoint actual variable supports. No body occurrence is required at a boundary label; the nonempty probes supply the corners.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.appendOfFn {Rel V : Type} [DecidableEq V] {F H : Logic.PL.CSP Rel V} {m n : ℕ} {p : Fin (m + 1) → V} {q : Fin (n + 1) → V} (w : Witness F (List.ofFn p)) (v : Witness H (List.ofFn q)) (hd : (F.vars ++ List.ofFn p).Disjoint (H.vars ++ List.ofFn q)) (hn : (List.ofFn p ++ List.ofFn q).Nodup) : Witness (F ++ H) (List.ofFn p ++ List.ofFn q)

Choose the checked literal body/boundary append supplied by the source witnesses.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.append {Rel V : Type} [DecidableEq V] {F H : Logic.PL.CSP Rel V} {x y : V} {ps qs : List V} (w : Witness F (x :: ps)) (v : Witness H (y :: qs)) (hd : (F.vars ++ x :: ps).Disjoint (H.vars ++ y :: qs)) (hn : (x :: ps ++ y :: qs).Nodup) : Witness (F ++ H) (x :: ps ++ y :: qs)

The same checked body append for ordinary nonempty boundary words.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.appendWords {Rel V : Type} [DecidableEq V] {F H : Logic.PL.CSP Rel V} {ps qs : List V} (w : Witness F ps) (v : Witness H qs) (hp : ps ≠ []) (hq : qs ≠ []) (hd : (F.vars ++ ps).Disjoint (H.vars ++ qs)) (hn : (ps ++ qs).Nodup) : Witness (F ++ H) (ps ++ qs)

Append two supplied nonempty boundary words, retaining exact body order.