The deepest node: the largest subtree's chain of first children reaches it,
because sizes are nonincreasing in child order.
226def participantTreeHeight =
227 (lambda unrestricted fanout : Nat .
228 (lambda unrestricted count : Nat .
229 (participantTreeDepthOf
230 (nat-eliminate
231 (lambda unrestricted remaining : Nat . (family ParticipantTreeNode))
232 (participantTreeRoot count)
233 (lambda unrestricted previous : Nat .
234 (lambda unrestricted node : (family ParticipantTreeNode) .
235 (nat-eliminate
236 (lambda unrestricted leaf : Nat . (family ParticipantTreeNode))
237 node
238 (lambda unrestricted predecessor : Nat .
239 (lambda unrestricted ignored : (family ParticipantTreeNode) .
240 (participantTreeChildNode fanout node 0)))
241 (naturalLess 1 (participantTreeSizeOf node)))))
242 (participantTreeFuel fanout count)))))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.