CGBLisp User Guide and Manual

Marek Rychlik December 24, 1997

Contents

1 The Gröbner Basis package 1 2 The String Interface to the Gröbner Basis package 10 3 The Comprehensive Gröbner basis package 12 4 The Coefficient Ring package 17 5 The Division Package 18 6 The Dynamical Systems package 18 7 The Geometric Theorem Prover package 21 8 The Monomial Order Package 22 9 The Polynomial Package 23 10 The Parser Package 25 11 Other packages 27 A All examples produced by the all-examples utility 35

1 The Gröbner Basis package

*grobner−debug* nil [VARIABLE]

If T, produce debugging and tracing output. *buchberger−merge−pairs* ’buchberger−merge−pairs−smallest−lcm [VARIABLE]

A variable holding the predicate used to sort critical pairs in the order of decreasing priority for the Buchberger algorithm.

*gebauer−moeller−merge−pairs* ’gebauer−moeller−merge−pairs−use−mock−spoly [VARIABLE] A variable holding the predicate used to sort critical pairs in the order of decreasing priority for the Gebauer−Moeller algorithm

*grobner−function* ’buchberger [VARIABLE] The name of the function used to calculate Grobner basis select−grobner−algorithm algorithm [FUNCTION ]

Select one of the several implementations of the Grobner basis algorithm.

