  Override and update are natural constructions for combining partial
functions, which arise in various program specification contexts. We use an
unexpected connection with combinatorial geometry to provide a complete finite
system of equational axioms for the first order theory of the override and
update constructions on partial functions, resolving the main unsolved problem
in the area.
