FWRL(Q,F,V)
[Formula write, linear. Q is the quantifier list, F the unquantified
matrix of a prenex formula in r variables, r>=1. V is a variable
list of length r. The prenex formula is written in the output
stream in a format that can be read back in.]
const EXIST=0,UNIVER=1.
safe r,q,Q'.
(1) r=LENGTH(V); f=r-LENGTH(Q);
Q'=Q; for i=f+1,...,r do { ADV(Q';q,Q');
CWRITE('('); if q==EXIST then CWRITE('E');
if q==UNIVER then CWRITE('A'); v=LELT(V,i);
CLOUT(v); CWRITE(')') }; QFFWL(F,V);
return..