О позитивных формулах на свободных полугруппах

Доказывается, что не существует алгоритма, позволяющего для произвольной позитивной формулы с константами $a_1$, $a_2$ и с приставкой типа $\exists\forall\exists^3$ определить, истинна ли эта формула на свободной полугруппе с образующими $a_1$, $a_2$. Доказана алгоритмическая неразрешимость вопроса об истинности на свободной полугруппе ранга $2$ без пустого слова позитивных формул без констант с приставкой типа $\exists^3\forall\exists^4$.