Deterministic typed occurrence enumeration

incidenceList lists every positional incidence in constraint and scope order. occurrences_eq_map_incidenceList identifies its records with the existing executable scan. The Boolean validity instance supports finite scans without importing augmentation.

def Cslib.Logic.PL.CSP.incidenceList {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : List F.Occurrence

Positional incidences in constraint order and then argument order. This is a typed view of CSP.occurrences, without choosing representatives or identifying repeated constraints.

theorem Cslib.Logic.PL.CSP.mem_incidenceList {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (o : F.Occurrence) : o ∈ F.incidenceList

Every incidence appears in the deterministic scan.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.instDecidableValidLabelingBool {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) : Decidable (ValidLabeling sem f)

theorem Cslib.Logic.PL.CSP.occurrences_eq_map_incidenceList {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : F.occurrences = List.map Occurrence.record F.incidenceList

Typed and untyped enumeration retain exactly the same order and positions.

theorem Cslib.Logic.PL.CSP.incidenceList_nodup {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : F.incidenceList.Nodup

Positional incidences are not duplicated by the typed scan.