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