paulson@10341
|
1 |
(* ID: $Id$ *)
|
paulson@10295
|
2 |
(* EXTRACT from HOL/ex/Primes.thy*)
|
paulson@10295
|
3 |
|
paulson@10295
|
4 |
theory Primes = Main:
|
paulson@10295
|
5 |
consts
|
paulson@10300
|
6 |
gcd :: "nat*nat \<Rightarrow> nat" (*Euclid's algorithm *)
|
paulson@10295
|
7 |
|
paulson@10300
|
8 |
recdef gcd "measure ((\<lambda>(m,n).n) ::nat*nat \<Rightarrow> nat)"
|
paulson@10295
|
9 |
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
|
paulson@10295
|
10 |
|
paulson@10295
|
11 |
|
paulson@10295
|
12 |
ML "Pretty.setmargin 64"
|
paulson@10295
|
13 |
ML "IsarOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*)
|
paulson@10295
|
14 |
|
paulson@10295
|
15 |
|
paulson@10295
|
16 |
text {*
|
paulson@10295
|
17 |
\begin{quote}
|
paulson@10295
|
18 |
@{thm[display]"dvd_def"}
|
paulson@10295
|
19 |
\rulename{dvd_def}
|
paulson@10295
|
20 |
\end{quote}
|
paulson@10295
|
21 |
*};
|
paulson@10295
|
22 |
|
paulson@10295
|
23 |
|
paulson@10295
|
24 |
(*** Euclid's Algorithm ***)
|
paulson@10295
|
25 |
|
paulson@10295
|
26 |
lemma gcd_0 [simp]: "gcd(m,0) = m"
|
paulson@10295
|
27 |
apply (simp);
|
paulson@10295
|
28 |
done
|
paulson@10295
|
29 |
|
paulson@10295
|
30 |
lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd(m,n) = gcd (n, m mod n)"
|
paulson@10295
|
31 |
apply (simp)
|
paulson@10295
|
32 |
done;
|
paulson@10295
|
33 |
|
paulson@10295
|
34 |
declare gcd.simps [simp del];
|
paulson@10295
|
35 |
|
paulson@10295
|
36 |
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*)
|
paulson@10295
|
37 |
lemma gcd_dvd_both: "(gcd(m,n) dvd m) \<and> (gcd(m,n) dvd n)"
|
paulson@10295
|
38 |
apply (induct_tac m n rule: gcd.induct)
|
paulson@10295
|
39 |
apply (case_tac "n=0")
|
paulson@10295
|
40 |
apply (simp_all)
|
paulson@10295
|
41 |
apply (blast dest: dvd_mod_imp_dvd)
|
paulson@10295
|
42 |
done
|
paulson@10295
|
43 |
|
paulson@10295
|
44 |
|
paulson@10295
|
45 |
text {*
|
paulson@10295
|
46 |
@{thm[display] dvd_mod_imp_dvd}
|
paulson@10295
|
47 |
\rulename{dvd_mod_imp_dvd}
|
paulson@10295
|
48 |
|
paulson@10295
|
49 |
@{thm[display] dvd_trans}
|
paulson@10295
|
50 |
\rulename{dvd_trans}
|
paulson@10295
|
51 |
|
paulson@10295
|
52 |
\begin{isabelle}
|
paulson@10295
|
53 |
proof\ (prove):\ step\ 3\isanewline
|
paulson@10295
|
54 |
\isanewline
|
paulson@10295
|
55 |
goal\ (lemma\ gcd_dvd_both):\isanewline
|
paulson@10295
|
56 |
gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n\isanewline
|
paulson@10295
|
57 |
\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk 0\ <\ n;\ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n)\isasymrbrakk \isanewline
|
paulson@10295
|
58 |
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ gcd\ (n,\ m\ mod\ n)\ dvd\ m
|
paulson@10295
|
59 |
\end{isabelle}
|
paulson@10295
|
60 |
*};
|
paulson@10295
|
61 |
|
paulson@10295
|
62 |
|
paulson@10295
|
63 |
lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
|
paulson@10295
|
64 |
lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
|
paulson@10295
|
65 |
|
paulson@10295
|
66 |
|
paulson@10295
|
67 |
text {*
|
paulson@10295
|
68 |
\begin{quote}
|
paulson@10295
|
69 |
@{thm[display] gcd_dvd1}
|
paulson@10295
|
70 |
\rulename{gcd_dvd1}
|
paulson@10295
|
71 |
|
paulson@10295
|
72 |
@{thm[display] gcd_dvd2}
|
paulson@10295
|
73 |
\rulename{gcd_dvd2}
|
paulson@10295
|
74 |
\end{quote}
|
paulson@10295
|
75 |
*};
|
paulson@10295
|
76 |
|
paulson@10295
|
77 |
(*Maximality: for all m,n,k naturals,
|
paulson@10295
|
78 |
if k divides m and k divides n then k divides gcd(m,n)*)
|
paulson@10295
|
79 |
lemma gcd_greatest [rule_format]:
|
paulson@10295
|
80 |
"(k dvd m) \<longrightarrow> (k dvd n) \<longrightarrow> k dvd gcd(m,n)"
|
paulson@10295
|
81 |
apply (induct_tac m n rule: gcd.induct)
|
paulson@10295
|
82 |
apply (case_tac "n=0")
|
paulson@10295
|
83 |
apply (simp_all add: dvd_mod);
|
paulson@10295
|
84 |
done;
|
paulson@10295
|
85 |
|
paulson@10295
|
86 |
theorem gcd_greatest_iff [iff]:
|
paulson@10295
|
87 |
"k dvd gcd(m,n) = (k dvd m \<and> k dvd n)"
|
paulson@10295
|
88 |
apply (blast intro!: gcd_greatest intro: dvd_trans);
|
paulson@10295
|
89 |
done;
|
paulson@10295
|
90 |
|
paulson@10295
|
91 |
|
paulson@10295
|
92 |
constdefs
|
paulson@10300
|
93 |
is_gcd :: "[nat,nat,nat] \<Rightarrow> bool" (*gcd as a relation*)
|
paulson@10295
|
94 |
"is_gcd p m n == p dvd m \<and> p dvd n \<and>
|
paulson@10295
|
95 |
(ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"
|
paulson@10295
|
96 |
|
paulson@10295
|
97 |
(*Function gcd yields the Greatest Common Divisor*)
|
paulson@10295
|
98 |
lemma is_gcd: "is_gcd (gcd(m,n)) m n"
|
paulson@10295
|
99 |
apply (simp add: is_gcd_def gcd_greatest);
|
paulson@10295
|
100 |
done
|
paulson@10295
|
101 |
|
paulson@10295
|
102 |
(*uniqueness of GCDs*)
|
paulson@10295
|
103 |
lemma is_gcd_unique: "\<lbrakk> is_gcd m a b; is_gcd n a b \<rbrakk> \<Longrightarrow> m=n"
|
paulson@10295
|
104 |
apply (simp add: is_gcd_def);
|
paulson@10295
|
105 |
apply (blast intro: dvd_anti_sym)
|
paulson@10295
|
106 |
done
|
paulson@10295
|
107 |
|
paulson@10295
|
108 |
|
paulson@10295
|
109 |
text {*
|
paulson@10295
|
110 |
@{thm[display] dvd_anti_sym}
|
paulson@10295
|
111 |
\rulename{dvd_anti_sym}
|
paulson@10295
|
112 |
|
paulson@10295
|
113 |
\begin{isabelle}
|
paulson@10295
|
114 |
proof\ (prove):\ step\ 1\isanewline
|
paulson@10295
|
115 |
\isanewline
|
paulson@10295
|
116 |
goal\ (lemma\ is_gcd_unique):\isanewline
|
paulson@10295
|
117 |
\isasymlbrakk is_gcd\ m\ a\ b;\ is_gcd\ n\ a\ b\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n\isanewline
|
paulson@10295
|
118 |
\ 1.\ \isasymlbrakk m\ dvd\ a\ \isasymand \ m\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ m);\isanewline
|
paulson@10295
|
119 |
\ \ \ \ \ \ \ n\ dvd\ a\ \isasymand \ n\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ n)\isasymrbrakk \isanewline
|
paulson@10295
|
120 |
\ \ \ \ \isasymLongrightarrow \ m\ =\ n
|
paulson@10295
|
121 |
\end{isabelle}
|
paulson@10295
|
122 |
*};
|
paulson@10295
|
123 |
|
paulson@10295
|
124 |
lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
|
paulson@10295
|
125 |
apply (rule is_gcd_unique)
|
paulson@10295
|
126 |
apply (rule is_gcd)
|
paulson@10295
|
127 |
apply (simp add: is_gcd_def);
|
paulson@10295
|
128 |
apply (blast intro: dvd_trans);
|
paulson@10295
|
129 |
done
|
paulson@10295
|
130 |
|
paulson@10295
|
131 |
text{*
|
paulson@10295
|
132 |
\begin{isabelle}
|
paulson@10295
|
133 |
proof\ (prove):\ step\ 3\isanewline
|
paulson@10295
|
134 |
\isanewline
|
paulson@10295
|
135 |
goal\ (lemma\ gcd_assoc):\isanewline
|
paulson@10295
|
136 |
gcd\ (gcd\ (k,\ m),\ n)\ =\ gcd\ (k,\ gcd\ (m,\ n))\isanewline
|
paulson@10295
|
137 |
\ 1.\ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ k\ \isasymand \isanewline
|
paulson@10295
|
138 |
\ \ \ \ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ m\ \isasymand \ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ n
|
paulson@10295
|
139 |
\end{isabelle}
|
paulson@10295
|
140 |
*}
|
paulson@10295
|
141 |
|
paulson@10295
|
142 |
|
paulson@10295
|
143 |
lemma gcd_dvd_gcd_mult: "gcd(m,n) dvd gcd(k*m, n)"
|
paulson@10295
|
144 |
apply (blast intro: dvd_trans);
|
paulson@10295
|
145 |
done
|
paulson@10295
|
146 |
|
paulson@10295
|
147 |
(*This is half of the proof (by dvd_anti_sym) of*)
|
paulson@10295
|
148 |
lemma gcd_mult_cancel: "gcd(k,n) = 1 \<Longrightarrow> gcd(k*m, n) = gcd(m,n)"
|
paulson@10295
|
149 |
oops
|
paulson@10295
|
150 |
|
paulson@10295
|
151 |
|
paulson@10295
|
152 |
|
paulson@10295
|
153 |
text{*\noindent
|
paulson@10295
|
154 |
Forward proof material: of, OF, THEN, simplify.
|
paulson@10295
|
155 |
*}
|
paulson@10295
|
156 |
|
paulson@10295
|
157 |
text{*\noindent
|
paulson@10295
|
158 |
SKIP most developments...
|
paulson@10295
|
159 |
*}
|
paulson@10295
|
160 |
|
paulson@10295
|
161 |
(** Commutativity **)
|
paulson@10295
|
162 |
|
paulson@10295
|
163 |
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
|
paulson@10295
|
164 |
apply (auto simp add: is_gcd_def);
|
paulson@10295
|
165 |
done
|
paulson@10295
|
166 |
|
paulson@10295
|
167 |
lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
|
paulson@10295
|
168 |
apply (rule is_gcd_unique)
|
paulson@10295
|
169 |
apply (rule is_gcd)
|
paulson@10295
|
170 |
apply (subst is_gcd_commute)
|
paulson@10295
|
171 |
apply (simp add: is_gcd)
|
paulson@10295
|
172 |
done
|
paulson@10295
|
173 |
|
paulson@10295
|
174 |
lemma gcd_1 [simp]: "gcd(m,1) = 1"
|
paulson@10295
|
175 |
apply (simp)
|
paulson@10295
|
176 |
done
|
paulson@10295
|
177 |
|
paulson@10295
|
178 |
lemma gcd_1_left [simp]: "gcd(1,m) = 1"
|
paulson@10295
|
179 |
apply (simp add: gcd_commute [of 1])
|
paulson@10295
|
180 |
done
|
paulson@10295
|
181 |
|
paulson@10295
|
182 |
text{*\noindent
|
paulson@10295
|
183 |
as far as HERE.
|
paulson@10295
|
184 |
*}
|
paulson@10295
|
185 |
|
paulson@10295
|
186 |
|
paulson@10295
|
187 |
text {*
|
paulson@10295
|
188 |
@{thm[display] gcd_1}
|
paulson@10295
|
189 |
\rulename{gcd_1}
|
paulson@10295
|
190 |
|
paulson@10295
|
191 |
@{thm[display] gcd_1_left}
|
paulson@10295
|
192 |
\rulename{gcd_1_left}
|
paulson@10295
|
193 |
*};
|
paulson@10295
|
194 |
|
paulson@10295
|
195 |
text{*\noindent
|
paulson@10295
|
196 |
SKIP THIS PROOF
|
paulson@10295
|
197 |
*}
|
paulson@10295
|
198 |
|
paulson@10295
|
199 |
lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
|
paulson@10295
|
200 |
apply (induct_tac m n rule: gcd.induct)
|
paulson@10295
|
201 |
apply (case_tac "n=0")
|
paulson@10295
|
202 |
apply (simp)
|
paulson@10295
|
203 |
apply (case_tac "k=0")
|
paulson@10295
|
204 |
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
|
paulson@10295
|
205 |
done
|
paulson@10295
|
206 |
|
paulson@10295
|
207 |
text {*
|
paulson@10295
|
208 |
@{thm[display] gcd_mult_distrib2}
|
paulson@10295
|
209 |
\rulename{gcd_mult_distrib2}
|
paulson@10295
|
210 |
*};
|
paulson@10295
|
211 |
|
paulson@10295
|
212 |
text{*\noindent
|
paulson@10295
|
213 |
of, simplified
|
paulson@10295
|
214 |
*}
|
paulson@10295
|
215 |
|
paulson@10295
|
216 |
|
paulson@10295
|
217 |
lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1];
|
paulson@10295
|
218 |
lemmas gcd_mult_1 = gcd_mult_0 [simplified];
|
paulson@10295
|
219 |
|
paulson@10295
|
220 |
text {*
|
paulson@10295
|
221 |
@{thm[display] gcd_mult_distrib2 [of _ 1]}
|
paulson@10295
|
222 |
|
paulson@10295
|
223 |
@{thm[display] gcd_mult_0}
|
paulson@10295
|
224 |
\rulename{gcd_mult_0}
|
paulson@10295
|
225 |
|
paulson@10295
|
226 |
@{thm[display] gcd_mult_1}
|
paulson@10295
|
227 |
\rulename{gcd_mult_1}
|
paulson@10295
|
228 |
|
paulson@10295
|
229 |
@{thm[display] sym}
|
paulson@10295
|
230 |
\rulename{sym}
|
paulson@10295
|
231 |
*};
|
paulson@10295
|
232 |
|
paulson@10295
|
233 |
lemmas gcd_mult = gcd_mult_1 [THEN sym];
|
paulson@10295
|
234 |
|
paulson@10295
|
235 |
lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
|
paulson@10295
|
236 |
(*better in one step!*)
|
paulson@10295
|
237 |
|
paulson@10295
|
238 |
text {*
|
paulson@10295
|
239 |
more legible
|
paulson@10295
|
240 |
*};
|
paulson@10295
|
241 |
|
paulson@10295
|
242 |
lemma gcd_mult [simp]: "gcd(k, k*n) = k"
|
paulson@10295
|
243 |
apply (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
|
paulson@10295
|
244 |
done
|
paulson@10295
|
245 |
|
paulson@10295
|
246 |
lemmas gcd_self = gcd_mult [of k 1, simplified];
|
paulson@10295
|
247 |
|
paulson@10295
|
248 |
|
paulson@10295
|
249 |
text {*
|
paulson@10295
|
250 |
Rules handy with THEN
|
paulson@10295
|
251 |
|
paulson@10295
|
252 |
@{thm[display] iffD1}
|
paulson@10295
|
253 |
\rulename{iffD1}
|
paulson@10295
|
254 |
|
paulson@10295
|
255 |
@{thm[display] iffD2}
|
paulson@10295
|
256 |
\rulename{iffD2}
|
paulson@10295
|
257 |
*};
|
paulson@10295
|
258 |
|
paulson@10295
|
259 |
|
paulson@10295
|
260 |
text {*
|
paulson@10295
|
261 |
again: more legible
|
paulson@10295
|
262 |
*};
|
paulson@10295
|
263 |
|
paulson@10295
|
264 |
lemma gcd_self [simp]: "gcd(k,k) = k"
|
paulson@10295
|
265 |
apply (rule gcd_mult [of k 1, simplified])
|
paulson@10295
|
266 |
done
|
paulson@10295
|
267 |
|
paulson@10295
|
268 |
lemma relprime_dvd_mult:
|
paulson@10295
|
269 |
"\<lbrakk> gcd(k,n)=1; k dvd (m*n) \<rbrakk> \<Longrightarrow> k dvd m";
|
paulson@10295
|
270 |
apply (insert gcd_mult_distrib2 [of m k n])
|
paulson@10295
|
271 |
apply (simp)
|
paulson@10295
|
272 |
apply (erule_tac t="m" in ssubst);
|
paulson@10295
|
273 |
apply (simp)
|
paulson@10295
|
274 |
done
|
paulson@10295
|
275 |
|
paulson@10295
|
276 |
|
paulson@10295
|
277 |
text {*
|
paulson@10295
|
278 |
Another example of "insert"
|
paulson@10295
|
279 |
|
paulson@10295
|
280 |
@{thm[display] mod_div_equality}
|
paulson@10295
|
281 |
\rulename{mod_div_equality}
|
paulson@10295
|
282 |
*};
|
paulson@10295
|
283 |
|
paulson@10295
|
284 |
lemma div_mult_self_is_m:
|
paulson@10295
|
285 |
"0<n \<Longrightarrow> (m*n) div n = (m::nat)"
|
paulson@10295
|
286 |
apply (insert mod_div_equality [of "m*n" n])
|
paulson@10295
|
287 |
apply (simp)
|
paulson@10295
|
288 |
done
|
paulson@10295
|
289 |
|
paulson@10295
|
290 |
lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m";
|
paulson@10295
|
291 |
apply (blast intro: relprime_dvd_mult dvd_trans)
|
paulson@10295
|
292 |
done
|
paulson@10295
|
293 |
|
paulson@10295
|
294 |
lemma relprime_20_81: "gcd(#20,#81) = 1";
|
paulson@10295
|
295 |
apply (simp add: gcd.simps)
|
paulson@10295
|
296 |
done
|
paulson@10295
|
297 |
|
paulson@10295
|
298 |
|
paulson@10295
|
299 |
text {*
|
paulson@10295
|
300 |
Examples of 'OF'
|
paulson@10295
|
301 |
|
paulson@10295
|
302 |
@{thm[display] relprime_dvd_mult}
|
paulson@10295
|
303 |
\rulename{relprime_dvd_mult}
|
paulson@10295
|
304 |
|
paulson@10295
|
305 |
@{thm[display] relprime_dvd_mult [OF relprime_20_81]}
|
paulson@10295
|
306 |
|
paulson@10295
|
307 |
@{thm[display] dvd_refl}
|
paulson@10295
|
308 |
\rulename{dvd_refl}
|
paulson@10295
|
309 |
|
paulson@10295
|
310 |
@{thm[display] dvd_add}
|
paulson@10295
|
311 |
\rulename{dvd_add}
|
paulson@10295
|
312 |
|
paulson@10295
|
313 |
@{thm[display] dvd_add [OF dvd_refl dvd_refl]}
|
paulson@10295
|
314 |
|
paulson@10295
|
315 |
@{thm[display] dvd_add [OF _ dvd_refl]}
|
paulson@10295
|
316 |
*};
|
paulson@10295
|
317 |
|
paulson@10295
|
318 |
lemma "\<lbrakk>(z::int) < #37; #66 < #2*z; z*z \<noteq> #1225; Q(#34); Q(#36)\<rbrakk> \<Longrightarrow> Q(z)";
|
paulson@10295
|
319 |
apply (subgoal_tac "z = #34 \<or> z = #36")
|
paulson@10295
|
320 |
apply blast
|
paulson@10295
|
321 |
apply (subgoal_tac "z \<noteq> #35")
|
paulson@10295
|
322 |
apply arith
|
paulson@10295
|
323 |
apply force
|
paulson@10295
|
324 |
done
|
paulson@10295
|
325 |
|
paulson@10295
|
326 |
text
|
paulson@10295
|
327 |
{*
|
paulson@10295
|
328 |
proof\ (prove):\ step\ 1\isanewline
|
paulson@10295
|
329 |
\isanewline
|
paulson@10295
|
330 |
goal\ (lemma):\isanewline
|
paulson@10295
|
331 |
\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline
|
paulson@10295
|
332 |
\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
|
paulson@10295
|
333 |
\ \ \ \ \ \ \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isasymrbrakk \isanewline
|
paulson@10295
|
334 |
\ \ \ \ \isasymLongrightarrow \ Q\ z\isanewline
|
paulson@10295
|
335 |
\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline
|
paulson@10295
|
336 |
\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36
|
paulson@10295
|
337 |
|
paulson@10295
|
338 |
|
paulson@10295
|
339 |
|
paulson@10295
|
340 |
proof\ (prove):\ step\ 3\isanewline
|
paulson@10295
|
341 |
\isanewline
|
paulson@10295
|
342 |
goal\ (lemma):\isanewline
|
paulson@10295
|
343 |
\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline
|
paulson@10295
|
344 |
\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
|
paulson@10295
|
345 |
\ \ \ \ \ \ \ z\ \isasymnoteq \ \#35\isasymrbrakk \isanewline
|
paulson@10295
|
346 |
\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isanewline
|
paulson@10295
|
347 |
\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline
|
paulson@10295
|
348 |
\ \ \ \ \isasymLongrightarrow \ z\ \isasymnoteq \ \#35
|
paulson@10295
|
349 |
*}
|
paulson@10295
|
350 |
|
paulson@10295
|
351 |
|
paulson@10295
|
352 |
end
|