Usage as LL-Formula
U is a ¡Èreliable¡É usage
i.e., For every I/O with capability,a corresponding O/I with obligation exists
[| U |] always reduces to 1
i.e., no unexpected garbage (producer/consumer) remains
e.g.[| Oo|Ic.- |] ?? 1 ? (m & 1) ? ((m ?? 1) ? 1) ?? 1