grobner f &optional (pred #’lex>) (start 0) (top−reduction−only nil) (ring *coefficient−ring*) [FUNCTION ]

Return Grobner basis of an ideal generated by polynomial list F. Assume that the monomials of each polynomial are ordered according to the admissible monomial order PRED. The result will be a list of polynomials ordered as well according to PRED. The polynomials from 0 to START−1 in the list F are assumed to be a Grobner basis, and thus certain critical pairs do not have to be calculated. If TOP−REDUCTION−ONLY is not NIL then only top reductions will be performed, instead of full division, and thus the returned Grobner basis will have its polynomials only top−reduced with respect to the preceding polynomials. RING should be set to the RING structure (see COEFFICIENT−RING package) corresponding to the coefficients of the polynomials in the list F. This function is currently just an interface to several algorithms which fine Grobner bases. Use SELECT−GROBNER−ALGORITHM in order to change the algorithm.

debug−cgb &rest args [MACRO]

This macro is used in printing debugging and tracing messages and its arguments are analogous to the FORMAT function, except that the stream argument is omitted. By default, the output is sent to *trace−output*, which can be set to produce output in a file.

spoly f g pred ring [FUNCTION ]

Return the S−polynomial of F and G, which should be two polynomials with terms ordered by PRED and coefficients in a ring whose operations are the slots of the RING structure.

grobner−primitive−part p ring [FUNCTION ]

Divide polynomial P with integer coefficients by gcd of its coefficients and return the result. Use the RING structure from the COEFFICIENT−RING package to perform the operations on the coefficients.

grobner−content p ring [FUNCTION ]

Greatest common divisor of the coefficients of the polynomial P. Use the RING structure to compute the greatest common divisor.

normal−form f fl pred top−reduction−only ring [FUNCTION ]

Calculate the normal form of the polynomial F with respect to the polynomial list FL. Destructive to F; thus, copy−tree should be used where F needs to be preserved. It returns multiple values. The first value is the polynomial R which is reduced (or top−reduced if TOP−REDUCTION−ONLY is not NIL). The second value is an integer which is the number of reductions actually performed. The third value is the coefficient by which F needs to be multiplied in order to be able to perform the division without actually having to divide in the coefficient ring (a form of pseudo−division is used). All operations on the coefficients are performed using the RING structure from the COEFFICIENT−RING package. buchberger f pred start top−reduction−only ring &aux (s (1− (length f))) b m [FUNCTION ]

An implementation of the Buchberger algorithm. Return Grobner basis of the ideal generated by the polynomial list F. The terms of each polynomial are ordered by the admissible monomial order PRED. Polynomials 0 to START−1 are assumed to be a Grobner basis already, so that certain critical pairs will not be examined. If TOP−REDUCTION−ONLY set, top reduction will be preformed. The RING structure is used to perform operations on coefficents (see COEFFICIENT−RING package).

grobner−op c1 c2 m a b pred ring &aux n a1 a2 [FUNCTION ]

Perform a calculation equivalent to (POLY− (SCALAR−TIMES−POLY C2 A) (SCALAR−TIMES−POLY C1 (MONOM−TIMES−POLY M B)) PRED) but more efficiently; it destructively modifies A and stores the result in it; A is returned.

buchberger−sort−pairs b g pred ring [FUNCTION ]

Sort critical pairs B by the function which is the value of the vairable *buchberger−merge−pairs*. G is the list of polynomials which the elemnts of B point into. PRED is the admissible monomial order. The RING structure holds operations on the coefficients as described in the COEFFICIENT−RING package.

mock−spoly f g pred [FUNCTION ]

Returns an upper−bound on the leading monomial of the S−polynomial of F and G, which are two polynomials sorted by the admissible monomial order PRED.

buchberger−merge−pairs−use−mock−spoly b c g pred ring [FUNCTION ]

Merges lists of critical pairs B and C into one list. The pairs are assumed to be ordered according to the increasing value of MOCK−SPOLY, as determined by the admissible monomial order PRED. G is the list of polynomials which the pairs of integers in B and C point into, and RING is the ring structure defined in the COEFFICIENT−RING package.

buchberger−merge−pairs−smallest−lcm b c g pred ring [FUNCTION ]

Merges lists of critical pairs B and C into a single ordered list. Implements a strategy of ordering pairs according to the smallest lcm of the leading monomials of the two polynomials − so called normal strategy.

buchberger−merge−pairs−use−smallest−degree b c g pred ring [FUNCTION ]

Mergest lists B and C of critical pairs. This strategy is based on ordering the pairs according to the smallest degree of the lcm of the leading monomials of the two polynomials.

buchberger−merge−pairs−use−smallest−length b c g pred ring [FUNCTION ]

Mergest lists B and C of critical pairs. This strategy is based on ordering the pairs according to the smallest total length of the two polynomials, where length is the number of terms.

buchberger−merge−pairs−use−smallest−coefficient−length b c g pred ring [FUNCTION ]

Mergest lists B and C of critical pairs. This strategy is based on ordering the pairs according to the smallest combined length of the coefficients of the two polynomials.

buchberger−set−pair−heuristic method  &aux  (strategy−fn  (ecase method  (:minimal−mock−spoly #’buchberger−merge−pairs−use−mock−spoly) (:minimal−lcm #’buchberger−merge−pairs−smallest−lcm) (:minimal−total−degree #’buchberger−merge−pairs−use−smallest−degree) (:minimal−length #’buchberger−merge−pairs−use−smallest−length) (:minimal−coefficient−length #’buchberger−merge−pairs−use−smallest−coefficient−length))) [FUNCTION ]

Simply sets the variable *buchberger−merge−pairs* to the heuristic function STRATEGY−FN implementing one of several strategies introduces before of selecting the most promising. METHOD should be one of the listed keywords.

criterion−1 pair g &aux (i (first pair)) (j (second pair)) [FUNCTION ]

Returns T if the leading monomials of the two polynomials in G pointed to by the integers in PAIR have disjoint (relatively prime) monomials. This test is known as the first Buchberger criterion.

criterion−2 pair g m &aux (i (first pair)) (j (second pair)) [FUNCTION ]

Returns T if the leading monomial of some element P of G divides the LCM of the leading monomials of the two polynomials in the polynomial list G, pointed to by the two integers in PAIR, and P paired with each of the polynomials pointed to by the the PAIR has already been treated, as indicated by the hash table M, which stores value T for every treated pair so far.

normalize−poly p ring [FUNCTION ]

Divide a polynomial by its leading coefficient. It assumes that the division is possible, which may not always be the case in rings which are not fields. The exact division operator is assumed to be provided by the RING structure of the COEFFICIENT−RING package.

normalize−basis plist ring [FUNCTION ]

Divide every polynomial in a list PLIST by its leading coefficient. Use RING structure to perform the division of the coefficients.

reduction p pred ring [FUNCTION ]

Reduce a list of polynomials P, so that non of the terms in any of the polynomials is divisible by a leading monomial of another polynomial. Return the reduced list.

reduced−grobner f &optional (pred #’lex>) (start 0) (top−reduction−only nil) (ring *coefficient−ring*) [FUNCTION ]

Return the reduced Grobner basis of the ideal generated by a polynomial list F. This combines calls to two functions: GROBNER and REDUCTION. The parameters have the same meaning as in GROBNER or BUCHBERGER.

monom−depends−p m k [FUNCTION ]

Return T if the monomial M depends on variable number K.

term−depends−p term k [FUNCTION ]

Return T if the term TERM depends on variable number K. poly−depends−p p k [FUNCTION ]

Return T if the term polynomial P depends on variable number K.

ring−intersection plist k &key (key #’identity) [FUNCTION ]

This function assumes that polynomial list PLIST is a Grobner basis and it calculates the intersection with the ring R[x[k+1],...,x[n]], i.e. it discards polynomials which depend on variables x[0], x[1], ..., x[k].

elimination−ideal flist k &key (primary−order #’lex>) (secondary−order #’lex>) (start 0) (order (elimination−order k :primary−order primary−order :secondary−order secondary−order)) (top−reduction−only nil) (ring *coefficient−ring*) [FUNCTION ]

Returns the K−th elimination ideal of the ideal generated by polynomial list FLIST. Thus, a Grobner basis of the ideal generated by FLIST is calculated and polynomials depending on variables 0−K are discarded. The monomial order in the calculation is an elimination order formed by combining two orders: PRIMARY−ORDER used on variables 0−K and SECONDARY−ORDER used on variables starting from variable K+1. Thus, if both orders are set to the lexicographic order #’LEX> then the resulting order is simply equivalent to #’LEX>. But one could use arbitrary two orders in this function, for instance, two copies of #’GREVLEX> (see ORDER package). When doing so, the caller must ensure that the same order has been used to sort the terms of the polynomials FLIST.

ideal−intersection f g pred top−reduction−only ring [FUNCTION ]

Return the Grobner basis of the intersection of the ideals generated by the polynomial lists F and G. PRED is an admissible monomial order with respect to which the terms of F and G have been sorted. This order is going to be used in the Grobner basis calculation. If TOP−REDUCTION−ONLY is not NIL, internally the Grobner basis algorithm will perform top reduction only. The RING parameter, as usual, should be set to a structure defined in the package COEFFICIENT−RING, and it will be used to perform all operations on coefficients.

poly−contract f &optional (k 1) [FUNCTION ]

Return a polynomial obtained from polynomial F by dropping the first K variables, if F does not depend on them. Note that this operation makes the polynomial incompatible for certain arithmetical operations with the original polynomial F. Calling this function on a polynomial F which does depend on variables 0−K will result in error.

poly−lcm f g &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Return LCM (least common multiple) of two polynomials F and G. The polynomials must be ordered according to monomial order PRED and their coefficients must be compatible with the RING structure defined in the COEFFICIENT−RING package.

grobner−gcd f g &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Return GCD (greatest common divisor) of two polynomials F and G. The polynomials must be ordered according to monomial order PRED and their coefficients must be compatible with the RING structure defined in the COEFFICIENT−RING package.

grobner−equal g1 g2 &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Returns T if two lists of polynomials G1 and G2, assumed to be Grobner bases, generate the same ideal, and NIL otherwise. grobner−subsetp g1 g2 &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Returns T if a list of polynomials G1 generates an ideal contained in the ideal generated by a polynomial list G2, both G1 and G2 assumed to be Grobner bases. Returns NIL otherwise.

grobner−member p g &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Returns T if a polynomial P belongs to the ideal generated by the polynomial list G, which is assumed to be a Grobner basis. Returns NIL otherwise.

ideal−equal f1 f2 pred top−reduction−only ring [FUNCTION ]

Returns T if two ideals generated by polynomial lists F1 and F2 are identical. Returns NIL otherwise.

ideal−subsetp f1 f2 &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Returns T if the ideal spanned by the polynomial list F1 is contained in the ideal spanned by the polynomial list F2. Returns NIL otherwise.

ideal−member p plist pred top−reduction−only ring [FUNCTION ]

Returns T if the polynomial P belongs to the ideal spanned by the polynomial list PLIST, and NIL otherwise.

ideal−saturation−1 f p pred start top−reduction−only ring &aux (pred (elimination−order−1 pred)) [FUNCTION ]

Returns the reduced Grobner basis of the saturation of the ideal generated by a polynomial list F in the ideal generated by a single polynomial P. The saturation ideal is defined as the set of polynomials H such for some natural number n (* (EXPT P N) H) is in the ideal F. Geometrically, over an algebraically closed field, this is the set of polynomials in the ideal generated by F which do not identically vanish on the variety of P.

add−variables plist n [FUNCTION ]

Add N new variables, adn the first N variables, to every polynomial in polynomial list PLIST. The resulting polynomial will not depend on these N variables.

extend−polynomials plist &aux (k (length plist)) [FUNCTION ]

Returns polynomial list {U1*P1’, U2*P2’, ... , UK*PK’} where Ui are new variables and PLIST={P1, P2, ... , PK} is a polynomial list. PI’ is obtained from PI by adding new variables U1, U2, ..., UN UK as the first K variables. Thus, the resulting list is consists of polynomials whose terms are ordered by the lexicographic order on variables UI, with ties resolved by the monomial order which was used to order the terms of the polynomials in PLIST. We note that the monomial order does not explicitly participate in this calculation, and neither do the variable names.

saturation−extension f plist ring &aux (k (length plist)) (d (+ k (length (caaar plist)))) [FUNCTION ]

Returns F’ union {U1*P1−1,U2*P2−1,...,UK*PK−1} where Ui are new variables and F’ is a polynomial list obtained from F by adding variables U1, U2, ..., Uk as the first K variables to each polynomial in F. Thus, the resulting list is consists of polynomials whose terms are ordered by the lexicographic order on variables Ui, with ties resolved by the monomial order which was used to order the terms of the polynomials in F. We note that the monomial order does not explicitly participate in this calculation, and neither do the variable names. polysaturation−extension f plist ring &aux (k (length plist)) (d (+ k (length (caaar plist)))) [FUNCTION ]

Returns F’ union {U1*P1+U2*P2+UK*PK−1} where Ui are new variables and F’ is a polynomial list obtained from F by adding variables U1, U2, ..., Uk as the first K variables to each polynomial in F. Thus, the resulting list is consists of polynomials whose terms are ordered by the lexicographic order on variables Ui, with ties resolved by the monomial order which was used to order the terms of the polynomials in F. We note that the monomial order does not explicitly participate in this calculation, and neither do the variable names.

saturation−extension−1 f p ring [FUNCTION ]

Return the list F’ union {U*P−1} where U is a new variable, where F’ is obtained from the polynomial list F by adding U as the first variable. The variable U will be added as the first variable, so that it can be easily eliminated.

ideal−polysaturation−1 f plist pred start top−reduction−only ring [FUNCTION ]

Returns the reduced Grobner basis of the ideal obtained by a sequence of successive saturations in the polynomials of the polynomial list PLIST of the ideal generated by the polynomial list F.

ideal−saturation f g pred start top−reduction−only ring &aux (k (length g)) (pred (elimination−order k :primary−order #’lex> :secondary−order pred)) [FUNCTION ]

Returns the reduced Grobner basis of the saturation of the ideal generated by a polynomial list F in the ideal generated a polynomial list G The saturation ideal is defined as the set of polynomials H such for some natural number n and some P in the ideal generated by G the polynomial P**N

* H is in the ideal spanned by F. Geometrically, over an algebraically closed field, this is the set of polynomials in the ideal generated by F which do not identically vanish on the variety of G.

ideal−polysaturation f ideal−list pred start top−reduction−only ring [FUNCTION ]

Returns the reduced Grobner basis of the ideal obtained by a successive applications of IDEAL−SATURATIONS to F and lists of polynomials in the list IDEAL−LIST.

buchberger−criterion g pred ring [FUNCTION ]

Returns T if G is a Grobner basis, by using the Buchberger criterion: for every two polynomials h1 and h2 in G the S−polynomial S(h1,h2) reduces to 0 modulo G.

grobner−test g f pred ring [FUNCTION ]

Test whether G is a Grobner basis and F is contained in G. Return T upon success and NIL otherwise.

minimization p pred [FUNCTION ]

Returns a sublist of the polynomial list P spanning the same monomial ideal as P but minimal, i.e. no leading monomial of a polynomial in the sublist divides the leading monomial of another polynomial.

add−minimized f gred pred [FUNCTION ]

Adds a polynomial f to GRED, reduced Grobner basis, preserving the property described in the documentation for MINIMIZATION. colon−ideal f g pred top−reduction−only ring [FUNCTION ]

Returns the reduced Grobner basis of the colon ideal Id(F):Id(G), where F and G are two lists of polynomials. The colon ideal I:J is defined as the set of polynomials H such that there is a polynomial W in J for which W*H belongs to I.

colon−ideal−1 f g pred top−reduction−only ring [FUNCTION ]

Returns the reduced Grobner basis of the colon ideal Id(F):Id({G}), where F is a list of polynomials and G is a polynomial.

pseudo−divide f fl pred ring [FUNCTION ]

Pseudo−divide a polynomial F by the list of polynomials FL. Return multiple values. The first value is a list of quotients A. The second value is the remainder R. The third value is an integer count of the number of reductions performed. Finally, the fourth argument is a scalar coefficient C, such that C*F can be divided by FL within the ring of coefficients, which is not necessarily a field. The resulting objects satisfy the equation: C*F= sum A[i]*FL[i] + R

gebauer−moeller f pred start top−reduction−only ring &aux b g f1 [FUNCTION ]

Compute Grobner basis by using the algorithm of Gebauer and Moeller. This algorithm is described as BUCHBERGERNEW2 in the book by Becker−Weispfenning entitled “Grobner Bases”

update g b h pred ring &aux c d e b−new g−new pair [FUNCTION ]

An implementation of the auxillary UPDATE algorithm used by the Gebauer−Moeller algorithm. G is a list of polynomials, B is a list of critical pairs and H is a new polynomial which possibly will be added to G. The naming conventions used are very close to the one used in the book of Becker−Weispfenning.

gebauer−moeller−merge−pairs−use−mock−spoly b c pred ring [FUNCTION ]

The merging strategy used by the Gebauer−Moeller algorithm, based on MOCK−SPOLY; see the documentation of BUCHBERGER−MERGE−PAIRS−USE−MOCK−SPOLY.

gebauer−moeller−merge−pairs−smallest−lcm b c pred ring [FUNCTION ]

The merging strategy based on the smallest−lcm (normal strategy); see the documentation of BUCHBERGER−MERGE−PAIRS−SMALLEST−LCM.

gebauer−moeller−merge−pairs−use−smallest−degree b c pred ring [FUNCTION ]

The merging strategy based on the smallest−lcm (normal strategy); see the documentation of BUCHBERGER−MERGE−PAIRS−USE−SMALLEST−DEGREE.

gebauer−moeller−merge−pairs−use−smallest−length b c pred ring [FUNCTION ]

gebauer−moeller−merge−pairs−use−smallest−coefficient−length b c pred ring [FUNCTION ]

The merging strategy based on the smallest−lcm (normal strategy); see the documentation of BUCHBERGER−MERGE−PAIRS−USE−SMALLEST−COEFFICIENT−LENGTH.

gebauer−moeller−set−pair−heuristic method  &aux  (strategy−fn  (ecase method  (:minimal−mock−spoly #’gebauer−moeller−merge−pairs−use−mock−spoly) (:minimal−lcm #’gebauer−moeller−merge−pairs−smallest−lcm) (:minimal−total−degree #’gebauer−moeller−merge−pairs−use−smallest−degree) (:minimal−length #’gebauer−moeller−merge−pairs−use−smallest−length) (:minimal−coefficient−length #’gebauer−moeller−merge−pairs−use−smallest−coefficient−length))) [FUNCTION ]

spoly−sugar f−with−sugar g−with−sugar ring [FUNCTION ]

Calculate the “sugar” of the S−polynomial of two polynomials with sugar. A polynomial with sugar is simply a pair (P . SUGAR) where SUGAR is an integer constant defined according to the following algorighm: the sugar of sum or difference of two polynomials with sugar is the MAX of the sugars of those two polynomials. The sugar of a product of a term and a polynomial is the sum of the degree of the term and the sugar of the polynomial. The idea is to accumulate sugar as we perform the arithmetic operations, and that polynomials with small (little) sugar should be given priority in the calculations. Thus, the “sugar strategy” of the critical pair selection is to select a pair with the smallest value of sugar of the resulting S−polynomial.

spoly−with−sugar f−with−sugar g−with−sugar pred ring [FUNCTION ]

The S−polynomials of two polynomials with SUGAR strategy.

normal−form−with−sugar f fl pred top−reduction−only ring [FUNCTION ]

Normal form of the polynomial with sugar F with respect to a list of polynomials with sugar FL. Assumes that FL is not empty. Parameters PRED, TOP−REDUCTION−ONLY and RING have the same meaning as in NORMAL−FORM. The parameter SUGAR−LIMIT should be set to a positive integer. If the sugar limit of the partial remainder exceeds SUGAR−LIMIT then the calculation is stopped and the partial remainder is returned, although it is not fully reduced with respect to FL.

buchberger−with−sugar f−no−sugar pred start top−reduction−only ring &aux (s (1− (length f−no−sugar))) b m f [FUNCTION ]

Returns a Grobner basis of an ideal generated by a list of ordinary polynomials F−NO−SUGAR. Adds initial sugar to the polynomials and performs the Buchberger algorithm with “sugar strategy”. It returns an ordinary list of polynomials with no sugar. One of the most effective algorithms for Grobner basis calculation.

buchberger−with−sugar−merge−pairs b c g m pred ring [FUNCTION ]

Merges lists of critical pairs. It orders pairs according to increasing sugar, with ties broken by smaller MOCK−SPOLY value of the two polynomials. In this function B must already be sorted.

buchberger−with−sugar−sort−pairs c g m pred ring [FUNCTION ]

Sorts critical pairs C according to sugar strategy.

criterion−1−with−sugar pair g &aux (i (first pair)) (j (second pair)) [FUNCTION ]

An implementation of Buchberger’s first criterion for polynomials with sugar. See the documentation of BUCHBERGER−CRITERION−1. criterion−2−with−sugar pair g m &aux (i (first pair)) (j (second pair)) [FUNCTION ]

An implementation of Buchberger’s first criterion for polynomials with sugar. See the documentation of BUCHBERGER−CRITERION−2.

gebauer−moeller−with−sugar f pred start top−reduction−only ring &aux b g f1 [FUNCTION ]

Compute Grobner basis by using the algorithm of Gebauer and Moeller. This algorithm is described as BUCHBERGERNEW2 in the book by Becker−Weispfenning entitled “Grobner Bases”

update−with−sugar g b h pred ring &aux c d e b−new g−new pair [FUNCTION ]

An implementation of the auxillary UPDATE algorithm used by the Gebauer−Moeller algorithm. G is a list of polynomials, B is a list of critical pairs and H is a new polynomial which possibly will be added to G. The naming conventions used are very close to the one used in the book of Becker−Weispfenning. Operates on polynomials with sugar.

gebauer−moeller−with−sugar−merge−pairs b c pred ring [FUNCTION ]

Merges lists of critical pairs. It orders pairs according to increasing sugar, with ties broken by smaller lcm of head monomials In this function B must already be sorted. Operates on polynomials with sugar.

grobner−primitive−part−with−sugar h ring [FUNCTION ]

2 The String Interface to the Gröbner Basis package

string−normal−form f fl vars &key (stream t) (print t) (order #’lex>) (top−reduction−only nil) (ring *coefficient−ring*) (suppress−value t) &aux (vars (read−vars vars)) [FUNCTION ]

string−grobner plist vars &key (order #’lex>) (start 0) (stream t) (reduce t) (reduce−before t) (suppress−value t) (top−reduction−only nil) (ring *coefficient−ring*) (print t) &aux (vars (read−vars vars)) [FUNCTION ]

string−elimination−ideal flist vars k &key (stream t) (key #’identity) (primary−order #’grevlex>) (secondary−order #’grevlex>) (suppress−value t) (order (elimination−order k :primary−order primary−order :secondary−order secondary−order)) &aux (vars (read−vars vars)) [FUNCTION ]

string−ideal−intersection f g vars &key (order #’lex>) (top−reduction−only nil) (ring *coefficient−ring*) (stream t) (suppress−value t) &aux (vars (read−vars vars)) (f (parse−string−to−sorted−alist f vars or- der)) (g (parse−string−to−sorted−alist g vars order)) [FUNCTION ] string−poly−lcm f g vars &key (order #’lex>) (ring *coefficient−ring*) (stream t) (suppress−value t) &aux (vars (read−vars vars)) (f (parse−string−to−sorted−alist f vars order)) (g (parse−string−to−sorted−alist g vars order)) [FUNCTION ] string−ideal−saturation−1 f p vars &key (order #’lex>) (start 0) (top−reduction−only nil) (ring *coefficient−ring*) (stream t) (suppress−value t) &aux (vars (read−vars vars)) (f (parse−string−to−sorted−alist f vars order)) (p (parse−string−to−sorted−alist p vars order)) [FUNCTION ] string−ideal−polysaturation−1 f plist vars &key (order #’lex>) (start 0) (top−reduction−only nil) (ring *coefficient−ring*) (stream t) (suppress−value t) &aux (vars (read−vars vars)) (f (parse−string−to−sorted−alist f vars order)) (plist (parse−string−to−sorted−alist plist vars order)) [FUNCTION ] string−ideal−saturation f g vars &key (order #’lex>) (start 0) (top−reduction−only nil) (ring *coefficient−ring*) (stream t) (suppress−value t) &aux (vars (read−vars vars)) (f (parse−string−to−sorted−alist f vars order)) (g (parse−string−to−sorted−alist g vars order)) [FUNCTION ] string−ideal−polysaturation f ideal−list vars &key (order #’lex>) (start 0) (top−reduction−only nil) (ring *coefficient−ring*) (stream t) (suppress−value t) &aux (vars (read−vars vars)) (f (parse−string−to−sorted−alist f vars order)) (ideal−list (mapcar #’(lambda (g) (parse−string−to−sorted−alist g vars order)) ideal−list)) [FUNCTION ]

string−colon−ideal f g vars &key (top−reduction−only nil) (ring *coefficient−ring*) (stream t) (order #’lex>) (suppress−value t) &aux (vars (read−vars vars)) (f (parse−string−to−sorted−alist f vars order)) (g (parse−string−to−sorted−alist g vars order)) [FUNCTION ] string−read−poly f vars &key (order #’lex>) (suppress−value nil) (stream t) (convert−rational−to−integer t) &aux (vars (read−vars vars)) (f (parse−string−to−sorted−alist f vars order)) [FUNCTION ] poly−rational−to−integer p &optional (ring *coefficient−ring*) [FUNCTION ] read−vars string−or−list [FUNCTION ]

Read a list of variables, specified either as a list of symbols or a string listing variables in the form of a comma−separated list, delimited by [,]

3 The Comprehensive Gröbner basis package

*colored−poly−debug* nil [VARIABLE]

If true debugging output is on.

debug−cgb &rest args [MACRO]

make−colored−poly poly k &key (key #’identity) (main−order #’lex>) (parameter−order #’lex>) &aux l [FUNCTION ]

Colored poly is represented as a list (TERM1 TERM2 ... TERMS) where each term is a triple (MONOM . (POLY . COLOR)) where monoms and polys have common number of variables while color is one of the three: :RED, :GREEN or :WHITE. This function translates an ordinary polynomial into a colored one by dividing variables into K and N−K, where N is the total number of variables in the polynomial poly; the function KEY can be called to select variables in arbitrary order.

make−colored−poly−list plist &rest rest [FUNCTION ]

Translate a list of polynomials PLIST into a list of colored polynomials by calling MAKE−COLORED−POLY. Returns the resulting list.

color−poly−list flist &optional (cond (list nil nil)) [FUNCTION ]

Add colors to an ordinary list of polynomials FLIST, according to a condition COND. A condition is a pair of polynomial lists. Each polynomial in COND is a polynomial in parameters only. The list (FIRST COND) is called the “green list” and it consists of polynomials which vanish for the parameters associated with the condition. The list (SECOND COND) is called the “red list

color−poly f &optional (cond (list nil nil)) [FUNCTION ]

Add color to a single polynomial F, according to condition COND. See the documentation of COLOR−POLY−LIST.

colored−poly−to−poly cpoly [FUNCTION ]

For a given colored polynomial CPOLY, removes the colors and it returns the polynomial as an ordinary polynomial with coefficients which are polynomials in parameters.

colored−poly−print poly vars &key (stream t) (beg t) (print−green−part nil) (mark−coefficients nil) [FUNCTION ]

Print a colored polynomial POLY. Use variables VARS to represent the variables. Some of the variables are going to be used as parameters, according to the length of the monomials in the main monomial and coefficient part of each term in POLY. The key variable STREAM may be used to redirect the output. If parameter PRINT−GREEN−PART is set then the coefficients which have color :GREEN will be printed, otherwise they are discarded silently. If MARK−COEFFICIENTS is not NIL then every coefficient will be marked according to its color, for instance G(U−1) would mean that U−1 is in the green list. Returns P.

colored−poly−print−list poly−list vars &key (stream t) (beg t) (print−green−part nil) (mark−coefficients nil) [FUNCTION ]

Pring a list of colored polynomials via a call to COLORED−POLY−PRINT. determine f &optional (cond (list nil nil)) (order #’lex>) (ring *coefficient−ring*) [FUNCTION ]

This function takes a list of colored polynomials F and a condition COND, and it returns a list of pairs (COND’ F’) such that COND’ cover COND and F’ is a “determined” version of the colored polynomial list F, i.e. every polynomial has its leading coefficient determined. This means that some of the initial coefficients in each polynomial in F’ are in the green list of COND, and the first non−green coefficient is in the red list of COND. We note that F’ differs from F only by different colors: some of the terms marked :WHITE are now marked either :GREEN or :RED. Coloring is done either by explicitly checking membership in red or green list of COND, or implicitly by performing Grobner basis calculations in the polynomial ring over the parameters. The admissible monomial order ORDER is used only in the parameter space. Also, the ring structure RING is used only for calculations on polynomials of the parameters only.

determine−1 cond p end gp order ring [FUNCTION ]

Determine a single colored polynomial P according to condition COND. Prepend green part GP to P. Cons the result with END, which should be a list of colored polynomials, and return the resulting list of polynomials. This is an auxillary function of DETERMINE.

determine−white−term cond term restp end gp order ring [FUNCTION ]

This is an auxillary function of DETERMINE. In this function the parameter COND is a condition. The parameters TERM, RESTP and GP are three parts of a polynomial being processed, where TERM is colored :WHITE. We test the membership in the red and green list of COND we try to determine whether the term is :RED or :GREEN. This is done by performing ideal membership tests in the polynomial ring. Let C be the coefficient of TERM. Thus, C is a polynomial in parameters. We find whether C is in the green list by performing a plain ideal membership test. However, to test properly whether C is in the red list, one needs a different strategy. In fact, we test whether adding C to the red list would produce a non−empty set of parameters in some algebraic extension. The test is whether 1 belongs to the saturation ideal of (FIRST COND) in (CONS C (SECOND COND)). Thus, we use POLY−SATURATION. If we are successful in determining the color of TERM, we simply change the color of the term and return the list ((COND P)) where P is obtained by appending GP, (LIST TERM) and RESTP. If we cannot determine whether TERM is :RED or :GREEN, we return the list ((COND’ P’) (COND” P

cond−system−print system vars params &key (suppress−value t) (print−green−part nil) (mark−coefficients nil) &aux (label 0) [FUNCTION ]

A conditional system SYSTEM is a list of pairs (COND PLIST), where COND is a condition (a pair (GREEN−LIST RED−LIST)) and PLIST is a list of colored polynomials. This function pretty−prints this list of pairs. A conditional system is the data structure returned by GROBNER−SYSTEM. This function returns SYSTEM, if SUPPRESS−VALUE is non−NIL and no value otherwise. If MARK−COEFFICIENTS is non−NIL coefficients will be marked as in G(u−1)*x+R(2)*y, which means that u−1 is :GREEN and 2 is :RED.

cond−print cond params [FUNCTION ]

Pretty−print a condition COND, using symbol list PARAMS as parameter names.

add−pairs gs pred [FUNCTION ]

The parameter GS shoud be a Grobner system, i.e. a set of pairs (CONDITION POLY−LIST) This functions adds the third component: the list of initial critical pairs (I J), as in the ordinary Grobner basis algorithm. In addition, it adds the length of of the POLY−LIST, less 1, as the fourth component. The resulting list of quadruples is returned. cond−part p [FUNCTION ]

Find the part of a colored polynomial P starting with the first non−green term.

cond−hm p [FUNCTION ]

Return the conditional head monomial of a colored polynomial P.

delete−green−polys gamma [FUNCTION ]

Delete totally green polynomials from in a grobner system GAMMA.

grobner−system f &key (cover (list ’(nil nil))) (main−order #’lex>) (parameter−order #’lex>) (reduce t) (green−reduce t) (top−reduction−only nil) (ring *coefficient−ring*) &aux (cover (saturate−cover cover parameter−order ring)) (gamma (delete−green−polys (mapcan #’(lambda (cond) (deter- mine f cond parameter−order ring)) cover))) [FUNCTION ]

This function returns a grobner system, given a list of colored polynomials F, Other parameters are: A cover COVER, i.e. a list of conditions, i.e. pairs of the form (GREEN−LIST RED−LIST), where GREEN−LIST and RED−LIST are to lists of ordinary polynomials in parameters. A monomial order MAIN−ORDER used on main variables (not parameters). A monomial order PARAMETER−ORDER used in calculations with parameters only. REDUCE, a flag deciding whether COLORED−REDUCTION will be performed on the resulting grobner system. GREEN−REDUCE, a flag deciding whether the green list of each condition will be reduced in a form of a reduced Grobner basis. TOP−REDUCTION−ONLY, a flag deciding whether in the internal calculations in the space of parameters top reduction only will be used. RING, a structure as in the package COEFFICIENT−RING, used in operations on the coefficients of the polynomials in parameters.

reorder−pairs b bnew g pred &optional (sort−first nil) [FUNCTION ]

Reorder pairs according to some heuristic. The heuristic at this time is ad hoc, in the future it should be replaced with sugar strategy and a mechanism for implementing new heuristic strategies, as in the GROBNER package.

colored−criterion−1 i j f [FUNCTION ]

Buchberger criterion 1 for colored polynomials.

colored−criterion−2 i j f b s [FUNCTION ]

Buchberger criterion 2 for colored polynomials.

cond−normal−form f fl main−order parameter−order top−reduction−only ring [FUNCTION ]

Returns the conditional normal form of a colored polynomial F with respect to the list of colored polynomials FL. The list FL is assumed to consist of determined polynomials, i.e. such that the first term which is not marked :GREEN is :RED.

cond−spoly f g main−order parameter−order ring [FUNCTION ]

Returns the conditional S−polynomial of two colored polynomials F and G. Both polynomials are assumed to be determined. cond−lm f [FUNCTION ]

Returns the conditional leading monomial of a colored polynomial F, which is assumed to be determined.

cond−lc f [FUNCTION ] Returns the conditional leading coefficient of a colored polynomial F, which is assumed to be determined.

colored−term−times−poly term f order ring [FUNCTION ]

Returns the product of a colored term TERM and a colored polynomial F. colored−scalar−times−poly c f ring [FUNCTION ]

Returns the product of an element of the coefficient ring C a colored polynomial F. colored−term* term1 term2 order ring [FUNCTION ]

Returns the product of two colored terms TERM1 and TERM2. color* c1 c2 [FUNCTION ]

Returns a product of two colores. Rules: :red * :red yields :red any * :green yields :green otherwise the result is :white.

color+ c1 c2 [FUNCTION ] Returns a sum of colors. Rules: :green + :green yields :green, :red + :green yields :red any other result is :white.

color− c1 c2 [FUNCTION ]

Identical to COLOR+. colored−poly+ p q main−order parameter−order ring [FUNCTION ]

Returns the sum of colored polynomials P and Q. colored−poly− p q main−order parameter−order ring [FUNCTION ]

Returns the difference of colored polynomials P and Q. colored−term−uminus term ring [FUNCTION ]

Returns the negation of a colored term TERM. colored−minus−poly p ring [FUNCTION ]

Returns the negation of a colored polynomial P. string−grobner−system f vars params &key (cover (list (list ”[]” ”[]”))) (main−order #’lex>) (parameter−order #’lex>) (ring *coefficient−ring*) (suppress−value t) (suppress−printing nil) (mark−coefficients nil) (reduce t) (green−reduce t) &aux (f (parse−to−colored−poly−list f vars params main−order parameter−order)) (cover (string−cover cover params parameter−order)) [FUNCTION ]

An interface to GROBNER−SYSTEM in which polynomials can be specified in infix notations as strings. Lists of polynomials are comma−separated list marked by a matchfix operators []

string−cond cond params &optional (order #’lex>) [FUNCTION ]

Return the internal representation of a condition COND, specified as pairs of strings (GREEN−LIST RED−LIST). GREEN−LIST and RED−LIST in the input are assumed to be strings which parse to two lists of polynomials with respect to variables whose names are in the list of symbols PARAMS. ORDER is the predicate used to sort the terms of the polynomials.

string−cover cover params &optional (order #’lex>) [FUNCTION ]

Returns the internal representation of COVER, given in the form of a list of conditions. See STRING−COND for description of a condition.

saturate−cover cover order ring [FUNCTION ]

Brings every condition of a list of conditions COVER to the form (G R) where G is saturated with respect to R and G is a Grobner basis We could reduce R so that the elements of R are relatively prime, but this is not currently done.

saturate−cond cond order ring [FUNCTION ]

Saturate a single condition COND. An auxillary function of SATURATE−COVER.

string−determine f vars params &key (cond ’([] [])) (main−order #’lex>) (parameter−order #’lex>) (suppress−value t) (suppress−printing nil) (mark−coefficients nil) (ring *coefficient−ring*) &aux (f (parse−to−colored−poly−list f vars params main−order parameter−order)) (cond (string−cond cond params parameter−order)) [FUNCTION ]

A string interface to DETERMINE. See the documentation of STRING−GROBNER−SYSTEM.

tidy−grobner−system gs main−order parameter−order reduce green−reduce ring [FUNCTION ]

Apply TIDY−PAIR to every pair of a Grobner system.

tidy−pair pair main−order parameter−order reduce green−reduce ring &aux gs [FUNCTION ]

Make the output of Grobner system more readable by performing certain simplifications on an element of a Grobner system. If REDUCE is non−NIL then COLORED−reduction will be performed. In addition TIDY−COND is called on the condition part of the pair PAIR.

tidy−cond cond order ring [FUNCTION ]

Currently saturates condition COND and does RED−REDUCTION on the red list. colored−reduction cond p main−order parameter−order ring &aux (open (list (list cond nil p))) closed [FUNCTION ]

Reduce a list of colored polynomials P. The difficulty as compared to the usual Buchberger algorithm is that the polys may have the same leading monomial which may result in cancellations and polynomials which may not be determined. Thus, when we find those, we will have to split the condition by calling determine. Returns a list of pairs (COND’ P’) where P’ is a reduced grobner basis with respect to any parameter choice compatible with condition COND’. Moreover, COND’ form a cover of COND.

green−reduce−colored−poly cond f parameter−order ring [FUNCTION ]

It takes a colored polynomial F and it returns a modified polynomial obtained by reducing coefficient of F modulo green list of the condition COND.

green−reduce−colored−list cond fl parameter−order ring [FUNCTION ]

Apply GREEN−REDUCE−COLORED−POLY to a list of polynomials FL.

cond−system−green−reduce gs parameter−order ring [FUNCTION ]

Apply GREEN−REDUCE−COLORED−LIST to every pair of a grobner system GS.

parse−to−colored−poly−list f vars params main−order parameter−order &aux (k (length vars)) (vars−params (append vars params)) [FUNCTION ]

Parse a list of polynomials F, given as a string, with respect to a list of variables VARS, given as a list of symbols, to the internal representation of a colored polynomial. The polynomials will be properly sorted by MAIN−ORDER, with the coefficients, which are polynomials in parameters, sorted by PARAMETER−ORDER. Both orders must be admissible monomial orders. This form is suitable for parsing polynomials with integer coefficients.

red−reduction p pred ring &aux (p (remove−if #’poly−constant−p p)) [FUNCTION ]

Takes a family of polynomials and produce a list whose prime factors are the same but they are relatively prime Repetitively used the following procedure: it finds two elements f, g of P which are not relatively prime; it replaces f and g with f/GCD(f,g), g/ GCD(f,f) and GCD(f,g).

4 The Coefficient Ring package

ring + − * / gcd lcm zerop unit length signum numerator denominator [STRUCTURE]

The structure whose slots are bound to functions performing usual ring operations. In addition to usual arithmetical operations, bindings for other common operations which increase efficiency of Grobner basis calculations are also included. They are as follows: GCD − greatest common divisor; LCM − least common multiple; ZEROP − test whether an element is zero; SIGNUM − the sign of a ring element (+1, −1 or zero); UNIT − the unit of the ring; NUMERATOR − the numerator, if a ring of fractions DENOMINATOR − the denominator, if a ring of fractions LENGTH − an integer giving the approximate length of the representation; for example, for integers its default binding is #’integer−length;

*ring−of−integers* (make−ring :+ #’+ :− #’− :* #’* :/ #’floor :gcd #’gcd :lcm #’lcm :zerop #’zerop :signum #’signum :unit 1 :length #’integer−length :nu- merator #’numerator :denominator #’denominator) [VARIABLE]

Operations in the ring of integers.

*field−of−rationals* (make−ring :+ #’+ :− #’− :* #’* :/ #’/ :gcd #’(lambda (&rest r) (declare (ignore r)) 1) :lcm #’(lambda (&rest r) (apply #’* r)) :zerop #’zerop :signum #’signum :unit 1 :length #’(lambda (x) (+ (integer−length (numerator x)) (integer−length (denominator x)))) :numerator #’numerator :denominator #’denominator) [VARIABLE]

Operations on the field of rational numbers.

field−modulo−prime modulus [FUNCTION ]

Return a RING structure with operations bound to the arithmetical operations modulo MODU-LUS, which should be a prime.

*coefficient−ring* *ring−of−integers* [VARIABLE]

The default RING structure, used in most operations on the coefficients of polynomials. It should be carefully set if rings other than the default ring is used.

5 The Division Package

divide f fl &optional (pred #’lex>) (ring *coefficient−ring*) &aux (s (length fl)) [FUNCTION ]

Divide polynomial F by a list of polynomials FL; use predicate PRED to sort monomials; assumes that the polynomials have initially been sorted according to PRED. It returnes multiple values. The first value is a list of quotients A. The second value is the remainder R. These object satisfy the quation F = SUM A[J]*FL[I] + R.

poly−exact−divide f g &optional (order #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Divide a polynomial F by another polynomial G. Assume that exact division with no remainder is possible. Returns the quotient.

6 The Dynamical Systems package

poly−scalar−composition f g &optional (order #’lex>) [FUNCTION ]

Returns a polynomial obtained by substituting a list of polynomials G=(G1,G2,...,GN) into a polynomial F(X1,X2,...,XN). All polynomials are assumed to be in the internal form, so variables do not explicitly apprear in the calculation.

poly−composition f g &optional (order #’lex>) [FUNCTION ]

Return the composition of a polynomial map F with a polynomial map G. Both maps are represented as lists of polynomials, and each polynomial is in the internal alist representation. The restriction is that the length of the list G must be the number of variables in the list F.

poly−dynamic−power f n &optional (order #’lex>) [FUNCTION ]

Calculate the composition FoFo...oF (n times), where F is a polynomial map represented as a list of polynomials.

poly−scalar−evaluate f x &optional (order #’lex>) [FUNCTION ]

Evaluate a polynomial F at a point X. This operation is implemented through POLY−SCALAR−COMPOSITION. poly−evaluate f x &optional (order #’lex>) [FUNCTION ]

Evaluate a polynomial map F, represented as list of polynomials, at a point X. factorial n &optional (k n) &aux (result 1) [FUNCTION ]

Return N!/(N−K)!=N(N−1)(N−K+1). poly−scalar−diff f m [FUNCTION ]

Return the partial derivative of a polynomial F over multiple variables according to multiindex M.

poly−diff f m [FUNCTION ] Return the partial derivative of a polynomial map F, represented as a list of polynomials, with respect to several variables, according to multi−index M.

standard−vector n k &optional (coeff 1) &aux (v (make−list n :initial−element 0)) [FUNCTION ]

Returns vector (0 0 ... 1 ... 0 0) of length N, where 1 appears on K−th place. scalar−partial f k &optional (l 1) [FUNCTION ]

Returns the L−th partial derivative of a polynomial F over the K−th variable. partial f k &optional (l 1) [FUNCTION ]

Returns the L−th partial derivative over the K−th variable, of a polynomial map F, represented as a list of polynomials.

determinant f &optional (order #’lex>) &aux (result nil) [FUNCTION ] Returns the determinant of a polynomial matrix F, which is a list of rows of the matrix, each row is a list of polynomials. The algorithm is recursive expansion along columns.

minor f i j &optional (order #’lex>) [FUNCTION ]

Calculate the minor of a polynomial matrix F with respect to entry (I,J). drop−row f i [FUNCTION ]

Discards the I−th row from a polynomial matrix F. drop−column f j [FUNCTION ]

Discards the J−th column from a polynomial matrix F. drop−elt lst j [FUNCTION ]

Discards the J−th element from a list LST. matrix− f g &optional (order #’lex>) [FUNCTION ]

Returns difference of two polynomial matrices F and G. scalar−times−matrix s f [FUNCTION ]

Returns a product of a polynomial S by a polynomial matrix F.

monom−times−matrix m f [FUNCTION ]

Returns a product of a monomial M by a polynomial matrix F.

term−times−matrix term f [FUNCTION ]

Returns a product of a term TERM by a polynomial matrix F.

poly−list− f g &optional (order #’lex>) [FUNCTION ]

Returns the list of differences of two lists of polynomials F and G (polynomial maps).

scalar−times−poly−list s f [FUNCTION ]

Returns the list of products of a polynomial S by the list of polynomials F.

monom−times−poly−list m f [FUNCTION ]

Returns the list of products of a monomial M by the list of polynomials F.

term−times−poly−list term f [FUNCTION ]

Returns the list of products of a term TERM by the list of polynomials F.

characteristic−combination a b &optional (order #’lex>) &aux (n (length b)) [FUNCTION ]

Returns A − U1 * B1 − U2 * B2 −... − UM * BM where A is a polynomial and B=(B1,B2,...,BM) is a polynomial list, where U1, U2, ... , UM are new variables. These variables will be added to every polynomial A and BI as the last M variables.

characteristic−combination−poly−list a b &optional (order #’lex>) [FUNCTION ]

Returns A − U1 * B1 − U2 * B2 − ... − UM * BM where A is a polynomial list and B=(B1, B2, ... , BM) is a list of polynomial lists, where U1, U2, ... ,UM are new variables. These variables will be added to every polynomial A and BI as the last M variables. Se also CHARACTERISTIC−COMBINATION.

characteristic−matrix a &optional (order #’lex>) (b (list (identity−matrix (length a) (length (caaaar a))))) [FUNCTION ]

Returns A − U1*B1 − U2*B2 − ... − UM * BM where A is a polynomial matrix and B=(B1,B2,...,BM) is a list of polynomial matrices, where U1, U2, .., UM are new variables. These variables will be added to every polynomial A and BI as the last M variables. Se also CHARACTERISTIC−COMBINATION.

characteristic−polynomial a &optional (order #’lex>) (b (list (identity−matrix (length a) (length (caaaar a))))) [FUNCTION ]

Returns the generalized characteristic polynomial, i.e. the determinant DET(A − U1 * B1 − U2 * B2 − ... − UM * BM), where A and BI are square polynomial matrices in N variables. The resulting polynomial will have N+M variables, with U1, U2, ..., UM added as the last M variables. identity−matrix dim nvars [FUNCTION ]

Return the polynomial matrix which is the identity matrix. DIM is the requested dimension and NVARS is the number of variables of each entry.

print−matrix f vars [FUNCTION ]

Prints a polynomial matrix F, using a list of symbols VARS as variable names.

jacobi−matrix f &optional (m (length f)) (n (length (caaaar f))) [FUNCTION ]

Returns the Jacobi matrix of a polynomial list F over the first N variables.

jacobian f &optional (order #’lex>) (m (length f)) (n (length (caaaar f))) [FUNCTION ]

Returns the Jacobian (determinant) of a polynomial list F over the first N variables.

7 The Geometric Theorem Prover package

*prover−order* #’grevlex> [VARIABLE]

Admissible monomial order used internally in the proofs of theorems.

csym symbol number [FUNCTION ]

Return symbol whose name is a concatenation of (SYMBOL−NAME SYMBOL) and a number NUMBER.

real−identical−points a b [MACRO]

Return [ (A1−B1)**2 + (A2−B2)**2 ] in lisp (prefix) notation. The second value is the list of variables (A1 B1 A2 B2). Note that if the distance between two complex points A, B is zero, it does not mean that the points are identical. Use IDENTICAL−POINTS to express the fact that A and B are really identical. Use this macro in conclusions of theorems, as it may not be possible to prove that A and B are trully identical in the complex domain.

identical−points a b [MACRO]

Return [ A1−B1, A2−B2 ] in lisp (prefix) notation. The second value is the list of variables (A1 B1 A2 B2). Note that sometimes one is able to prove only that (A1−B1)**2 + (A2−B2)**2 = 0. This equation in the complex domain has solutions with A and B distinct. Use REAL−IDENTICAL−POINTS to express the fact that the distance between two points is 0. Use this macro in assumptions of theorems, although this is seldom necessary because we assume most of the time that in assumptions all points are distinct if they are denoted by different symbols.

perpendicular a b c d [MACRO]

Return [ (A1−B1) * (C1−D1) + (A2−B2) * (C2−D2) ] in lisp (prefix) notation. The second value is the list of variables (A1 A2 B1 B2 C1 C2 D1 D2).

parallel a b c d [MACRO]

Return [ (A1−B1) * (C2−D2) − (A2−B2) * (C1−D1) ] in lisp (prefix) notation. The second value is the list of variables (A1 A2 B1 B2 C1 C2 D1 D2). collinear a b c [MACRO]

Return the determinant det([[A1,A2,1],[B1,B2,1],[C1,C2,1]]) in lisp (prefix) notation. The second value is the list of variables (A1 A2 B1 B2 C1 C2).

equidistant a b c d [MACRO]

Return the polynomial [(A1−B1)**2+(A2−B2)**2−(C1−D1)**2−(C2−D2)**2] in lisp (prefix) notation. The second value is the list of variables (A1 A2 B1 B2 C1 C2 D1 D2).

euclidean−distance a b r [MACRO]

Return the polynomial [(A1−B1)**2+(A2−B2)**2−Rˆ 2] in lisp (prefix) notation. The second value is the list of variables (A1 A2 B1 B2 R).

midpoint a b c [MACRO]

Express the fact that C is a midpoint of the segment AB. Returns the list [ 2*C1−A1−B1, 2*C2−A2−B2 ]. The second value returned is the list of variables (A1 A2 B1 B2 C1 C2).

translate−statements &rest statements [MACRO]

translate−assumptions &rest assumptions [MACRO]

translate−conclusions &rest conclusions [MACRO]

translate−theorem (&rest assumptions) (&rest conclusions) [MACRO]

Translates a planar geometry theorem into a system of polynomial equations. Each assumption or conclusion takes form of a declaration (RELATION−NAME A B C ...) where A B C are points, entered as symbols and RELATION−NAME is a name of a geometric relation, for example, (COLLINEAR A B C) means that points A, B, C are all collinear. The translated equations use the convention that (A1,A2) are the coordinates of the point A. This macro returns multiple values. The first value is a list of polynomial expressions and the second value is an automatically generated list of variables from points A, B, C, etc. For convenience, several macros have been defined in order to make specifying common geometric relations easy.

prove−theorem (&rest assumptions) (&rest conclusions) &key (order *prover−order*) [MACRO]

Proves a geometric theorem, specified in the same manner as in the macro TRANSLATE−THEOREM. The proof is achieved by a call to IDEAL−POLYSATURATION. The theorem is true if the returned value is a trivial ideal containing 1.

8 The Monomial Order Package

lex> p q &optional (start 0) (end (length p)) [FUNCTION ]

Return T if P>Q with respect to lexicographic order, otherwise NIL. The second returned value is T if P=Q, otherwise it is NIL. total−degree m &optional (start 0) (end (length m)) [FUNCTION ]

Return the todal degree of a monomoal M. grlex> p q &optional (start 0) (end (length p)) [FUNCTION ]

Return T if P>Q with respect to graded lexicographic order, otherwise NIL. The second returned value is T if P=Q, otherwise it is NIL.

grevlex> p q &optional (start 0) (end (length p)) [FUNCTION ] Return T if P>Q with respect to graded reverse lexicographic order, NIL otherwise. The second returned value is T if P=Q, otherwise it is NIL.

revlex> p q &optional (start 0) (end (length p)) [FUNCTION ] Return T if P>Q with respect to reverse lexicographic order, NIL otherwise. The second returned value is T if P=Q, otherwise it is NIL. This is not and admissible monomial order because some sets do not have a minimal element. This order is useful in constructing other orders.

invlex> p q &optional (start 0) (end (length p)) [FUNCTION ] Return T if P>Q with respect to inverse lexicographic order, NIL otherwise The second returned value is T if P=Q, otherwise it is NIL.

elimination−order k &key (primary−order #’lex>) (secondary−order #’lex>) [FUNCTION ] Return a predicate which compares monomials according to the K−th elimination order. Two optional arguments are PRIMARY−ORDER and SECONDARY−ORDER and they should be term orders which are used on the first K and the remaining variables.

elimination−order−1 order [FUNCTION ] A special case of the ELIMINATION−ORDER when there is only one primary variable.

9 The Polynomial Package

scalar−times−poly c p &optional (ring *coefficient−ring*) [FUNCTION ]

Return product of a scalar C by a polynomial P with coefficient ring RING. term−times−poly term f &optional (ring *coefficient−ring*) [FUNCTION ]

Return product of a term TERM by a polynomial F with coefficient ring RING. monom−times−poly m f [FUNCTION ]

Return product of a monomial M by a polynomial F with coefficient ring RING. minus−poly f &optional (ring *coefficient−ring*) [FUNCTION ]

Changes the sign of a polynomial F with coefficients in coefficient ring RING, and returns the result. sort−poly poly &optional (pred #’lex>) (start 0) (end (unless (null poly) (length (caar poly)))) [FUNCTION ]

Destructively Sorts a polynomial POLY by predicate PRED; the predicate is assumed to take arguments START and END in addition to the pair of monomials, as the functions in the ORDER package do.

poly+ p q &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Returns the sum of two polynomials P and Q with coefficients in ring RING, with terms ordered according to monomial order PRED.

poly− p q &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Returns the difference of two polynomials P and Q with coefficients in ring RING, with terms ordered according to monomial order PRED.

poly* p q &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Returns the product of two polynomials P and Q with coefficients in ring RING, with terms ordered according to monomial order PRED.

poly−op f m g pred ring [FUNCTION ]

Returns F−M*G, where F and G are polynomials with coefficients in ring RING, ordered according to monomial order PRED and M is a monomial.

poly−expt poly n &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Exponentiate a polynomial POLY to power N. The terms of the polynomial are assumed to be ordered by monomial order PRED and with coefficients in ring RING. Use the Chinese algorithm; assume N>=0 and POLY is non−zero (not NIL).

poly−mexpt plist monom &optional (pred #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Raise a polynomial vector represented ad a list of polynomials PLIST to power MULTIINDEX. Every polynomial has its terms ordered by predicate PRED and coefficients in the ring RING.

poly−constant−p p [FUNCTION ]

Returns T if P is a constant polynomial.

poly−extend p &optional (m (list 0)) [FUNCTION ]

Given a polynomial P in k[x[r+1],...,xn], it returns the same polynomial as an element of k[x1,...,xn], optionally multiplying it by a monomial x1ˆ m1*x2ˆ m2*...*xrˆ mr, where m=(m1,m2,...,mr) is a multiindex.

poly−extend−end p &optional (m (list 0)) [FUNCTION ]

Similar to POLY−EXTEND, but it adds new variables at the end.

poly−zerop p [FUNCTION ]

Returns T if P is a zero polynomial. lt p [FUNCTION ]

Returns the leading term of a polynomial P.

lm p [FUNCTION ]

Returns the leading monomial of a polynomial P.

lc p [FUNCTION ]

Returns the leading coefficient of a polynomial P.

10 The Parser Package

parse &optional stream [FUNCTION ]

Parser of infis expressions with integer/rational coefficients The parser will recognize two kinds of polynomial expressions: − polynomials in fully expanded forms with coefficients written in front of symbolic expressions; constants can be optionally enclosed in (); for example, the infix form Xˆ 2−Yˆ 2+(−4/3)*Uˆ 2*Wˆ 3−5 parses to (+ (− (EXPT X 2) (EXPT Y 2)) (* (− (/ 4 3)) (EXPT U 2) (EXPT W 3)) (− 5)) − lists of polynomials; for example [X−Y, Xˆ 2+3*Z] parses to (:[ (− X Y) (+ (EXPT X 2) (* 3 Z))) where the first symbol [ marks a list of polynomials. −other infix expressions, for example [(X−Y)*(X+Y)/Z,(X+1)ˆ 2] parses to: (:[ (/ (* (− X Y) (+ X Y)) Z) (EXPT (+ X 1) 2)) Currently this function is implemented using M. Kantrowitz’s INFIX package.

alist−form plist vars [FUNCTION ]

Translates an expression PLIST, which should be a list of polynomials in variables VARS, to an alist representation of a polynomial. It returns the alist. See also PARSE−TO−ALIST.

alist−form−1 p vars &aux (ht (make−hash−table :test #’equal :size 16)) stack [FUNCTION ]

powers monom vars &aux (tab (pairlis vars (make−list (length vars) :initial−element 0))) [FUNCTION ]

parse−to−alist vars &optional stream [FUNCTION ]

Parse an expression already in prefix form to an association list form according to the internal CG-Blisp polynomial syntax: a polynomial is an alist of pairs (MONOM . COEFFICIENT). For example: (WITH−INPUT−FROM−STRING (S ”Xˆ 2−Yˆ 2+(−4/3)*Uˆ 2*Wˆ 3−5”) (PARSE−TO−ALIST ’(X Y U W) S)) evaluates to (((0 0 2 3) . −4/3) ((0 2 0 0) . −1) ((2 0 0 0) . 1) ((0 0 0 0) . −5))

parse−string−to−alist str vars [FUNCTION ]

Parse string STR and return a polynomial as a sorted association list of pairs (MONOM . COEFFICIENT). For example: (parse−string−to−alist ”[xˆ 2−yˆ 2+(−4/3)*uˆ 2*wˆ 3−5,y]” ’(x y u w)) ([ (((0 0 2 3) . −4/3) ((0 2 0 0) . −1) ((2 0 0 0) . 1) ((0 0 0 0) . −5)) (((0 1 0 0) . 1))) The functions PARSE−TO−SORTED−ALIST and PARSE−STRING−TO−SORTED−ALIST sort terms by the predicate defined in the ORDER package. parse−to−sorted−alist vars &optional (order #’lex>) (stream t) [FUNCTION ]

Parses streasm STREAM and returns a polynomial represented as a sorted alist. For example: (WITH−INPUT−FROM−STRING (S ”Xˆ 2−Yˆ 2+(−4/3)*Uˆ 2*Wˆ 3−5”) (PARSE−TO−SORTED−ALIST ’(X Y U W) S)) returns (((2 0 0 0) . 1) ((0 2 0 0) . −1) ((0 0 2 3) . −4/3) ((0 0 0 0) . −5)) and (WITH−INPUT−FROM−STRING (S ”Xˆ 2−Yˆ 2+(−4/3)*Uˆ 2*Wˆ 3−5”) (PARSE−TO−SORTED−ALIST ’(X Y U W) T #’GRLEX>) S) returns (((0 0 2 3) . −4/3) ((2 0 0 0) . 1) ((0 2 0 0) . −1) ((0 0 0 0) . −5))

parse−string−to−sorted−alist str vars &optional (order #’lex>) [FUNCTION ]

Parse a string to a sorted alist form, the internal representation of polynomials used by our system.

sort−poly−1 p order [FUNCTION ]

Sort the terms of a single polynomial P using an admissible monomial order ORDER. Returns the sorted polynomial. Destructively modifies P.

sort−poly poly−or−poly−list &optional (order #’lex>) [FUNCTION ]

Sort POLY−OR−POLY−LIST, which could be either a single polynomial or a list of polynomials in internal alist representation, using admissible monomial order ORDER. Each polynomial is sorted using SORT−POLY−1.

poly−eval−1 expr vars order ring &aux (n (length vars)) [FUNCTION ]

Evaluate an expression EXPR as polynomial by substituting operators + − * expt with corresponding polynomial operators and variables VARS with monomials (1 0 ... 0), (0 1 ... 0) etc. We use special versions of binary operators $poly+, $poly−, $minus−poly, $poly* and $poly−expt which work like the corresponding functions in the POLY package, but accept scalars as arguments as well.

poly−eval expr vars &optional (order #’lex>) (ring *coefficient−ring*) [FUNCTION ]

Evaluate an expression EXPR, which should be a polynomial expression or a list of polynomial expressions (a list of expressions marked by prepending keyword :[ to it) given in lisp prefix notation, in variables VARS, which should be a list of symbols. The result of the evaluation is a polynomial or a list of polynomials (marked by prepending symbol ’[) in the internal alist form. This evaluator is used by the PARSE package to convert input from strings directly to internal form.

monom−basis n &aux (basis (copy−tree (make−list n :initial−element (list ’quote (list (cons (make−list n :initial−element 0) 1)))))) [FUNCTION ]

Generate a list of monomials ((1 0 ... 0) (0 1 0 ... 0) ... (0 0 ... 1) which correspond to linear monomials X1, X2, ... XN.

convert−number number−or−poly n [FUNCTION ]

Returns NUMBER−OR−POLY, if it is a polynomial. If it is a number, it converts it to the constant monomial in N variables. If the result is a number then convert it to a polynomial in N variables.

$poly+ p q n order ring [FUNCTION ]

Add two polynomials P and Q, where each polynomial is either a numeric constant or a polynomial in internal representation. If the result is a number then convert it to a polynomial in N variables.

$poly− p q n order ring [FUNCTION ]

Subtract two polynomials P and Q, where each polynomial is either a numeric constant or a polynomial in internal representation. If the result is a number then convert it to a polynomial in N variables.

$minus−poly p n ring [FUNCTION ]

Negation of P is a polynomial is either a numeric constant or a polynomial in internal representation. If the result is a number then convert it to a polynomial in N variables.

$poly* p q n order ring [FUNCTION ]

Multiply two polynomials P and Q, where each polynomial is either a numeric constant or a polynomial in internal representation. If the result is a number then convert it to a polynomial in N variables.

$poly/ p q ring [FUNCTION ]

Divide a polynomials P which is either a numeric constant or a polynomial in internal representation, by a number Q.

$poly−expt p l n order ring [FUNCTION ]

Raise polynomial P, which is a polynomial in internal representation or a numeric constant, to power L. If P is a number, convert the result to a polynomial in N variables.

11 Other packages

makelist−1 expr var lo hi &optional (step 1) [MACRO]

makelist expr (var lo hi &optional (step 1)) &rest more [MACRO]

sum &body body [MACRO]

list−of expr (var lst) &rest more [MACRO]

list−of−1 expr var lst [MACRO]

union−of expr (var lst) &rest more [MACRO] union−of−1 expr var lst [MACRO]

set−of expr (var lst) &rest more [MACRO]

set−of−1 expr var lst [MACRO]

select ind lst [FUNCTION ]

monom/ m1 m2 [FUNCTION ]

Divide monomial M1 by monomial M2. monom* m1 m2 [FUNCTION ]

Multiply monomial M1 by monomial M2. nmonom* m1 m2 [FUNCTION ]

Multiply monomials M1 and M2 − destructive version. M1 is destructively modified, M2 is not modified.

monom−divides−p m1 m2 [FUNCTION ]

Returns T if monomial M1 divides monomial M2, NIL otherwise. monom−divisible−by−p m1 m2 [FUNCTION ]

Returns T if monomial M1 is divisible by monomial M2, NIL otherwise. monom−rel−prime m1 m2 [FUNCTION ]

Returns T if two monomials M1 and M2 are relatively prime (disjoint). monom−equal m1 m2 [FUNCTION ]

Returns T if two monomials M1 and M2 are equal. monom−lcm m1 m2 [FUNCTION ]

Returns least common multiple of monomials M1 and M2. monom−gcd m1 m2 [FUNCTION ]

Returns greatest common divisor of monomials M1 and M2. poly−gcd a b [FUNCTION ] poly−pseudo−divide f g [FUNCTION ] poly−pseudo−remainder f g [FUNCTION ] mdeg b [FUNCTION ] lcoeff b [FUNCTION ] lrest b [FUNCTION ] lpart b [FUNCTION ] poly−primitive−part f [FUNCTION ] poly−content f [FUNCTION ] poly−with−sugar−poly p [FUNCTION ] poly−with−sugar−sugar p [FUNCTION ] poly−with−sugar−tail p [FUNCTION ] (setf poly−with−sugar−poly) poly [SETF MAPPING] (setf poly−with−sugar−sugar) sugar [SETF MAPPING] (setf poly−with−sugar−tail) tail [SETF MAPPING] monom−sugar m [FUNCTION ] coefficient−sugar c ring [FUNCTION ] term−sugar term ring [FUNCTION ] poly−add−sugar poly ring [FUNCTION ] scalar−times−poly−with−sugar c p ring [FUNCTION ] term−times−poly−with−sugar term f ring [FUNCTION ] monom−times−poly−with−sugar m f [FUNCTION ] minus−poly−with−sugar f ring [FUNCTION ] poly−with−sugar+ p q pred ring [FUNCTION ] poly−with−sugar− p q pred ring [FUNCTION ] poly−with−sugar−op f term g pred ring [FUNCTION ] poly−with−sugar−nreverse p [FUNCTION ] poly−with−sugar−append p q [FUNCTION ] poly−with−sugar−zerop p [FUNCTION ] poly−with−sugar−lm p [FUNCTION ] poly−with−sugar−lc p [FUNCTION ] poly−with−sugar−lt p [FUNCTION ] poly−print plist vars &optional (stream t) [FUNCTION ]

Prints a polynomial or a list of polynomials PLIST using infix syntax compatible with most software systems. The following data representations are assumed: 1) Polynomial list is ([ poly1 poly2 ...) 2) Polynomial is a list (term1 term2 ...) 3) Term is (monom . number) 4) Monom is (number1 number2 ...) and is a list of powers at corresponding variables Variable names must be provided to the printer explicitly.

poly−print−1 p vars &optional (stream t) [FUNCTION ]

An auxillary function of POLY−PRINT. It prints a single polynomial P. poly−print−2 plist vars stream &optional (beg t) [FUNCTION ]

An auxillary function of POLY−PRINT. It prints a comma−separated list of polynomials PLIST. print−term l vars &optional (stream t) beg [FUNCTION ]

An auxillary function of POLY−PRINT. It prints a single term L. print−monom l vars &optional (stream t) beg [FUNCTION ]

An auxillary function of POLY−PRINT. It prints a single monomial L. num p [FUNCTION ] denom p [FUNCTION ] rat−simplify−2 num denom [FUNCTION ] rat−simplify p [FUNCTION ] rat+ p q [FUNCTION ] rat− p q [FUNCTION ] rat* p q [FUNCTION ] rat/ p q [FUNCTION ] scalar−times−rat scalar p [FUNCTION ] scalar−div−rat scalar p [FUNCTION ] rat−zerop p [FUNCTION ] rat−uminus p [FUNCTION ] rat−expt p n [FUNCTION ] rat−constant c n [FUNCTION ]

Make a constant rational function equal to c with n variables rat−to−poly p [FUNCTION ]

Attempt to convert a rational function to a polynomial by dividing numerator by denominator. Error if not divisible

ratpoly+ p q [FUNCTION ]

Add polynomials P and Q. ratpoly− p q [FUNCTION ] ratpoly−uminus p [FUNCTION ] ratpoly* p q [FUNCTION ]

Multiply polynomials P and Q. scalar−times−ratpoly scalar p [FUNCTION ]

Multiply scalar SCALAR by a polynomial P. rat−times−ratpoly scalar p [FUNCTION ]

Multiply rational function SCALAR by a polynomial P. ratpoly−divide f g [FUNCTION ]

Divide polynomial F by G. Return quotient and remainder as multiple values. ratpoly−remainder f g [FUNCTION ]

The remainder of the division of a polynomial F by G. ratpoly−gcd f g [FUNCTION ]

Return GCD of polynomials F and G. ratpoly−diff f [FUNCTION ]

Differentiate a polynomial. ratpoly−square−free f [FUNCTION ]

Return the square−free part of a polynomial F. ratpoly−normalize f [FUNCTION ]

Divide a non−zero polynomial by the coefficient at the highest power. ratpoly−resultant f g [FUNCTION ]

Return the resultant of polynomials F and G. deg s [FUNCTION ]

lead s [FUNCTION ]

ratpoly−discriminant p &aux (l (deg p)) [FUNCTION ]

The discriminant of a polynomial P. ratpoly−print p vars &optional (stream t) (beg t) (p−orig p) [FUNCTION ]

poly−to−ratpoly p [FUNCTION ] poly−to−poly1 p &aux (htab (make−hash−table)) q [FUNCTION ] poly1−to−ratpoly p [FUNCTION ] ratpoly−to−poly1 p [FUNCTION ]

Convert every coefficient of ratpoly to polynomial if possible poly1−to−poly p [FUNCTION ]

Convert a ratpoly, whose coeffs have been converted to poly, into a poly structure, i.e. tack in powers of first variable.

ratpoly−to−poly p [FUNCTION ] poly−resultant f g [FUNCTION ]

Calculate resultant of F and G given in poly i.e. alist representation. term* term1 term2 &optional (ring *coefficient−ring*) [FUNCTION ] term/ term1 term2 &optional (ring *coefficient−ring*) [FUNCTION ] monom−times−term m term [FUNCTION ] term−divides−p term1 term2 [FUNCTION ] term−monom term [MACRO] term−coefficient term [MACRO] (setf term−monom) monom [SETF MAPPING] (setf term−coefficient) coefficient [SETF MAPPING] xgcd x y [FUNCTION ]

Extended gcd; the call (xgcd X Y) returns a multiple value list: − GCD − U,V such that they solve the equation GCD=U*X+V*Y − U1,V1 such that LCM=U1*X=V1*Y (up to the sign).

A All examples produced by the all-examples utility

;;----------------------------------------------------------------
;;
;; (STRING-GROBNER "[x^2+y,x-y]" '(X Y))
;;
;;----------------------------------------------------------------
Args:[ X^2 + Y, X - Y ]
[ X - Y, Y^2 + Y ]
;;----------------------------------------------------------------
;;
;; (STRING-GROBNER "[y-x^2,z-x^3]" '(X Y Z) :ORDER #'GREVLEX>)
;;
;;----------------------------------------------------------------
Args:[  - X^2 + Y,  - X^3 + Z ]
[ X^2 - Y, X * Y - Z, Y^2 - X * Z ]
;;----------------------------------------------------------------
;;
;; (STRING-GROBNER-SYSTEM "[u*x+y,x+y]" '(X Y) '(U))
;;
;;----------------------------------------------------------------
------------------- CASE 1 -------------------
Condition:
  Green list: [ U ]
  Red list: [  ]
 Basis: [ (1) * Y, (1) * X ]
------------------- CASE 2 -------------------
Condition:
  Green list: [  ]
  Red list: [ U, U - 1 ]
 Basis: [ (U - 1) * X, ( - U + 1) * Y ]
------------------- CASE 3 -------------------
Condition:
  Green list: [ U - 1 ]
  Red list: [ U ]
 Basis: [ (1) * X + (1) * Y ]
;;----------------------------------------------------------------
;;
;; (STRING-GROBNER-SYSTEM "[u*x+y,x+y]" '(X Y) '(U) :COVER '(("[u-1]" "[]")))
;;
;;----------------------------------------------------------------
------------------- CASE 1 -------------------
Condition:
  Green list: [ U - 1 ]
  Red list: [ U ]
 Basis: [ (1) * X + (1) * Y ]
;;----------------------------------------------------------------
;;
;; (STRING-READ-POLY "[x^3+3*x^2+3*x+1]" '(X))
;;
;;----------------------------------------------------------------
Args:[ X^3 + 3 * X^2 + 3 * X + 1 ]
[ RETURN VALUE 1]-->> ([ (((3) . 1) ((2) . 3) ((1) . 3) ((0) . 1)))

;;----------------------------------------------------------------
;;
;; (STRING-ELIMINATION-IDEAL "[x^2+y^2-2,x*y-1]" '(X Y) 1)
;;
;;----------------------------------------------------------------
Args:[ X^2 + Y^2 - 2, X * Y - 1 ]
[ Y^4 - 2 * Y^2 + 1 ]
;;----------------------------------------------------------------
;;
;; (STRING-IDEAL-SATURATION-1 "[x^2*y,y^3]" "x" '(X Y))
;;
;;----------------------------------------------------------------
[ Y ]
;;----------------------------------------------------------------
;;
;; (STRING-IDEAL-POLYSATURATION-1 "[x^2*y,y^3]" "[x,y]" '(X Y))
;;
;;----------------------------------------------------------------
Args1:[ X^2 * Y, Y^3 ]
Args2:[ X, Y ]
[ 1 ]
;;----------------------------------------------------------------
;;
;; (STRING-COND '("[u^2-v]" "[v-1]") '(U V) #'GREVLEX>)
;;
;;----------------------------------------------------------------
[ RETURN VALUE 1]-->> (((((2 0) . 1) ((0 1) . -1))) ((((0 1) . 1) ((0 0) . -1))))
;;----------------------------------------------------------------
;;
;; (STRING-COVER '(("[u^2-v]" "[u]") ("[u+v]" "[]")) '(U V) #'GREVLEX>)
;;
;;----------------------------------------------------------------
[ RETURN VALUE 1]-->> ((((((2 0) . 1) ((0 1) . -1))) ((((1 0) . 1)))) (((((1 0) . 1) ((0 1) . 1))) NIL))
;;----------------------------------------------------------------
;;
;; (STRING-DETERMINE "[u*x+y,v*x^2+y^2]" '(X Y) '(U V) :COND '("[u,v]" "[v-1]") :MAIN-ORDER #'LEX>)
;;
;;----------------------------------------------------------------
------------------- CASE 1 -------------------
Condition:
  Green list: [ U, V ]
  Red list: [ V - 1, 1 ]
 Basis: [ (1) * Y, (1) * Y^2 ]
;;----------------------------------------------------------------
;;
;; (PARSE-STRING-TO-SORTED-ALIST "x^2+y^3" '(X Y) #'GREVLEX>)
;;
;;----------------------------------------------------------------
[ RETURN VALUE 1]-->> (((0 3) . 1) ((2 0) . 1))
;;----------------------------------------------------------------
;;
;; (PARSE-STRING-TO-SORTED-ALIST "[x^2+y^3,x-y]" '(X Y) #'GREVLEX>)
;;
;;----------------------------------------------------------------

[ RETURN VALUE 1]-->> ([ (((0 3) . 1) ((2 0) . 1)) (((1 0) . 1) ((0 1) . -1)))
;;----------------------------------------------------------------
;;
;; (TRANSLATE-STATEMENTS (COLLINEAR A B C) (PERPENDICULAR A B A C))
;;
;;----------------------------------------------------------------
[ RETURN VALUE 1]-->> ((((+ (- (* B1 C2) (* B2 C1)) (- (* A2 C1) (* A1 C2)) (- (* A1 B2) (* A2 B1))))
                        ((+ (* (- A1 B1) (- A1 C1)) (* (- A2 B2) (- A2 C2)))))
                       (B1 B2 A1 A2 C1 C2))
;;----------------------------------------------------------------
;;
;; (TRANSLATE-THEOREM ((PERPENDICULAR A B C D) (PERPENDICULAR C D E F))
                      ((PARALLEL A B E F) (IDENTICAL-POINTS C D)))
;;
;;----------------------------------------------------------------
[ RETURN VALUE 1]-->> (((+ (* (- A1 B1) (- C1 D1)) (* (- A2 B2) (- C2 D2)))
                        (+ (* (- C1 D1) (- E1 F1)) (* (- C2 D2) (- E2 F2))))
                       (A1 A2 B1 B2 C1 C2 D1 D2 E1 E2 F1 F2))
[ RETURN VALUE 2]-->> ((((- (* (- A1 B1) (- E2 F2)) (* (- A2 B2) (- E1 F1)))) ((- C1 D1) (- C2 D2)))
                       (A1 A2 B1 B2 E1 E2 F1 F2 C1 C2 D1 D2))
;;----------------------------------------------------------------
;;
;; (TRANSLATE-THEOREM ((PERPENDICULAR A B A C) (MIDPOINT B C M) (MIDPOINT A M O) (COLLINEAR B H C)
                       (PERPENDICULAR A H B C))
                      ((EQUIDISTANT M O H O) (IDENTICAL-POINTS B C)))
;;
;;----------------------------------------------------------------
[ RETURN VALUE 1]-->> (((+ (* (- A1 B1) (- A1 C1)) (* (- A2 B2) (- A2 C2))) (- (* 2 M1) B1 C1)
                        (- (* 2 M2) B2 C2) (- (* 2 O1) A1 M1) (- (* 2 O2) A2 M2)
                        (+ (- (* H1 C2) (* H2 C1)) (- (* B2 C1) (* B1 C2)) (- (* B1 H2) (* B2 H1)))
                        (+ (* (- A1 H1) (- B1 C1)) (* (- A2 H2) (- B2 C2))))
                       (M1 M2 O1 O2 A1 A2 H1 H2 B1 B2 C1 C2))
[ RETURN VALUE 2]-->> ((((- (+ (EXPT (- M1 O1) 2) (EXPT (- M2 O2) 2))
                            (+ (EXPT (- H1 O1) 2) (EXPT (- H2 O2) 2))))
                        ((- B1 C1) (- B2 C2)))
                       (M1 M2 H1 H2 O1 O2 B1 B2 C1 C2))
;;----------------------------------------------------------------
;;
;; (PROVE-THEOREM ((PERPENDICULAR A B C D) (PERPENDICULAR C D E F)) ((PARALLEL A B E F) (IDENTICAL-POINTS C D)))
;;
;;----------------------------------------------------------------
[ 1 ]
;;----------------------------------------------------------------
;;
;; (PROVE-THEOREM ((PERPENDICULAR A B A C) (MIDPOINT B C M) (MIDPOINT A M O) (COLLINEAR B H C)
                   (PERPENDICULAR A H B C))
                  ((EQUIDISTANT M O H O) (IDENTICAL-POINTS B C)))
;;
;;----------------------------------------------------------------
[ 1 ]
;;----------------------------------------------------------------
;;
;; (PROVE-THEOREM ((PERPENDICULAR A B A C) (IDENTICAL-POINTS B C))
                  ((IDENTICAL-POINTS A B) (IDENTICAL-POINTS A C)))

;;
;;----------------------------------------------------------------
[ B1 - C1, B2 - C2, A1^2 + A2^2 - 2 * A1 * C1 + C1^2 - 2 * A2 * C2 + C2^2 ]
;;----------------------------------------------------------------
;;
;; (PROVE-THEOREM ((PERPENDICULAR A B A C) (IDENTICAL-POINTS B C))
                  ((IDENTICAL-POINTS A B) (REAL-IDENTICAL-POINTS A C)))
;;
;;----------------------------------------------------------------
[ 1 ]