The Data.Time.LocalTime.TimeZone.Series module in Haskell provides the TimeZoneSeries datatype, and functions to work with it. A TimeZoneSeries describes the various clock settings that occur in a single time zone. This module is available in the timezone-series package on Hackage.
When a clock change moves the clock forward, the local times in the range between the times just before and just after the clock change cannot occur. We say that these times are "invalid".
Similarly, when a clock change moves the clock backward, the local times in the range between the times just after and just before the clock change occur twice. We say that these times are "redundant".
The functions isValidLocalTime and isRedundantLocalTime in Data.Time.LocalTime.TimeZone.Series allow you to determine whether a local time is invalid or redundant for a given TimeZoneSeries.
Theoretically, a TimeZoneSeries could describe a very complex and jittery set of time change rules that move the clock back and forth several times across the same clock time.
Although this scenario is unlikely to occur in a real time zone, the isValidLocalTime and isRedundantLocalTime functions are designed to handle these cases correctly.
To do so, they use the following fact:
Theorem: If G is the set of individual time changes for which clock time t is invalid ("in the Gap"), and O is the set of individual time changes for which t is redundant ("in the Overlap"), then t is invalid for the full set of changes iff #G > #O, and t is redundant for the full set of changes iff #G < #O.
Aristid Breitkreuz has provided the following proof for this theorem.
Now, let's look at the three cases of the different lengths:
This completes the proof.