pub fn functionality_lemmas(premises: &[ProofExpr]) -> Vec<ProofExpr>Expand description
FUNCTIONALITY — the missing half of a grid’s bijection. Each closure
∀x(guard(x) → L1 ∨ L2 ∨ … ∨ Ln) says a row takes AT LEAST one value; this emits
the AT MOST ONE companion ∀x(Li → ¬Lj) for every ordered pair of distinct
disjuncts. A trip is in exactly one state (one year, …), so a value assigned to a
row EXCLUDES the row’s other values — the propagation that, together with
value-uniqueness, determines the whole grid. Sound: for a square grid functionality
is entailed by closure + value-uniqueness + counting, and it is in any case the
inherent single-valuedness of the attribute. Each Li must be an atom mentioning
the bound variable (a genuine closure), so unrelated ∀→∨ premises are skipped.