Quantifier elimination algorithm to boolean combination of $\mathrm{\exists }\mathrm{\forall }$-formulas in the theory of a free group

It was proved by Sela and by the authors that every formula in the theory of a free group $F$ is equivalent to a boolean combination of $\mathrm{\exists }\mathrm{\forall }$-formulas. We also proved that the elementary theory of a free group is decidable (there is an algorithm given a sentence to decide whether this sentence belongs to $Th(F)$). In this paper we give an algorithm for reduction of a first order formula over a free group to an equivalent boolean combination of $\mathrm{\exists }\mathrm{\forall }$-formulas.