The ALLOWED Schema

This just gives the set of allowed floors. <#1280#>ALLOWED<#1280#> allowed : (P P) by+ Alternatively we might want to define ``allowed'' as being a function from the current users to the set of allowed floors: <#1281#>ALLOWED<#1281#> allowed : P (P P) u : P, p : (P P) p (allowed \ u) p (u u) by+ It is not important at this stage, but we assume that it is defined as in the former case.