Actual occurrence coordinates for an appended scope

The old constraint occurrences and the new scope positions give disjoint coordinates on the existing dependent CSP.Occurrence type. Repeated variables and identical constraints retain their separate positions. The inverse is finite choice on these actual occurrence records; this structural equivalence carries no runtime or planarity assertion.

theorem Cslib.Logic.PL.CSP.occurrences_append_scope {Rel V : Type} (F : CSP Rel V) (r : Rel) (scope : List V) : (F ++ [(r, scope)]).occurrences = F.occurrences ++ List.map (fun (x : V × ℕ) => match x with | (v, j) => (List.length F, j, v)) scope.zipIdx

The complete occurrence word consists of the old body and the appended indexed scope.

noncomputable def Cslib.Logic.PL.CSP.occurrenceRecordEquiv {Rel V : Type} (F : CSP Rel V) : F.Occurrence ≃ { record : ℕ × ℕ × V // record ∈ F.occurrences }

Inverse coordinates for actual valid occurrence records; no new occurrence model.

theorem Cslib.Logic.PL.CSP.occurrenceRecordEquiv_apply {Rel V : Type} (F : CSP Rel V) (o : F.Occurrence) : ↑(F.occurrenceRecordEquiv o) = o.record

The forward record coordinates are precisely the existing occurrence's original record.

theorem Cslib.Logic.PL.CSP.record_occurrenceRecordEquiv_symm {Rel V : Type} (F : CSP Rel V) (record : { record : ℕ × ℕ × V // record ∈ F.occurrences }) : (F.occurrenceRecordEquiv.symm record).record = ↑record

Decoding a valid record recovers that very constraint/argument/variable triple.

noncomputable def Cslib.Logic.PL.CSP.appendScopeOccurrenceEquiv {Rel V : Type} (F : CSP Rel V) (r : Rel) (scope : List V) : F.Occurrence ⊕ Fin scope.length ≃ (F ++ [(r, scope)]).Occurrence

Original-body occurrences and the appended scope indices parametrize the exact original occurrence type. Constraint and argument positions remain distinct when variable labels repeat.

theorem Cslib.Logic.PL.CSP.record_appendScopeOccurrenceEquiv_inl {Rel V : Type} (F : CSP Rel V) (r : Rel) (scope : List V) (o : F.Occurrence) : ((F.appendScopeOccurrenceEquiv r scope) (Sum.inl o)).record = o.record

Old-body coordinates retain exactly their original positional record.

theorem Cslib.Logic.PL.CSP.record_appendScopeOccurrenceEquiv_inr {Rel V : Type} (F : CSP Rel V) (r : Rel) (scope : List V) (j : Fin scope.length) : ((F.appendScopeOccurrenceEquiv r scope) (Sum.inr j)).record = (List.length F, ↑j, scope[↑j])

New-scope coordinates retain the fresh constraint index and the actual selected variable.

noncomputable def Cslib.Logic.PL.CSP.appendOfFnOccurrenceEquiv {Rel V : Type} (F : CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) : F.Occurrence ⊕ Fin n ≃ (F ++ [(r, List.ofFn scope)]).Occurrence

Function-indexed scopes use the same actual occurrence coordinates, without replacing source scope positions by a set of variable names.

theorem Cslib.Logic.PL.CSP.record_appendOfFnOccurrenceEquiv_inl {Rel V : Type} (F : CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (o : F.Occurrence) : ((F.appendOfFnOccurrenceEquiv r scope) (Sum.inl o)).record = o.record

Function-indexed old-body coordinates retain their actual original occurrence record.

theorem Cslib.Logic.PL.CSP.record_appendOfFnOccurrenceEquiv_inr {Rel V : Type} (F : CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (j : Fin n) : ((F.appendOfFnOccurrenceEquiv r scope) (Sum.inr j)).record = (List.length F, ↑j, scope j)

The appended function-indexed scope has precisely its supplied variable at each position.