equal
deleted
inserted
replaced
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
10 *) |
10 *) |
11 |
11 |
12 Acc = WF + |
12 Acc = WF + |
13 |
13 |
|
14 constdefs |
|
15 pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) |
|
16 "pred x r == {y. (y,x):r}" |
|
17 |
14 consts |
18 consts |
15 pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) |
|
16 acc :: "('a * 'a)set => 'a set" (*Accessible part*) |
19 acc :: "('a * 'a)set => 'a set" (*Accessible part*) |
17 |
|
18 defs |
|
19 pred_def "pred x r == {y. (y,x):r}" |
|
20 |
20 |
21 inductive "acc(r)" |
21 inductive "acc(r)" |
22 intrs |
22 intrs |
23 pred "pred a r: Pow(acc(r)) ==> a: acc(r)" |
23 pred "pred a r: Pow(acc(r)) ==> a: acc(r)" |
24 monos "[Pow_mono]" |
24 monos "[Pow_mono]" |