793def chOperationAdmitted =
794 (lambda unrestricted role : Nat .
795 (lambda unrestricted operation : (family CoordinateRoundOperation) .
796 (eliminate
797 CoordinateRoundOperation
798 (lambda unrestricted current : (family CoordinateRoundOperation) . Nat)
799 operation
800 (branch CoordinateCombine value . (chCombineOperationAdmitted role value))
801 (branch CoordinateInstallCombined . (naturalLess role coordinateCount))
802 (branch CoordinateBackwardUpdate . (naturalLess role coordinateCount))
803 (branch CoordinatePrepareAcknowledgment . (naturalEqual role 1))
804 (branch CoordinateAcceptAcknowledgment . (naturalEqual role 0)))))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.