RZ is never pending
167def sbMasksAnyPending =
168 (lambda unrestricted pending : (family ScoreboardMasks) .
169 (lambda unrestricted registers : (family StdList Nat) .
170 (eliminate StdList
171 (lambda unrestricted current : (family StdList Nat) . Nat)
172 registers
173 (branch StdListEmpty . zero)
174 (branch StdListCons register tail induction .
175 (nat-eliminate (lambda unrestricted current : Nat . Nat)
176 induction
177 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat .
178 (nat-eliminate (lambda unrestricted current : Nat . Nat)
179 induction
180 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (succ zero)))
181 (sbMasksLookup pending register))))
182 (nat-add (nat-less-than register 255) (nat-less-than 255 register)))))))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.