The decidability of simultaneous rigid E-unification with one variable

We show that simultaneous rigid E-unication, or SREU for short, is decidable and in fact EXPTIME-complete in the case of one variable. This result implies that the 898 fragment of intuitionistic logic with equality is decidable. Together with a previous result regarding the undecidability of the 99-fragment, we obtain a complete classication of decidability of the prenex fragment of intuitionistic logic with equality, in terms of the quantier prex. It is also proved that SREU with one variable and a constant bound on the number of rigid equations is Pcomplete.