redlog/ofsf/ofsfsiat.red

64       if w eq 'stsq then return 'false;
67       if ww eq 'stsq then return 'false;
101       if w eq 'stsq then return 'true;
104       if ww eq 'stsq then return 'true;
152       if (s1 := ofsf_posdefp lhs) eq 'stsq then
155       if (s2 := ofsf_posdefp w) eq 'stsq then
167       if s1 eq 'stsq then
171       if ofsf_posdefp cdr x eq 'stsq then
178       if ofsf_posdefp car x eq 'stsq then
181       if ofsf_posdefp w eq 'stsq then <<
195       if not (ofsf_posdefp car x eq 'stsq) then
211       if ofsf_posdefp cdr x eq 'stsq then
223       if s1 eq 'stsq then
225       else if s2 eq 'stsq then <<
248       if ofsf_posdefp cdr x eq 'stsq then
260       if s1 eq 'stsq then
262       else if s2 eq 'stsq then <<
280       if (s1 := ofsf_posdefp lhs) eq 'stsq then
283       if (s2 := ofsf_posdefp w) eq 'stsq then  % Proposition 3.3 (ii)
295       if s1 eq 'stsq then  % in particular, 1 is an stsq.
299       if ofsf_posdefp cdr x eq 'stsq then
306       if ofsf_posdefp car x eq 'stsq then
309       if ofsf_posdefp w eq 'stsq then <<
335    % an SF. Returns ['stsq] if [u] is positive definite, ['tsq] if [u]
343    % positive QE. [u] is an SF. Returns ['stsq] if [u] is positive
351    % positive QE subroutine. [u] is an SF. Returns ['stsq] if [u] is
354       (if not minusf u then 'stsq)