FREAD(V,f;Q,F) [Formula read. V is a variable list in r variables, r>=1. f is a @beta@-digit with 0<=f<=r. A formula in prenex form with r-f quantifiers whose variables all occur in V is read from the input stream. Q is its quantifier list, and F is its unquantified matrix.] const EXIST=0,UNIVER=1,EQOP=1. safe C,i,j,r. (1) [Read quantifier list.] Q=(); r=LENGTH(V); for i=f+1,...,r do { C=CREADB(); if C~='(' then { print "left parenthesis expected"; go to 3 }; C=CREADB(); if C=='A' then Q=COMP(UNIVER,Q) else if C=='E' then Q=COMP(EXIST,Q) else { print "quantifier expected"; go to 3 }; v=VREAD(); j=VLSRCH(v,V); if i~=j then { print "unexpected variable"; go to 3 }; C=CREADB(); if C~=')' then { print "right parenthesis expected"; go to 3 } }; Q=INV(Q). (2) [Read unquantified matrix.] F=QFFRD(V); return. (3) [Error exit.] DIBUFF; print "reading through next $"; while C~='$' do C=CREADB(); print "the q.f.f. 0=0 returned"; F=LIST2(EQOP,0); Q=(); return.. Ę#˜JšĎfĂ˜Ă—…—Fo