1: \begin{definition}

2: Recall from Theorem~\ref{t:osnf} that any formula in ${\ofoe}^+(A)$ is 

3: equivalent to a disjunction of formulas of the form 

4: $\posdbnfofoe{\vlist{T}}{\Sigma}$, whereas any formula in ${\ofoei}^+(A)$ is 

5: equivalent to a disjunction of formulas of the form 

6: $\posdbnfolque{\vlist{T}}{\Pi}{\Sigma}$. 

7: Based on these normal forms, for both one-step languages $\oslang={\ofoe}$ and 

8: $\oslang={\ofoei}$, we define the translation 

9: $(\cdot)^{\tmod} : {\oslang}^+(A) \to \ofo^+(A)$ by setting

10: % \[

11: % \Big( \posdbnfofoe{\vlist{T}}{\Sigma} \Big)^{\tmod} = 

12: % \Big( \posdbnfolque{\vlist{T}}{\Pi}{\Sigma} \Big)^{\tmod} 

13: % \df

14: % \bigwedge_{i} \exists x_i. \tau^+_{T_i}(x_i) \land 

15: % \forall x. \bigvee_{S\in\Sigma} \tau^+_S(x),

16: % \]

17: \[

18: \left.\begin{array}{l}

19:    \Big( \posdbnfofoe{\vlist{T}}{\Sigma} \Big)^{\tmod} 

20: \\ \Big( \posdbnfolque{\vlist{T}}{\Pi}{\Sigma} \Big)^{\tmod} 

21: \end{array}\right\}

22: \df \bigwedge_{i} \exists x_i. \tau^+_{T_i}(x_i) \land 

23: \forall x. \bigvee_{S\in\Sigma} \tau^+_S(x),

24: \]

25: and for $\al = \bigvee_{i} \al_{i}$ we define $\al^{\tmod} \df \bigvee 

26: \al_{i}^{\tmod}$.

27: \end{definition}

28: