Validate ordered coverage in one pass over fragments, not over coordinates.
Checking only summed lengths would accept an overlap paired with a hole.
Requiring the next begin to equal the previous end detects both, including
at the boundaries. Unordered input must be canonicalized by its owner first.
75def intervalPartitionValid :
76 (pi unrestricted extent : Nat .
77 (pi unrestricted intervals : (family StdList (family LogicalInterval)) . Nat)) =
78 (lambda unrestricted extent : Nat .
79 (lambda unrestricted intervals : (family StdList (family LogicalInterval)) .
80 (app
81 (eliminate
82 StdList
83 (lambda unrestricted current : (family StdList (family LogicalInterval)) .
84 (pi unrestricted cursor : Nat . Nat))
85 intervals
86 (branch StdListEmpty . (lambda unrestricted cursor : Nat . (naturalEqual cursor extent)))
87 (branch
88 StdListCons
89 head
90 tail
91 induction
92 .
93 (lambda unrestricted cursor : Nat .
94 (naturalAnd
95 (naturalEqual cursor (intervalBegin head))
96 (naturalAnd (intervalWithin extent head) (induction (intervalEnd head)))))))
97 0)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.