// liveness
multi
(
Pmin
=?[
F
(
l
=
4
)],
P
<=
0
[
G
F
(
t
=
2
)] )