reduce-historical/r37/packages/redlog/ofsfqe.red

% ----------------------------------------------------------------------
% $Id: ofsfqe.red,v 1.23 1999/03/23 07:41:28 dolzmann Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: ofsfqe.red,v $
% Revision 1.23  1999/03/23 07:41:28  dolzmann
% Changed copyright information.
% Changed comments for exc.
%
% Revision 1.22  1999/03/21 13:37:38  dolzmann
% Changed in procedure ofsf_thregen '(false) into {'false}.
% Fixed a bug in ofsf_thregen: ofsf_thregen returned an atomic formula
% instead of a list of atomic formulas for an disjunctive f.
% Corrected comments.
%
% Revision 1.21  1999/03/18 14:08:21  sturm
% Added new service rl_specelim!* in cl_qe for covering the "super
% quadratic special case' for ofsf. This method is toggled by switch
% rlsqsc, which is off by default. Context dvfsf uses cl_specelim which
% is constantly "false." Context acfsf does not use cl_qe at all.
%
% Revision 1.20  1999/01/17 16:10:35  dolzmann
% Added and corrected comments.
%
% Revision 1.19  1998/04/09 11:00:04  sturm
% Added switch rlqeqsc for quadratic special case. This now OFF by default!
%
% Revision 1.18  1997/10/02 09:14:13  sturm
% Fixed a bug in answer computation with shift.
%
% Revision 1.17  1997/08/14 10:10:31  sturm
% Renamed rldecdeg to rldecdeg1.
% Added service rldecdeg.
%
% Revision 1.16  1997/06/27 13:04:51  sturm
% Fixed a bug in ofsf_decdeg1.
%
% Revision 1.15  1997/04/15 11:31:44  dolzmann
% New procedure ofsf_decdeg offers a symbolic mode interface for
% decrementing the degree of variables in formulas.
% Modified procedure ofsf_transform accordingly.
% ofsf_subsimpl now outputs an exclamation mark if it enlarges the
% theory.
%
% Revision 1.14  1997/04/08 14:31:12  sturm
% Sort the answer substitution list wrt. ordp of the right hand side kernels.
%
% Revision 1.13  1996/10/23 11:24:16  dolzmann
% Added and corrected comments.
% Moved procedure ofsf_mkstrict into module ofsf.
%
% Revision 1.12  1996/10/15 15:47:21  dolzmann
% Fixed a bug in ofsf_qefsolset.
%
% Revision 1.11  1996/10/08 13:54:35  dolzmann
% Renamed "degree parity decomposition" to "parity decomposition".
% Adapted names of procedures and switches accordingly.
%
% Revision 1.10  1996/10/07 12:03:30  sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.9  1996/09/30 16:53:54  sturm
% Fixed a bug in ofsf_gelimset.
% Cleaned up the use of several (conditional) negate-relation procedures.
%
% Revision 1.8  1996/09/05 11:15:56  dolzmann
% Added comments.
% Minor changes in ofsf_mksol21q and ofsf_elimsetscq. New handling of
% root expressions with c=1.
% Renamed procedure ofsf_translat1lin to ofsf_translatlin.
% Renamed procedure ofsf_translat1qua to ofsf_translatqua.
% Completely rewritten Gauss elimination code: removed procedures
% ofsf_trygauss, ofsf_findeqsol, and ofsf_bettergaussp. Added
% implementation for black boxes rl_qefsolset, rl_bettergaussp!*,
% rl_bestgaussp, and rl_esetunion.
% Introduced new switch !*rlqegenct and related code.
%
% Revision 1.7  1996/07/07 14:43:06  sturm
% Removed use of fluid zehn!*.
% Call cl_nnfnot instead of cl_nnf1.
% Fixed a bug in ofsf_gelimset.
%
% Revision 1.6  1996/06/07 08:49:54  sturm
% Fixed bugs in ofsf_translat, ofsf_gelimset, and ofsf_decdegat.
%
% Revision 1.5  1996/05/13 13:45:24  dolzmann
% Improved ordering between the several kinds of Gauss elimination.
%
% Revision 1.4  1996/05/12 14:54:27  dolzmann
% Check for occurrence of variable in substitution.
% Modified ofsf_transform: Optimized treatment of atomic formulas x^n*r R 0.
%
% Revision 1.3  1996/05/12 08:27:33  sturm
% Added code for generic branch computation.
% Changes in ofsf_trygauss: Introduced an ordering between the several
% kinds of Gauss elimination.
% Added code for service ofsf_thsimpl.
%
% Revision 1.2  1996/04/18 14:30:47  sturm
% Improved root substitution in procedure ofsf_qesubrord1.
% Fixed a bug in ofsf_getsubrcoeffs.
%
% Revision 1.1  1996/03/22 12:14:14  sturm
% Moved and split.
%
% ----------------------------------------------------------------------
lisp <<
   fluid '(ofsf_qe_rcsid!* ofsf_qe_copyright!*);
   ofsf_qe_rcsid!* := "$Id: ofsfqe.red,v 1.23 1999/03/23 07:41:28 dolzmann Exp $";
   ofsf_qe_copyright!* := "Copyright (c) 1995-1999 by A. Dolzmann and T. Sturm"
>>;

module ofsfqe;
% Ordered field standard form quantifier elimination. Submodule of [ofsf].

%DS
% <variable> ::= <kernel>

procedure ofsf_varsel(f,vl,theo);
   % Ordered field standard form variable selection. [vl] is a list
   % of variables; [f] is a quantifier-free formula; [theo] is the
   % current theory. Returns a variable.
   begin scalar v,a,scvl,atl,ifacl,terml;
      atl := cl_atl1 f;
      scvl := vl;
      while scvl and not v do <<
	 a := car scvl;
	 scvl := cdr scvl;
	 if ofsf_linp(atl,a,delq(a,vl)) then v := a
      >>;
      if v then return v;
      scvl := vl;
      while scvl and not v do <<
	 a := car scvl;
	 scvl := cdr scvl;
	 if ofsf_qscp(atl,a) then v := a
      >>;
      if v then return v;
      terml := for each x in atl collect ofsf_arg2l x;
      scvl := vl;
      while scvl and not v do <<
	 a := car scvl;
	 scvl := cdr scvl;
	 if ofsf_pseudp(terml,a,1) then v := a
      >>;
      if v then return v;
      scvl := vl;
      while scvl and not v do <<
	 a := car scvl;
	 scvl := cdr scvl;
	 if ofsf_pseudp(terml,a,2) then v := a
      >>;
      if v then return v;
      if !*rlverbose then ioto_prin2 "(SVF";
      ifacl := for each x in atl join
	 for each p in cdr fctrf ofsf_arg2l x collect car x;
      if !*rlverbose then ioto_prin2 ")";
      scvl := vl;
      while scvl and not v do <<
	 a := car scvl;
	 scvl := cdr scvl;
	 if ofsf_pseudp(ifacl,a,1) then v := a
      >>;
      if v then return v;
      scvl := vl;
      while scvl and not v do <<
	 a := car scvl;
	 scvl := cdr scvl;
	 if ofsf_pseudp(ifacl,a,2) then v := a
      >>;
      if v then return v;
      return car vl
   end;

procedure ofsf_linp(atl,v,vl);
   % Ordered field standard form linear formula predicate. [atl] is a
   % list of atomic formulas; [v] is a variable; [vl] is a list of
   % variables. Returns [T] if every formula containing the atomic
   % formulas from [atl] is linear in [v] wrt. to [vl], i.e. the total
   % degree of [v] is 1 and no coefficient from [v] contains variables
   % from [vl].
   begin scalar linp,w,u,g;
      linp := T;
      w := setkorder {v};
      while atl and linp do <<
	 u := reorder ofsf_arg2l car atl;
	 atl := cdr atl;
	 g := degr(u,v);
	 if g > 1 or (g = 1 and intersection(kernels lc u,vl)) then
	    linp := nil
      >>;
      setkorder w;
      return linp
   end;

procedure ofsf_qscp(atl,v);
   % Ordered field standard form quadratic special case predicate.
   % [atl] is a list of atomic formulas; [v] is a variable. Returns
   % [T] if the quadratic special case is applicable to each formula
   % containing the atomic formulas from [atl].
   begin scalar a,hit,d;
      if not !*rlqeqsc then
	 return nil;
      while atl do <<
	 a := car atl;
	 atl := cdr atl;
	 d := degreef(ofsf_arg2l a,v);
	 if d>2 then
	    atl := hit := nil
	 else if d=2 and ofsf_op a memq '(greaterp lessp geq leq neq) then
	    if hit then
	       atl := hit := nil
	    else
	       hit := T
      >>;
      return hit
   end;

procedure ofsf_pseudp(ifacl,v,n);
   % Ordered field standard form pseudo high degree predicate.
   % [ifacl] is a list of SF's; [v] is a variable; [n] is a
   % non-negative integer. Returns [T] if the degree of each SF in
   % [ifacl] wrt. [v] is less than or equal to [n].
   begin scalar ok;
      ok := T;
      while ifacl and ok do
	 if degreef(car ifacl,v) > n then
	    ok := nil
	 else
	    ifacl := cdr ifacl;
      return ok
   end;

%DS root expression
% A list $(a,b,c,d)$ of SF's encoding the expression $(a+b\sqrt{c})/d$
% The denominator of a root expression $r=(a,b,c,d)$ is $d$ and the
% disciminante of $r$ is $c$. A root expression $r$ is called valid
% iff the demominator of $r$ is not equal to zero and the
% discriminante of $r$ is greater then 0.

procedure ofsf_qesubcr1(bvl,theo,f,v,co,u);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 1 root. [bvl] is a list of variables; [theo] is the
   % current theory; [f] is a quantifier-free formula; [v] is a
   % variable; [u] is a root expression; [co] is a quantifier-free
   % formula which implies that [u] is valid. Returns a pair $(\Theta'
   % . \phi)$ where $\Theta'$ is a theory and $\phi$ is a
   % quantifier-free formula. $\phi$ is equivalent to $[co] \land
   % [f]([v]/[u])$ under the theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,ofsf_qesubr(f,v,u)})
   end;

procedure ofsf_qesubcr2(bvl,theo,f,v,co,u1,u2);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 1 root. [bvl] is a list of variables; [theo] is the
   % current theory; [f] is a quantifier-free formula; [v] is a
   % variable; [u1], [u2] are root expression; [co] is a
   % quantifier-free formula which implies that both [u1] and [u2] are
   % valid. Returns a pair $(\Theta' . \phi)$ where $\Theta'$ is a
   % theory and $\phi$ is a quantifier-free formula. $\phi$ is
   % equivalent to $[co] \land ([f]([v]/[u1]) \lor [f]([v]/[u2]))$
   % under the theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,rl_mkn('or,{
      	 ofsf_qesubr(f,v,u1),ofsf_qesubr(f,v,u2)})})
   end;

