Combined with the distinct-leaf check, cardinality plus containment proves
exact set coverage without enumerating a compact group's ranks. Lookup uses
the admitted index. This explicit-tree planner still traverses every tree
node and retains its existing duplicate check; compact membership alone is
not a fleet collective schedule or a proof of linear planning complexity.
528def combineCoverageValid =
529 (lambda unrestricted participants : Nat .
530 (lambda unrestricted coverage : (family CombineCoverage) .
531 (lambda unrestricted leaves : (family StdList Nat) .
532 (eliminate
533 CombineCoverage
534 (lambda unrestricted current : (family CombineCoverage) . Nat)
535 coverage
536 (branch
537 CombineOrderedMembers
538 members
539 .
540 (stdBoolToNatural (stdListNaturalEqual members leaves)))
541 (branch
542 CombineParticipantGroup
543 group
544 nodes
545 depth
546 .
547 (eliminate
548 StdResult
549 (lambda unrestricted current : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) .
550 Nat)
551 (participantAdmit group nodes depth)
552 (branch StdFailure reason . 0)
553 (branch
554 StdSuccess
555 index
556 .
557 (naturalAnd
558 (naturalEqual participants (participantUniverseOf group))
559 (naturalAnd
560 (naturalEqual (bytes-length (participantGroupDigest group)) 32)
561 (naturalAnd
562 (naturalEqual (stdListLength Nat leaves) (participantCountOf index))
563 (eliminate
564 StdList
565 (lambda unrestricted current : (family StdList Nat) . Nat)
566 leaves
567 (branch StdListEmpty . 1)
568 (branch
569 StdListCons
570 head
571 tail
572 induction
573 .
574 (naturalAnd (participantContains index head) induction)))))))))))))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.