Projection preserves bodies once, and does not enumerate fleet membership.
This helper requires admission; planParticipantProtocol is the checked entry.
294def projectGlobalProtocol =
295 (lambda erased operation : Type 0 .
296 (lambda erased payload : Type 0 .
297 (lambda erased decision : Type 0 .
298 (lambda unrestricted participant : Nat .
299 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
300 (eliminate
301 GlobalProtocol
302 (lambda unrestricted current : (family GlobalProtocol operation payload decision) .
303 (family ParticipantProtocol operation payload decision))
304 program
305 (branch
306 GlobalProtocolEnd
307 .
308 (constructor ParticipantProtocol ParticipantProtocolEnd operation payload decision))
309 (branch
310 GlobalProtocolLocal
311 owner
312 value
313 rest
314 induction
315 .
316 (nat-eliminate
317 (lambda unrestricted flag : Nat .
318 (family ParticipantProtocol operation payload decision))
319 induction
320 (lambda unrestricted prior : Nat .
321 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
322 (constructor
323 ParticipantProtocol
324 ParticipantProtocolLocal
325 operation
326 payload
327 decision
328 value
329 induction)))
330 (naturalEqual participant owner)))
331 (branch
332 GlobalProtocolTransfer
333 identity
334 value
335 rest
336 induction
337 .
338 (nat-eliminate
339 (lambda unrestricted flag : Nat .
340 (family ParticipantProtocol operation payload decision))
341 (nat-eliminate
342 (lambda unrestricted flag : Nat .
343 (family ParticipantProtocol operation payload decision))
344 induction
345 (lambda unrestricted prior : Nat .
346 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
347 (constructor
348 ParticipantProtocol
349 ParticipantProtocolTransfer
350 operation
351 payload
352 decision
353 (constructor ProtocolDirection ProtocolReceive)
354 identity
355 value
356 induction)))
357 (naturalEqual participant (regionTransferReceiver identity)))
358 (lambda unrestricted prior : Nat .
359 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
360 (constructor
361 ParticipantProtocol
362 ParticipantProtocolTransfer
363 operation
364 payload
365 decision
366 (constructor ProtocolDirection ProtocolSend)
367 identity
368 value
369 induction)))
370 (naturalEqual participant (regionTransferSender identity))))
371 (branch
372 GlobalProtocolRepeat
373 count
374 body
375 rest
376 bodyProjection
377 restProjection
378 .
379 (nat-eliminate
380 (lambda unrestricted flag : Nat .
381 (family ParticipantProtocol operation payload decision))
382 restProjection
383 (lambda unrestricted prior : Nat .
384 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
385 (constructor
386 ParticipantProtocol
387 ParticipantProtocolRepeat
388 operation
389 payload
390 decision
391 count
392 bodyProjection
393 restProjection)))
394 (naturalMultiply
395 count
396 (naturalEqual
397 (participantProtocolEmpty operation payload decision bodyProjection)
398 0))))
399 (branch
400 GlobalProtocolChoice
401 identity
402 selector
403 announcements
404 zeroBody
405 oneBody
406 rest
407 zeroProjection
408 oneProjection
409 restProjection
410 .
411 (let unrestricted projectedAnnouncements =
412 (projectProtocolAnnouncements payload participant announcements)
413 in
414 (nat-eliminate
415 (lambda unrestricted flag : Nat .
416 (family ParticipantProtocol operation payload decision))
417 (constructor
418 ParticipantProtocol
419 ParticipantProtocolChoice
420 operation
421 payload
422 decision
423 participant
424 identity
425 selector
426 projectedAnnouncements
427 zeroProjection
428 oneProjection
429 restProjection)
430 (lambda unrestricted prior : Nat .
431 (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) .
432 restProjection))
433 (naturalAnd
434 (protocolAnnouncementsEmpty payload projectedAnnouncements)
435 (naturalAnd
436 (participantProtocolEmpty operation payload decision zeroProjection)
437 (participantProtocolEmpty operation payload decision oneProjection))))))))))))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.