The latest cycle any of `pending` is ready at for its slowest reader
(`latency` of the writer's class after it issued), and `start`.
1842def sm121LowerDrained =
1843 (lambda unrestricted pending : (family SM121LowerPending) .
1844 (lambda unrestricted latency : (pi unrestricted writer : (family SM121LowerClass) . Nat) .
1845 (lambda unrestricted start : Nat .
1846 (eliminate
1847 SM121LowerPending
1848 (lambda unrestricted current : (family SM121LowerPending) . Nat)
1849 pending
1850 (branch SM121LowerPendingEnd . start)
1851 (branch SM121LowerPendingNext entry issued class tail induction .
1852 (sm121LowerMaximum (nat-add issued (latency class)) 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.