FWRITE(Q,F,V)
[Formula write. Q is the quantifier list and 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. The output buffer is emptied beforehand and afterwards.]
const EXIST=0,UNIVER=1,PSIZE=57.
safe r,q,Q'.
safe G,g.
global G[80].
global g.
(1) EMPTOB; BLINES(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(')') }; g=0; QFFWRS(F,V,0);
POLWR(PSIZE-3); return..