1209def deviceArenaIntervalsNamed =
1210 (lambda unrestricted windows : (family ArenaResidents) .
1211 (lambda unrestricted named : (family ArenaResidents) .
1212 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
1213 (eliminate
1214 DeviceArenaIntervals
1215 (lambda unrestricted current : (family DeviceArenaIntervals) . Nat)
1216 intervals
1217 (branch DeviceArenaIntervalsEnd . 1)
1218 (branch
1219 DeviceArenaIntervalsNext
1220 low
1221 high
1222 tail
1223 induction
1224 .
1225 (naturalAnd
1226 (naturalOr
1227 (naturalIsZero (deviceArenaMeets windows low high))
1228 (deviceArenaWithin named low high))
1229 induction))))))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.