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