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