always((![X](B(X)=>(A(X)&~L(X)))) & (l=>?[X]A(X)) & (![X](A(X)=>next B(X))) & 
       (![X] sometime L(X)) & (sometime l))