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
- <#1237#> speaker<#1237#> f u = 0
in which case p is on only a listener of the current floor.
- <#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+