251def resourceGraphValid =
252 (lambda unrestricted graph : (family ResourceGraph) .
253 (naturalAnd
254 (naturalNonzero (stdListLength (family ResourceEndpoint) (resourceGraphEndpoints graph)))
255 (naturalAnd
256 (resourceDistinct
257 (family ResourceEndpoint)
258 (lambda unrestricted a : (family ResourceEndpoint) .
259 (lambda unrestricted b : (family ResourceEndpoint) .
260 (naturalOr
261 (naturalEqual (resourceEndpointId a) (resourceEndpointId b))
262 (bytes-equal (resourceEndpointIdentity a) (resourceEndpointIdentity b)))))
263 (resourceGraphEndpoints graph))
264 (naturalAnd
265 (resourceDistinct
266 (family ResourceDomain)
267 (lambda unrestricted a : (family ResourceDomain) .
268 (lambda unrestricted b : (family ResourceDomain) .
269 (naturalOr
270 (naturalEqual (resourceDomainId a) (resourceDomainId b))
271 (bytes-equal (resourceDomainName a) (resourceDomainName b)))))
272 (resourceGraphDomains graph))
273 (naturalAnd
274 (resourceDistinct
275 (family ResourceLink)
276 (lambda unrestricted a : (family ResourceLink) .
277 (lambda unrestricted b : (family ResourceLink) .
278 (naturalEqual (resourceLinkId a) (resourceLinkId b))))
279 (resourceGraphLinks graph))
280 (naturalAnd
281 (resourceAll (family ResourceDomain) resourceDomainValid (resourceGraphDomains graph))
282 (naturalAnd
283 (resourceAll
284 (family ResourceEndpoint)
285 (resourceEndpointValid graph)
286 (resourceGraphEndpoints graph))
287 (naturalAnd
288 (resourceAll
289 (family ResourceLink)
290 (resourceLinkValid graph)
291 (resourceGraphLinks graph))
292 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.