% ----------------------------------------------------------------------
% $Id: ofsf.red,v 1.24 1999/03/23 12:26:33 sturm Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: ofsf.red,v $
% Revision 1.24 1999/03/23 12:26:33 sturm
% Renamed switch rlsisqf to rlsiatadv.
%
% Revision 1.23 1999/03/23 07:40:16 dolzmann
% Changed copyright information.
% Added list of exported procedures and import list.
%
% Revision 1.22 1999/03/21 13:37:18 dolzmann
% Use cl_bnfsimpl instead of acfsf_bnfsimpl.
% Removed black box rl_zero.
%
% Revision 1.21 1999/03/18 14:08:20 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 1998/04/09 11:00:03 sturm
% Added switch rlqeqsc for quadratic special case. This now OFF by default!
%
% Revision 1.19 1997/08/24 16:18:50 sturm
% Added service rl_surep with black box rl_multsurep.
% Added service rl_siaddatl.
%
% Revision 1.18 1997/08/14 10:10:30 sturm
% Renamed rldecdeg to rldecdeg1.
% Added service rldecdeg.
%
% Revision 1.17 1997/08/13 12:44:38 dolzmann
% Introduced service rldecdeg.
%
% Revision 1.16 1996/10/23 11:24:48 dolzmann
% Added procedure ofsf_mkstrict.
%
% Revision 1.15 1996/10/20 15:54:57 sturm
% Added switches rlnzden, rlposden, and rladdcond and corresponding code
% handling the input of reciprocal terms.
%
% Revision 1.14 1996/10/17 13:52:07 sturm
% Introduced services rlvarl, rlfvarl, and rlbvarl. Renamed cl_varl to
% cl_varl1 for this.
%
% Revision 1.13 1996/10/14 16:03:08 sturm
% Declared !*rlqeheu fluid for the optimizer.
%
% Revision 1.12 1996/10/08 13:54:33 dolzmann
% Renamed "degree parity decomposition" to "parity decomposition".
% Adapted names of procedures and switches accordingly.
%
% Revision 1.11 1996/10/01 10:23:07 reiske
% Added ofsf services rlqews and rlqeipo.
% Introduced new service rltnf and related code.
%
% Revision 1.10 1996/09/30 16:55:30 sturm
% Switched to new tableau code.
%
% Revision 1.9 1996/09/29 14:22:57 sturm
% Introduced services rlqea and rlgqea.
%
% Revision 1.8 1996/09/26 11:48:55 dolzmann
% Do not use T as formal parameter.
%
% Revision 1.7 1996/09/05 11:14:46 dolzmann
% Introduced new switch !*rlqegenct.
% Using cl black box implementation for black box rl_trygauss.
% Introduced new black boxes rl_qefsolset, rl_bettergaussp!*, rl_bestgaussp,
% rl_esetunion, rl_structat, rl_ifstructat, and rl_termmlat.
% Introduced new services rl_ifacml, rl_struct, rl_ifstruct, rl_termml, and
% rl_terml.
% Added lost procedure ofsf_simpterm.
%
% Revision 1.6 1996/08/01 11:45:27 reiske
% Added services rl_natab, rl_nitab, and rl_gentheo.
% Added black boxes rl_a2cdl and rl_getineq.
%
% Revision 1.5 1996/07/13 11:09:33 dolzmann
% Introduced new switches !*rlgsbnf and !*rlgsutord.
% Using cl black box implementations for black boxes rl_smsimpl!-impl
% and rl_smsimpl!-equiv1.
%
% Revision 1.4 1996/07/07 14:38:14 sturm
% Introduced new service rl_nnfnot.
% Introduced new black box rl_eqnrhskernels.
%
% Revision 1.3 1996/05/21 17:14:07 sturm
% Added service rl_subfof and black boxes rl_subat, rl_subalchk.
%
% Revision 1.2 1996/05/12 08:27:19 sturm
% Loading rltools now.
% Introduced new switch rlsitsqspl.
% Introduced internal switch !*rlqegen.
% Removed context control for switch ezgcd.
% Introduced new services rl_thsimpl and rl_gqe.
%
% Revision 1.1 1996/03/22 12:13:59 sturm
% Moved and split.
%
% Revision 1.25 1996/03/18 15:46:31 sturm
% Moved switch defaults to module rl.
% Removed ofsf_enter, ofsf_exit, and ofsf_svezgcd!*. The ezgcd is treated
% as context switch now.
% Added service rl_atml.
% Removed properties ofsf_prepfn from the ofsf predicates.
% Removed properties "prepfnname", "prepdefault", "resimpfnname", and
% "resimpdefault" from "ofsf."
% Added property "rl_prepat" to "ofsf."
% Added procedures ofsf_prepat, ofsf_resimpat, ofsf_lengthat,
% Added service rl_atml.
% Removed procedure ofsf_tordp.
% Adapted black box implementation ofsf_fctrat: the content is dropped now.
%
% Revision 1.24 1996/03/11 13:19:23 reiske
% Added black box implementations ofsf_fctrat and ofsf_tordp.
%
% Revision 1.23 1996/03/10 13:03:49 sturm
% Added default setting for switch !*rlqeheu.
% Added service rl_matrix.
% Changed verbosity output in module ofsfqe.
% Removed Gauss code that was commented out previously.
%
% Revision 1.22 1996/03/10 12:48:54 dolzmann
% Set services rl_dnf to ofsf_dnf and rl_cnf to ofsf_cnf respectively.
% Added procedures ofsf_dnf, ofsf_cnf. These procedures call
% cl_cnf/cl_cnf with !*rlsiso on where necessary.
% Introduced new switch !*rlgsvb and corresponding code. Groebner
% simplifier gives verbosity output only with both !*rlverbose and
% !*rlgsvb on.
%
% Revision 1.21 1996/03/09 13:36:02 sturm
% Added switch rlqesr and corresponding code.
% Renamed constructors:
% ofsf_constr2 -> ofsf_mk2
% ofsf_0constr2 -> ofsf_0mk2
% ofsf_constrn -> ofsf_mkn
% Changes in module ofsfqe:
% Added procedures ofsf_qesubcr1, ofsf_qesubcrpe1 and ofsf_qesubcrme1.
% Added parameter "ans" to procedures ofsf_translat, ofsf_trygauss, and
% ofsf_findeqsol.
% Fixed a bug in (former) ofsf_qemkans.
% Added procedures ofsf_qemkans1 and ofsf_qebacksub for answer
% back-substitution.
%
% Revision 1.20 1996/03/04 17:11:41 sturm
% Added ofsf_enter, ofsf_exit, and fluid ofsf_svezgcd!* for turning on
% ezgcd while in ofsf context.
% Added black box implementations ofsf_transform, ofsf_updatr.
% Fixed a bug in ofsf_qscp.
% Added detection of formulas that are linear after factorization to
% ofsf_varsel. The same for quadratic formulas.
% Added handling of answer transformations to ofsf_qemkans.
% Moved ofsf_reorder to module sfto.
%
% Revision 1.19 1996/03/04 13:09:19 dolzmann
% Removed loading of groebner packages.
% Added switch !*rlbnfsac.
% Added black box implementations ofsf_bnfsimpl, ofsf_sacat, ofsf_sacatlp.
% New module ofsf_bnf. Moved code for bnf computation from ofsf_below to
% ofsf_bnf.
% Turned off !*rlsiexpla with groebner simplifier
% Moved procedures gs_groebnerf, gs_preducef, gs_greducef to module sfto.
% Moved procedure ofsf_gsatlp to module cl.
%
% Revision 1.18 1996/02/28 13:15:24 sturm
% Added quadratic special case detection to ofsf_varsel.
% Fixed bugs in elimination set computation.
%
% Revision 1.17 1996/02/26 12:46:51 sturm
% Started the implementation of a proper ofsf_varsel.
% Added factorization to the ofsf_translat and ofsf_trygauss black box
% implementations. Degree violations are communicated to the module cl
% now.
% Fixed a bug in ofsf_elimsetscl.
% Removed treatment of ...2q keys from the elimination set computation.
%
% Revision 1.16 1996/02/18 15:55:14 sturm
% Turned rlsiexpla on by default.
%
% Revision 1.15 1996/02/18 14:27:58 sturm
% Updated export list.
% Added factorization to ofsf_simplequal and ofsf_simplneq. Added
% corresponding switch !*rlsifac.
% Removed switch !*rlsdnf.
% Added black box implementation ofsf_trygauss.
% Changed default settings for the switches !*rlqedfs and !*rlsimpl.
% Added service rlatl.
% Added procedures ofsf_rotrel, ofsf_crotrel, and ofsf_reorder.
% Moved ofsf_splitterm and ofsf_mksol from module ofsfqe to
% ofsf_optsplitterm and ofsf_optmksol resp. in module ofsfopt.
% Rewritten module ofsfqe. Implemented quadratic elimination. This module
% is under development.
%
% Revision 1.14 1996/02/18 12:46:07 dolzmann
% Added default value for switch !*rlgserf.
% Rewritten module ofsfgs.
%
% Revision 1.13 1995/11/16 08:06:36 sturm
% Added default setting for switch rlsimpl.
%
% Revision 1.12 1995/10/18 08:53:05 sturm
% Added switches rlbnfsb, rlbnfsm, parameter rlsubsumption!*, and
% respective code.
% Bug fix: atomic formulas are made unique in ofsf_entry2at now.
% Made ofsf_gsd use DNF computation.
%
% Revision 1.11 1995/09/05 08:05:15 sturm
% Reimplemented parts of smart simplification. Added switches rlsipo,
% rlsipw; fixed a bug in smart simplification of impl.
% Modified procedure ofsf_esaord: improved substitution, added switch
% rlqesdnf.
%
% Revision 1.10 1995/08/31 08:40:47 sturm
% Added RTYPEFN property to all relations except equal.
%
% Revision 1.9 1995/08/30 08:09:15 sturm
% Moved interface code to file rlsf and adapted the tag properties.
% Fixed a bug: renamed cl_smsimpl!-equiv to ofsf_smsimpl!-equiv1.
% Major changes in module ofsfopt:
% Added BFS option to ofsf_opt2 using switch rlqedfs.
% Changed return protocol in ofsf_opt2.
% Added elimination set computation wrt. "z". Code contains some
% experimental switches.
% Added counting of tree nodes with verbose output.
%
% Revision 1.8 1995/08/08 10:18:18 sturm
% Added smart simplification code for impl and equiv.
% Adapted calls to cl_simpl to the new knowl argument.
%
% Revision 1.7 1995/08/03 05:39:06 dolzmann
% Added procedures ofsf_gsn, ofsf_gsatlp.
%
% Revision 1.6 1995/08/02 08:19:08 sturm
% Split module ofsfsimpl into ofsfsimplat and ofsfsmsimpl. Rewritten
% smart simplification code.
% Minor changes in module ofsfgs; fixed term ordering to REVGRADLEX.
% Changed copyright messages.
%
% Revision 1.5 1995/07/12 15:08:54 sturm
% Added procedure ofsf_optsubstat to module ofsfopt.
% Added procedures ofsf_ordatp and ofsf_ordrelp.
% Set service rl_identifyonoff to cl_identifyonoff.
%
% Revision 1.4 1995/07/07 11:12:25 sturm
% Removed remflag statement for load!-package.
% Removed "_" in switch names.
% Added export statement.
% Added switch rlopt1s.
% Added procedures ofsf_qemkans (parameter function), ofsf_simpterm,
% ofsf_prepterm, and ofsf_mkterm.
% Added comments.
% Changes in module ofsfopt.
% Renamed Groebner simplifiers: ofsf_gbcsimpl to ofsf_gsc and
% ofsf_gbdsimpl to ofsf_gsd.
% Changed verbosity output, ioto is used now.
%
% Revision 1.3 1995/06/21 10:42:02 sturm
% Removed declarations of non-used local variables.
% Turned on switch rl_tabib by default.
% Updated create!-package commented it out.
% Many changes in module ofsfqe.
% Added smart simplification code in module ofsfsimpl; ofsf_simpl1 is
% used instead of of_simpl1 now.
% Added module ofsfopt.
%
% Revision 1.2 1995/06/01 13:54:04 dolzmann
% Added switch rl_verbose.
% Fixed bugs in ofsf_simplleq and ofsf_simplgreaterp.
% Added module ofsfgs containing a Groebner simplifier. Parts of the
% interface have already been part of the previous revision.
%
% Revision 1.1 1995/05/29 14:47:21 sturm
% Initial check-in.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(ofsf_rcsid!* ofsf_copyright!*);
ofsf_rcsid!* := "$Id: ofsf.red,v 1.24 1999/03/23 12:26:33 sturm Exp $";
ofsf_copyright!* := "Copyright (c) 1995-1999 by A. Dolzmann and T. Sturm"
>>;
module ofsf;
% Ordered field standard form. Main module. Algorithms on first-order
% formulas over ordered fields. The language contains binary relations
% ['equal], ['neq], ['greaterp], ['lessp], ['geq], ['leq].
create!-package('(ofsf ofsfsiat ofsfsism ofsfbnf ofsfqe ofsfopt ofsfgs
ofsfmisc),nil);
load!-package 'cl;
load!-package 'rltools;
exports ofsf_simpterm,ofsf_prepat,ofsf_resimpat,ofsf_lengthat,ofsf_chsimpat,
ofsf_simpat,ofsf_op,ofsf_arg2l,ofsf_arg2r,ofsf_argn,ofsf_mk2,ofsf_0mk2,
ofsf_mkn,ofsf_opp,ofsf_mkstrict,ofsf_simplat1,ofsf_smrmknowl,ofsf_smcpknowl,
ofsf_smupdknowl,ofsf_smmkatl,ofsf_dnf,ofsf_cnf,ofsf_subsumption,
ofsf_sacatlp,ofsf_sacat,ofsf_varsel,ofsf_qesubcr1,ofsf_qesubcr2,ofsf_qesubr,
ofsf_qesubcq,ofsf_qesubq,ofsf_qesubi,ofsf_qesubcrpe1,ofsf_qesubcrme1,
ofsf_qesubcrpe2,ofsf_qesubcrme2,ofsf_qesubrpe,ofsf_qesubrme,ofsf_qesubcqpe,
ofsf_qesubcqme,ofsf_qesubqpe,ofsf_qesubqme,ofsf_valassp,ofsf_translat,
ofsf_surep,ofsf_elimset,ofsf_bettergaussp,ofsf_esetunion,ofsf_bestgaussp,
ofsf_qefsolset,ofsf_qemkans,ofsf_preprexpr,ofsf_decdeg,ofsf_decdeg1,
ofsf_transform,ofsf_updatr,ofsf_thsimpl,ofsf_specelim,ofsf_opt,ofsf_gsn,
ofsf_gsc,ofsf_gsd,ofsf_gssimplify,ofsf_gssimplify0,ofsf_termprint,
ofsf_canegrel,ofsf_anegrel,ofsf_clnegrel,ofsf_lnegrel,ofsf_fctrat,
ofsf_negateat,ofsf_varlat,ofsf_varsubstat,ofsf_ordatp,ofsf_ordrelp,
ofsf_a2cdl,ofsf_t2cdl,ofsf_subat,ofsf_subalchk,ofsf_eqnrhskernels,
ofsf_getineq,ofsf_structat,ofsf_ifstructat,ofsf_termmlat,ofsf_multsurep;
imports cl,rltools;
fluid '(!*rlsiatadv !*rlsipd !*rlsiexpl !*rlsiexpla !*rlgssub !*rlsiso !*rlqesr
!*rlgsrad !*rlgsred !*rlgsprod !*rlgserf !*rlverbose !*rlqedfs !*rlsipw
!*rlsipo !*rlparallel !*rlopt1s !*rlsifac !*rlbnfsac !*rlgsvb !*rlqegen
!*rlsitsqspl !*rlgsbnf !*rlgsutord !*rlqegenct !*rlqeheu !*rlnzden
!*rlposden !*rladdcond !*rlqeqsc !*rlqesqsc !*rlsusi);
flag('(ofsf),'rl_package);
% Parameters
put('ofsf,'rl_params,'(
(rl_subat!* . ofsf_subat)
(rl_subalchk!* . ofsf_subalchk)
(rl_eqnrhskernels!* . ofsf_eqnrhskernels)
(rl_ordatp!* . ofsf_ordatp)
(rl_qemkans!* . ofsf_qemkans)
(rl_simplat1!* . ofsf_simplat1)
(rl_smupdknowl!* . ofsf_smupdknowl)
(rl_smrmknowl!* . ofsf_smrmknowl)
(rl_smcpknowl!* . ofsf_smcpknowl)
(rl_smmkatl!* . ofsf_smmkatl)
(rl_smsimpl!-impl!* . cl_smsimpl!-impl)
(rl_smsimpl!-equiv1!* . cl_smsimpl!-equiv1)
(rl_negateat!* . ofsf_negateat)
(rl_varlat!* . ofsf_varlat)
(rl_varsubstat!* . ofsf_varsubstat)
(rl_translat!* . ofsf_translat)
(rl_elimset!*. ofsf_elimset)
(rl_trygauss!* . cl_trygauss)
(rl_varsel!* . ofsf_varsel)
(rl_subsumption!* . ofsf_subsumption)
(rl_bnfsimpl!* . cl_bnfsimpl)
(rl_sacat!* . ofsf_sacat)
(rl_sacatlp!* . ofsf_sacatlp)
(rl_fctrat!* . ofsf_fctrat)
(rl_tordp!* . ordp)
(rl_transform!* . ofsf_transform)
(rl_updatr!* . ofsf_updatr)
(rl_a2cdl!* . ofsf_a2cdl)
(rl_t2cdl!* . ofsf_t2cdl)
(rl_getineq!* . ofsf_getineq)
(rl_qefsolset!* . ofsf_qefsolset)
(rl_bettergaussp!* . ofsf_bettergaussp)
(rl_bestgaussp!* . ofsf_bestgaussp)
(rl_esetunion!* . ofsf_esetunion)
(rl_structat!* . ofsf_structat)
(rl_ifstructat!* . ofsf_ifstructat)
(rl_termmlat!* . ofsf_termmlat)
(rl_multsurep!* . ofsf_multsurep)
(rl_specelim!* . ofsf_specelim)));
% Services
put('ofsf,'rl_services,'(
(rl_subfof!* . cl_subfof)
(rl_identifyonoff!* . cl_identifyonoff)
(rl_simpl!* . cl_simpl)
(rl_thsimpl!* . ofsf_thsimpl)
(rl_nnf!* . cl_nnf)
(rl_nnfnot!* . cl_nnfnot)
(rl_pnf!* . cl_pnf)
(rl_cnf!* . ofsf_cnf)
(rl_dnf!* . ofsf_dnf)
(rl_all!* . cl_all)
(rl_ex!* . cl_ex)
(rl_atnum!* . cl_atnum)
(rl_tab!* . cl_tab)
(rl_atab!* . cl_atab)
(rl_itab!* . cl_itab)
(rl_gsc!* . ofsf_gsc)
(rl_gsd!* . ofsf_gsd)
(rl_gsn!* . ofsf_gsn)
(rl_qe!* . cl_qe)
(rl_qea!* . cl_qea)
(rl_gqe!* . cl_gqe)
(rl_gqea!* . cl_gqea)
(rl_qeipo!* . cl_qeipo)
(rl_qews!* . cl_qews)
(rl_opt!* . ofsf_opt)
(rl_ifacl!* . cl_ifacl)
(rl_ifacml!* . cl_ifacml)
(rl_matrix!* . cl_matrix)
(rl_apnf!* . cl_apnf)
(rl_atml!* . cl_atml)
(rl_tnf!* . cl_tnf)
(rl_atl!* . cl_atl)
(rl_struct!* . cl_struct)
(rl_ifstruct!* . cl_ifstruct)
(rl_termml!* . cl_termml)
(rl_terml!* . cl_terml)
(rl_varl!* . cl_varl)
(rl_fvarl!* . cl_fvarl)
(rl_bvarl!* . cl_bvarl)
(rl_gentheo!* . cl_gentheo)
(rl_decdeg!* . ofsf_decdeg)
(rl_decdeg1!* . ofsf_decdeg1)
(rl_surep!* . cl_surep)
(rl_siaddatl!* . cl_siaddatl)));
% Admin
put('ofsf,'simpfnname,'ofsf_simpfn);
put('ofsf,'simpdefault,'ofsf_simprel);
put('ofsf,'rl_prepat,'ofsf_prepat);
put('ofsf,'rl_resimpat,'ofsf_resimpat);
put('ofsf,'rl_lengthat,'ofsf_lengthat);
put('ofsf,'rl_prepterm,'prepf);
put('ofsf,'rl_simpterm,'ofsf_simpterm);
algebraic infix equal;
put('equal,'ofsf_simpfn,'ofsf_chsimpat);
put('equal,'number!-of!-args,2);
algebraic infix neq;
put('neq,'ofsf_simpfn,'ofsf_chsimpat);
put('neq,'number!-of!-args,2);
put('neq,'rtypefn,'quotelog);
newtok '((!< !>) neq);
algebraic infix leq;
put('leq,'ofsf_simpfn,'ofsf_chsimpat);
put('leq,'number!-of!-args,2);
put('leq,'rtypefn,'quotelog);
algebraic infix geq;
put('geq,'ofsf_simpfn,'ofsf_chsimpat);
put('geq,'number!-of!-args,2);
put('geq,'rtypefn,'quotelog);
algebraic infix lessp;
put('lessp,'ofsf_simpfn,'ofsf_chsimpat);
put('lessp,'number!-of!-args,2);
put('lessp,'rtypefn,'quotelog);
algebraic infix greaterp;
put('greaterp,'ofsf_simpfn,'ofsf_chsimpat);
put('greaterp,'number!-of!-args,2);
put('greaterp,'rtypefn,'quotelog);
flag('(equal neq leq geq lessp greaterp),'spaced);
flag('(ofsf_chsimpat),'full);
procedure ofsf_simpterm(u);
numr simp u;
procedure ofsf_prepat(f);
{ofsf_op f,prepf ofsf_arg2l f,prepf ofsf_arg2r f};
procedure ofsf_resimpat(f);
ofsf_mk2(ofsf_op f,
numr resimp !*f2q ofsf_arg2l f,numr resimp !*f2q ofsf_arg2r f);
procedure ofsf_lengthat(f);
2;
procedure ofsf_chsimpat(u);
rl_smkn('and,for each x in ofsf_chsimpat1 u collect ofsf_simpat x);
procedure ofsf_chsimpat1(u);
begin scalar leftl,rightl,lhs,rhs;
lhs := cadr u;
if pairp lhs and ofsf_opp car lhs then <<
leftl := ofsf_chsimpat1 lhs;
lhs := caddr lastcar leftl
>>;
rhs := caddr u;
if pairp rhs and ofsf_opp car rhs then <<
rightl := ofsf_chsimpat1 rhs;
rhs := cadr car rightl
>>;
return nconc(leftl,{car u,lhs,rhs} . rightl)
end;
procedure ofsf_simpat(u);
% Ordered field simp atomic formula. [u] is Lisp prefix. Returns an
% atomic formula.
begin scalar op,lhs,rhs,nlhs,f;
op := car u;
lhs := simp cadr u;
if not (!*rlnzden or !*rlposden or (domainp denr lhs)) then
typerr(u,"atomic formula");
rhs := simp caddr u;
if not (!*rlnzden or !*rlposden or (domainp denr rhs)) then
typerr(u,"atomic formula");
lhs := subtrsq(lhs,rhs);
nlhs := numr lhs;
if !*rlposden and not domainp denr lhs then <<
f := ofsf_0mk2(op,nlhs);
if !*rladdcond then
f := if op memq '(lessp leq greaterp geq) then
rl_mkn('and,{ofsf_0mk2('greaterp,denr lhs),f})
else
rl_mkn('and,{ofsf_0mk2('neq,denr lhs),f});
return f
>>;
if !*rlnzden and not domainp denr lhs then <<
if op memq '(lessp leq greaterp geq) then
nlhs := multf(nlhs,denr lhs);
f := ofsf_0mk2(op,nlhs);
if !*rladdcond then
f := rl_mkn('and,{ofsf_0mk2('neq,denr lhs),f});
return f
>>;
return ofsf_0mk2(op,nlhs)
end;
procedure ofsf_op(atf);
% Ordered field operator. [atf] is an atomic formula
% $R(t_1,t_2)$. Returns $R$.
car atf;
procedure ofsf_arg2l(atf);
% Ordered field binary operator left hand side argument. [atf] is
% an atomic formula $R(t_1,t_2)$. Returns $t_1$.
cadr atf;
procedure ofsf_arg2r(atf);
% Ordered field binary operator right hand side argument. [atf] is
% an atomic formula $R(t_1,t_2)$. Returns $t_2$.
caddr atf;
procedure ofsf_argn(atf);
% Ordered field binary operator right hand side argument. [atf] is
% an atomic formula $R(t_1,t_2)$. Returns the list $(t_1,t_2)$.
{cadr atf,caddr atf};
procedure ofsf_mk2(op,lhs,rhs);
% Ordered field constructor for binary operator. [op] is a relation
% [lhs] and [rhs] are terms. Returns the atomic formula
% $[op]([lhs],[rhs])$.
{op,lhs,rhs};
procedure ofsf_0mk2(op,lhs);
% Ordered field zero constructor for binary operator. [op] is a
% relation [lhs] is a term. Returns the atomic formula
% $[op]([lhs],0)$.
{op,lhs,nil};
procedure ofsf_mkn(op,argl);
% Ordered field constructor for binary operator. [op] is a relation
% [argl] is a list $(t_1,t_2)$ of terms. Returns the atomic formula
% $[op](t_1,t_2)$.
{op,car argl,cadr argl};
procedure ofsf_opp(op);
% Orderd field standard form operator predicate. [op] is an
% S-expression. Returns [nil] if op is not a relation.
op memq '(lessp leq equal neq geq greaterp);
procedure ofsf_mkstrict(r);
% Ordered field standard form make strict. [r] is an ordering
% relation. Returns the strict part of [r].
if r eq 'leq then 'lessp else if r eq 'geq then 'greaterp else r;
endmodule; % [ofsf]
end; % of file