В бульдік айнымалы кідіріс шартын береді, ал S – аяқталуға кепілдігі бар операторлар тізбегінің тізімі ( мысалы, меншіктеу операторының тізбегі).Операторы бөлінбейтін әрекет ретінде орындалатындығын көрсету үшін үшбұрыш жақшаға алынады. Дербес жағдайда S орындала бастағанда және S тегі ешбір аралық қалып-күй басқа процесстерге көрінбейтін болса В өрнегі «ақиқат» мәніне ие болады. Мысалы,