Сужение

Выражение (tА) обозначает протокол t, суженный на множество символов А; он строится из t отбрасыванием всех символов, не принадлежащих А.

Сужение дистрибутивно и поэтому строго.

L1.<>A = <>.

L2.(s^t)A = (sA)^(tA).

Эффект сужения на одноэлементных последовательностях очевиден:

LЗ.<х>А =<х>, если х А.

L4.<y>А =<>,если y А.

Приведенные ниже законы раскрывают взаимосвязь суженияи операций над множествами.

L5.s{} = <>.

L6.(sA)B = s(A B).