The FLOOR Schema

Given the set of all people <#1229#> P<#1229#>, a floor is a set of ordered pairs of People, where each ordered pair suggests a directional communication channel from the first of the pair to the second. Of course the floor should only be made up of the users currently in the conference, and we keep track of the users of the system. Then all this information is captured by: <#1230#>FLOOR<#1230#> floor : (P P) users : P floor users users by+ By way of example we define some types of floor. Firstly the floor where everybody has a communication channel with everyone else - except themselves. <#1232#>OPENFLOOR<#1232#> FLOOR floor = { x,y : P \ | \ x,y users (x,y) } - { x : P \ | \ x users (x,x) } by+ Then the (we imagine) very common floor where one speaker talks to all the other people in the conference: <#1233#>SPEAKERFLOOR<#1233#> FLOOR p,q : P \ | \ p,q floor fst \ p = fst \ q # floor \ = \ # users - 1 by+