(A) and (B): 1 when the globals and every phase's planes are placed
328def deviceArenaPlaced =
329 (lambda unrestricted globals : (family ArenaResidents) .
330 (lambda unrestricted phases : (family DeviceArenaPhases) .
331 (naturalAnd
332 (arenaCertificate deviceArenaWordMaximum globals)
333 (eliminate
334 DeviceArenaPhases
335 (lambda unrestricted current : (family DeviceArenaPhases) . Nat)
336 phases
337 (branch DeviceArenaPhasesEnd . 1)
338 (branch
339 DeviceArenaPhasesNext
340 head
341 tail
342 induction
343 .
344 (naturalAnd
345 (arenaCertificate
346 deviceArenaWordMaximum
347 (deviceArenaAppend (deviceArenaPhasePlanes head) globals))
348 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.