\begin{verbatim}
;;----------------------------------------------------------------
;;
;; (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 ]
\end{verbatim}