Positional occurrences under body concatenation

Every original constraint and argument position has its own image. The right constraint block is shifted by the left body length. No occurrence, repeated record or nullary constraint is discarded. Directed cyclic argument successors retain their source order.

def Cslib.Logic.PL.CSP.appendOccurrence {Rel V : Type} (F H : CSP Rel V) : F.Occurrence ⊕ H.Occurrence → (F ++ H).Occurrence

Place each original occurrence at its exact position in the concatenated bodies.

noncomputable def Cslib.Logic.PL.CSP.appendOccurrenceEquiv {Rel V : Type} (F H : CSP Rel V) : F.Occurrence ⊕ H.Occurrence ≃ (F ++ H).Occurrence

The exact complete left-then-right occurrence correspondence, without deduplication.

theorem Cslib.Logic.PL.CSP.record_appendOccurrenceEquiv_inl {Rel V : Type} (F H : CSP Rel V) (o : F.Occurrence) : ((F.appendOccurrenceEquiv H) (Sum.inl o)).record = o.record

Original left constraint positions and labels are unchanged.

theorem Cslib.Logic.PL.CSP.record_appendOccurrenceEquiv_inr {Rel V : Type} (F H : CSP Rel V) (o : H.Occurrence) : ((F.appendOccurrenceEquiv H) (Sum.inr o)).record = (List.length F + ↑o.fst, ↑o.snd, o.var)

Original right argument positions and labels are unchanged; constraint positions shift.

theorem Cslib.Complexity.CSP.argumentSuccessor_appendOccurrenceEquiv {Rel V : Type} (F H : Logic.PL.CSP Rel V) (o : F.Occurrence ⊕ H.Occurrence) : argumentSuccessor ((F.appendOccurrenceEquiv H) o) = (F.appendOccurrenceEquiv H) (Sum.map argumentSuccessor argumentSuccessor o)

The complete concatenation correspondence preserves each directed source argument cycle.