a different plane over any byte of `resident`
227def deviceArenaOverlapsOther =
228 (lambda unrestricted resident : (family ArenaResident) .
229 (lambda unrestricted residents : (family ArenaResidents) .
230 (eliminate
231 ArenaResidents
232 (lambda unrestricted current : (family ArenaResidents) . Nat)
233 residents
234 (branch ArenaResidentsEnd . 0)
235 (branch
236 ArenaResidentsNext
237 head
238 tail
239 induction
240 .
241 (naturalOr
242 (naturalAnd
243 (naturalIsZero
244 (bytes-equal
245 (deviceArenaResidentIdentity head)
246 (deviceArenaResidentIdentity resident)))
247 (naturalIsZero (arenaDisjoint head resident)))
248 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.