202def resourceEndpointValid =
203 (lambda unrestricted graph : (family ResourceGraph) .
204 (lambda unrestricted endpoint : (family ResourceEndpoint) .
205 (naturalAnd
206 (naturalLessOrEqual (resourceEndpointId endpoint) resourceWordLimit)
207 (naturalAnd
208 (naturalNonzero (bytes-length (resourceEndpointIdentity endpoint)))
209 (naturalAnd
210 (naturalNonzero (bytes-length (resourceEndpointRealization endpoint)))
211 (naturalAnd
212 (resourceAll
213 Bytes
214 (lambda unrestricted cap : Bytes . (naturalNonzero (bytes-length cap)))
215 (resourceEndpointCapabilities endpoint))
216 (naturalAnd
217 (resourceDistinct
218 Bytes
219 (lambda unrestricted a : Bytes .
220 (lambda unrestricted b : Bytes . (bytes-equal a b)))
221 (resourceEndpointCapabilities endpoint))
222 (naturalAnd
223 (resourceAll
224 Nat
225 (lambda unrestricted id : Nat . (resourceHasDomain graph id))
226 (resourceEndpointDomains endpoint))
227 (naturalAnd
228 (resourceDistinct
229 Nat
230 (lambda unrestricted a : Nat .
231 (lambda unrestricted b : Nat . (naturalEqual a b)))
232 (resourceEndpointDomains endpoint))
233 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.