reduce-historical/r37/packages/redlog/xxx

acfsfbnf.red:   if gor eq 'or then (
acfsfbnf.red:   ) else  % [gor eq 'and]
acfsfbnf.red:   if r1 eq r2 then 'keep else 'drop;
acfsfgs.red:      if phi eq 'inctheo then return 'inctheo;
acfsfgs.red:      if phi eq 'inctheo then return 'inctheo;
acfsfgs.red:      if phi eq 'inctheo then return 'inctheo;
acfsfgs.red:      if phi eq 'inctheo then return 'inctheo;
acfsfgs.red:      if rl_op(f) eq 'and then acfsf_gsd(f,atl) else acfsf_gsc(f,atl)
acfsfgs.red:      if rl_op(f) eq 'and then acfsf_gsc(f,atl) else acfsf_gsd(f,atl);
acfsfgs.red:      if atl eq 'inctheo or acfsf_gsinctheop(atl) then
acfsfgs.red:      if (cl_atfp f) or (rl_op f eq 'or) then  % degenerated cnf
acfsfgs.red:	 if gprem eq 'false then return 'false;
acfsfgs.red:      return w eq 'false
acfsfgs.red:	    if (w := acfsf_gsdis!-type rl_argn phi) eq 'impl then
acfsfgs.red:	    else if w eq 'noneq then
acfsfgs.red:	    else << % [if w eq 'equal then]
acfsfgs.red:      if op eq 'neq then return 'impl;
acfsfgs.red:      if w eq 'impl then return 'impl;
acfsfgs.red:      if op eq 'equal and w eq 'equal then return 'equal;
acfsfgs.red:      if rprod eq 'true then <<
acfsfgs.red:      if w eq 'true then <<
acfsfgs.red:      if natl eq 'true then <<
acfsfgs.red:	 if w eq 'true then
acfsfgs.red:      if w eq 'true then return 'true;
acfsfgs.red:	 if w eq 'true then
acfsfgs.red:      if w eq 'true then return 'true;
acfsfgs.red:	    if a eq 'equal then
acfsfgs.red:	    else if a eq 'cequal then
acfsfgs.red:	    else if a eq 'neq then
acfsfgs.red:   (if w eq 'equal then
acfsfgs.red:   else if w eq 'neq then
acfsfgs.red:      if (op eq 'neq) or (flag and op eq 'equal) then return nil;
acfsfgs.red:      if (rl_tvalp nat) or (op eq 'equal) or (null !*rlgsrad) then
acfsfmisc.red:   if r eq 'equal then 'neq
acfsfmisc.red:   else if r eq 'neq then 'equal
acfsfmisc.red:   r1 eq r2 or r1 eq 'equal;
acfsfmisc.red:	 if acfsf_op atf eq 'neq and
acfsfmisc.red:      if vl eq 'fvarl then
acfsfmisc.red:	    while (not domainp a) and (mvar a eq v) and dgcd neq 1 do <<
acfsfmisc.red:      if not domainp w and null red w and mvar w eq v then
acfsfmisc.red:   if acfsf_op at eq 'equal then
acfsfmisc.red:	 if acfsf_op a eq 'equal and quotf(c,acfsf_arg2l a) then <<
acfsfmisc.red:      return a eq 'found
acfsfmisc.red:	 if acfsf_op a eq 'neq and quotf(acfsf_arg2l a,c) then <<
acfsfmisc.red:      return a eq 'found
acfsfqe.red:   if car qblk eq 'ex then
acfsfqe.red:      fl := if rl_op f eq 'or then rl_argn f else {f};
acfsfqe.red:	 if acfsf_op at eq 'equal then
acfsfsiat.red:      if rel eq 'equal then return acfsf_simplequal(lhs,sop);
acfsfsiat.red:      if rel eq 'neq then return acfsf_simplneq(lhs,sop)
acfsfsiat.red:   if rel eq 'equal then null lhs
acfsfsiat.red:   else if rel eq 'neq then not null lhs
acfsfsism.red:	 a := if op eq 'and then car atl else acfsf_negateat car atl;
acfsfsism.red:	    if cdr w eq 'false then <<
acfsfsism.red:   acfsf_0mk2(acfsf_clnegrel(car entry,op eq 'and),
acfsfsism.red:      if w eq 'false then return 'false;
acfsfsism.red:      if w eq 'true then return db;
acfsfsism.red:	 if w eq 'true then <<
acfsfsism.red:	 >> else if w eq 'false then <<
acfsfsism.red:      if a eq 'false then return 'false;
acfsfsism.red:      if a eq 'true then return db;
acfsfsism.red:      	 if w eq 'false then return 'false;
acfsfsism.red:	 % [w eq r1]
acfsfsism.red:      if r1 eq r2 then r1 else 'false;
acfsfsism.red:   if r1 eq 'equal and r2 eq 'equal then
acfsfsism.red:      'equal . (r1 eq 'equal);
cl.red:   (rl_tvalp f) or (cl_atfp f) or (rl_op f eq 'and and cl_ncflp rl_argn f)
cl.red:      or ((rl_op f eq 'or) and cl_dnfp1 rl_argn f);
cl.red:      ((rl_op car fl eq 'and) and (cl_ncflp rl_argn car fl))) and
cl.red:   (rl_tvalp f) or (cl_atfp f) or (rl_op f eq 'or and cl_ncflp rl_argn f)
cl.red:      or ((rl_op f eq 'and) and cl_cnfp1 rl_argn f);
cl.red:      ((rl_op car fl eq 'or) and (cl_ncflp rl_argn car fl))) and
cl.red:      or ((rl_op f eq 'and) and cl_cnfp1 rl_argn f) or
cl.red:	 ((rl_op f eq 'or) and cl_dnfp1 rl_argn f);
clbnf.red:	 if w eq 'keep1 then
clbnf.red:	 else if w eq 'keep2 then
clbnf.red:      while l1 and l2 and car l1 eq car l2 do <<
clbnf.red:      gand := if gor eq 'or then 'and else 'or;
clbnf.red:      if op eq gor then
clbnf.red:      if op eq gand then <<
clbnf.red:      if op eq gand then
clbnf.red:	 if rl_op subf eq gand then subf else rl_mkn(gand,{subf}))
clbnf.red:      if w eq 'break then
clbnf.red:	 return rl_mkn(gor,{rl_mkn(gand,{cl_cflip('true,gor eq 'or)})});
clbnf.red:	 return rl_mkn(gor,{rl_mkn(gand,{cl_cflip('true,gor eq 'or)})});
clbnf.red:   % [l] is as a g-DNF equivalent to ['true] in case of ['gor eq 'or]
clbnf.red:   % and equivalent to ['false] in case ['gor eq 'and]. The lists are
clbnf.red:	 if w eq 'break then <<
clbnf.red:   % case of ['gor eq 'or] and equivalent to ['false] in case ['gor eq
clbnf.red:	 if w eq 'break then <<
clbnf.red:      if flg eq 'break then
clbnf.red:   % case of ['gor eq 'or] and equivalent to ['false] in case ['gor eq
clbnf.red:   % equivalent to ['true] in the case ['gor eq 'or] or to ['false] in
clbnf.red:   % the case ['gor eq 'and].
clbnf.red:      while ll and ((w := cl_subandcut(c, car ll,gor)) eq 'keep1) do
clbnf.red:      if w eq 'keep2 then return (nil . ll);
clbnf.red:      if w eq 'break then
clbnf.red:      if w eq 'keep2 then <<
clbnf.red:      >> else if w eq 'keep1 then <<
clbnf.red:      if w eq 'keep1 then return state;
clbnf.red:	 if at eq 'drop then
clbnf.red:      if w eq 'keep2 then
clmisc.red:   if op eq 'and then 'or
clmisc.red:   else if op eq 'or then 'and
clmisc.red:   else if op eq 'all then 'ex
clmisc.red:   else if op eq 'ex then 'all
clmisc.red:   else if op eq 'true then 'false
clmisc.red:   else if op eq 'false then 'true
clmisc.red:	 if rl_var f eq oldv then
clmisc.red:      rl_gsd(at,atl) eq 'true or rl_multsurep(at,atl)
clmisc.red:      rl_simpl(at,atl,-1) eq 'true or rl_multsurep(at,atl);
clmisc.red:	 if w eq q then
clnf.red:      if op eq 'impl then
clnf.red:      if op eq 'repl then
clnf.red:      if op eq 'equiv then
clnf.red:      if op eq 'not then
clnf.red:      if op eq 'impl then
clnf.red:      if op eq 'repl then
clnf.red:      if op eq 'equiv then
clnf.red:      if (null cdr e) or (rl_op phi eq rl_op car e) then
clnf.red:      	    if rl_op car l1 eq 'all then onlyex := nil;
clnf.red:      	    if rl_op car l2 eq 'ex then onlyall := nil
clnf.red:      if car phi1 eq car phi2 then
clnf.red:      	    while rl_op f eq a do <<
clnf.red:      if op eq 'ex then
clnf.red:      if op eq 'all then
clnf.red:      if op eq 'ex then
clnf.red:      if op eq 'all then
clnf.red:      if op eq 'or then <<
clnf.red:      if op eq 'and then <<
clnf.red: 	 if var eq rl_var phi then
clnf.red:	 if w eq 'true then <<
clnf.red:	 >> else if w eq 'inctheo then
clnf.red:	 if w eq 'true then <<
clqe.red:      if f eq 'inctheo then return 'inctheo;
clqe.red:      if q eq 'ex then
clqe.red:      % [q eq 'all]
clqe.red:	       if vlv eq length cvl then
clqe.red:	       if cl_covl car w eq 'break then <<
clqe.red:	    if elimres eq 'true then <<
clqe.red:	       if rl_op elimres eq 'or then
clqe.red:      else if op eq 'not then
clqe.red:      else if op eq 'impl then
clqe.red:      else if op eq 'repl then
clqe.red:      else if op eq 'equiv then
clqe.red:	 if op eq 'and then
clqe.red:	 if op eq 'or then
clqe.red:	 if q eq 'ex then
clqe.red:	 if w eq 'failed then <<
clqe.red:      if w eq 'failed then return 'failed;
clqe.red:      if car csol eq 'failed then return 'failed;
clqe.red:      else if rl_op f eq 'and then
clqe.red:      else if rl_op f eq 'or then
clqe.red:      if car grv1 eq 'failed or car grv2 eq 'failed then
clqe.red:      tag := if car grv1 eq 'gignore then
clqe.red:      else if car grv2 eq 'gignore then
clqe.red:   if car grv1 eq 'gignore and car grv2 eq 'gignore then
clqe.red:   else if car grv1 eq 'gignore then grv2
clqe.red:   else if car grv2 eq 'gignore then grv1
clsimpl.red:      if atl eq 'inctheo then
clsimpl.red:      if w eq 'false then return 'inctheo;
clsimpl.red:	 if w eq 'false then <<
clsimpl.red:      if atf eq 'inctheo then
clsimpl.red:      if op eq 'not then <<
clsimpl.red:      if op eq 'impl then
clsimpl.red:      if op eq 'repl then
clsimpl.red:      if op eq 'equiv then
clsimpl.red:	 if newknowl eq 'false then return 'false;
clsimpl.red:   if rl_op f eq 'not then rl_arg1 f else rl_mk1('not,f);
clsimpl.red:      gtrue := cl_cflip('true,gand eq 'and);
clsimpl.red:	 if a eq gfalse then <<
clsimpl.red:	    if rl_op a eq gand then <<
clsimpl.red:      break := cl_cflip('false,op eq 'and);
clsimpl.red:      if newknowl eq 'false then return {break};
clsimpl.red:	 if wop eq break then <<
clsimpl.red:	 >> else if wop eq op then <<
clsimpl.red:	    if newknowl eq 'false then <<
clsimpl.red:      if a eq break then return {break};
clsimpl.red:      if prem eq 'false or concl eq 'true then
clsimpl.red:   if prem eq 'true then
clsimpl.red:   else if concl eq 'false then
clsimpl.red:   else if prem eq 'false or concl eq 'true then
clsimpl.red:   if lhs eq 'true then
clsimpl.red:   else if rhs eq 'true then
clsimpl.red:   else if lhs eq 'false then
clsimpl.red:   else if rhs eq 'false then
clsimpl.red:	 if knowl eq 'false then <<
clsimpl.red:      if at eq 'break then
clsimpl.red:      if op eq 'or then <<
clsimpl.red:      if op eq 'or then
clsimpl.red:      if atl eq 'inctheo then
clsimpl.red:      sicd := if c eq 'true then
clsimpl.red:      if w eq 'false then
clsimpl.red:	 return {cl_cflip(res,op eq 'and)};
clsimpl.red:      if res eq 'inctheo then 	              % Das hatte man auch frueher
clsimpl.red:	 return cl_cflip('false,op eq 'and);  % wissen koennen.
clsimpl.red:      if op eq 'or then
clsimpl.red:	 if knowl eq 'false then <<
clsimpl.red:      if at eq 'break then
clsimpl.red:   if op eq 'and then
clsimpl.red:   else % We know [op eq 'or]
clsimpl.red:	 if w eq 'false then  % What happens with atoms neq false ???
clsimpl.red:      if w eq 'false then return 'false;
clsimpl.red:	 if knowl eq 'false then
clsimpl.red:	 if car p eq 'delete or car p eq 'ignore then
clsimpl.red:%      	 if car p eq 'ignore then   % We ignore ['ignore]!
clsimpl.red:%      	 else if car p eq 'delete then
clsimpl.red:      	 else if car p eq 'add then
dvfsfmisc.red:      if op eq 'equal then
dvfsfmisc.red:      if op eq 'neq then
dvfsfmisc.red:      if op eq 'div then
dvfsfmisc.red:      if op eq 'sdiv then
dvfsfmisc.red:      if op eq 'assoc then
dvfsfmisc.red:      if op eq 'nassoc then
dvfsfmisc.red:   if gor eq 'or then (
dvfsfmisc.red:   ) else  % [gor eq 'and]
dvfsfmisc.red:      if not (op eq 'assoc or op eq 'nassoc) then
dvfsfmisc.red:	 if op eq 'assoc and (sop eq 'and or null sop) then
dvfsfmisc.red:      	 if op eq 'nassoc and (sop eq 'or or null sop) then
dvfsfmisc.red:   rl_smkn(if op eq 'assoc then 'and else 'or,
dvfsfmisc.red:	    where dvfsf_p!*=fac) eq fu
dvfsfmisc.red:      op := if u eq 'false then 'nassoc else 'assoc;
dvfsfmisc.red:      return rl_smkn(if u eq 'false then 'or else 'and,
dvfsfmisc.red:   else if mvar f eq ' p then
dvfsfqe.red:      if op eq 'neq then
dvfsfqe.red:      if op eq 'assoc then
dvfsfqe.red:      if op eq 'nassoc then
dvfsfqe.red:   if (c := cl_simpl(c,nil,-1)) eq 'false then
dvfsfsiat.red:      if op eq 'equal or op eq 'neq then
dvfsfsiat.red: 	 return if op eq 'sdiv or op eq 'nassoc then 'false else 'true;
dvfsfsiat.red:    	 if op eq 'sdiv then return 'false;
dvfsfsiat.red:	 if op eq 'nassoc then return dvfsf_safield('neq,rhs,sop);
dvfsfsiat.red:    	 if op eq 'sdiv or op eq 'nassoc then
dvfsfsiat.red:    	 if op eq 'assoc then
dvfsfsiat.red:    	 % We know [op eq 'div] now.
dvfsfsiat.red:      junct := if op eq 'sdiv or op eq 'nassoc then 'and else 'or;
dvfsfsiat.red:      if junct eq 'and then <<
dvfsfsiat.red:	 if natf1 eq 'false then return 'false;
dvfsfsiat.red:      % We know [junct eq 'or].
dvfsfsiat.red:      if natf1 eq 'true then return natf1;
dvfsfsiat.red:   if op eq 'or and (at eq 'true or f eq 'true) then
dvfsfsiat.red:   else if op eq 'and and (at eq 'false or f eq 'false) then
dvfsfsiat.red:   else if (at eq 'true) or (at eq 'false) then
dvfsfsiat.red:   else if (f eq 'true) or (f eq 'false) then
dvfsfsiat.red:      if (op eq 'assor or op eq 'nassoc) and ordp(rhs,lhs) then
dvfsfsiat.red:	 if op eq 'assoc then
dvfsfsiat.red:	 if op eq 'nassoc then
dvfsfsiat.red:	 if op eq 'sdiv then
dvfsfsiat.red:	 % We know [op eq 'div] now.
dvfsfsiat.red:	 if op eq 'equal then
dvfsfsiat.red:	 else  % [op eq 'neq]
dvfsfsiat.red:	 return if op eq 'equal then 'false else 'true;
dvfsfsiat.red:      junct := if op eq 'equal then 'or else 'and;
dvfsfsiat.red:      if w eq 'failed then
dvfsfsiat.red: 	 return if op eq 'nassoc then 'false else 'true;
dvfsfsiat.red:      	 if op eq 'assoc then
dvfsfsiat.red:      	 else if op eq 'nassoc then
dvfsfsiat.red:      	 else if op eq 'div then
dvfsfsiat.red:      	 else if op eq 'sdiv then
dvfsfsiat.red:      	 if op eq 'assoc then
dvfsfsiat.red:      	 else if op eq 'nassoc then
dvfsfsiat.red:      	 else if op eq 'div then
dvfsfsiat.red:      	 else if op eq 'sdiv then
dvfsfsiat.red:      return null cdr w and car w eq 'p
dvfsfsiat.red:	 if w eq 'failed then
dvfsfsiat.red:      if w eq 'failed then
dvfsfsiat.red:      if w eq 'failed then
dvfsfsiat.red:   else if op eq 'assoc or op eq 'nassoc then
dvfsfsiat.red:   else if op eq 'div then
dvfsfsiat.red:   else if op eq 'sdiv then
dvfsfsiat.red:   if not(not(domainp lhs) and mvar lhs eq 'p and ldeg lhs = 1
dvfsfsiat.red:      if op eq 'equal then 'false else 'true
dvfsfsiat.red:      dvfsf_mk2(if op eq 'equal then 'nassoc else 'assoc,
dvfsfsiat.red:      if op eq 'sdiv then <<
dvfsfsiat.red:      if op eq 'div then <<
dvfsfsism.red:      if (oop eq 'equal or oop eq 'neq) and nop neq 'equal and nop neq 'neq and
dvfsfsism.red:      if (nop eq 'equal or nop eq 'neq) and oop neq 'equal and oop neq 'neq and
dvfsfsism.red:   if rold eq rnew then
dvfsfsism.red:   else if rold eq 'neq then
dvfsfsism.red:      if rnew eq 'equal then
dvfsfsism.red:      else if rnew eq 'sdiv or rnew eq 'nassoc then
dvfsfsism.red:   else if rold eq 'sdiv then
dvfsfsism.red:      if rnew eq 'neq or rnew eq 'div or rnew eq 'nassoc then
dvfsfsism.red:   else if rold eq 'div then
dvfsfsism.red:      if rnew eq 'sdiv or rnew eq 'assoc or rnew eq 'equal then
dvfsfsism.red:      else if rnew eq 'nassoc then
dvfsfsism.red:   else if rold eq 'assoc then
dvfsfsism.red:      if rnew eq 'sdiv or rnew eq 'nassoc then
dvfsfsism.red:      else if rnew eq 'div then
dvfsfsism.red:      else if rnew eq 'equal then
dvfsfsism.red:      else  % [rnew eq 'neq]
dvfsfsism.red:   else if rold eq 'equal then
dvfsfsism.red:      if rnew eq 'neq or rnew eq 'sdiv or rnew eq 'nassoc then
dvfsfsism.red:   else if rold eq 'nassoc then
dvfsfsism.red:      if rnew eq 'sdiv then
dvfsfsism.red:      else if rnew eq 'assoc or rnew eq 'equal then
dvfsfsism.red:      else if rnew eq 'div then
dvfsfsism.red:      else  % [rnew eq 'neq]
dvfsfsism.red:   if rold eq 'div then
dvfsfsism.red:      if rnew eq 'sdiv then
dvfsfsism.red:      else if rnew eq 'div then
dvfsfsism.red:      else if rnew eq 'assoc then
dvfsfsism.red:      else if rnew eq 'nassoc then
dvfsfsism.red:   else if rold eq 'sdiv then
dvfsfsism.red:      if rnew eq 'div or rnew eq 'sdiv or rnew eq 'assoc then
dvfsfsism.red:      else if rnew eq 'nassoc then
dvfsfsism.red:   else if rold eq 'nassoc then
dvfsfsism.red:      if rnew eq 'sdiv then
dvfsfsism.red:      else if rnew eq 'div then
dvfsfsism.red:   else if rold eq 'assoc then
dvfsfsism.red:      if rnew eq 'sdiv then
dvfsfsism.red:      else if rnew eq 'div then
lto.red:      if l then if car l eq x then cdr l else car l . delq(x,cdr l);
lto.red:      else if u eq car v then
lto.red:      % list, such that [not(car v eq u)]. Returns a list. The first
lto.red:      else if u eq cadr v then
ofsf.red:   if r eq 'leq then 'lessp else if r eq 'geq then 'greaterp else r;
ofsfbnf.red:   if gor eq 'or then (
ofsfbnf.red:   ) else  % [gor eq 'and]
ofsfbnf.red:   if gor eq 'or then
ofsfgs.red:      if phi eq 'inctheo then return 'inctheo;
ofsfgs.red:      if phi eq 'inctheo then return 'inctheo;
ofsfgs.red:      if phi eq 'inctheo then return 'inctheo;
ofsfgs.red:      if phi eq 'inctheo then return 'inctheo;
ofsfgs.red:      if rl_op(f) eq 'and then ofsf_gsd(f,atl) else ofsf_gsc(f,atl)
ofsfgs.red:      if rl_op(f) eq 'and then ofsf_gsc(f,atl) else ofsf_gsd(f,atl);
ofsfgs.red:      if atl eq 'inctheo or ofsf_gsinctheop(atl) then
ofsfgs.red:      if (cl_atfp f) or (rl_op f eq 'or) then  % degenerated cnf
ofsfgs.red:	 if gprem eq 'false then return 'false;
ofsfgs.red:      return w eq 'false
ofsfgs.red:	    if (w := ofsf_gsdis!-type rl_argn phi) eq 'impl then
ofsfgs.red:	    else if w eq 'noneq then
ofsfgs.red:	    else << % [if w eq 'equal then]
ofsfgs.red:      if op eq 'neq then return 'impl;
ofsfgs.red:      if w eq 'impl then return 'impl;
ofsfgs.red:      if op eq 'equal and w eq 'equal then return 'equal;
ofsfgs.red:      if rprod eq 'true then <<
ofsfgs.red:      if w eq 'true then <<
ofsfgs.red:      if natl eq 'true then <<
ofsfgs.red:	 if w eq 'true then
ofsfgs.red:      if w eq 'true then return 'true;
ofsfgs.red:	 if w eq 'true then
ofsfgs.red:      if w eq 'true then return 'true;
ofsfgs.red:	    if a eq 'equal then
ofsfgs.red:	    else if a eq 'cequal then
ofsfgs.red:	    else if a eq 'neq then
ofsfgs.red:   (if w eq 'equal then
ofsfgs.red:   else if w eq 'neq then
ofsfgs.red:      if (op eq 'neq) or (flag and op eq 'equal) then return nil;
ofsfgs.red:      if (rl_tvalp nat) or (op eq 'equal) or (null !*rlgsrad) then
ofsfmisc.red:   if r eq 'equal then 'neq
ofsfmisc.red:   else if r eq 'neq then 'equal
ofsfmisc.red:   else if r eq 'leq then 'greaterp
ofsfmisc.red:   else if r eq 'lessp then 'geq
ofsfmisc.red:   else if r eq 'geq then 'lessp
ofsfmisc.red:   else if r eq 'greaterp then 'leq
ofsfmisc.red:   if ofsf_op at eq 'equal then
ofsfmisc.red:	 if ofsf_op a eq 'equal and quotf(c,ofsf_arg2l a) then <<
ofsfmisc.red:      return a eq 'found
ofsfmisc.red:	 if ofsf_op a eq 'neq and quotf(ofsf_arg2l a,c) then <<
ofsfmisc.red:      return a eq 'found
ofsfopt.red:	 if junct eq 'break then
ofsfopt.red:      if junct eq 'pbase then
ofsfopt.red:      else if junct eq 'break then
ofsfopt.red:	 if v eq z then <<
ofsfopt.red:      if ofsf_op a eq 'equal and v memq ofsf_varlat a then <<
ofsfopt.red:      if w eq 'false then return 'false;
ofsfopt.red:      if w eq 'true then return nil;
ofsfopt.red:      if op eq 'and then
ofsfopt.red:	       	  if car w eq 'lb then <<
ofsfopt.red:	       	  >> else if car w eq 'ub then <<
ofsfopt.red:      if op eq 'equal then return 'equal . sol;
ofsfopt.red:      if ofsf_xor(op eq 'geq,minusf lc u) then return 'lb . sol;
ofsfopt.red:      if not (op eq 'equal or ofsf_xor(op eq 'geq,minusf lc u)) then
ofsfopt.red:      if atf eq 'false then return nil;
ofsfopt.red:      if ans eq 'break then return {simp '(minus infinity),nil};
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      if r eq 'equal or r eq 'neq then
ofsfqe.red:   (if r eq 'equal then w else cl_nnfnot w)
ofsfqe.red:   if r eq 'leq or r eq 'lessp then
ofsfqe.red:   else  % [r eq 'geq or r eq 'greaterp]
ofsfqe.red:      w := if r eq 'leq then
ofsfqe.red:      while not domainp w and mvar w eq 'ofsf_sqrt do <<
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      w := if op eq 'equal or op eq 'neq then numr w else multf(numr w,denr w);
ofsfqe.red:      if op eq 'equal or op eq 'neq then
ofsfqe.red:   if op eq 'equal then
ofsfqe.red:   else  % [op eq 'neq]
ofsfqe.red:      while not domainp lhs and mvar lhs eq v do <<
ofsfqe.red:      an := if inf eq 'minf and not evenp ldeg f then
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      if cdr w eq 'false then
ofsfqe.red:      if op eq 'equal or op eq 'neq then
ofsfqe.red:   if degreef(f,v) eq 0 then
ofsfqe.red:      if car w eq 'failed then return w;
ofsfqe.red:   if r eq 'equal or r eq 'neq then
ofsfqe.red:   else if r eq 'lessp or r eq 'greaterp then
ofsfqe.red:      if w eq 'failed then
ofsfqe.red:      if car w eq 'onequot then <<
ofsfqe.red:      >> else if car w eq 'tworoot then <<
ofsfqe.red:   cl_simpl(f,theo,-1) eq 'true;
ofsfqe.red:      if ldeg x eq 2 then <<
ofsfqe.red:      return if not domainp x and mvar x eq v then
ofsfqe.red:      if a eq 'failed or null nzf then return nil;
ofsfqe.red:      if car grv1 eq 'failed then
ofsfqe.red:      if car grv2 eq 'failed then
ofsfqe.red:   not(car grv eq 'failed) and not(car grv eq 'gignore) and
ofsfqe.red:      cadar grv eq 'lin and caddar grv eq 'con and   % Linear, concrete coeff.
ofsfqe.red:      if w eq 'failed then return '(failed . nil);
ofsfqe.red:      if tag eq 'gen then v := "!" . v;
ofsfqe.red:      if null cdr eset and caar eset eq 'ofsf_qesubcq then
ofsfqe.red:   else if cl_simpl(ofsf_0mk2('equal,u),theo,-1) eq 'false then
ofsfqe.red:	 w := if sub eq 'ofsf_qesubi then <<
ofsfqe.red:	 >> else if sub eq 'ofsf_qesubcq then
ofsfqe.red:	 else if sub eq 'ofsf_qesubcr1 then
ofsfqe.red:	 else if sub eq 'ofsf_qesubcqme then
ofsfqe.red:	 else if sub eq 'ofsf_qesubcqpe then
ofsfqe.red:	 else if sub eq 'ofsf_qesubcrme1 then
ofsfqe.red:	 else if sub eq 'ofsf_qesubcrpe1 then
ofsfqe.red:	    rl_mkn(if op eq 'ex then 'and else 'impl,{gamma,car w})
ofsfqe.red:      if vl eq 'fvarl then
ofsfqe.red:	 if w eq 'odd and null oddp then
ofsfqe.red:	    while (not domainp a) and (mvar a eq v) and dgcd neq 1 do <<
ofsfqe.red:	 if dgcd > 0 and oddp eq 'odd then <<
ofsfqe.red:      if not domainp w and null red w and mvar w eq v then
ofsfqe.red:   else if f eq at then
ofsfqe.red:      if op eq 'neq then
ofsfqe.red:      if op eq 'equal then <<
ofsfqe.red:      if op eq 'leq then <<
ofsfqe.red:      if op eq 'geq then <<
ofsfqe.red:      if op eq 'lessp then <<
ofsfqe.red:      if op eq 'greaterp then <<
ofsfsiat.red:      if rel eq 'equal then return ofsf_simplequal(lhs,sop);
ofsfsiat.red:      if rel eq 'neq then return ofsf_simplneq(lhs,sop);
ofsfsiat.red:      if rel eq 'leq then return ofsf_simplleq(lhs,sop);
ofsfsiat.red:      if rel eq 'geq then return ofsf_simplgeq(lhs,sop);
ofsfsiat.red:      if rel eq 'lessp then return ofsf_simpllessp(lhs,sop);
ofsfsiat.red:      if rel eq 'greaterp then return ofsf_simplgreaterp(lhs,sop)
ofsfsiat.red:      if w eq 'stsq then return 'false;
ofsfsiat.red:      if ww eq 'stsq then return 'false;
ofsfsiat.red:	 if ww eq 'tsq then return ofsf_tsqsplequal ff;
ofsfsiat.red:	 if w eq 'tsq then return ofsf_tsqsplequal lhs
ofsfsiat.red:      if w eq 'stsq then return 'true;
ofsfsiat.red:      if ww eq 'stsq then return 'true;
ofsfsiat.red:	 if ww eq 'tsq then return ofsf_tsqsplneq ff;
ofsfsiat.red:	 if w eq 'tsq then return ofsf_tsqsplneq lhs
ofsfsiat.red:      if (s1 := sfto_tsqsumf lhs) eq 'stsq then  % necessary?
ofsfsiat.red:      if (s2 := sfto_tsqsumf w) eq 'stsq then
ofsfsiat.red:      if !*rlsiexpla or (!*rlsiexpl and (sop eq 'or)) then
ofsfsiat.red:      if !*rlsiexpla or (!*rlsiexpl and (sop eq 'or)) then
ofsfsiat.red:      if !*rlsiexpla or (!*rlsiexpl and (sop eq 'and)) then
ofsfsiat.red:      if (s1 := sfto_tsqsumf lhs) eq 'stsq then  % necessary?
ofsfsiat.red:      if (s2 := sfto_tsqsumf w) eq 'stsq then
ofsfsiat.red:      if !*rlsiexpla or (!*rlsiexpl and (sop eq 'and)) then
ofsfsiat.red:   if rel eq 'equal then null lhs
ofsfsiat.red:   else if rel eq 'neq then not null lhs
ofsfsiat.red:   else if rel eq 'leq then minusf lhs or null lhs
ofsfsiat.red:   else if rel eq 'geq then not minusf lhs
ofsfsiat.red:   else if rel eq 'lessp then minusf lhs
ofsfsiat.red:   else if rel eq 'greaterp then not (minusf lhs or null lhs)
ofsfsism.red:	 a := if op eq 'and then car atl else ofsf_negateat car atl;
ofsfsism.red:	    if cdr w eq 'false then <<
ofsfsism.red:   if op eq 'and then
ofsfsism.red:   else  % [op eq 'or]
ofsfsism.red:      if w eq 'neq then
ofsfsism.red:      	    if car ne eq 'lessp then
ofsfsism.red:	    % We know [car ne eq 'greaterp].
ofsfsism.red:      if w eq 'neq then
ofsfsism.red:      	    if car ne eq 'lessp then
ofsfsism.red:	    % We know [car ne eq 'greaterp]!
ofsfsism.red:      	 % We know [car ne eq 'equal].
ofsfsism.red:   ofsf_0mk2(ofsf_clnegrel(car entry,op eq 'and),numr addsq(parasq,cdr entry));
ofsfsism.red:      if w eq 'false then return 'false;
ofsfsism.red:      if w eq 'true then return db;
ofsfsism.red:	 if w eq 'true then <<
ofsfsism.red:	 >> else if w eq 'false then <<
ofsfsism.red:      if a eq 'false then return 'false;
ofsfsism.red:      if a eq 'true then return db;
ofsfsism.red:      	 if w eq 'false then return 'false;
ofsfsism.red:	 if r1 eq w then return 'true;
redlog.red:      if nop eq 'and then 'true else 'false
redlog.red:   x eq 'ex or x eq 'all;
redlog.red:   x eq 'or or x eq 'and;
redlog.red:   rl_junctp x or x eq 'not;
redlog.red:   x eq 'impl or x eq 'repl or x eq 'equiv;
redlog.red:   x eq 'true or x eq 'false;
rlami.red:   if u eq 'true or u eq 'false then
rlami.red:	 if w eq 'logical or w eq 'equation or w eq 'scalar then
rlami.red:   if u eq 'fvarl then 'fvarl else rl_a2s!-varl u;
rlami.red:   if f eq 'inctheo then rederr "inconsistent theory" else rl_mk!*fof f;
rlami.red:   if res eq 'inctheo then
rlami.red:   if res eq 'inctheo then
rlami.red:   if res eq 'inctheo then
rlami.red:   if res eq 'infeasible then
rlami.red:   if !*mode eq 'symbolic then
rlami.red:   if !*mode eq 'symbolic then