theorem Trestle.Encode.Cardinality.List.countP_eq_countP_range {α : Type u_1} (P : α → Bool) (L : List α) : List.countP P L = List.countP (fun (x : Fin L.length) => P L[x]) (List.finRange L.length)

theorem Trestle.Encode.Cardinality.List.countP_eq_one_of_nodup {α : Type u_1} (P : α → Bool) (L : List α) (nodup : L.Nodup) : List.countP P L = 1 ↔ ∃! l : α, l ∈ L ∧ P l = true

theorem Trestle.Encode.Cardinality.exactly_one_iff_unique_idx {ν : Type u_1} (lits : Array (Literal ν)) (τ : Model.PropAssignment ν) : exactly 1 (↑lits.toList) τ ↔ ∃! i : ℕ, ∃ (x : i < lits.size), τ ⊨ LitVar.toPropFun lits[i]

Sinz sequential counter exactly one.

def Trestle.Encode.Cardinality.sinzExactlyOne.spec {ν : Type (max u_1 u_2)} (lits : Array (Literal ν)) (pos : lits.size > 0) : Model.PropPred (ν ⊕ Fin lits.size)

Equations

• One or more equations did not get rendered due to their size.

theorem Trestle.Encode.Cardinality.sinzExactlyOne.correct {ν : Type (max u_1 u_2)} (lits : Array (Literal ν)) (pos : lits.size > 0) (τ : Model.PropAssignment ν) : (∃ (σ : Model.PropAssignment (ν ⊕ Fin lits.size)), τ = Model.PropAssignment.map Sum.inl σ ∧ spec lits pos σ) ↔ exactly 1 (↑lits.toList) τ

def Trestle.Encode.Cardinality.sinzExactlyOne {ν : Type} [DecidableEq ν] (lits : Array (Literal ν)) : VEncCNF ν Unit (exactly 1 ↑lits.toList)

Equations

• One or more equations did not get rendered due to their size.

def Trestle.Encode.Cardinality.sinzExactlyOne.body {ν : Type} [DecidableEq ν] (lits : Array (Literal ν)) (h : lits.size > 0) : VEncCNF (ν ⊕ Fin lits.size) Unit (spec lits h)

Equations

• One or more equations did not get rendered due to their size.