procedure ofsf_qesubr(f,v,u);
   % Ordered field standard form quantifier elimination substitute
   % root. [f] is a quantifier-free formula; [v] is a variable; [u] is
   % a root expression. Returns a quantifier-free formula equivalent
   % to $[f]([v]/[u])$ provided that [u] is valid..
   if caddr u = 1 then
      cl_apply2ats1(f,'ofsf_qesubqat,{v,
	 quotsq(!*f2q addf(car u,cadr u),!*f2q cadddr u)})
   else
      cl_apply2ats1(f,'ofsf_qesubrat,{v,u});

procedure ofsf_qesubrat(atf,v,u);
   % Ordered field standard form quantifier elimination substitute
   % root into atomic formula. [atf] is an atomic formula; [v] is a
   % variable; [u] is a root expression. Returns a quantifier-free
   % formula equivalent to $[f]([v]/[u])$ provided that that [u] is
   % valid.
   if not (v memq ofsf_varlat atf) then
      atf
   else
      ofsf_qesubrat1(ofsf_op atf,ofsf_arg2l atf,v,u);

procedure ofsf_qesubrat1(r,f,x,rform);
   % Ordered field standard form quantifier elimination substitute
   % root into atomic formula subroutine. [r] is a relation; [f] is an
   % SF; [x] is a variable; [r] is a root expression. Returns a
   % quantifier-free formula equivalent to $[r]([f],0)([x]/[rform])$
   % that does not contain any root provided [rform] is valid..
   begin scalar w,dd;
      w := ofsf_getsubrcoeffs(f,x,rform);
      if r eq 'equal or r eq 'neq then
 	 return ofsf_qesubreq(r,car w,cadr w,caddr w);
      dd := car sfto_pdecf cadddr w;
      return ofsf_qesubrord(r,car w,cadr w,caddr w,dd)
   end;

procedure ofsf_qesubreq(r,aa,bb,c);
   % Ordered field standard form quantifier elimination substitute
   % root with equality relation. [r] is one of ['equal], ['neq]; [aa],
   % [bb], and [c] are SF's. Returns a quantifier-free formula
   % equivalent to $[r](([aa]+[bb]\sqrt{[c]})/d,0)$ for any nonzero
   % $d$ provided that $c \geq 0$.
   (if r eq 'equal then w else cl_nnfnot w)
      where w=ofsf_qesubreq1(aa,bb,c);

procedure ofsf_qesubreq1(aa,bb,c);
   % Ordered field standard form quantifier elimination substitute
   % root with equation. [aa], [bb], and [c] are SF's. Returns a
   % quantifier-free formula equivalent to $([aa]+[bb]\sqrt{[c]})/d=0$
   % for any nonzero $d$ provided that $c \geq 0$.
   if null bb then
      ofsf_0mk2('equal,aa)
   else
      rl_mkn('and,{ofsf_0mk2('leq,multf(aa,bb)),
	 ofsf_0mk2('equal,addf(exptf(aa,2),negf multf(exptf(bb,2),c)))});

procedure ofsf_qesubrord(r,aa,bb,c,dd);
   % Ordered field standard form quantifier elimination substitute
   % root with ordering relation. [r] is any ordering relation;
   % [delta] is $0$ or $1$; [aa], [bb], [c], and [dd] are SF's.
   % Returns a quantifier-free formula equivalent to
   % $[r](([aa]+[bb]\sqrt{[c]})/d^[delta],0)$ provided that $d \neq 0$
   % and $c \geq 0$.
   if r eq 'leq or r eq 'lessp then
      ofsf_qesubrord1(r,aa,bb,c,dd)
   else  % [r eq 'geq or r eq 'greaterp]
      cl_nnfnot ofsf_qesubrord1(ofsf_lnegrel r,aa,bb,c,dd);

procedure ofsf_qesubrord1(r,aa,bb,c,dd);
   % Ordered field standard form quantifier elimination substitute
   % root with ordering relation subroutine. [r] is one of [leq],
   % [lessp]; [delta] is $0$ or $1$; [aa], [bb], [c], and [d] are
   % SF's. Returns a quantifier-free formula equivalent to
   % $[r](([aa]+[bb]\sqrt{[c]})/d^[delta],0)$ provided that $d \neq 0$
   % and $c \geq 0$.
   begin scalar ad,a2b2c,w;
      ad := multf(aa,dd);
      if null bb then
      	 return ofsf_0mk2(r,ad);
      a2b2c := addf(exptf(aa,2),negf multf(exptf(bb,2),c));
      w := if r eq 'leq then
	 ofsf_0mk2('leq,a2b2c)
      else
	 rl_mkn('or,{ofsf_0mk2('lessp,ad),ofsf_0mk2('lessp,a2b2c)});
      return rl_mkn('or,{
	 rl_mkn('and,{ofsf_0mk2(r,ad),ofsf_0mk2(ofsf_anegrel r,a2b2c)}),
	 rl_mkn('and,{ofsf_0mk2('leq,multf(bb,dd)),w})})
   end;

procedure ofsf_getsubrcoeffs(f,x,rform);
   % Ordered field standard form get coefficients for root
   % substitution. [f] is an SF; [x] is a variable; [rform] is a root
   % expression $(a,b,c,d)$. Returns a list $(a',b',c,d')$ of SF's
   % such that $a'+b'\sqrt{c}/d'$ is $[f]([x]/[rform])$ reduced to
   % lowest terms. We assume $d \neq 0$ and $c \geq 0$.
   begin scalar w,rpol,aa,bb,dd,a,b,c,d;
      a := prepf car rform;
      b := prepf cadr rform;
      c := caddr rform;
      d := prepf cadddr rform;
      rpol := {'quotient,{'plus,a,{'times,b,'ofsf_sqrt}},d};
      w := subf(f,{x . rpol});
      dd := denr w;
      w := sfto_reorder(numr w,'ofsf_sqrt);
      while not domainp w and mvar w eq 'ofsf_sqrt do <<
	 if evenp ldeg w then
	    aa := addf(aa,multf(reorder lc w,exptf(c,ldeg w / 2)))
	 else
	    bb := addf(bb,multf(reorder lc w,exptf(c,ldeg w / 2)));
	 w := red w
      >>;
      aa := addf(aa,reorder w);
      return {aa,bb,c,dd}
   end;

procedure ofsf_qesubcq(bvl,theo,f,v,co,u);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 1 quotient. [bvl] is a list of variables, [theo] is
   % the current theory, [f] is a quantifier-free formula; [v] is a
   % variable; [co] is a formula which implies that the denominator of
   % [u] is nonzero; [u] is an SQ. Returns a pair $(\Theta' . \phi)$
   % where $\Theta'$ is a theory and $\phi$ is a quantifier-free
   % formula. $\phi$ is equivalent to $[co] \land [f]([v]/[u])$ under
   % the theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,ofsf_qesubq(f,v,u)})
   end;

procedure ofsf_qesubq(f,v,u);
   % Ordered field standard form quantifier elimination substitute
   % quotient. [f] is a quantifier-free formula; [v] is a variable;
   % [u] is an SQ. Returns a quantifier-free formula equivalent to
   % $[f]([v]/[u])$ provided that the denominator of [u] is nonzero.
   cl_apply2ats1(f,'ofsf_qesubqat,{v,u});

procedure ofsf_qesubqat(atf,v,u);
   % Ordered field standard form quantifier elimination substitute
   % quotient into atomic formula. [atf] is an atomic formula; [v] is
   % a variable; [u] is an SQ. Returns a quantifier-free formula
   % equivalent to $[atf]([v]/[u])$ provided that the denominator of
   % [u] is nonzero.
   begin scalar w,op;
      if not (v memq ofsf_varlat atf) then return atf;
      w := subf(ofsf_arg2l atf,{v . prepsq u});
      op := ofsf_op atf;
      w := if op eq 'equal or op eq 'neq then numr w else multf(numr w,denr w);
      return ofsf_0mk2(op,w)
   end;

procedure ofsf_qesubi(bvl,theo,f,v,inf);
   % Ordered field standard form quantifier elimination substitute
   % infinite element. [bvl] is a list of variables, [theo] is the
   % current theory; [f] is a quantifier-free formula; [v] is a
   % variable; [inf] is one of ['minf], ['pinf] which stand for
   % $-\infty$ and $\infty$ resp. Returns a pair $(\Theta' . \phi)$
   % where $\Theta'$ is a theory and $\phi$ is a quantifier-free
   % formula. $\phi$ is equivalent to $[f]([v]/[inf])$ under the
   % theory $[th] \cup \Theta'$. $\Theta' is currently always [nil].
   nil . cl_apply2ats1(f,'ofsf_qesubiat,{v,inf});

procedure ofsf_qesubiat(atf,v,inf);
   % Ordered field standard form quantifier elimination substitute
   % infinite element into atomic formula. [atf] is an atomic formula;
   % [v] is a variable; [inf] is one of ['minf], ['pinf] which stand for
   % $-\infty$ and $\infty$ resp. Returns a quantifier-free formula
   % equivalent to $[atf]([v]/[inf])$.
   begin scalar op,lhs;
      if not (v memq ofsf_varlat atf) then return atf;
      op := ofsf_op atf;
      lhs := ofsf_arg2l atf;
      if op eq 'equal or op eq 'neq then
	 return ofsf_qesubtranseq(op,lhs,v);
      % [op] is an ordering relation.
      return ofsf_qesubiord(op,lhs,v,inf)
   end;

procedure ofsf_qesubtranseq(op,lhs,v);
   % Ordered field standard form quantifier elimination substitute
   % transcendental element with equality relation. [op] is one of
   % ['equal], ['neq]; [lhs] is an SF; [v] is a variable. Returns a
   % quantifier-free formula equivalent to $[r]([lhs],0)([v]/\alpha)$
   % for any transcendental $\alpha$.
   if op eq 'equal then
      ofsf_qesubtransequal(lhs,v)
   else  % [op eq 'neq]
      cl_nnfnot ofsf_qesubtransequal(lhs,v);

procedure ofsf_qesubtransequal(lhs,v);
   % Ordered field standard form quantifier elimination substitute
   % transcendental element into equation. [lhs] is an SF; [v] is a
   % variable. Returns a quantifier-free formula equivalent to
   % $[lhs]([v]/\alpha)=0$ for any transcendental $\alpha$.
   ofsf_qesubtransequal1(sfto_reorder(lhs,v),v);

procedure ofsf_qesubtransequal1(lhs,v);
   % Ordered field standard form quantifier elimination substitute
   % transcendental element into equation. [lhs] is an SF reordered
   % wrt. [v]; [v] is a variable. Returns a quantifier-free formula
   % equivalent to $[lhs]([v]/\alpha)=0$ for any transcendental
   % $\alpha$.
   begin scalar cl;
      while not domainp lhs and mvar lhs eq v do <<
	 cl := ofsf_0mk2('equal,reorder lc lhs) . cl;
	 lhs := red lhs
      >>;
      cl := ofsf_0mk2('equal,reorder lhs) . cl;
      return rl_smkn('and,cl)
   end;

procedure ofsf_qesubiord(op,f,v,inf);
   % Ordered field standard form quantifier elimination substitute
   % infinite element with ordering relation. [op] is an ordering
   % relation. [f] is an SF; [v] is a variable; [inf] is one of
   % ['minf], ['pinf] which stand for $-\infty$ and $\infty$ resp.
   % Returns a quantifier-free formula equivalent to
   % $[op]([lhs]([v]/[inf]),0)$.
   ofsf_qesubiord1(op,sfto_reorder(f,v),v,inf);

procedure ofsf_qesubiord1(op,f,v,inf);
   % Ordered field standard form quantifier elimination substitute
   % infinite element with ordering relation subroutine. [op] is an
   % ordering relation. [f] is an SF, which is reordered wrt. [v]; [v]
   % is a variable; [inf] is one of ['minf], ['pinf] which stand for
   % $-\infty$ and $\infty$ resp. Returns a quantifier-free formula
   % equivalent to $[op]([lhs]([v]/[inf]),0)$.
   begin scalar an;
      if domainp f or mvar f neq v then
      	 return ofsf_0mk2(op,reorder f);
      an := if inf eq 'minf and not evenp ldeg f then
 	 negf reorder lc f
      else
 	 reorder lc f;
      % The use of [an] is correct in the equal case.   % Generic QE!
      return rl_mkn('or,{ofsf_0mk2(ofsf_mkstrict op,an),rl_mkn(
	 'and,{ofsf_0mk2('equal,an),ofsf_qesubiord1(op,red f,v,inf)})})
   end;

procedure ofsf_qesubcrpe1(bvl,theo,f,v,co,r);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 1 root plus epsilon. [bvl] is a list of variables;
   % [theo] is the current theory; [f] is a quantifier-free formula;
   % [v] is a variable; [r] is a root expression; [co] is a formula
   % which implies that [r] is valid. Returns a pair $(\Theta' .
   % \phi)$ where $\Theta'$ is a theory and $\phi$ is a
   % quantifier-free formula. $\phi$ is equivalent to $[co] \land
   % [f]([v]/[r1]+\epsilon)$ under the theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,ofsf_qesubrpe(f,v,r)})
   end;

procedure ofsf_qesubcrme1(bvl,theo,f,v,co,r);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 1 root minus epsilon. [bvl] is a list of variables;
   % [theo] is the current theory; [f] is a quantifier-free formula;
   % [v] is a variable; [r] is a root expression; [co] is a formula
   % which implies that [r] is valid. Returns a pair $(\Theta' .
   % \phi)$ where $\Theta'$ is a theory and $\phi$ is a
   % quantifier-free formula. $\phi$ is equivalent to $[co] \land
   % [f]([v]/[r1]-\epsilon)$ under the theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,ofsf_qesubrme(f,v,r)})
   end;

procedure ofsf_qesubcrpe2(bvl,theo,f,v,co,r1,r2);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 2 roots plus epsilon. [bvl] is a list of variables;
   % [theo] is the current theory; [f] is a quantifier-free formula;
   % [v] is a variable; [r1] and [r2] are root expression; [co] is a
   % formula which implies that both [r1] and [r2] are valid. Returns
   % a pair $(\Theta' . \phi)$ where $\Theta'$ is a theory and $\phi$
   % is a quantifier-free formula. $\phi$ is equivalent to $[co] \land
   % ([f]([v]/[r1]+\epsilon) \lor [f]([v]/[r2]+\epsilon))$ under the
   % theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,rl_mkn('or,{
      	 ofsf_qesubrpe(f,v,r1),ofsf_qesubrpe(f,v,r2)})})
   end;

procedure ofsf_qesubcrme2(bvl,theo,f,v,co,r1,r2);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 2 roots minus epsilon. [bvl] is a list of variables;
   % [theo] is the current theory; [f] is a quantifier-free formula;
   % [v] is a variable; [r1] and [r2] are root expression; [co] is a
   % formula which implies that both [r1] and [r2] are valid. Returns
   % a pair $(\Theta' . \phi)$ where $\Theta'$ is a theory and $\phi$
   % is a quantifier-free formula. $\phi$ is equivalent to $[co] \land
   % ([f]([v]/[r1]-\epsilon) \lor [f]([v]/[r2]-\epsilon))$ under the
   % theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,rl_mkn('or,{
      	 ofsf_qesubrme(f,v,r1),ofsf_qesubrme(f,v,r2)})})
   end;

