A topologically ordered tree has one authority and one incoming decision
per receiver. Admission checks the declared edges only. The current source
implementation uses a persistent membership predicate (quadratic in edges
in the worst case); hierarchical fleet planning must bound per-cell edges.
45def protocolAnnouncementsAdmitted =
46 (lambda erased payload : Type 0 .
47 (lambda unrestricted participants : Nat .
48 (lambda unrestricted anchor : (family RegionTransferIdentity) .
49 (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
50 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
51 (app
52 (eliminate
53 ProtocolAnnouncements
54 (lambda unrestricted current : (family ProtocolAnnouncements payload) .
55 (pi unrestricted known : (pi unrestricted role : Nat . Nat) . Nat))
56 announcements
57 (branch
58 ProtocolAnnouncementsEnd
59 .
60 (lambda unrestricted known : (pi unrestricted role : Nat . Nat) . 1))
61 (branch
62 ProtocolAnnouncementsNext
63 identity
64 value
65 rest
66 induction
67 .
68 (lambda unrestricted known : (pi unrestricted role : Nat . Nat) .
69 (naturalAnd
70 (known (regionTransferSender identity))
71 (naturalAnd
72 (naturalEqual (known (regionTransferReceiver identity)) 0)
73 (naturalAnd
74 (naturalLess (regionTransferReceiver identity) participants)
75 (naturalAnd
76 (regionTransferIdentityEqual
77 (regionTransferWithRoute
78 anchor
79 (regionTransferSender identity)
80 (regionTransferReceiver identity))
81 identity)
82 (naturalAnd
83 (transfer identity value)
84 (naturalAnd
85 (induction
86 (lambda unrestricted role : Nat .
87 (naturalOr
88 (known role)
89 (naturalEqual role (regionTransferReceiver identity)))))
90 1)))))))))
91 (lambda unrestricted role : Nat . (naturalEqual role (regionTransferSender anchor)))))))))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.