10496
|
1 |
(* Title: HOL/BCV/Kildall.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2000 TUM
|
|
5 |
|
|
6 |
Kildall's algorithm
|
|
7 |
*)
|
|
8 |
|
|
9 |
header "Kildall's Algorithm"
|
|
10 |
|
|
11 |
theory Kildall = DFA_Framework:
|
|
12 |
|
|
13 |
constdefs
|
|
14 |
pres_type :: "(nat => 's => 's) => nat => 's set => bool"
|
|
15 |
"pres_type step n A == !s:A. !p<n. step p s : A"
|
|
16 |
|
|
17 |
mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool"
|
|
18 |
"mono r step n A ==
|
|
19 |
!s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"
|
|
20 |
|
|
21 |
consts
|
|
22 |
iter :: "('s sl * (nat => 's => 's) * (nat => nat list))
|
|
23 |
* 's list * nat set => 's list"
|
|
24 |
propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set"
|
|
25 |
|
|
26 |
primrec
|
|
27 |
"propa f [] t ss w = (ss,w)"
|
|
28 |
"propa f (q#qs) t ss w = (let u = t +_f ss!q;
|
|
29 |
w' = (if u = ss!q then w else insert q w)
|
|
30 |
in propa f qs t (ss[q := u]) w')"
|
|
31 |
|
|
32 |
recdef iter
|
|
33 |
"same_fst (%((A,r,f),step,succs). semilat(A,r,f) & acc r)
|
|
34 |
(%((A,r,f),step,succs).
|
|
35 |
{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset)"
|
|
36 |
"iter(((A,r,f),step,succs),ss,w) =
|
|
37 |
(if semilat(A,r,f) & acc r & (!p:w. p < size ss) &
|
|
38 |
bounded succs (size ss) & set ss <= A & pres_type step (size ss) A
|
|
39 |
then if w={} then ss
|
|
40 |
else let p = SOME p. p : w
|
|
41 |
in iter(((A,r,f),step,succs),
|
|
42 |
propa f (succs p) (step p (ss!p)) ss (w-{p}))
|
|
43 |
else arbitrary)"
|
|
44 |
|
|
45 |
constdefs
|
|
46 |
unstables ::
|
|
47 |
"'s binop => (nat => 's => 's) => (nat => nat list) => 's list => nat set"
|
|
48 |
"unstables f step succs ss ==
|
|
49 |
{p. p < size ss & (? q:set(succs p). step p (ss!p) +_f ss!q ~= ss!q)}"
|
|
50 |
|
|
51 |
kildall :: "'s sl => (nat => 's => 's) => (nat => nat list)
|
|
52 |
=> 's list => 's list"
|
|
53 |
"kildall Arf step succs ss ==
|
|
54 |
iter((Arf,step,succs),ss,unstables (snd(snd Arf)) step succs ss)"
|
|
55 |
|
|
56 |
consts merges :: "'s binop => 's => nat list => 's list => 's list"
|
|
57 |
primrec
|
|
58 |
"merges f s [] ss = ss"
|
|
59 |
"merges f s (p#ps) ss = merges f s ps (ss[p := s +_f ss!p])"
|
|
60 |
|
|
61 |
|
|
62 |
lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric];
|
|
63 |
|
|
64 |
|
|
65 |
lemma pres_typeD:
|
|
66 |
"[| pres_type step n A; s:A; p<n |] ==> step p s : A"
|
|
67 |
by (unfold pres_type_def, blast)
|
|
68 |
|
|
69 |
lemma boundedD:
|
|
70 |
"[| bounded succs n; p < n; q : set(succs p) |] ==> q < n"
|
|
71 |
by (unfold bounded_def, blast)
|
|
72 |
|
|
73 |
lemma monoD:
|
|
74 |
"[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t"
|
|
75 |
by (unfold mono_def, blast)
|
|
76 |
|
|
77 |
(** merges **)
|
|
78 |
|
|
79 |
lemma length_merges [rule_format, simp]:
|
|
80 |
"!ss. size(merges f t ps ss) = size ss"
|
|
81 |
by (induct_tac ps, auto)
|
|
82 |
|
|
83 |
lemma merges_preserves_type [rule_format, simp]:
|
|
84 |
"[| semilat(A,r,f) |] ==>
|
|
85 |
!xs. xs : list n A --> x : A --> (!p : set ps. p<n)
|
|
86 |
--> merges f x ps xs : list n A"
|
|
87 |
apply (frule semilatDclosedI)
|
|
88 |
apply (unfold closed_def)
|
|
89 |
apply (induct_tac ps)
|
|
90 |
apply auto
|
|
91 |
done
|
|
92 |
|
|
93 |
lemma merges_incr [rule_format]:
|
|
94 |
"[| semilat(A,r,f) |] ==>
|
|
95 |
!xs. xs : list n A --> x : A --> (!p:set ps. p<size xs) --> xs <=[r] merges f x ps xs"
|
|
96 |
apply (induct_tac ps)
|
|
97 |
apply simp
|
|
98 |
apply simp
|
|
99 |
apply clarify
|
|
100 |
apply (rule order_trans)
|
|
101 |
apply simp
|
|
102 |
apply (erule list_update_incr)
|
|
103 |
apply assumption
|
|
104 |
apply simp
|
|
105 |
apply simp
|
|
106 |
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
|
|
107 |
done
|
|
108 |
|
|
109 |
lemma merges_same_conv [rule_format]:
|
|
110 |
"[| semilat(A,r,f) |] ==>
|
|
111 |
(!xs. xs : list n A --> x:A --> (!p:set ps. p<size xs) -->
|
|
112 |
(merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))"
|
|
113 |
apply (induct_tac ps)
|
|
114 |
apply simp
|
|
115 |
apply clarsimp
|
|
116 |
apply (rename_tac p ps xs)
|
|
117 |
apply (rule iffI)
|
|
118 |
apply (rule context_conjI)
|
|
119 |
apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
|
|
120 |
apply (force dest!: le_listD simp add: nth_list_update)
|
|
121 |
apply (erule subst, rule merges_incr)
|
|
122 |
apply assumption
|
|
123 |
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
|
|
124 |
apply assumption
|
|
125 |
apply simp
|
|
126 |
apply clarify
|
|
127 |
apply (rotate_tac -2)
|
|
128 |
apply (erule allE)
|
|
129 |
apply (erule impE)
|
|
130 |
apply assumption
|
|
131 |
apply (erule impE)
|
|
132 |
apply assumption
|
|
133 |
apply (drule bspec)
|
|
134 |
apply assumption
|
|
135 |
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
|
|
136 |
apply clarify
|
|
137 |
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
|
|
138 |
done
|
|
139 |
|
|
140 |
|
|
141 |
lemma list_update_le_listI [rule_format]:
|
|
142 |
"set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->
|
|
143 |
x <=_r ys!p --> semilat(A,r,f) --> x:A -->
|
|
144 |
xs[p := x +_f xs!p] <=[r] ys"
|
|
145 |
apply (unfold Listn.le_def lesub_def semilat_def)
|
|
146 |
apply (simp add: list_all2_conv_all_nth nth_list_update)
|
|
147 |
done
|
|
148 |
|
|
149 |
lemma merges_pres_le_ub:
|
|
150 |
"[| semilat(A,r,f); t:A; set ts <= A; set ss <= A;
|
|
151 |
!p. p:set ps --> t <=_r ts!p;
|
|
152 |
!p. p:set ps --> p<size ts;
|
|
153 |
ss <=[r] ts |]
|
|
154 |
==> merges f t ps ss <=[r] ts"
|
|
155 |
proof -
|
|
156 |
{ fix A r f t ts ps
|
|
157 |
have
|
|
158 |
"!!qs. [| semilat(A,r,f); set ts <= A; t:A;
|
|
159 |
!p. p:set ps --> t <=_r ts!p;
|
|
160 |
!p. p:set ps --> p<size ts |] ==>
|
|
161 |
set qs <= set ps -->
|
|
162 |
(!ss. set ss <= A --> ss <=[r] ts --> merges f t qs ss <=[r] ts)"
|
|
163 |
apply (induct_tac qs)
|
|
164 |
apply simp
|
|
165 |
apply (simp (no_asm_simp))
|
|
166 |
apply clarify
|
|
167 |
apply (rotate_tac -2)
|
|
168 |
apply simp
|
|
169 |
apply (erule allE, erule impE, erule_tac [2] mp)
|
|
170 |
apply (simp (no_asm_simp) add: closedD)
|
|
171 |
apply (simp add: list_update_le_listI)
|
|
172 |
done
|
|
173 |
} note this [dest]
|
|
174 |
|
|
175 |
case antecedent
|
|
176 |
thus ?thesis by blast
|
|
177 |
qed
|
|
178 |
|
|
179 |
|
|
180 |
lemma nth_merges [rule_format]:
|
|
181 |
"[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A -->
|
|
182 |
(!p:set ps. p<n) -->
|
|
183 |
(merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)"
|
|
184 |
apply (induct_tac "ps")
|
|
185 |
apply simp
|
|
186 |
apply (simp add: nth_list_update closedD listE_nth_in)
|
|
187 |
done
|
|
188 |
|
|
189 |
|
|
190 |
(** propa **)
|
|
191 |
|
|
192 |
lemma decomp_propa [rule_format]:
|
|
193 |
"!ss w. (!q:set qs. q < size ss) -->
|
|
194 |
propa f qs t ss w =
|
|
195 |
(merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)"
|
|
196 |
apply (induct_tac qs)
|
|
197 |
apply simp
|
|
198 |
apply (simp (no_asm))
|
|
199 |
apply clarify
|
|
200 |
apply (rule conjI)
|
|
201 |
apply (simp add: nth_list_update)
|
|
202 |
apply blast
|
|
203 |
apply (simp add: nth_list_update)
|
|
204 |
apply blast
|
|
205 |
done
|
|
206 |
|
|
207 |
(** iter **)
|
|
208 |
|
|
209 |
ML_setup {*
|
|
210 |
let
|
|
211 |
val thy = the_context ()
|
|
212 |
val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
|
|
213 |
in
|
|
214 |
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
|
10661
|
215 |
by (REPEAT(rtac wf_same_fst 1));
|
10496
|
216 |
by (split_all_tac 1);
|
|
217 |
by (asm_full_simp_tac (simpset() addsimps [thm "lesssub_def"]) 1);
|
10661
|
218 |
by (REPEAT(rtac wf_same_fst 1));
|
10496
|
219 |
by (rtac wf_lex_prod 1);
|
|
220 |
by (rtac wf_finite_psubset 2);
|
|
221 |
by (Clarify_tac 1);
|
|
222 |
by (dtac (thm "semilatDorderI" RS (thm "acc_le_listI")) 1);
|
|
223 |
by (assume_tac 1);
|
|
224 |
by (rewrite_goals_tac [thm "acc_def",thm "lesssub_def"]);
|
|
225 |
by (assume_tac 1);
|
|
226 |
qed "iter_wf"
|
|
227 |
end
|
|
228 |
*}
|
|
229 |
|
|
230 |
lemma inter_tc_lemma:
|
|
231 |
"[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==>
|
|
232 |
ss <[r] merges f t qs ss |
|
|
233 |
merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w"
|
|
234 |
apply (unfold lesssub_def)
|
|
235 |
apply (simp (no_asm_simp) add: merges_incr)
|
|
236 |
apply (rule impI)
|
|
237 |
apply (rule merges_same_conv [THEN iffD1, elim_format])
|
|
238 |
apply assumption+
|
|
239 |
defer
|
|
240 |
apply (rule sym, assumption)
|
|
241 |
apply (simp cong add: conj_cong add: le_iff_plus_unchanged [symmetric])
|
|
242 |
apply (blast intro!: psubsetI elim: equalityE)
|
|
243 |
apply simp
|
|
244 |
done
|
|
245 |
|
|
246 |
ML_setup {*
|
|
247 |
let
|
|
248 |
val thy = the_context ()
|
|
249 |
val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
|
|
250 |
in
|
|
251 |
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc));
|
|
252 |
by (asm_simp_tac (simpset() addsimps [same_fst_def,thm "pres_type_def"]) 1);
|
|
253 |
by (clarify_tac (claset() delrules [disjCI]) 1);
|
|
254 |
by (subgoal_tac "(@p. p:w) : w" 1);
|
|
255 |
by (fast_tac (claset() addIs [someI]) 2);
|
|
256 |
by (subgoal_tac "ss : list (size ss) A" 1);
|
|
257 |
by (blast_tac (claset() addSIs [thm "listI"]) 2);
|
|
258 |
by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
|
|
259 |
by (blast_tac (claset() addDs [thm "boundedD"]) 2);
|
|
260 |
by (rotate_tac 1 1);
|
|
261 |
by (asm_full_simp_tac (simpset() delsimps [thm "listE_length"]
|
|
262 |
addsimps [thm "decomp_propa",finite_psubset_def,thm "inter_tc_lemma",
|
|
263 |
bounded_nat_set_is_finite]) 1);
|
|
264 |
qed "iter_tc"
|
|
265 |
end
|
|
266 |
*}
|
|
267 |
|
|
268 |
lemma iter_induct:
|
|
269 |
"(!!A r f step succs ss w.
|
|
270 |
(!p. p = (@ p. p : w) & w ~= {} & semilat(A,r,f) & acc r &
|
|
271 |
(!p:w. p < length ss) & bounded succs (length ss) &
|
|
272 |
set ss <= A & pres_type step (length ss) A
|
|
273 |
--> P A r f step succs (merges f (step p (ss!p)) (succs p) ss)
|
|
274 |
({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))
|
|
275 |
==> P A r f step succs ss w) ==> P A r f step succs ss w"
|
|
276 |
proof -
|
|
277 |
case antecedent
|
|
278 |
show ?thesis
|
|
279 |
apply (rule_tac P = P in iter_tc [THEN iter_wf [THEN iter.induct]])
|
|
280 |
apply (rule antecedent)
|
|
281 |
apply clarify
|
|
282 |
apply simp
|
|
283 |
apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
|
|
284 |
apply (rotate_tac -1)
|
|
285 |
apply (simp add: decomp_propa)
|
|
286 |
apply (subgoal_tac "(@p. p:w) : w")
|
|
287 |
apply (blast dest: boundedD)
|
|
288 |
apply (fast intro: someI)
|
|
289 |
done
|
|
290 |
qed
|
|
291 |
|
|
292 |
lemma iter_unfold:
|
|
293 |
"[| semilat(A,r,f); acc r; set ss <= A; pres_type step (length ss) A;
|
|
294 |
bounded succs (size ss); !p:w. p<size ss |] ==>
|
|
295 |
iter(((A,r,f),step,succs),ss,w) =
|
|
296 |
(if w={} then ss
|
|
297 |
else let p = SOME p. p : w
|
|
298 |
in iter(((A,r,f),step,succs),merges f (step p (ss!p)) (succs p) ss,
|
|
299 |
{q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))"
|
|
300 |
apply (rule iter_tc [THEN iter_wf [THEN iter.simps [THEN trans]]])
|
|
301 |
apply simp
|
|
302 |
apply (rule impI)
|
|
303 |
apply (subst decomp_propa)
|
|
304 |
apply (subgoal_tac "(@p. p:w) : w")
|
|
305 |
apply (blast dest: boundedD)
|
|
306 |
apply (fast intro: someI)
|
|
307 |
apply simp
|
|
308 |
done
|
|
309 |
|
|
310 |
lemma stable_pres_lemma:
|
|
311 |
"[| semilat (A,r,f); pres_type step n A; bounded succs n;
|
|
312 |
ss : list n A; p : w; ! q:w. q < n;
|
|
313 |
! q. q < n --> q ~: w --> stable r step succs ss q; q < n;
|
|
314 |
q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q;
|
|
315 |
q ~: w | q = p |]
|
|
316 |
==> stable r step succs (merges f (step p (ss!p)) (succs p) ss) q"
|
|
317 |
apply (unfold stable_def)
|
|
318 |
apply (subgoal_tac "step p (ss!p) : A")
|
|
319 |
defer
|
|
320 |
apply (blast intro: listE_nth_in pres_typeD)
|
|
321 |
apply simp
|
|
322 |
apply clarify
|
|
323 |
apply (subst nth_merges)
|
|
324 |
apply assumption
|
|
325 |
apply assumption
|
|
326 |
prefer 2
|
|
327 |
apply assumption
|
|
328 |
apply (blast dest: boundedD)
|
|
329 |
apply (blast dest: boundedD)
|
|
330 |
apply (subst nth_merges)
|
|
331 |
apply assumption
|
|
332 |
apply assumption
|
|
333 |
prefer 2
|
|
334 |
apply assumption
|
|
335 |
apply (blast dest: boundedD)
|
|
336 |
apply (blast dest: boundedD)
|
|
337 |
apply simp
|
|
338 |
apply (rule conjI)
|
|
339 |
apply clarify
|
|
340 |
apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
|
|
341 |
intro: order_trans dest: boundedD)
|
|
342 |
apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
|
|
343 |
intro: order_trans dest: boundedD)
|
|
344 |
done
|
|
345 |
|
|
346 |
lemma merges_bounded_lemma [rule_format]:
|
|
347 |
"[| semilat (A,r,f); mono r step n A; bounded succs n;
|
|
348 |
step p (ss!p) : A; ss : list n A; ts : list n A; p < n;
|
|
349 |
ss <=[r] ts; ! p. p < n --> stable r step succs ts p |]
|
|
350 |
==> merges f (step p (ss!p)) (succs p) ss <=[r] ts"
|
|
351 |
apply (unfold stable_def)
|
|
352 |
apply (blast intro!: listE_set monoD listE_nth_in le_listD less_lengthI
|
|
353 |
intro: merges_pres_le_ub order_trans
|
|
354 |
dest: pres_typeD boundedD)
|
|
355 |
done
|
|
356 |
|
|
357 |
ML_setup {*
|
|
358 |
Unify.trace_bound := 80;
|
|
359 |
Unify.search_bound := 90;
|
|
360 |
*}
|
|
361 |
|
|
362 |
lemma iter_properties [rule_format]:
|
|
363 |
"semilat(A,r,f) & acc r & pres_type step n A & mono r step n A &
|
|
364 |
bounded succs n & (! p:w. p < n) & ss:list n A &
|
|
365 |
(!p<n. p~:w --> stable r step succs ss p)
|
|
366 |
--> iter(((A,r,f),step,succs),ss,w) : list n A &
|
|
367 |
stables r step succs (iter(((A,r,f),step,succs),ss,w)) &
|
|
368 |
ss <=[r] iter(((A,r,f),step,succs),ss,w) &
|
|
369 |
(! ts:list n A.
|
|
370 |
ss <=[r] ts & stables r step succs ts -->
|
|
371 |
iter(((A,r,f),step,succs),ss,w) <=[r] ts)"
|
|
372 |
apply (unfold stables_def)
|
|
373 |
apply (rule_tac A = A and r = r and f = f and step = step and ss = ss and w = w in iter_induct)
|
|
374 |
apply clarify
|
|
375 |
apply (frule listE_length)
|
|
376 |
apply hypsubst
|
|
377 |
apply (subst iter_unfold)
|
|
378 |
apply assumption
|
|
379 |
apply assumption
|
|
380 |
apply (simp (no_asm_simp))
|
|
381 |
apply assumption
|
|
382 |
apply assumption
|
|
383 |
apply assumption
|
|
384 |
apply (simp (no_asm_simp) del: listE_length)
|
|
385 |
apply (rule impI)
|
|
386 |
apply (erule allE)
|
|
387 |
apply (erule impE)
|
|
388 |
apply (simp (no_asm_simp) del: listE_length)
|
|
389 |
apply (subgoal_tac "(@p. p:w) : w")
|
|
390 |
prefer 2
|
|
391 |
apply (fast intro: someI)
|
|
392 |
apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A")
|
|
393 |
prefer 2
|
|
394 |
apply (blast intro: pres_typeD listE_nth_in)
|
|
395 |
apply (erule impE)
|
|
396 |
apply (simp (no_asm_simp) del: listE_length le_iff_plus_unchanged [symmetric])
|
|
397 |
apply (rule conjI)
|
|
398 |
apply (blast dest: boundedD)
|
|
399 |
apply (rule conjI)
|
|
400 |
apply (blast intro: merges_preserves_type dest: boundedD)
|
|
401 |
apply clarify
|
|
402 |
apply (blast intro!: stable_pres_lemma)
|
|
403 |
apply (simp (no_asm_simp) del: listE_length)
|
|
404 |
apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
|
|
405 |
prefer 2
|
|
406 |
apply (blast dest: boundedD)
|
|
407 |
apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A")
|
|
408 |
prefer 2
|
|
409 |
apply (blast intro: pres_typeD)
|
|
410 |
apply (rule conjI)
|
|
411 |
apply (blast intro!: merges_incr intro: le_list_trans)
|
|
412 |
apply clarify
|
|
413 |
apply (drule bspec, assumption, erule mp)
|
|
414 |
apply (simp del: listE_length)
|
|
415 |
apply (blast intro: merges_bounded_lemma)
|
|
416 |
done
|
|
417 |
|
|
418 |
|
|
419 |
lemma is_dfa_kildall:
|
|
420 |
"[| semilat(A,r,f); acc r; pres_type step n A;
|
|
421 |
mono r step n A; bounded succs n|]
|
|
422 |
==> is_dfa r (kildall (A,r,f) step succs) step succs n A"
|
|
423 |
apply (unfold is_dfa_def kildall_def)
|
|
424 |
apply clarify
|
|
425 |
apply simp
|
|
426 |
apply (rule iter_properties)
|
|
427 |
apply (simp add: unstables_def stable_def)
|
|
428 |
apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
|
|
429 |
dest: boundedD pres_typeD)
|
|
430 |
done
|
|
431 |
|
|
432 |
lemma is_bcv_kildall:
|
|
433 |
"[| semilat(A,r,f); acc r; top r T;
|
|
434 |
pres_type step n A; bounded succs n;
|
|
435 |
mono r step n A |]
|
|
436 |
==> is_bcv r T step succs n A (kildall (A,r,f) step succs)"
|
|
437 |
apply (intro is_bcv_dfa is_dfa_kildall semilatDorderI)
|
|
438 |
apply assumption+
|
|
439 |
done
|
|
440 |
|
|
441 |
end
|