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