Note: K cannot be an event because the resulting formula is always false.
| 0 | [] K |
| 1 | [] K |
| 0 | <> M -> ( K U M ) |
| 1 | <> / M -> ( / M P ! K ) |
| 0 | [] ( L -> [] K ) |
| 1 | [] ( / L -> o [] K ) |
| 0 | [] ( ( L && <> M ) -> ( K U M ) ) |
| 1 | [] ( ( L && <> / M && ! / M ) -> o ( / M P ! K ) ) |
| 0 | [] ( L -> K W M ) |
| 1 | [] ( / L -> ( if <> / M then ( o ( / M P ! K ) ) else [] K ) ) |