Useful Functions

First let us define the set of functions which take the set of users and a floor and return the number of users to which that user is talking to, that is, the number of open channels from that user, to other users: <#1235#>SPEAKER?<#1235#> speaker : (P P) P f: (P P), u : P speaker \ f \ u = n # { p : P \ | \ (u,p) f p } = n by+ There are two cases. For a floor f, and a user u, either
  1. <#1237#> speaker<#1237#> f u = 0 in which case p is on only a listener of the current floor.
  2. <#1238#> speaker<#1238#> f u ;SPM_gt; 0 in which case p is talking to someone in that floor. In this case we say, unsurprisingly, that p is a <#1239#> speaker<#1239#> of the floor s.
Next let us define the notion of the maximal speaker of a floor s. Which is/are the users/s which is/are speaking to more conference users than any one else. <#1241#>MAXIMAL<#1241#> maximal : P (P P) u \ maximal \ f p : P \ | \ speaker \ f \ p speaker \ f \ u by+