pub fn column_closure_lemmas(premises: &[ProofExpr]) -> Vec<ProofExpr>Expand description
HIDDEN SINGLE — the COLUMN closure, dual of the row closure. Each Exactly one φ
premise (∃x(φ(x) ∧ ∀y(φ(y) → y = x)), e.g. “exactly one trip is in Florida”)
entails that AT LEAST ONE row holds the value: ⋁_{r∈dom} value(r). The row closure
says a row takes SOME value; this says a value is taken by SOME row. Together with
functionality (a row takes at most one value), it is the deduction a human calls a
“hidden single” — once every other row is excluded from a value, the remaining row
MUST hold it, and the EXISTING literal unit-propagation forces it.
Grounded over the guard sort’s finite domain into a pure value-literal disjunction
(the sort guard Trip(r) is dropped — every r in the domain is a trip). Sound:
∃x φ(x) is just the existence half of “exactly one”, here merely grounded — compile
otherwise SKIPS the ∃, so the solver never sees the column closure without this.
Structural over any declared square bijection; never keyed to a particular puzzle.