#local l1 P_0.(wait == 1)
#local l2 P_0.(cs == 0)
EF(l1 && EG(l2))