457def participantContains =
458 (lambda unrestricted index : (family ParticipantIndex) .
459 (eliminate
460 ParticipantIndex
461 (lambda unrestricted current : (family ParticipantIndex) . (pi unrestricted role : Nat . Nat))
462 index
463 (branch
464 ParticipantStrideIndex
465 bounds
466 stride
467 .
468 (lambda unrestricted role : Nat .
469 (naturalAnd
470 (naturalLessOrEqual (participantBoundsLower bounds) role)
471 (naturalAnd
472 (naturalLessOrEqual role (participantBoundsUpper bounds))
473 (naturalIsZero
474 (naturalModuloUnchecked
475 (naturalSaturatingSubtract role (participantBoundsLower bounds))
476 stride))))))
477 (branch
478 ParticipantRepeatIndex
479 bounds
480 stride
481 inner
482 induction
483 .
484 (lambda unrestricted role : Nat .
485 (naturalAnd
486 (naturalLessOrEqual (participantBoundsLower bounds) role)
487 (naturalAnd
488 (naturalLessOrEqual role (participantBoundsUpper bounds))
489 (induction
490 (naturalAdd
491 (participantLowerOf inner)
492 (naturalModuloUnchecked
493 (naturalSaturatingSubtract role (participantBoundsLower bounds))
494 stride)))))))
495 (branch
496 ParticipantJoinIndex
497 bounds
498 left
499 right
500 leftResult
501 rightResult
502 .
503 (lambda unrestricted role : Nat .
504 (nat-eliminate
505 (lambda unrestricted flag : Nat . Nat)
506 (rightResult role)
507 (lambda unrestricted prior : Nat .
508 (lambda unrestricted ignored : Nat . (leftResult role)))
509 (naturalLessOrEqual role (participantUpperOf left)))))))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.