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.. #Jf