the identities of the runs meeting [first, first + count), then `rest`
1541def deviceArenaRangeInstances =
1542 (lambda unrestricted runs : (family DeviceArenaRuns) .
1543 (lambda unrestricted first : Nat .
1544 (lambda unrestricted count : Nat .
1545 (lambda unrestricted rest : (family DeviceArenaInstances) .
1546 (eliminate
1547 DeviceArenaRuns
1548 (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaInstances))
1549 runs
1550 (branch DeviceArenaRunsEnd . rest)
1551 (branch
1552 DeviceArenaRunsNext
1553 identity
1554 runFirst
1555 runCount
1556 tail
1557 induction
1558 .
1559 (nat-eliminate
1560 (lambda unrestricted meets : Nat . (family DeviceArenaInstances))
1561 induction
1562 (lambda unrestricted p : Nat .
1563 (lambda unrestricted ignored : (family DeviceArenaInstances) .
1564 (constructor DeviceArenaInstances DeviceArenaInstancesNext identity induction)))
1565 (naturalAnd
1566 (naturalLess runFirst (naturalAdd first count))
1567 (naturalLess first (naturalAdd runFirst runCount))))))))))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.