procedure ofsf_qesubrpe(f,v,r);
   % Ordered field standard form quantifier elimination substitute
   % root plus epsilon. [f] is a quantifier-free formula; [v] is a
   % variable; [r] is a root expression- Returns a formula equivalent
   % to $[f]([v]/[r]+\epsilon)$ provided that [r] is valid.
   cl_apply2ats1(f,'ofsf_qesubpmeat,{v,r,'ofsf_qesubr,T});

procedure ofsf_qesubrme(f,v,r);
   % Ordered field standard form quantifier elimination substitute
   % root minus epsilon. [f] is a quantifier-free formula; [v] is a
   % variable; [r] is a root expression- Returns a formula equivalent
   % to $[f]([v]/[r]-\epsilon)$ provided that [r] is valid.
   cl_apply2ats1(f,'ofsf_qesubpmeat,{v,r,'ofsf_qesubr,nil});

procedure ofsf_qesubcqpe(bvl,theo,f,v,co,q);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 1 quotient plus epsilon. [bvl] is a list of
   % variables, [theo] is the current theory, [f] is a quantifier-free
   % formula; [v] is a variable; [co] is a formula which implies that
   % the denominator of [q] is nonzero; [q] is an SQ. Returns a pair
   % $(\Theta' . \phi)$ where $\Theta'$ is a theory and $\phi$ is a
   % quantifier-free formula. $\phi$ is equivalent to $[co] \land
   % [f]([v]/[q]+\epsilon)$ under the theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,ofsf_qesubqpe(f,v,q)})
   end;

procedure ofsf_qesubcqme(bvl,theo,f,v,co,q);
   % Ordered field standard form quantifier elimination substitute
   % conditionally 1 quotient minus epsilon. [bvl] is a list of
   % variables, [theo] is the current theory, [f] is a quantifier-free
   % formula; [v] is a variable; [co] is a formula which implies that
   % the denominator of [q] is nonzero; [q] is an SQ. Returns a pair
   % $(\Theta' . \phi)$ where $\Theta'$ is a theory and $\phi$ is a
   % quantifier-free formula. $\phi$ is equivalent to $[co] \land
   % [f]([v]/[q]-\epsilon)$ under the theory $[th] \cup \Theta'$.
   begin scalar w;
      w := ofsf_subsimpl(bvl,co,theo);
      if cdr w eq 'false then
      	 return car w . 'false;
      return car w . rl_mkn('and,{cdr w,ofsf_qesubqme(f,v,q)})
   end;

procedure ofsf_qesubqpe(f,v,q);
   % Ordered field standard form quantifier elimination substitute
   % quotient plus epsilon. [f] is a quantifier-free formula; [v] is a
   % variable; [q] is an SQ. Returns a quantifier-free formula
   % equivalent to $[f]([v]/[q]+\epsilon)$ provided that the
   % denominator of [q] is nonzero.
   cl_apply2ats1(f,'ofsf_qesubpmeat,{v,q,'ofsf_qesubq,T});

procedure ofsf_qesubqme(f,v,q);
   % Ordered field standard form quantifier elimination substitute
   % quotient minus epsilon. [f] is a quantifier-free formula; [v] is a
   % variable; [q] is an SQ. Returns a quantifier-free formula
   % equivalent to $[f]([v]/[q]-\epsilon)$ provided that the
   % denominator of [q] is nonzero.
   cl_apply2ats1(f,'ofsf_qesubpmeat,{v,q,'ofsf_qesubq,nil});

procedure ofsf_qesubpmeat(atf,v,u,finsub,ple);
   % Ordered field standard form quantifier elimination substitute
   % plus/minus epsilon into atomic formula. [atf] is an atomic
   % formula; [v] is a variable; [u] is any field element;
   % [finsub(atf,v,u)] is a procedure that can substitute [u] into a
   % formula; [ple] is Boolean, non-[nil] means $+\epsilon$. Returns a
   % quantifier-free formula equivalent to $[atf]([v]/[u]\pm\epsilon)$
   % provided that the denominator of [u] is nonzero.
   begin scalar op,lhs;
      if not (v memq ofsf_varlat atf) then return atf;
      op := ofsf_op atf;
      lhs := ofsf_arg2l atf;
      if op eq 'equal or op eq 'neq then
	 return ofsf_qesubtranseq(op,lhs,v);
      % [op] is an ordering relation.
      return apply(finsub,{ofsf_qesubpmeord(op,lhs,v,ple),v,u})
   end;

procedure ofsf_qesubpmeord(op,f,v,ple);
   % Ordered field standard form quantifier elimination substitute
   % plus/minus epsilon with ordering relation. [op] is an ordering
   % relation. [f] is an SF; [v] is a variable; [ple] is Boolean,
   % non-[nil] means $+\epsilon$. Returns a quantifier-free formula
   % $\phi$ such that $\phi(v/u)$ is equivalent to
   % $[op]([f]([v]/u\pm\epsilon),0)$ for any field element $u$ with
   % nonzero denominator.
   if degreef(f,v) eq 0 then
      ofsf_0mk2(op,f)
   else
      rl_mkn('or,{ofsf_0mk2(ofsf_mkstrict op,f),rl_mkn('and,{
	 ofsf_0mk2('equal,f),ofsf_qesubpmeord(
	    op,if ple then diff(f,v) else negf diff(f,v),v,ple)})});

