Reindexing the positions of one actual appended scope

The original body is retained literally, and only the selected last constraint's argument positions are permuted. The existing occurrence type records the resulting coordinates. This does not preserve prescribed cyclic order for arbitrary permutations; that condition must be proved separately, and is essential in ordered incidence transport.

noncomputable def Cslib.Logic.PL.CSP.reindexLastScopeOccurrenceEquiv {Rel V : Type} (F : CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) : (F ++ [(r, List.ofFn scope)]).Occurrence ≃ (F ++ [(r, List.ofFn (scope ∘ ⇑q))]).Occurrence

Reindex the final scope by q, using its inverse to locate each old argument in the new list. Body occurrences retain their original constraint and argument positions.

theorem Cslib.Logic.PL.CSP.reindexLastScopeOccurrenceEquiv_apply {Rel V : Type} (F : CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (o : F.Occurrence ⊕ Fin n) : (F.reindexLastScopeOccurrenceEquiv r scope q) ((F.appendOfFnOccurrenceEquiv r scope) o) = (F.appendOfFnOccurrenceEquiv r (scope ∘ ⇑q)) (((Equiv.refl F.Occurrence).sumCongr (Equiv.symm q)) o)

The reindexing is the literal conjugated body/last-scope coordinate map.

theorem Cslib.Logic.PL.CSP.header_reindexLastScopeOccurrenceEquiv {Rel V : Type} (F : CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (o : (F ++ [(r, List.ofFn scope)]).Occurrence) : (↑((F.reindexLastScopeOccurrenceEquiv r scope q) o).fst, ((F.reindexLastScopeOccurrenceEquiv r scope q) o).var) = (↑o.fst, o.var)

Every occurrence retains its original variable and constraint position, including repeated variables; only argument positions of the last scope can differ.