317def resourceLeaseValid =
318 (lambda unrestricted graph : (family ResourceGraph) .
319 (lambda unrestricted lease : (family ResourceLease) .
320 (naturalAnd
321 (naturalNonzero (bytes-length (resourceLeaseIdentity lease)))
322 (naturalAnd
323 (naturalNonzero (resourceLeaseAmount lease))
324 (naturalAnd
325 (naturalLessOrEqual (resourceLeaseAmount lease) resourceWordLimit)
326 (naturalAnd
327 (naturalLess (resourceLeaseBegin lease) (resourceLeaseUntil lease))
328 (naturalAnd
329 (naturalLessOrEqual (resourceLeaseUntil lease) resourceWordLimit)
330 (naturalAnd
331 (naturalNonzero
332 (resourceCount
333 (family ResourceEndpoint)
334 (lambda unrestricted endpoint : (family ResourceEndpoint) .
335 (naturalAnd
336 (naturalEqual (resourceEndpointId endpoint) (resourceLeaseEndpoint lease))
337 (naturalAnd
338 (naturalNonzero
339 (resourceCount
340 Nat
341 (lambda unrestricted id : Nat .
342 (naturalEqual id (resourceLeaseDomain lease)))
343 (resourceEndpointDomains endpoint)))
344 1)))
345 (resourceGraphEndpoints graph)))
346 (naturalAnd
347 (naturalNonzero
348 (resourceCount
349 (family ResourceDomain)
350 (lambda unrestricted domain : (family ResourceDomain) .
351 (naturalAnd
352 (naturalEqual (resourceDomainId domain) (resourceLeaseDomain lease))
353 (naturalAnd
354 (resourceDomainUnitMatches domain (resourceLeaseUnit lease))
355 1)))
356 (resourceGraphDomains graph)))
357 1)))))))))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.