procedure ofsf_subsimpl(bvl,f,th);
   % Ordered field standard form substitution condition
   % simplification. [bvl] is a list of variables; [f] is a formula;
   % [th] is the current theory. Returns a pair $(\Theta'.\phi)$, such
   % that $phi$ is equivalent to [f] under the theory
   % $[th]\cup\Theta'$. All atomic formulas in $\Theta'$ contain only
   % terms [u] such that [ofsf_valassp(bvl,u)] holds.
   begin scalar nth;
      f := cl_simpl(f,th,-1);
      if not !*rlqegen then
	 return nil . f;
      nth := for each atf in cl_atl1 f join
	 if ofsf_op atf='equal and ofsf_valassp(bvl,ofsf_arg2l atf) then
	    {ofsf_0mk2('neq,ofsf_arg2l atf)};
      if nth then <<
	 ioto_prin2 "!";
      	 return nth . cl_simpl(f,append(nth,th),-1)
      >>;
      return nil . f
   end;

procedure ofsf_valassp(bvl,sf);
   % Ordered field standard form valid assumption. [bvl] is a list of
   % variables; [sf] is a standard form. Returns [T] if an assumption
   % containing [sf] is valid. Depends on switch [!*rlqegenct].
   (!*rlqegenct or sfto_monfp sf) and null intersection(bvl,kernels sf);

%DS ALP
% A pair of ALIST's encoding the set of possible elimination terms.

% Keys created by ofsf_translat1:
% equal1: linear equations
% equal21q: quadratic equations 1 quotient
% equal22r: quadratic equations 2 roots
% neq1: linear inequalities
% neq21q: quadratic inequalities 1 quotient
% neq22r: quadratic inequalities 2 roots
% geq1: linear weak lower bounds
% leq1: linear weak upper bounds
% greaterp1: linear strong lower bounds
% lessp1: linear strong upper bounds
% wo1: linear weak orderings
% wo21q: quadratic weak orderings 1 quotient
% wo22r: quadratic weak orderings 2 roots
% so1: linear strong orderings
% so21q: quadratic strong orderings 1 quotient
% so22r: quadratic strong orderings 2 roots

smacro procedure ofsf_mkalp(tag,l);
   % Ordered field standard form make alist pair. [tag] is a key; [l]
   % is an entry. Returns an ALP.
   {tag . l} . {tag . 1};

smacro procedure ofsf_ceterm1a(m,u);
   % Ordered field standard form conditional elimination term 1
   % condition atomic other parameter. [m] is a SF; [u] is an
   % elimination term.
   {ofsf_0mk2('neq,m),u};

smacro procedure ofsf_ceterm2a(a,m,u);
   % Ordered field standard form conditional elimination term 2
   % conditions atomic other parameter. [a], [m] are SF's; [u] is an
   % elimination term.
   if a then
      {rl_mkn('and,{ofsf_0mk2('equal,a),ofsf_0mk2('neq,m)}),u}
   else
      {ofsf_0mk2('neq,m),u};

smacro procedure ofsf_ceterm1l(a,l);
   % Ordered field standard form conditional elimination term 1
   % condition parameter list.
   ofsf_0mk2('neq,a) . l;

smacro procedure ofsf_ceterm2l(a,d,l);
   % Ordered field standard form conditional elimination term 2
   % conditions parameter list. [a], [d] are SF's; [l] is a list of
   % elimination terms.
   rl_mkn('and,{ofsf_0mk2('neq,a),ofsf_0mk2('geq,d)}) . l;

smacro procedure ofsf_mktag1(x);
   % Ordered field standard form make tag linear case. [x] is an
   % identifier. Returns the interned identifier [x]1.
   intern compress(nconc(explode x,'(!1)));

smacro procedure ofsf_mktag2(x,y);
   % Ordered field standard form make tag quadratic case. [x], [y] are
   % identifiers. Returns the interned identifier [x]2[y].
   intern compress(nconc(explode x,'!2 . explode y));

procedure ofsf_translat(atf,v,theo,pos,ans);
   % Ordered field standard form translate atomic formula. [atf] is an
   % atomic formula $\rho(t,0)$; [v] is a variable; [theo] is the
   % current theory; [pos], [ans] are Bool. Returns an ALP. If [pos]
   % is non-[nil] [atf] is consided as [not(atf)]. The switch [rlqesr]
   % is turned on if [ans] is non-[nil]. If [v] is not in $t$ the
   % result is $([nil] . [nil])$. Else $t$ is of the form $\prod_i
   % a_i[v]^2+b_i[v]+c_i$, and the result is $(((\rho' . (-b . a))) .
   % ((\rho' . 1)))$ where $\rho'=\rho$ for non-[nil] [pos] and the
   % negation of $\rho$ else.
   begin scalar svrlqesr,res;
      if ans then <<
      	 svrlqesr := !*rlqesr;
	 on1 'rlqesr
      >>;
      if v memq ofsf_varlat atf then <<
      	 res := if pos then
 	    ofsf_translat1(atf,v,theo)
      	 else
	    ofsf_translat1(ofsf_negateat atf,v,theo);
	 if res = '(nil . nil) then
	    res := {'anypoint . nil} . {'anypoint . 1}
      >> else
 	 res := nil . nil;
      if ans and null svrlqesr then
	 off1 'rlqesr;
      return res
   end;

procedure ofsf_translat1(atf,v,theo);
   % Ordered field standard form translate atomic formula subroutine.
   % [atf] is an atomic formula; [v] is a variable; [theo] is the
   % current theory. Returns an ALP or a pair of the key ['failed] and
   % an error message.
   begin scalar w,rel;
      w := ofsf_mktriplel(ofsf_arg2l atf,v);
      if car w eq 'failed then return w;
      rel := ofsf_op atf;
      if null car w then
	 return ofsf_translat2(rel,cadr w,theo);
      return cl_alpunion for each x in cdr w join
	 if rel memq '(geq leq lessp greaterp) then
	    {ofsf_translat2(rel,x,theo),
	       ofsf_translat2(ofsf_anegrel rel,x,theo)}
	 else
	    {ofsf_translat2(rel,x,theo)}
   end;

procedure ofsf_translat2(rel,trip,theo);
   % Ordered field standard form translate atomic formula subroutine.
   % [rel] is a relation, [trip] is a triple; [theo] is the current
   % theory. Returns an ALP.
   if null car trip then
      ofsf_translatlin(rel,cadr trip,caddr trip,theo,nil)
   else
      ofsf_translatqua(rel,car trip,cadr trip,caddr trip,theo);

procedure ofsf_translatlin(r,m,b,theo,xc);
   % Ordered field standard form translate atomic formula linear case.
   % [r] is a relation; [m], [b] are the 2nd and 3rd constituent of a
   % triple generated from a linear term; [theo] is the current
   % theory; [xc] is a SF encoding an extra condition. Returns an ALP.
   ofsf_mkalp(ofsf_tlltag(r,m,theo),{ofsf_ceterm2a(xc,m,ofsf_mksol1(m,b))});

procedure ofsf_tlltag(r,m,theo);
   % Ordered field standard form translate atomic formula linear case
   % make tag. [r] is a relation; [m] is the 2nd constituent of a
   % triple generated from a linear term; [theo] is the current
   % theory. Returns a tag.
   if r eq 'equal or r eq 'neq then
      ofsf_mktag1 r
   else if ofsf_surep(ofsf_0mk2('geq,m),theo) then
      ofsf_mktag1 r
   else if ofsf_surep(ofsf_0mk2('leq,m),theo) then
      ofsf_mktag1 ofsf_anegrel r
   else if r eq 'lessp or r eq 'greaterp then
      'so1
   else % [r memq '(leq geq)]
      'wo1;

procedure ofsf_translatqua(r,a,b,c,theo);
   % Ordered field standard form translate atomic formula subroutine
   % quadratic case. [r] is a relation; [a], [b], and [c] are the
   % constituent of a triple; [theo] is the current theory. Returns an
   % ALP.
   begin scalar w,tagbase,tag,eset;
      w := ofsf_mksol2(a,b,c);
      if w eq 'failed then
	 return nil . nil;
      tagbase := if r memq '(lessp greaterp) then
 	 'so
      else if r memq '(leq geq) then
 	 'wo
      else  % [if r memq '(equal neq) then]
 	 r;
      if car w eq 'onequot then <<
	 tag := ofsf_mktag2(tagbase,'!1q);
	 eset := {ofsf_ceterm1a(a,cdr w)}
      >> else if car w eq 'tworoot then <<
	 if !*rlqesr then <<
	    tag := ofsf_mktag2(tagbase,'!1r);
	    eset := {ofsf_ceterm2l(a,cadr w,{caddr w}),
	       ofsf_ceterm2l(a,cadr w,{cadddr w})}
	 >> else <<
	    tag := ofsf_mktag2(tagbase,'!2r);
	    eset := {ofsf_ceterm2l(a,cadr w,{caddr w,cadddr w})}
	 >>
      >>;
      if not null b then <<
      	 w :=  ofsf_translatlin(r,b,c,theo,a);
      	 return {tag . eset,caar w} . {tag . 1,cadr w}
      >>;
      return ofsf_mkalp(tag,eset)
   end;

procedure ofsf_surep(f,theo);
   % Ordered field standard form sure predicat. [f] is a formula;
   % [theo] is a theory. Returns [T] if $f$ holds under the theory
   % [theo].
   cl_simpl(f,theo,-1) eq 'true;

procedure ofsf_mktriplel(u,v);
   % Ordered field standard form make triple list. [v] is a variable,
   % [u] is a SF containing [v]. Returns a pair $k . l$, where $k$ is
   % one off ['failed], ['fac], [nil] and $l$ is a list. If $k$ is
   % [nil], then the degree of [u] in [v] is less than or equal to 2,
   % if [k] is ['fac] then the degree of all irreducible factors of
   % [u] in [v] is less than or equal to 2, and if $k$ is ['failed]
   % then at least one factor of [u] has an degree greater than 2 in
   % [v]. If $k$ is not ['failed] then $l$ is the list of all triples
   % of the factors of [u]. If $k$ is ['failed] then $l$ encodes a
   % warning-message. Notice that if $k$ is [nil] the list $l$
   % contains only one element.
   begin scalar w,g,fl,a,ul;
      w := setkorder {v};
      u := reorder u;
      if ldeg u <= 2 then <<
	 setkorder w;
	 return nil . {ofsf_reotrip ofsf_mktriple u}
      >>;
      % Try to factorize.
      if !*rlverbose then ioto_prin2{"."};
      fl := cdr fctrf u;
      while fl do <<
	 a := car fl;
	 fl := cdr fl;
	 g := degr(car a,v);
	 if g > 2 then <<
	    ul := 'failed . {"degree of",v,"is",g,"in",prepf car a};
	    fl := nil
	 >> else if g > 0 then
 	    ul := car a . ul
      >>;
      setkorder w;
      if car ul = 'failed then return ul;
      return 'fac . for each x in ul collect ofsf_reotrip ofsf_mktriple x
   end;

procedure ofsf_mktriple(x);
   % Ordered field standard form make triple. [x] is a SF of the form
   % $a[v]^2+b[v]+c$, not necessarily in the current kernel order.
   % Returns the triple $(a,b,c)$.
   begin scalar a,v;
      v := mvar x;
      if ldeg x eq 2 then <<
      	 a := lc x;
      	 x := red x
      >>;
      return if not domainp x and mvar x eq v then
   	 {a,lc x,red x}
      else
   	 {a,nil,x}
   end;

procedure ofsf_reotrip(trip);
   % Orderd field standard form reorder triple. [trip] is a triple
   % $(a,b,c)$ of SF's. Returns the triple $(a',b',c')$ of SF's, where
   % $a'$, $b'$, and $c'$ are reorderd wrt. the current kernel order.
   {reorder car trip,reorder cadr trip,reorder caddr trip};

procedure ofsf_mksol1(m,b);
   % Orderd field standard form make solution linear case. [m] and [b]
   % are standard forms. Returns $-[b]/m$ as SQ.
   quotsq(!*f2q negf b,!*f2q m);

procedure ofsf_mksol2(a,b,c);
   % Orderd field standard form make solution quadratic case. [a],
   % [b], and [c] are SF's. Returns either ['failed] or a pair $(k .
   % f)$. $k$ is one of ['onequot], ['tworoot]. If $k$ is ['onequot]
   % then $[b]^2-4[a][c]=0$ and $f$ is the SQ $-[b]/2[a]$. If $k$ is
   % ['tworoot] then $f$ is a pair $(\delta . l)$ where $\delta$ is
   % the discriminante of $a x^2+b x+c$ and $l$ is a list of the two
   % root expressions coding $(-[b]\pm\sqrt{[b]^2-4[a][c]})/2[a]$.
   begin scalar disc,w,c;
      disc := addf(exptf(b,2),negf multf(4,multf(a,c)));
      if domainp disc and minusf disc then
      	 return 'failed;
      a := multf(2,a);
      b := negf b;
      if null disc then
      	 return 'onequot . quotsq(!*f2q b,!*f2q a);
      w := sfto_sqrtf disc;
      if w then
	 return 'tworoot . nil . ofsf_mksol21q(b,w,a);
      return 'tworoot . disc . ofsf_mksol21r(b,disc,a)
   end;

procedure ofsf_mksol21q(mb,discr,ta);
   % Orderd field standard form make solution quadratic case 1
   % quotient. [mb], [discr] and [ta] are SF's. Returns a list of the
   % two root expressions $([mb],\pm[discr],1,ta)$.
   {{mb,negf discr,1,ta},{mb,discr,1,ta}};

procedure ofsf_mksol21r(mb,disc,ta);
   % Orderd field standard form make solution quadratic case 1 root.
   % [mb], [disc] and [ta] are SF's. Returns a list of the two root
   % expressions $([mb],\pm1,[disc],ta)$.
   {{mb,-1,disc,ta},{mb,1,disc,ta}};

%DS elimination_set
% A list $(...,(p . (l_1,...,l_n)),...)$ where the $p$ are procedures
% and the $l_i$ are parameter lists $(l_{i1},...,l_{im})$ such that
% there is $p(f,v,l_{i1},...,l_{im})$ called for substitution, where
% $f$ is the considered formula, and $v$ the considered variable.

procedure ofsf_elimset(v,alp);
   % Ordered field standard form elimination set. [v] is a variable;
   % [alp] is a pair of alists. Returns an elimination set.
   begin scalar atfal,w,lpart,qpart,npart;
      atfal := car alp;
      if null cdr atfal and caar atfal = 'anypoint then
 	 return '((ofsf_qesubcq . ((true (nil . nil)))));
      % Treat some special cases.
      w := ofsf_elimsetscq(atfal);
      if w then <<
	 if !*rlverbose then ioto_prin2 "#q";
	 return w
      >>;
      w := ofsf_elimsetscl(atfal);
      if w then <<
	 if !*rlverbose then ioto_prin2 "#l";
	 return w
      >>;
      w := ofsf_elimsetlin1s(atfal);
      lpart := cdr w;
      qpart := ofsf_elimsetqua(atfal,car w);
      npart := ofsf_elimsetneq(atfal,car w);
      return lto_nconcn {lpart,qpart,npart}
   end;

procedure ofsf_elimsetscq(atfal);
   % Elimination set computation quadratic special case. [atfal] is an
   % alist. Returns an elimination set or [nil]. Check if there is
   % exactly one point coming from a quadratic non-equation. If so, we
   % test the zero of the corresponding derivative, $\pm \infty$, and
   % all linear upper and lower bounds. Equations and inequations are
   % treated as usual.
   begin scalar w,l,a,nzf,zero,d,dfzero,hl;
      if not !*rlqeqsc then
	 return nil;
      l := '(neq21q neq22r wo21q wo22r so21q so22r neq21r wo21r so21r);
      while l do <<
	 a := car l;
	 l := cdr l;
	 if (w := lto_catsoc(a,atfal)) then
	    if nzf or a memq '(neq21r wo21r so21r) and cddr w or
	       a memq '(neq21q neq22r wo21q wo22r so21q so22r) and cdr w
 	    then <<
	       l := nil;
	       a := 'failed
	    >> else <<
	       zero := car w;  % The only entry in w
	       nzf := car reversip explode a
	    >>
      >>;
      if a eq 'failed or null nzf then return nil;
      % Construct the zero of the derivative from [zero] which is a
      % zero of the polynomial itself.
      if nzf = 'q then   % bad, but not relevant with !*rlsipd on
      	 dfzero := zero
      else <<  % [nzf = 'r]
	 zero := cadr zero;  % first solution
      	 d := cadddr zero;
      	 dfzero := {ofsf_0mk2('neq,d),ofsf_mksol1(d,negf car zero)}
      >>;
      hl := {'ofsf_qesubcq . (dfzero . lto_catsoc('equal21q,atfal)),
	 'ofsf_qesubcr2 . lto_catsoc('equal22r,atfal),
	    '(ofsf_qesubi (pinf) (minf))};
      return lto_nconcn {hl,ofsf_elimsetlinbs(atfal),ofsf_elimsetneqbs(atfal)}
   end;

smacro procedure ofsf_setvlin();
   % Ordered field standard form set variables for elimination set
   % computation linear case.
   <<
      equal1 := lto_catsoc('equal1,atfal);
      leq1 := lto_catsoc('leq1,atfal);
      geq1 := lto_catsoc('geq1,atfal);
      greaterp1 := lto_catsoc('greaterp1,atfal);
      lessp1 := lto_catsoc('lessp1,atfal);
      wo1 := lto_catsoc('wo1,atfal);
      so1 := lto_catsoc('so1,atfal)
   >>;

procedure ofsf_elimsetlinbs(atfal);
   % Ordered field standard form elimination set linear case both
   % sides. [atfal] is an alist. Returns an elimination set.
   begin
      scalar equal1,leq1,geq1,greaterp1,lessp1,wo1,so1,qesubcql,
	 qesubcqmel,qesubcqpel;
      ofsf_setvlin();
      qesubcql := 'ofsf_qesubcq . lto_nconcn{equal1,leq1,geq1,wo1};
      qesubcqmel := 'ofsf_qesubcqme . lto_nconcn{so1,lessp1};
      qesubcqpel := 'ofsf_qesubcqpe . lto_nconcn{so1,greaterp1};
      return {qesubcql,qesubcqmel,qesubcqpel}
   end;

procedure ofsf_elimsetneqbs(atfal);
   % Elimination set [neq] test both sides.
   begin scalar neq1,neq21q,neq21r,neq22r;
      neq1 := lto_catsoc('neq1,atfal);
      neq21q := lto_catsoc('neq21q,atfal);
      neq22r := lto_catsoc('neq22r,atfal);
      neq21r := lto_catsoc('neq21r,atfal);
      return {'ofsf_qesubcqme . nconc(neq1,neq21q),'ofsf_qesubcrme2 . neq22r,
	 'ofsf_qesubcrme1 . neq21r,'ofsf_qesubcrpe1 . neq21r,
      	 'ofsf_qesubcqpe . nconc(neq1,neq21q),'ofsf_qesubcrpe2 . neq22r}
   end;

smacro procedure ofsf_setvscl();
   % Ordered field standard form set variables for elimination set
   % computation linear special case.
   <<
      equal1 := lto_catsoc('equal1,atfal);
      equal21q := lto_catsoc('equal21q,atfal);
      equal21r := lto_catsoc('equal21r,atfal);
      equal22r := lto_catsoc('equal22r,atfal);
      leq1 := lto_catsoc('leq1,atfal);
      geq1 := lto_catsoc('geq1,atfal);
      greaterp1 := lto_catsoc('greaterp1,atfal);
      lessp1 := lto_catsoc('lessp1,atfal);
      wo1 := lto_catsoc('wo1,atfal);
      so1 := lto_catsoc('so1,atfal);
      o2p := lto_catsoc('wo21q,atfal) or lto_catsoc('wo21r,atfal) or
	 lto_catsoc('wo22r,atfal) or lto_catsoc('so21q,atfal) or
 	 lto_catsoc('so21r,atfal) or lto_catsoc('so22r,atfal)
   >>;

procedure ofsf_elimsetscl(atfal);
   % Elimination set computation linear special case. [atfal] is an
   % alist. Returns an elimination set or [nil]. Computes an
   % elimination set for the following two special cases: (1) There is
   % no quadratic bound, the linear bounds there are either all upper
   % bounds or all lower bounds. Then the opposite inifinity can be
   % tested. The inequations can be ignored. (2) There is exactly one
   % bound, which is linear and parametric. Then $\pm \infty$ can be
   % tested. The inequations can be ignored. In both cases the
   % equations are treated as usual.
   begin
      scalar equal1,equal21q,equal21r,equal22r,leq1,geq1,greaterp1,lessp1,
	 o2p,nub,nlb,infsubl,wo1,so1;
      ofsf_setvscl();
      if o2p then return nil;  % Any quadratic bound
      nub := null (leq1 or lessp1);  % No concrete upper bound
      nlb := null (geq1 or greaterp1);  % No concrete lower bound
      if null (wo1 or so1) then  % No parametric bound
      	 (if nub then
	    infsubl := '(ofsf_qesubi . ((pinf)))
      	 else if nlb then
            infsubl := '(ofsf_qesubi . ((minf))))
      else if nub and nlb and
      	 (null wo1 and null cdr so1 or null so1 and null cdr wo1)
      then  % Exactly one bound, which is linear and parametric.
	 infsubl := '(ofsf_qesubi . ((pinf) (minf)));
      if infsubl then
	 return {infsubl,'ofsf_qesubcr1 . equal21r,
	    'ofsf_qesubcq . nconc(equal1,equal21q),'ofsf_qesubcr2 . equal22r}
   end;

procedure ofsf_elimsetlin1s(atfal);
   % Ordered field standard form elimination set linear part decide
   % for one side. [atfal] is an alist. Returns a pair $a . d$ where
   % $d$ is an elimination set, and $a$ is one of [T], [nil] which
   % means we have decided to test lower bounds or upper bound resp.
   begin
      scalar equal1,leq1,geq1,greaterp1,lessp1,wo1,so1,qesubcql,qesubil,esubl;
      integer l1n,g1n;
      ofsf_setvlin();
      l1n := length leq1 + length lessp1;
      g1n := length geq1 + length greaterp1;
      if l1n <= g1n then <<
      	 qesubcql := 'ofsf_qesubcq . lto_nconcn{equal1,leq1,wo1};
	 esubl := 'ofsf_qesubcqme . nconc(so1,lessp1);
	 qesubil := '(ofsf_qesubi . ((pinf)));
	 return nil . {qesubcql,esubl,qesubil}
      >>;
      qesubcql := 'ofsf_qesubcq . lto_nconcn{equal1,geq1,wo1};
      esubl := 'ofsf_qesubcqpe . nconc(so1,greaterp1);
      qesubil := '(ofsf_qesubi . ((minf)));
      return T . {qesubcql,esubl,qesubil}
   end;

procedure ofsf_elimsetqua(atfal,ple);
   % Ordered field standard form elimination set quadratic part.
   % [atfal] is an alist; [ple] is bool where [T] means we have
   % decided for lower bounds in the linear part. Returns an
   % elimination set.
   begin
      scalar equal21q,equal22r,wo21q,wo22r,so21q,so22r,qesubcql,qesubcr1l,
	 qesubcr2l,esubcql,esubcr1l,esubcr2l,equal21r,wo21r,so21r;
      equal21q := lto_catsoc('equal21q,atfal);
      equal21r := lto_catsoc('equal21r,atfal);
      equal22r := lto_catsoc('equal22r,atfal);
      wo21q := lto_catsoc('wo21q,atfal);
      wo21r := lto_catsoc('wo21r,atfal);
      wo22r := lto_catsoc('wo22r,atfal);
      so21q := lto_catsoc('so21q,atfal);
      so21r := lto_catsoc('so21r,atfal);
      so22r := lto_catsoc('so22r,atfal);
      if ple then <<
	 esubcql := 'ofsf_qesubcqpe . so21q;
	 esubcr1l := 'ofsf_qesubcrpe1 . so21r;
	 esubcr2l := 'ofsf_qesubcrpe2 . so22r
      >> else <<
	 esubcql := 'ofsf_qesubcqme . so21q;
	 esubcr1l := 'ofsf_qesubcrme1 . so21r;
	 esubcr2l := 'ofsf_qesubcrme2 . so22r
      >>;
      qesubcql := 'ofsf_qesubcq . nconc(equal21q,wo21q);
      qesubcr1l := 'ofsf_qesubcr1 . nconc(equal21r,wo21r);
      qesubcr2l := 'ofsf_qesubcr2 . nconc(equal22r,wo22r);
      return {qesubcql,qesubcr1l,qesubcr2l,esubcql,esubcr1l,esubcr2l}
   end;

smacro procedure ofsf_setvneq();
   % Ordered field standard form set variables for elimination set
   % computation [neq] treatment.
   <<
      neq1 := lto_catsoc('neq1,atfal);
      neq21q := lto_catsoc('neq21q,atfal);
      neq21r := lto_catsoc('neq21r,atfal);
      neq22r := lto_catsoc('neq22r,atfal);
      leq1 := lto_catsoc('leq1,atfal);
      geq1 := lto_catsoc('geq1,atfal);
      wo1 := lto_catsoc('wo1,atfal);
      wo21q := lto_catsoc('wo21q,atfal);
      wo21r := lto_catsoc('wo21r,atfal);
      wo22r := lto_catsoc('wo22r,atfal)
   >>;

procedure ofsf_elimsetneq(atfal,ple);
   % Ordered field standard form elimination set treatment of ['neq].
   % [atfal] is an alist; [ple] is bool where [T] means we have
   % decided for lower bounds in the linear part. Returns an
   % elimination set.
   begin
      scalar neq1,neq21q,neq21r,neq22r,leq1,geq1,wo1,wo21q,wo21r,wo22r,
	 neqn,wbn,esubcq,esubcr1,esubcr2,wb1;
      ofsf_setvneq();
      neqn := length neq1 + length neq21q + length neq21r + 2*(length neq22r);
      if neqn = 0 then return nil;
      wbn := length wo1 + length wo21q + length wo21r +
 	 2*(length wo22r);  % + ...
      if ple then <<
	 esubcq := 'ofsf_qesubcqpe;
	 esubcr1 := 'ofsf_qesubcrpe1;
	 esubcr2 := 'ofsf_qesubcrpe2;
	 wb1 := geq1;
	 wbn := wbn + length geq1
      >> else <<
	 esubcq := 'ofsf_qesubcqme;
	 esubcr1 := 'ofsf_qesubcrme1;
	 esubcr2 := 'ofsf_qesubcrme2;
	 wb1 := leq1;
	 wbn := wbn + length leq1
      >>;
      if neqn < wbn then
	 return {esubcq .
 	    nconc(neq1,neq21q),esubcr1 . neq21r,esubcr2 . neq22r};
      if !*rlverbose then ioto_prin2 {"(ANEQ:",neqn,"|",wbn,")"};
      return {esubcq . lto_nconcn{wb1,wo1,wo21q},esubcr1 . wo21r,
	 esubcr2 . wo22r}
   end;

procedure ofsf_bettergaussp(grv1,grv2);
   % Ordered field standard form better Gauss predicate. [grv1] and
   % [grv2] are GRV's. Returns [T] if [grv1] encodes a better Gauss
   % application than [grv2] encodes.
   begin scalar w1,w2;
      if car grv1 eq 'failed then
      	 return nil;
      if car grv2 eq 'failed then
      	 return T;
      w1 := cadar grv1;
      w2 := cadar grv2;
      if w1 neq w2 then
      	 return (w1 memq cdr (w2 memq '(fac quar qua2q quaq lin)));
      w1 := caddar grv1;
      w2 := caddar grv2;
      if w1 neq w2 then
      	 return w1 memq cdr (w2 memq '(gen td con));
      w1 := ofsf_esetlength cadr grv1;
      w2 := ofsf_esetlength cadr grv2;
      if w1 neq w2 then
      	 return w1 < w2;
      w1 := caddar grv1;
      w2 := caddar grv2;
%      if w1 neq w2 then
      return w1 memq cdr (w2 memq '(gen td con));
   end;

procedure ofsf_esetlength(e);
   % Ordered field standard form elimination set length. [e] is an
   % elimination set. Returns the number of elimination terms in [e].
   for each p in e sum
      for each x in p sum
	 length cdr p;

procedure ofsf_esetunion(e1,e2);
   % Ordered field standard form elimination set union. [e1] and [e2]
   % are elimination sets. Returns the union of [e1] and [e2].
   lto_alunion({e1,e2});

procedure ofsf_bestgaussp(grv);
   % Ordered field standard form best Gauss predicate. [grv] is a GRV.
   % Returns [T] if the Gauss application encoded in GRV is the best
   % Gauss application under all possible Gauss applications.
   not(car grv eq 'failed) and not(car grv eq 'gignore) and
      cadar grv eq 'lin and caddar grv eq 'con and   % Linear, concrete coeff.
      null cdr cadr grv and null cddar cadr grv;     % Only one elim. term

procedure ofsf_qefsolset(a,v,theo,ans,bvl);
   % Ordered field standard form quantifier elimination finite
   % solution set. [a] is an atomic formula; [v] is a variable; [theo]
   % is the current theory; [ans] is Boolean; [bvl] is a list of
   % variables. Returns an IGRV.
   begin scalar w;
      if ofsf_op a neq 'equal then
	 return '(failed . nil);
      w := ofsf_varlat a;
      if v memq w then
      	 return  ofsf_findeqsol(a,v,theo,ans,bvl);
      if !*rlqegen and ofsf_valassp(bvl,ofsf_arg2l a) then
      	 return ('gignore . (nil . {ofsf_0mk2('neq,ofsf_arg2l a)}));
      return '(failed . nil);
   end;

procedure ofsf_findeqsol(a,v,theo,ans,bvl);
   % Ordered field standard form find solution of non-trivial equation
   % subroutine. [a] is an atomic formula; [v] is a variable; [theo]
   % is a list of atomic formulas, the current theory; [ans] is
   % Boolean; [bvl] is a list of variables that are considered
   % non-parametric. Returns $[failed] . [nil]$ or a form $(\tau . (e
   % . \theta))$ where $\tau$ is an identifier tag encoding the degree
   % of the Gauss application, [e] is an elimination set, and $\theta$
   % is the new theory. If [!*rlqegen] is off, we know
   % $\theta'=[nil]$.
   begin scalar w,d,theop,tag;
      w := ofsf_pnontrivial(ofsf_arg2l a,v,theo,bvl);
      tag := car w;
      if not tag then
      	 return '(failed . nil);
      if cdr w then
      	 theop := {cdr w};
      d := degreef(ofsf_arg2l a,v);
      w := ofsf_gelimset ofsf_translat(a,v,theo,T,ans);
      if w eq 'failed then return '(failed . nil);
      return ofsf_mkgtag(d,tag,w,theo) . (w . theop)
   end;

procedure ofsf_mkgtag(d,tag,eset,theo);
   % Ordered field standard form make Gauss tag. [d] is positive
   % integer; [tag] is an identifier; [eset] is an elimination set;
   % [theo] is the current theory.
   begin scalar w,v;
      w := if d=1 then 'lin else if d=2 then ofsf_mkgtagq(eset,theo) else 'fac;
      v := if d=1 then v := "l" . v else if d=2 then v := "q" . v;
      if tag eq 'gen then v := "!" . v;
      return {v,w,tag}
   end;

procedure ofsf_mkgtagq(eset,theo);
   % Ordered field standard form make Gauss tag quadratic case. [eset]
   % is an elimination set; [theo] is the current theory.
   begin scalar a;
      if null cdr eset and caar eset eq 'ofsf_qesubcq then
 	 return 'quaq;
      a := atsoc('ofsf_qesubcr2,eset) or atsoc('ofsf_qesubcr1,eset);
      % We know [a neq nil].
      if null cadr cadr cadr a then  % $b$ of the first root expression.
   	 return 'qua2q;
      return 'quar
   end;

procedure ofsf_gelimset(alp);
   % Gauss elimination set. [alp] is a pair of alists obtained from
   % [ofsf_translat]. Returns an elimination set.
   begin scalar eset;
      eset := car alp;
      if eset = 'failed then return 'failed;
      if null cdr eset and caar eset = 'anypoint then
 	 return {'ofsf_qesubcq . {'(true (nil . nil))}};
      for each x in eset do
	 if car x memq '(equal1 equal21q) then
 	    car x := 'ofsf_qesubcq
	 else if car x = 'equal21r then
	    car x := 'ofsf_qesubcr1
	 else if car x = 'equal22r then
	    car x := 'ofsf_qesubcr2
	 else
	    rederr "BUG IN ofsf_gelimset";
      return eset
   end;

procedure ofsf_pnontrivial(u,v,theo,bvl);
   % Possibly non-trivial. [u] is an SF; [v] is a variable; [theo] is
   % a list of atomic formulas, the current theory; [bvl] is a list of
   % variables that are considered non-parametric. Returns a pair $p .
   % \theta'$ where $\theta'$ is an inequation or [nil], and $p$ is
   % non-[nil] iff one of the coefficients of [u] wrt. [v] may be
   % assumed nonzero under the assumption $[theo] \cup \{\theta'\}$.
   % If [!*rlqegen] is off, we know $\theta'=[nil]$.
   begin scalar vcoeffs;
      vcoeffs := for each x in coeffs sfto_reorder(u,v) collect reorder x;
      return ofsf_maybenonzerol(vcoeffs,theo,bvl)
   end;

procedure ofsf_maybenonzerol(l,theo,bvl);
   % Maybe not a list of zero SF's. [l] is a list of SF's; [theo] is a
   % list of atomic formulas, the current theory; [bvl] is a list of
   % variables that are considered non-parametric. Returns a pair $p .
   % \theta'$ where $\theta'$ is an inequation or [nil], and $p$ is
   % non-[nil] iff one of the elements of [l] may be assumed nonzero under
   % the assumption $[theo] \cup \{\theta'\}$. If [!*rlqegen] is
   % off, we know $\theta'=[nil]$.
   begin scalar w,result;
      result := '(nil . nil);
      while l do <<
	 w := ofsf_maybenonzero(car l,theo,bvl);
	 l := cdr l;
	 if car w then <<
	    result := w;
	    l := nil
      	 >>
      >>;
      return result
   end;

procedure ofsf_maybenonzero(u,theo,bvl);
   % Maybe a non-zero SF's. [u] is an SF's; [theo] is a list of atomic
   % formulas, the current theory; [bvl] is a list of variables that
   % are considered non-parametric. Returns a pair $p . \theta'$ where
   % $\theta'$ is an inequation or [nil], and $p$ is non-[nil] iff [u] may
   % be assumed nonzero under the assumption $[theo] \cup
   % \{\theta'\}$. If [!*rlqegen] is off, we know $\theta'=[nil]$.
   if domainp u then
      if null u then
      	 '(nil . nil)
      else
	 '(con . nil)   % con = concrete
   else if cl_simpl(ofsf_0mk2('equal,u),theo,-1) eq 'false then
      '(td . nil)   % td = theory derived
   else if !*rlqegen and ofsf_valassp(bvl,u) then
      'gen . ofsf_0mk2('neq,u)  % gen = generic
   else
      '(nil . nil);


procedure ofsf_qemkans(an,atr);
   sort(
      ofsf_qeapplyatr ofsf_qebacksub ofsf_qemkans1 an,
      function(lambda(x,y); ordp(cadr x,cadr y)));

procedure ofsf_qemkans1(an);
   % Ordered field standard form quantifier elimination make answer
   % subroutine. [an] is an answer. Returns a list $((e,a),...)$,
   % where $e$ is an equation and $a$ is an answer translation.
   begin scalar v,sub,xargl,w,atr;
      return for each y in an collect <<
	 v := car y;
	 sub := cadr y;
	 xargl := caddr y;
	 atr := cadddr y;
	 w := if sub eq 'ofsf_qesubi then <<
	    atr := nil;
      	    (if car xargl = 'pinf then
	       'infinity
      	    else if car xargl = 'minf then
	       '(minus infinity))
	 >> else if sub eq 'ofsf_qesubcq then
	    prepsq cadr xargl
	 else if sub eq 'ofsf_qesubcr1 then
	    ofsf_preprexpr(cadr xargl)
	 else if sub eq 'ofsf_qesubcqme then
	    {'difference,prepsq cadr xargl,'epsilon}
	 else if sub eq 'ofsf_qesubcqpe then
	    {'plus,prepsq cadr xargl,'epsilon}
	 else if sub eq 'ofsf_qesubcrme1 then
	    {'difference,ofsf_preprexpr(cadr xargl),'epsilon}
	 else if sub eq 'ofsf_qesubcrpe1 then
	    {'plus,ofsf_preprexpr(cadr xargl),'epsilon}
	 else
	    rederr "BUG IN ofsf_qemkans";
	 {{'equal,v,w},atr}
      >>
   end;

procedure ofsf_qebacksub(eql);
   % Quantifier elimination back substitution. [eql] is a list
   % $((e,a),...)$, where $e$ is an equation and $a$ is an answer
   % translation. Returns a list of the same form.
   begin scalar subl,rhs,ioe,atr,e; integer ic,ec;
      return for each w in eql collect <<
	 e := car w;
	 atr := cadr w;
	 rhs := simp caddr e;
	 if smemq('infinity,rhs) then <<
	    ic := ic+1;
	    ioe := mkid('infinity,ic);
	    rhs := subsq(rhs,{'infinity . ioe})
	 >>;
	 if smemq('epsilon,rhs) then <<
	    ec := ec+1;
	    ioe := mkid('epsilon,ec);
	    flag({ioe},'constant);
	    put(ioe,'!:rd!:,'rdzero!*);
	    rhs := subsq(rhs,{'epsilon . ioe})
	 >>;
	 e := {'equal,cadr e,prepsq subsq(rhs,subl)};
	 subl := (cadr e . caddr e) . subl;
	 {e,atr}
      >>
   end;

procedure ofsf_qeapplyatr(eql);
   % Ordered field standard form quantifier elimination apply answer
   % translation. [eql] is a list $((e,a),...)$, where $e$ is an
   % equation and $a$ is an answer translation. Returns a list of
   % equations.
   begin scalar rhs,atr,pow,eqn;
      return for each w in eql collect <<
	 eqn := car w;
	 rhs := caddr eqn;
	 atr := cadr w;
	 if null atr then
	    eqn
	 else <<
	    pow := lto_catsoc(cadr eqn,atr) or 1;
	    {'equal,cadr eqn,ofsf_croot(rhs,pow)}
      	 >>
      >>
   end;

procedure ofsf_croot(u,n);
   if null n then u else reval {'expt,u,{'quotient,1,n}};

procedure ofsf_preprexpr(r);
   {'quotient,{'plus,prepf car r,{'times,prepf cadr r,{'sqrt,prepf caddr r}}},
      prepf cadddr r};

procedure ofsf_decdeg(f);
   % Ordered field standard form decrease degrees. [f] is a formula.
   % Returns a formula equivalent to [f], hopefully decreasing the
   % degrees of the bound variables.
   ofsf_decdeg0 cl_rename!-vars f;

procedure ofsf_decdeg0(f);
   begin scalar op,w,gamma,newmat;
      op := rl_op f;
      if rl_boolp op then
	 return rl_mkn(op,for each subf in rl_argn f collect
   	    ofsf_decdeg0 subf);
      if rl_quap op then <<
	 w := ofsf_decdeg1(ofsf_decdeg0 rl_mat f,{rl_var f});
	 newmat := if null cdr w or not evenp cdr car cdr w then
	    car w
	 else <<
	    gamma := ofsf_0mk2('geq,numr simp car car cdr w);
	    rl_mkn(if op eq 'ex then 'and else 'impl,{gamma,car w})
	 >>;
	 return rl_mkq(op,rl_var f,newmat)
      >>;
      % [f] is not complex.
      return f
   end;

procedure ofsf_decdeg1(f,vl);
   % Ordered field standard form decremet degrees. [f] is a formula;
   % [vl] is a list of variables $v$ such that $v$ does not occur
   % boundly in [f], or ['fvarl]. Returns a pair $(\phi . l)$; $\phi$
   % is a formula, and $l$ is a list of pairs $(v . d)$ where $v$ in
   % [vl] and $d$ is an integer. We have $\exists [vl] [f]$ equivalent
   % to $\exists [vl] (\phi \land \bigwedge_{(v . d) \in [vl]}(v^d
   % \geq 0))$, where $\phi$ is obtained from [f] by substituting $v$
   % for $v^d$ for each $(v . d)$ in $l$. ['fvarl] stands for the list
   % of all free variables in [f].
   begin scalar dvl; integer n;
      if vl eq 'fvarl then
	 vl := cl_fvarl1 f;
      for each v in vl do <<
	 n := ofsf_decdeg2(f,v);
	 if n>1 then <<
	    f := ofsf_decdeg3(f,v,n);
	    dvl := (v . n) . dvl
	 >>
      >>;
      return f . dvl
   end;

procedure ofsf_decdeg2(f,v);
   % Ordered field standard form decrement degree subroutine. [f] is a
   % formula; [v] is a variable. Returns an INTEGER $n$. The degree of [v]
   % in [f] can be decremented using the substitution $[v]^n=v$.
   begin scalar a,w,atl,dgcd,!*gcd,oddp;
      !*gcd := T;
      atl := cl_atl1 f;
      dgcd := 0;
      while atl and dgcd neq 1 do <<
	 a := car atl;
	 atl := cdr atl;
	 w := ofsf_ignshift(a,v);
	 if w eq 'odd and null oddp then
	    oddp := 'odd
	 else if null w then <<
	    a := sfto_reorder(ofsf_arg2l a,v);
	    while (not domainp a) and (mvar a eq v) and dgcd neq 1 do <<
	       dgcd := gcdf(dgcd,ldeg a);
	       a := red a
	    >>
      	 >>;
	 if dgcd > 0 and oddp eq 'odd then <<
	    oddp := T;
	    while w := quotf(dgcd,2) do
	       dgcd := w
	 >>
      >>;
      if dgcd = 0 then
	 return 1;
      return dgcd
   end;

procedure ofsf_transform(f,v);
   % Ordered field standard form transform formula. [f] is a
   % quantifier-free formula; [v] is a variable. Returns a pair $(\phi
   % . a)$. $\phi$ is a formula such that $\exists [v]([f])$ is
   % equivalent to $\exists [v](\phi)$. $a$ is either [nil] or a pair
   % $([v] . d)$. If $a$ is not [nil] then the degree $d'$ of [v] in
   % [f] is reduced to $d'/d$. If $a$ is nil then $[f]=\phi$.
   begin scalar dgcd;
      dgcd := ofsf_decdeg2(f,v);
      if dgcd = 1 then
	 return f . nil;
      if !*rlverbose then ioto_prin2 {"(",v,"^",dgcd,")"};
      f := ofsf_decdeg3(f,v,dgcd);
      if evenp dgcd then
	 f := rl_mkn('and,{ofsf_0mk2('geq,numr simp v),f});
      return f . (v . dgcd)
   end;

procedure ofsf_ignshift(at,v);
   % Orderd field standard form ignore shift. [at] is an atomic
   % formula; [v] is a variable. Returns [nil], ['ignore], or ['odd].
   begin scalar w;
      w := sfto_reorder(ofsf_arg2l at,v);
      if not domainp w and null red w and mvar w eq v then
	 if ofsf_op at memq '(equal neq) or evenp ldeg w then
	    return 'ignore
	 else
	    return 'odd
   end;

procedure ofsf_decdeg3(f,v,n);
   % Ordered field standard form decrement degree. [f] is a formula;
   % [v] is a variable; [n] is an integer. Returns a formula.
   cl_apply2ats1(f,'ofsf_decdegat,{v,n});

procedure ofsf_decdegat(atf,v,n);
   % Ordered field standard form decrement degree atomic formula. [f]
   % is an atomic formula; [v] is a variable; [n] is an integer. Returns
   % an atomic formula.
   if ofsf_ignshift(atf,v) then
      atf
   else
      ofsf_0mk2(ofsf_op atf,sfto_decdegf(ofsf_arg2l atf,v,n));

procedure ofsf_updatr(atr,upd);
   % Ordered field standard form update answer translation. [atr] is
   % an answer translation; [upd] is information which has to be added
   % to [atr]. Returns an answer translation.
   upd . atr;

procedure ofsf_thsimpl(atl);
   % Ordered field standard form theory simplification. [atl] is a
   % theory. Returns an equivalent theory. The returned theory is
   % hopefully somehow simpler than the original one.
   begin scalar !*rlsiexpla,!*rlsipo;
      !*rlsiexpla := T;
      return sort(ofsf_thregen cl_simpl(rl_smkn('and,atl),nil,-1),'rl_ordatp)
   end;

procedure ofsf_thregen(f);
   % Ordered field standard form re-generate theory. [f] is a formula.
   % Returns a possibly empty list of atomic formulas equivalent to
   % [f] or the list [{'false}] if [f] is recognized as a
   % contradiction.
   begin scalar op;
      op := rl_op f;
      if op = 'and then
 	 return for each x in rl_argn f collect ofsf_thregen!-or x;
      if op = 'or then
	 return {ofsf_thregen!-or f};
      if op = 'true then
	 return nil;
      if op = 'false then
	 {'false};
      % [f] is atomic.
      return {f}
   end;

procedure ofsf_thregen!-and(f);
   % Ordered field standard form re-generate theory conjunction case.
   % [f] is a conjunction. Returns an atomic formula equivalent to
   % [f].
   cl_nnfnot ofsf_thregen!-or cl_nnfnot f;

procedure ofsf_thregen!-or(f);
   % Ordered field standard form re-generate theory disjunction case.
   % [f] is a disjunction. Returns an atomic formula equivalent to
   % [f].
   begin scalar w;
      if cl_atfp f then
	 return f;
      w := car rl_argn f;
      if rl_op w = 'and then
	 w := ofsf_thregen!-and w;
      if rl_op w = 'equal then
      	 return ofsf_thregen!-equal(w . cdr rl_argn f);
      if rl_op w = 'neq then
      	 return ofsf_thregen!-neq(w . cdr rl_argn f);
      rederr "BUG IN ofsf_thregen!-or"
   end;

procedure ofsf_thregen!-equal(eql);
   % Ordered field standard form re-generate theory equality
   % disjunction case. [eql] is a list of equations or complex
   % formulas which can be contracted to one equation. The list is
   % considered disjunctive. Returns an atomic formula equivalent to
   % $\bigvee [eql]$ constructed by multiplication of the left hand
   % sides.
   begin scalar w;
      w := 1;
      for each x in eql do <<
	 if rl_op x = 'and then
	    x := ofsf_thregen!-and x;
	 if rl_op x neq 'equal then
            rederr "BUG IN ofsf_thregen!-equal";
	 w := multf(w,ofsf_arg2l x)
      >>;
      return ofsf_0mk2('equal,w)
   end;

procedure ofsf_thregen!-neq(neql);
   % Ordered field standard form re-generate theory [neq] disjunction
   % case. [neql] is a list of inequalities or complex formulas which
   % can be contracted to one inequality. The list is considered
   % disjunctive. Returns an atomic formula equivalent to $\bigvee
   % [neql]$ constructed by addition of the squares of the left hand
   % sides.
   begin scalar w;
      for each x in neql do <<
	 if rl_op x = 'and then
	    x := ofsf_thregen!-and x;
	 if rl_op x neq 'neq then
            rederr "BUG IN ofsf_thregen!-neq";
	 w := addf(w,exptf(ofsf_arg2l x,2))
      >>;
      return ofsf_0mk2('neq,w)
   end;

procedure ofsf_specelim(f,vl,theo,ans,bvl);
   % Ordered field standard form special elimination.
   if (not !*rlqesqsc) or ans or !*rlqegen then
      'failed
   else
      ofsf_sqsc(f,vl,theo,ans,bvl);

procedure ofsf_sqsc(f,vl,theo,ans,bvl);
   % Ordered field standard form super quadratic special case.
   begin scalar w,atl,scvl,lin,a,at;
      atl := cl_atl1 f;
      scvl := if !*rlqevarsel then vl else {car vl};
      while scvl and not lin do <<
	 a := car scvl;
	 scvl := cdr scvl;
	 lin := ofsf_linp(atl,a,delq(a,vl))
      >>;
      if lin then
	 return 'failed;
      scvl := if !*rlqevarsel then vl else {car vl};
      while scvl and not at do <<
	 a := car scvl;
	 scvl := cdr scvl;
	 at := ofsf_sqsc!-test(atl,a)
      >>;
      if not at then
 	 return 'failed;
      if !*rlverbose then
	 ioto_prin2 "#Q";
      vl := delq(a,vl);
      f := cl_simpl(ofsf_sqsc1(f,at,a,theo),theo,-1);
      return (t . {cl_mkcoel(vl,f,nil,nil)}) . theo
   end;

procedure ofsf_sqsc1(f,at,v,theo);
   if cl_cxfp f then
      rl_mkn(rl_op f,for each x in rl_argn f collect ofsf_sqsc1(x,at,v,theo))
   else if f eq at then
      ofsf_sqsc1at(at,v,theo)
   else
      f;

procedure ofsf_sqsc1at(at,v,theo);
   begin scalar op,w,a,b,c,discr;
      op := ofsf_op at;
      w := ofsf_mktriple(sfto_reorder(ofsf_arg2l at,v));
      a := reorder car w;
      b := reorder cadr w;
      c := reorder caddr w;
      if op eq 'neq then
	 return rl_mkn('or,
	    {ofsf_0mk2('neq,a),ofsf_0mk2('neq,b),ofsf_0mk2('neq,c)});
      discr := addf(exptf(b,2),negf multf(4,multf(a,c)));
      if op eq 'equal then <<
	 if ofsf_surep(ofsf_0mk2('neq,a),theo) then
	    return ofsf_0mk2('geq,discr);
	 return rl_mkn('or,
	    {ofsf_0mk2('greaterp,discr),ofsf_0mk2('equal,c),
	       rl_mkn('and,{ofsf_0mk2('equal,discr),ofsf_0mk2('neq,b)})})
      >>;
      if op eq 'leq then <<
	 if ofsf_surep(ofsf_0mk2('greaterp,a),theo) then
	    return ofsf_0mk2('geq,discr);
	 return rl_mkn('or,
	    {ofsf_0mk2('lessp,a),ofsf_0mk2('leq,c),
	       rl_mkn('and,{ofsf_0mk2('geq,discr),ofsf_0mk2('neq,b)})})
      >>;
      if op eq 'geq then <<
	 if ofsf_surep(ofsf_0mk2('lessp,a),theo) then
	    return ofsf_0mk2('geq,discr);
	 return rl_mkn('or,
	    {ofsf_0mk2('greaterp,a),ofsf_0mk2('geq,c),
	       rl_mkn('and,{ofsf_0mk2('geq,discr),ofsf_0mk2('neq,b)})})
      >>;
      if op eq 'lessp then <<
	 if ofsf_surep(ofsf_0mk2('greaterp,a),theo) then
	    return ofsf_0mk2('greaterp,discr);
      	 return rl_mkn('or,{ofsf_0mk2('greaterp,discr),
	    ofsf_0mk2('lessp,a),ofsf_0mk2('lessp,c)})
      >>;
      if op eq 'greaterp then <<
	 if ofsf_surep(ofsf_0mk2('lessp,a),theo) then
	    return ofsf_0mk2('greaterp,discr);
      	 return rl_mkn('or,{ofsf_0mk2('greaterp,discr),
	    ofsf_0mk2('greaterp,a),ofsf_0mk2('greaterp,c)})
      >>;
      rederr {"ofsf_sqsc1at: unknown operator ",op}
   end;

procedure ofsf_sqsc!-test(atl,v);
   begin scalar hit,a,d;
      while atl do <<
	 a := car atl;
	 atl := cdr atl;
	 d := degreef(ofsf_arg2l a,v);
	 if d=1 then
	    atl := hit := nil
	 else if d=2 then
	    if hit then
	       atl := hit := nil
	    else
	       hit := a
      >>;
      return hit
   end;

endmodule;  % [ofsfqe]

end;  % of file