[1] | 1 | \begin{verbatim}
|
---|
| 2 | ;;----------------------------------------------------------------
|
---|
| 3 | ;;
|
---|
| 4 | ;; (STRING-GROBNER "[x^2+y,x-y]" '(X Y))
|
---|
| 5 | ;;
|
---|
| 6 | ;;----------------------------------------------------------------
|
---|
| 7 | Args:[ X^2 + Y, X - Y ]
|
---|
| 8 | [ X - Y, Y^2 + Y ]
|
---|
| 9 | ;;----------------------------------------------------------------
|
---|
| 10 | ;;
|
---|
| 11 | ;; (STRING-GROBNER "[y-x^2,z-x^3]" '(X Y Z) :ORDER #'GREVLEX>)
|
---|
| 12 | ;;
|
---|
| 13 | ;;----------------------------------------------------------------
|
---|
| 14 | Args:[ - X^2 + Y, - X^3 + Z ]
|
---|
| 15 | [ X^2 - Y, X * Y - Z, Y^2 - X * Z ]
|
---|
| 16 | ;;----------------------------------------------------------------
|
---|
| 17 | ;;
|
---|
| 18 | ;; (STRING-GROBNER-SYSTEM "[u*x+y,x+y]" '(X Y) '(U))
|
---|
| 19 | ;;
|
---|
| 20 | ;;----------------------------------------------------------------
|
---|
| 21 | ------------------- CASE 1 -------------------
|
---|
| 22 | Condition:
|
---|
| 23 | Green list: [ U ]
|
---|
| 24 | Red list: [ ]
|
---|
| 25 | Basis: [ (1) * Y, (1) * X ]
|
---|
| 26 | ------------------- CASE 2 -------------------
|
---|
| 27 | Condition:
|
---|
| 28 | Green list: [ ]
|
---|
| 29 | Red list: [ U, U - 1 ]
|
---|
| 30 | Basis: [ (U - 1) * X, ( - U + 1) * Y ]
|
---|
| 31 | ------------------- CASE 3 -------------------
|
---|
| 32 | Condition:
|
---|
| 33 | Green list: [ U - 1 ]
|
---|
| 34 | Red list: [ U ]
|
---|
| 35 | Basis: [ (1) * X + (1) * Y ]
|
---|
| 36 | ;;----------------------------------------------------------------
|
---|
| 37 | ;;
|
---|
| 38 | ;; (STRING-GROBNER-SYSTEM "[u*x+y,x+y]" '(X Y) '(U) :COVER '(("[u-1]" "[]")))
|
---|
| 39 | ;;
|
---|
| 40 | ;;----------------------------------------------------------------
|
---|
| 41 | ------------------- CASE 1 -------------------
|
---|
| 42 | Condition:
|
---|
| 43 | Green list: [ U - 1 ]
|
---|
| 44 | Red list: [ U ]
|
---|
| 45 | Basis: [ (1) * X + (1) * Y ]
|
---|
| 46 | ;;----------------------------------------------------------------
|
---|
| 47 | ;;
|
---|
| 48 | ;; (STRING-READ-POLY "[x^3+3*x^2+3*x+1]" '(X))
|
---|
| 49 | ;;
|
---|
| 50 | ;;----------------------------------------------------------------
|
---|
| 51 | Args:[ X^3 + 3 * X^2 + 3 * X + 1 ]
|
---|
| 52 | [ RETURN VALUE 1]-->> ([ (((3) . 1) ((2) . 3) ((1) . 3) ((0) . 1)))
|
---|
| 53 |
|
---|
| 54 | ;;----------------------------------------------------------------
|
---|
| 55 | ;;
|
---|
| 56 | ;; (STRING-ELIMINATION-IDEAL "[x^2+y^2-2,x*y-1]" '(X Y) 1)
|
---|
| 57 | ;;
|
---|
| 58 | ;;----------------------------------------------------------------
|
---|
| 59 | Args:[ X^2 + Y^2 - 2, X * Y - 1 ]
|
---|
| 60 | [ Y^4 - 2 * Y^2 + 1 ]
|
---|
| 61 | ;;----------------------------------------------------------------
|
---|
| 62 | ;;
|
---|
| 63 | ;; (STRING-IDEAL-SATURATION-1 "[x^2*y,y^3]" "x" '(X Y))
|
---|
| 64 | ;;
|
---|
| 65 | ;;----------------------------------------------------------------
|
---|
| 66 | [ Y ]
|
---|
| 67 | ;;----------------------------------------------------------------
|
---|
| 68 | ;;
|
---|
| 69 | ;; (STRING-IDEAL-POLYSATURATION-1 "[x^2*y,y^3]" "[x,y]" '(X Y))
|
---|
| 70 | ;;
|
---|
| 71 | ;;----------------------------------------------------------------
|
---|
| 72 | Args1:[ X^2 * Y, Y^3 ]
|
---|
| 73 | Args2:[ X, Y ]
|
---|
| 74 | [ 1 ]
|
---|
| 75 | ;;----------------------------------------------------------------
|
---|
| 76 | ;;
|
---|
| 77 | ;; (STRING-COND '("[u^2-v]" "[v-1]") '(U V) #'GREVLEX>)
|
---|
| 78 | ;;
|
---|
| 79 | ;;----------------------------------------------------------------
|
---|
| 80 | [ RETURN VALUE 1]-->> (((((2 0) . 1) ((0 1) . -1))) ((((0 1) . 1) ((0 0) . -1))))
|
---|
| 81 |
|
---|
| 82 | ;;----------------------------------------------------------------
|
---|
| 83 | ;;
|
---|
| 84 | ;; (STRING-COVER '(("[u^2-v]" "[u]") ("[u+v]" "[]")) '(U V) #'GREVLEX>)
|
---|
| 85 | ;;
|
---|
| 86 | ;;----------------------------------------------------------------
|
---|
| 87 | [ RETURN VALUE 1]-->> ((((((2 0) . 1) ((0 1) . -1))) ((((1 0) . 1)))) (((((1 0) . 1) ((0 1) . 1))) NIL))
|
---|
| 88 |
|
---|
| 89 | ;;----------------------------------------------------------------
|
---|
| 90 | ;;
|
---|
| 91 | ;; (STRING-DETERMINE "[u*x+y,v*x^2+y^2]" '(X Y) '(U V) :COND '("[u,v]" "[v-1]") :MAIN-ORDER #'LEX>)
|
---|
| 92 | ;;
|
---|
| 93 | ;;----------------------------------------------------------------
|
---|
| 94 | ------------------- CASE 1 -------------------
|
---|
| 95 | Condition:
|
---|
| 96 | Green list: [ U, V ]
|
---|
| 97 | Red list: [ V - 1, 1 ]
|
---|
| 98 | Basis: [ (1) * Y, (1) * Y^2 ]
|
---|
| 99 | ;;----------------------------------------------------------------
|
---|
| 100 | ;;
|
---|
| 101 | ;; (PARSE-STRING-TO-SORTED-ALIST "x^2+y^3" '(X Y) #'GREVLEX>)
|
---|
| 102 | ;;
|
---|
| 103 | ;;----------------------------------------------------------------
|
---|
| 104 | [ RETURN VALUE 1]-->> (((0 3) . 1) ((2 0) . 1))
|
---|
| 105 |
|
---|
| 106 | ;;----------------------------------------------------------------
|
---|
| 107 | ;;
|
---|
| 108 | ;; (PARSE-STRING-TO-SORTED-ALIST "[x^2+y^3,x-y]" '(X Y) #'GREVLEX>)
|
---|
| 109 | ;;
|
---|
| 110 | ;;----------------------------------------------------------------
|
---|
| 111 | [ RETURN VALUE 1]-->> ([ (((0 3) . 1) ((2 0) . 1)) (((1 0) . 1) ((0 1) . -1)))
|
---|
| 112 |
|
---|
| 113 | ;;----------------------------------------------------------------
|
---|
| 114 | ;;
|
---|
| 115 | ;; (TRANSLATE-STATEMENTS (COLLINEAR A B C) (PERPENDICULAR A B A C))
|
---|
| 116 | ;;
|
---|
| 117 | ;;----------------------------------------------------------------
|
---|
| 118 | [ RETURN VALUE 1]-->> ((((+ (- (* B1 C2) (* B2 C1)) (- (* A2 C1) (* A1 C2)) (- (* A1 B2) (* A2 B1))))
|
---|
| 119 | ((+ (* (- A1 B1) (- A1 C1)) (* (- A2 B2) (- A2 C2)))))
|
---|
| 120 | (B1 B2 A1 A2 C1 C2))
|
---|
| 121 |
|
---|
| 122 | ;;----------------------------------------------------------------
|
---|
| 123 | ;;
|
---|
| 124 | ;; (TRANSLATE-THEOREM ((PERPENDICULAR A B C D) (PERPENDICULAR C D E F))
|
---|
| 125 | ((PARALLEL A B E F) (IDENTICAL-POINTS C D)))
|
---|
| 126 | ;;
|
---|
| 127 | ;;----------------------------------------------------------------
|
---|
| 128 | [ RETURN VALUE 1]-->> (((+ (* (- A1 B1) (- C1 D1)) (* (- A2 B2) (- C2 D2)))
|
---|
| 129 | (+ (* (- C1 D1) (- E1 F1)) (* (- C2 D2) (- E2 F2))))
|
---|
| 130 | (A1 A2 B1 B2 C1 C2 D1 D2 E1 E2 F1 F2))
|
---|
| 131 | [ RETURN VALUE 2]-->> ((((- (* (- A1 B1) (- E2 F2)) (* (- A2 B2) (- E1 F1)))) ((- C1 D1) (- C2 D2)))
|
---|
| 132 | (A1 A2 B1 B2 E1 E2 F1 F2 C1 C2 D1 D2))
|
---|
| 133 |
|
---|
| 134 | ;;----------------------------------------------------------------
|
---|
| 135 | ;;
|
---|
| 136 | ;; (TRANSLATE-THEOREM ((PERPENDICULAR A B A C) (MIDPOINT B C M) (MIDPOINT A M O) (COLLINEAR B H C)
|
---|
| 137 | (PERPENDICULAR A H B C))
|
---|
| 138 | ((EQUIDISTANT M O H O) (IDENTICAL-POINTS B C)))
|
---|
| 139 | ;;
|
---|
| 140 | ;;----------------------------------------------------------------
|
---|
| 141 | [ RETURN VALUE 1]-->> (((+ (* (- A1 B1) (- A1 C1)) (* (- A2 B2) (- A2 C2))) (- (* 2 M1) B1 C1)
|
---|
| 142 | (- (* 2 M2) B2 C2) (- (* 2 O1) A1 M1) (- (* 2 O2) A2 M2)
|
---|
| 143 | (+ (- (* H1 C2) (* H2 C1)) (- (* B2 C1) (* B1 C2)) (- (* B1 H2) (* B2 H1)))
|
---|
| 144 | (+ (* (- A1 H1) (- B1 C1)) (* (- A2 H2) (- B2 C2))))
|
---|
| 145 | (M1 M2 O1 O2 A1 A2 H1 H2 B1 B2 C1 C2))
|
---|
| 146 | [ RETURN VALUE 2]-->> ((((- (+ (EXPT (- M1 O1) 2) (EXPT (- M2 O2) 2))
|
---|
| 147 | (+ (EXPT (- H1 O1) 2) (EXPT (- H2 O2) 2))))
|
---|
| 148 | ((- B1 C1) (- B2 C2)))
|
---|
| 149 | (M1 M2 H1 H2 O1 O2 B1 B2 C1 C2))
|
---|
| 150 |
|
---|
| 151 | ;;----------------------------------------------------------------
|
---|
| 152 | ;;
|
---|
| 153 | ;; (PROVE-THEOREM ((PERPENDICULAR A B C D) (PERPENDICULAR C D E F)) ((PARALLEL A B E F) (IDENTICAL-POINTS C D)))
|
---|
| 154 | ;;
|
---|
| 155 | ;;----------------------------------------------------------------
|
---|
| 156 | [ 1 ]
|
---|
| 157 | ;;----------------------------------------------------------------
|
---|
| 158 | ;;
|
---|
| 159 | ;; (PROVE-THEOREM ((PERPENDICULAR A B A C) (MIDPOINT B C M) (MIDPOINT A M O) (COLLINEAR B H C)
|
---|
| 160 | (PERPENDICULAR A H B C))
|
---|
| 161 | ((EQUIDISTANT M O H O) (IDENTICAL-POINTS B C)))
|
---|
| 162 | ;;
|
---|
| 163 | ;;----------------------------------------------------------------
|
---|
| 164 | [ 1 ]
|
---|
| 165 | ;;----------------------------------------------------------------
|
---|
| 166 | ;;
|
---|
| 167 | ;; (PROVE-THEOREM ((PERPENDICULAR A B A C) (IDENTICAL-POINTS B C))
|
---|
| 168 | ((IDENTICAL-POINTS A B) (IDENTICAL-POINTS A C)))
|
---|
| 169 | ;;
|
---|
| 170 | ;;----------------------------------------------------------------
|
---|
| 171 | [ B1 - C1, B2 - C2, A1^2 + A2^2 - 2 * A1 * C1 + C1^2 - 2 * A2 * C2 + C2^2 ]
|
---|
| 172 | ;;----------------------------------------------------------------
|
---|
| 173 | ;;
|
---|
| 174 | ;; (PROVE-THEOREM ((PERPENDICULAR A B A C) (IDENTICAL-POINTS B C))
|
---|
| 175 | ((IDENTICAL-POINTS A B) (REAL-IDENTICAL-POINTS A C)))
|
---|
| 176 | ;;
|
---|
| 177 | ;;----------------------------------------------------------------
|
---|
| 178 | [ 1 ]
|
---|
| 179 | \end{verbatim}
|
---|