% ----------------------------------------------------------------------
% $Id: pasfsism.red,v 1.11 2004/02/22 21:08:15 lasaruk Exp $
% ----------------------------------------------------------------------
% Copyright (c) 2003 Andreas Dolzmann and Andreas Seidl
% ----------------------------------------------------------------------
% $Log: pasfsism.red,v $
% Revision 1.11 2004/02/22 21:08:15 lasaruk
% Added switch rlsusisubst for substitution of equalities. Substitution
% results in smaller formulas or formulas with less free variables.
% Up to 80% length reduction. Switch rlsusitr should not be used yet.
%
% Revision 1.10 2003/12/16 10:19:58 dolzmann
% Removed wrong return values of pasf_susibinad. Added code for
% substituting equations into atomic formulas occuring in the theory.
%
% Revision 1.9 2003/12/16 07:45:34 lasaruk
% Redlog normal form in the simplifier.
%
% Revision 1.8 2003/12/11 10:51:19 lasaruk
% Smart simplification improoved.
%
% Revision 1.7 2003/12/02 09:04:06 dolzmann
% Removed parser error.
%
% Revision 1.6 2003/12/02 07:43:08 lasaruk
% Additive smart simplification added.
%
% Revision 1.5 2003/11/28 09:36:54 sturm
% Fixes in pasf_susibineq: do nothing for congrunces with different moduli.
% Exchanged T with nil at two points.
%
% Revision 1.4 2003/11/28 09:11:11 dolzmann
% Inserted a linebreak after rcsid!*.
%
% Revision 1.3 2003/11/27 19:30:40 lasaruk
% Smart simplification added
%
% Revision 1.2 2003/11/05 13:27:14 lasaruk
% Some major redlog programming rules applied to the code.
% Formulas are made positive acc. to the current kernel order.
%
% Revision 1.1 2003/07/22 12:42:59 seidl
% Smart simplification with theory based on susi started.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(pasf_sism_rcsid!* pasf_sism_copyright!*);
pasf_sism_rcsid!* :=
"$Id: pasfsism.red,v 1.11 2004/02/22 21:08:15 lasaruk Exp $";
pasf_sism_copyright!* :=
"Copyright (c) 2003 by A. Dolzmann. A. Seidl and T. Sturm"
>>;
module pasfsism;
% PASF smart simplification. Submodule of [pasf].
procedure pasf_smwupdknowl(op,atl,knowl,n);
% Presburger arithmetic standard form update knowledge. [op] is an
% operator; [atl] is the list of atomic formulas to add to the
% knowledge; [knowl] is a knowledge; [n] is the level. Returns
% modified knowledge.
if !*rlsusi then
cl_susiupdknowl(op,atl,knowl,n)
else
cl_smupdknowl(op,atl,knowl,n);
procedure pasf_smwrmknowl(knowl,v);
% Presburger arithmetic standard form remove variable from the
% knowledge. [knowl] is a knowledge; [v] is the variable to
% remove. Returns modified knowledge.
if !*rlsusi then
pasf_susirmknowl(knowl,v)
else
cl_smrmknowl(knowl,v);
procedure pasf_smwcpknowl(knowl);
% Presburger arithmetic standard form copy knowledge. [knowl] is a
% knowledge. Returns a copy of the knowledge.
if !*rlsusi then
cl_susicpknowl(knowl)
else
cl_smcpknowl(knowl);
procedure pasf_smwmkatl(op,knowl,newknowl,n);
% Presburger arithmetic standard form ...?
if !*rlsusi then
cl_susimkatl(op,knowl,newknowl,n)
else
cl_smmkatl(op,knowl,newknowl,n);
procedure pasf_susirmknowl(knowl,v);
% Presburger arithmetic standard form remove knowledge. [knowl] is
% a KNOWL; [v] is a variable. Returns a KNOWL. Remove all
% information about [v] from [knowl].
for each p in knowl join
if v memq pasf_varlat car p then nil else {p};
procedure pasf_susibin(old,new);
% Presburger arithmetic standard form susi binary smart
% simplification. [old] and [new] are LAT's. Returns ['false] or a
% SUSIPRG. We assume that [old] is a part of a already existence
% KNOWL and new has to be added to this KNOWL.
begin scalar x,rm;
% Do not make conclusion simplification
if cdr old eq 'ignore and cdr new eq 'ignore then
return nil;
x := pasf_susibinad(old,new);
% print "-----------------------";
% mathprint rl_mk!*fof car old;
% print cdr old;
% mathprint rl_mk!*fof car new;
% print cdr old;
% print "sisibin->ouput";
% print x;
if x and listp x and
(cdr new eq 'ignore or cdr old eq 'ignore) and
not cdr x and caar x eq 'delete then <<
print x;
% Abort replacing theory with conclusions
return nil
>>
else
return x
end;
procedure pasf_susibinad(old,new);
% Presburger standard form additive smart simplification. [old] is
% the old atomic formula in the theory; [new] is the new atomic
% formula found. Returns a susiprog that simplifies the formula.
begin scalar od,nd,level,atf,olevel,res;
level := cl_susiminlevel(cdr old,cdr new);
olevel := cdr old;
old := car old;
new := car new;
% Check for possible substitution
if !*rlsusisubst and
(pasf_opn old eq 'equal or pasf_opn new eq 'equal) then <<
res := pasf_susibinsubst(old,new,level);
if res then
return res
>>;
% Equal lefthand sides simplification
if pasf_arg2l old = pasf_arg2l new then
return pasf_susibineq(pasf_arg2l old,pasf_op old,pasf_op new,level);
% Decomposing both atomic formulas for additive simplification
od := pasf_susidec(pasf_arg2l old);
nd := pasf_susidec(pasf_arg2l new);
if car od = car nd then
% Equal parametric parts
return pasf_susibinord(pasf_op old,pasf_arg2l old,cdr od,
pasf_op new,pasf_arg2l new,cdr nd,level);
% Transitive simplification
if !*rlsusitr then
return pasf_susibintr(old,new,level)
else
return nil;
end;
procedure pasf_atf2susiprog(atf,level,act);
% Presburger arithmetic standard form atomic formula to susiprog
% conversion. [atf] is an atomic formula; [level] is the level of
% [atf] in the formula; [act] is the action to do with old or new
% formula. Returns $'false$ if [atf] is a contradiction, {(delete
% . T)} if [atf] is a tautology and {'(delete . [act]),('add . (atf
% . level)} else.
if atf eq 'true then
% New formula is always true under theory conditions
{('delete . act)}
else if atf eq 'false then
% Contradiction
'false
else
{('delete . act),('add . (atf . level))};
procedure pasf_susibinsubst(old,new,level);
% Presburger arithmetic standard form smart substitution
% simplification. [old] and [new] are atomic formulas; [level] is
% the recursion level. Returns a susiprog.
begin scalar res,subst,into,atf,flag;
% Determining what formula is substituted
if pasf_opn old eq 'equal and pasf_opn new eq 'equal then
% If both atomic formulas are equalities the result atomic formula
% should contain less free variables as the input formula with the
% biggest amount of free variables to avoid cyclic
% substitutions. Substituted is the formula with smallest amount of
% free variables.
if length rl_fvarl old < length rl_fvarl new then <<
% Substituting old into the new
subst := old;
into := new;
flag := T
>> else <<
% Substituting new into the old
subst := new;
into := old;
flag := nil
>>
else if pasf_opn old eq 'equal then <<
% Substituting old into the new
subst := old;
into := new;
flag := T
>> else <<
% Substituting new into the old
subst := new;
into := old;
flag := nil
>>;
% Testing the substitution condition
atf := pasf_simplat1 pasf_0mk2(pasf_op into,
addf(pasf_arg2l into,negf pasf_arg2l subst));
if length rl_fvarl atf < length rl_fvarl into and not rl_tvalp atf then
return {('delete . flag), ('add . (atf . level))};
atf := pasf_simplat1 pasf_0mk2(pasf_op into,
addf(pasf_arg2l into,pasf_arg2l subst));
if length rl_fvarl atf < length rl_fvarl into and not rl_tvalp atf then
return {('delete . flag), ('add . (atf . level))};
% Nothing could be done
return nil;
end;
procedure pasf_susibintr(old,new,level);
% Presburger arithmetic standard form smart transitive
% simplification. [old] and [new] are atomic formulas; [level] is
% the recursion level. Returns a susiprog.
begin scalar res,sw;
% First testing if simplification works in the order new into old
res := pasf_susibintr1(old,new,level);
if not res then <<
% Simplification in the order old into new
res := pasf_susibintr1(new,old,level);
sw := 't;
>>;
if res eq 'false then
return res;
return res;
end;
procedure pasf_susibintr1(old,new,level);
% Presburger arithmetic standard form smart transitive
% simplification subprocedure. [old] and [new] are atomic formulas;
% [level] is the recursion level. Returns a susiprog.
begin scalar atf,rel,cold,aw;
rel := pasf_smtrtable(pasf_opn old,pasf_opn new);
% No simplification in this direction is possible
if not rel then
return nil;
atf := pasf_simplat1
pasf_0mk2(rel,addf(pasf_arg2l old,negf pasf_arg2l new));
% Amount of free variables in both atomic formulas
cold := length rl_fvarl pasf_mkn('and,{old,new});
% Amount of free variables that are eliminated
aw := cold - length rl_fvarl atf;
% Only simplify if the amount of free variables goes down
if aw > 0 then <<
% Transitive simplification turns out to be an equivalence
% operation if the substituted atomic formula is an equality.
if pasf_opn old eq 'equal or pasf_opn new eq 'equal then <<
% Under this assumptions a real contradiction is found
if atf eq 'false then
return 'false;
if atf eq 'true then
rederr {"True in transitive simplification shound not occur"};
return {('add . (atf . level))}
>>;
% Drawing an implicative conclusion
return {('add . (atf . 'ignore))}
>>;
return nil
end;
procedure pasf_susibineq(u,oop,nop,level);
% Presburger arithmetic standard form smart simplification be equal
% lefthand terms. [u] is the (common) lefthand term; [oop] is the
% old operator in the theory; [nop] is the new operator in the
% found atomic formula; [level] is the recursion level of the new
% found atomic formula. Returns a susiprog that simplifies the
% formula.
begin scalar w;
% Congruences with different moduli
if pairp oop and pairp nop and cdr oop neq cdr nop then
return pasf_susibineqcong(u,oop,nop,level);
% ASSUMPTION: A congruence is never in the output of pasf_smeqtable
w := pasf_smeqtable(
if pairp oop then car oop else oop,
if pairp nop then car nop else nop);
if car w eq nil then
% Nothing can be done
return nil
else if car w eq 'false then
% Contradiction found
return 'false
else if car w eq 1 then
% Remove new atomic formula from the level
return {'(delete . T)}
else if car w eq 2 then
% Remove old atomic formula from the theory, add new atomic
% formula to the knowledge
return {'(delete . nil)}
else if car w eq 3 then
% Remove old atomic formula from the theory, remove new
% atomic formula from the level, add modified atomic formula to
% the level
return {'(delete . nil), '(delete . T),
('add . (pasf_0mk2(cdr w, u) . level))}
else if car w eq 4 then
% Remove new atomic formula from the level, add modified
% atomic formula to the level
return {'(delete . T),
('add . (pasf_0mk2(cdr w, u) . level))}
else
% Remove old atomic formula from the theory, add modified
% atomic formula to the level
return {'(delete . nil),
('add . (pasf_0mk2(cdr w, u) . level))};
end;
procedure pasf_susidec(u);
% Presburger arithmetic standard form decompose atomic
% fqormula. [u] is a SF. Returns a pair $(p . a)$, where $p$ and
% $a$ are SF's. $p$ is the parametric part of [u] and
% $a$ is the absolut part of [u].
begin scalar par,absv,c;
absv := u;
while not domainp absv do
absv := red absv;
return (addf(u,negf absv) . absv)
end;
procedure pasf_susibineqcong(u,oop,nop,level);
% Presburger arithmetic standard form smart equal simplification
% with equal lefthand terms in congruences with different
% moduli. [u] is the (common) lefthand term; [oop] is the old
% operator in the theory; [nop] is the new operator in the found
% atomic formula; [level] is the recursion level of the new found
% atomic formula. Returns a susiprog that simplifies the formula.
begin
scalar n,m;
n := cdr oop;
m := cdr nop;
% Both formulas are congruences
if car oop eq 'cong and car nop eq 'cong then
return{'(delete . nil),'(delete . T),
('add . (pasf_0mk2(pasf_mkop('cong,lcm(m,n)),u) . level))};
% Old formula is a congruence and new is a incongruence
if car oop eq 'cong and car nop eq 'ncong then
if remainder(n,m) = 0 then
return 'false
else
return nil;
% Old formula is an incongruence and new is a congurence
if car oop eq 'ncong and car nop eq 'cong then
if remainder(m,n) = 0 then
return 'false
else
return nil;
% Both formulas are incongruences
if remainder(m,n) = 0 then
return {'(delete . T)}
else if remainder(n,m) = 0 then
return {'(delete . nil)}
else
return nil;
end;
procedure pasf_susibinord(oop,ot,oabs,nop,nt,nabs,level);
% Presburger arithmetic standard form additive simplification.
% [oop] and [nop] are the old and the new relation operators; [ot]
% and [nt] are the corresponding lefthand sides of the terms;
% [oabs] and [nabs] are the corresponding constant parts; [level]
% is the recursion level. Returns a suseproc that simplifies the
% two atomic formulas.
begin scalar w;
% Congruences are treated differently
if pairp oop and pairp nop then
if cdr oop = cdr nop then
return pasf_susibinordcongeq(oop,nop)
else
return pasf_susibinordcong(oop,ot,oabs,nop,nt,nabs,level);
% Nothing to do for congruences times order relations
if pairp oop or pairp nop then
return nil;
w := pasf_smordtable(if pairp oop then car oop else oop,
if pairp nop then car nop else nop,oabs,nabs);
if car w eq nil then
% Nothing can be done
return nil
else if car w eq 'false then
% Contradiction found
return 'false
else if car w eq 1 then
% Remove new atomic formula from the level
return {'(delete . T)}
else if car w eq 2 then
% Remove old atomic formula from the theory, add new atomic
% formula to the knowledge
return {'(delete . nil)}
end;
procedure pasf_susibinordcongeq(oop,nop);
% Presburger arithmetic standard form smart additive simplification
% be equal lefthand terms in congruences with equai moduli.[oop]
% and [nop] are the old and the new relation operators; [ot] and
% [nt] are the corresponding lefthand sides of the terms; [oabs]
% and [nabs] are the corresponding constant parts; [level] is the
% recursion level. Returns a susiprog that simplifies the formula.
begin
scalar n,m;
n := cdr oop;
m := cdr nop;
% Both formulas are congruences
if car oop eq 'cong and car nop eq 'cong then
return 'false;
% Old formula is a congruence and new is a incongruence
if car oop eq 'cong and car nop eq 'ncong then
return {'(delete . T)};
% Old formula is an incongruence and new is a congurence
if car oop eq 'ncong and car nop eq 'cong then
return {'(delete . nil)};
% Both formulas are incongruences
return nil;
end;
procedure pasf_susibinordcong(oop,ot,oabs,nop,nt,nabs,level);
% Presburger arithmetic standard form smart additive simplification
% be equal lefthand terms in congruences with different
% moduli. [oop] and [nop] are the old and the new relation
% operators; [ot] and [nt] are the corresponding lefthand sides of
% the terms; [oabs] and [nabs] are the corresponding constant
% parts; [level] is the recursion level. Returns a susiprog that
% simplifies the formula.
begin
scalar n,m;
n := cdr oop;
m := cdr nop;
% Both formulas are congruences
if car oop eq 'cong and car nop eq 'cong then
return nil;
return nil;
end;
procedure pasf_susipost(atl,knowl);
% Presburger arithmetic standad form susi post
% simplification. [atl] is a list of atomic formulas. [knowl] is a
% KNOWL. Returns a list $\lambda$ of atomic formulas, such that
% $\bigwedge[knowl]\land\bigwedge\lambda$ is equivalent to
% $\bigwedge[knowl]\and\bigwedge[atl]$
atl;
procedure pasf_susitf(at,knowl);
% Presburger arithmetic standard form susi transform. [at] is an
% atomic formula, [knowl] is a knowledge. Returns an atomic formula
% $\alpha$ such that $\alpha\land\bigwedge[knowl]$ is equivalent to
% $[at]\land\bigwedge[knowl]$. $\alpha$ has possibly a more
% convenient relation than [at].
at;
procedure pasf_smeqtable(r1,r2);
% Presburger arithmetic standard form smart simplify equal absolute
% summands table. [r1], [r2] are relations. Returns [false] or a
% relation $R$ such that $R(f+a,0)$ is equivalent to $[r1](f+a,0)
% \land [r2](f+a,0)$.
begin scalar al;
al := '(
(equal .
((equal . (1 . nil))
(neq . (false . nil))
(geq . (1 . nil))
(leq . (1 . nil))
(greaterp . (false . nil))
(lessp . (false . nil))
(cong . (1 . nil))
(ncong . (false . nil))))
(neq .
((equal . (false . nil))
(neq . (1 . nil))
(geq . (3 . greaterp))
(leq . (3 . lessp))
(greaterp . (2 . nil))
(lessp . (2 . nil))
(cong . (nil . nil))
(ncong . (2 . nil))))
(geq .
((equal . (2 . nil))
(neq . (3 . greaterp))
(geq . (1 . nil))
(leq . (3 . equal))
(greaterp . (2 . nil))
(lessp . (false . nil))
(cong . (nil . nil))
(ncong . (5 . greaterp))))
(leq .
((equal . (2 . nil))
(neq . (3 . lessp))
(geq . (3 . equal))
(leq . (1 . nil))
(greaterp . (false . nil))
(lessp . (2 . nil))
(cong . (nil . nil))
(ncong . (5 . lessp))))
(greaterp .
((equal . (false . nil))
(neq . (1 . nil))
(geq . (1 . nil))
(leq . (false . nil))
(greaterp . (1 . nil))
(lessp . (false . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(lessp .
((equal . (false . nil))
(neq . (1 . nil))
(geq . (false . nil))
(leq . (1 . nil))
(greaterp . (false . nil))
(lessp . (1 . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(cong .
((equal . (2 . nil))
(neq . (nil . nil))
(geq . (nil . nil))
(leq . (nil . nil))
(greaterp . (nil . nil))
(lessp . (nil . nil))
(cong . (1 . nil))
(ncong . (nil . nil))))
(ncong .
((equal . (false . nil))
(neq . (1 . nil))
(geq . (4 . greaterp))
(leq . (4 . lessp))
(greaterp . (nil . nil))
(lessp . (nil . nil))
(cong . (false . nil))
(ncong . (1 . nil)))));
return cdr (atsoc(r2,atsoc(r1,al)))
end;
procedure pasf_smordtable(r1,r2,s,tt);
% Presburger arithmetic standard form smart simplify ordered
% absolute summands. [r1], [r2] are relations, [s] is the constant
% part of [r1], [t] is the one of [r2]. Returns $(nil . nil)$ if no
% simplification is possible; $(false . nil)$ if contradiction was
% found; $(1 . nil)$ if the new formula does not bring any
% knowledge and can be so removed from the actual level; $(2
% . nil)$ if the old formula should be removed and the new added.
if minusf addf(s, negf tt) then
% -s < -t => s > t
pasf_smordtable2(r1,r2)
else
% -s > -t => s < t
pasf_smordtable1(r1,r2);
procedure pasf_smordtable1(r1,r2);
% Presburger arithmetic standard form smart simplify ordered
% absolute summands table if absoulte summand of [r1] is less as
% the one of [r2].
begin scalar al;
al := '(
(lessp .
((lessp . (1 . nil))
(leq . (1 . nil))
(equal . (false . nil))
(neq . (1 . nil))
(geq . (false . nil))
(greaterp . (false . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(leq .
((lessp . (1 . nil))
(leq . (1 . nil))
(equal . (false . nil))
(neq . (1 . nil))
(geq . (false . nil))
(greaterp . (false . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(equal .
((lessp . (1 . nil))
(leq . (1 . nil))
(equal . (false . nil))
(neq . (1 . nil))
(geq . (false . nil))
(greaterp . (false . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(neq .
((lessp . (nil . nil))
(leq . (nil . nil))
(equal . (2 . nil))
(neq . (nil . nil))
(geq . (2 . nil))
(greaterp . (2 . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(geq .
((lessp . (nil . nil))
(leq . (nil . nil))
(equal . (2 . nil))
(neq . (nil . nil))
(geq . (2 . nil))
(greaterp . (2 . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(greaterp .
((lessp . (nil . nil))
(leq . (nil . nil))
(equal . (2 . nil))
(neq . (nil . nil))
(geq . (2 . nil))
(greaterp . (2 . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(cong .
((lessp . (nil . nil))
(leq . (nil . nil))
(equal . (2 . nil))
(neq . (nil . nil))
(geq . (2 . nil))
(greaterp . (2 . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(ncong .
((lessp . (nil . nil))
(leq . (nil . nil))
(equal . (nil . nil))
(neq . (nil . nil))
(geq . (nil . nil))
(greaterp . (nil . nil))
(cong . (nil . nil))
(ncong . (nil . nil)))));
return cdr (atsoc(r2,atsoc(r1,al)))
end;
procedure pasf_smordtable2(r1,r2);
% Presburger arithmetic standard form smart simplify ordered
% absolute summands table if absoulte summand of [r1] is less as
% the one of [r2].
begin scalar al;
al := '(
(lessp .
((lessp . (2 . nil))
(leq . (2 . nil))
(equal . (2 . nil))
(neq . (nil . nil))
(geq . (nil . nil))
(greaterp . (nil . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(leq .
((lessp . (2 . nil))
(leq . (2 . nil))
(equal . (2 . nil))
(neq . (nil . nil))
(geq . (nil . nil))
(greaterp . (nil . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(equal .
((lessp . (false . nil))
(leq . (false . nil))
(equal . (false . nil))
(neq . (1 . nil))
(geq . (1 . nil))
(greaterp . (1 . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(neq .
((lessp . (2 . nil))
(leq . (2 . nil))
(equal . (2 . nil))
(neq . (nil . nil))
(geq . (nil . nil))
(greaterp . (nil . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(geq .
((lessp . (false . nil))
(leq . (false . nil))
(equal . (false . nil))
(neq . (1 . nil))
(geq . (1 . nil))
(greaterp . (1 . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(greaterp .
((lessp . (false . nil))
(leq . (false . nil))
(equal . (false . nil))
(neq . (1 . nil))
(geq . (1 . nil))
(greaterp . (1 . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(cong .
((lessp . (nil . nil))
(leq . (nil . nil))
(equal . (nil . nil))
(neq . (nil . nil))
(geq . (nil . nil))
(greaterp . (nil . nil))
(cong . (nil . nil))
(ncong . (nil . nil))))
(ncong .
((lessp . (nil . nil))
(leq . (nil . nil))
(equal . (nil . nil))
(neq . (nil . nil))
(geq . (nil . nil))
(greaterp . (nil . nil))
(cong . (nil . nil))
(ncong . (nil . nil)))));
return cdr (atsoc(r2,atsoc(r1,al)))
end;
procedure pasf_smtrtable(r1,r2);
% Presburger arithmetic standard form smart transitive
% simplification table. [r1] is the theory relation; [r2] is the
% new level relation. Returns a new transitive concluded relation
% or nil if no conclusion can be done.
begin scalar al;
% For these operations no transitive simplification is done
if r1 memq '(neq greaterp cong ncong) then
return nil;
al := '(
(equal .
((equal . equal)
(greaterp . lessp)
(geq . leq)
(leq . nil)
(lessp . nil)
(neq . nil)
(cong . nil)
(ncong . nil)))
(lessp .
((equal . lessp)
(greaterp . lessp)
(geq . lessp)
(leq . nil)
(lessp . nil)
(neq . nil)
(cong . nil)
(ncong . nil)))
(geq .
((equal . nil)
(greaterp . nil)
(geq . nil)
(leq . nil)
(lessp . nil)
(neq . nil)
(cong . nil)
(ncong . nil)))
(leq .
((equal . leq)
(greaterp . lessp)
(geq . leq)
(leq . nil)
(lessp . nil)
(neq . nil)
(cong . nil)
(ncong . nil))));
return cdr (atsoc(r2,atsoc(r1,al)))
end;
endmodule; % [pasfsism]
end; % of file