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}
|
---|