|
1478
|
1 |
(* Title: ZF/AC/recfunAC16.thy
|
|
1196
|
2 |
ID: $Id$
|
|
1478
|
3 |
Author: Krzysztof Grabczewski
|
|
1196
|
4 |
|
|
|
5 |
A recursive definition used in the proof of WO2 ==> AC16
|
|
|
6 |
*)
|
|
|
7 |
|
|
2469
|
8 |
recfunAC16 = Cardinal + Epsilon +
|
|
1196
|
9 |
|
|
2469
|
10 |
constdefs
|
|
|
11 |
recfunAC16 :: [i, i, i, i] => i
|
|
1196
|
12 |
|
|
|
13 |
"recfunAC16(f,fa,i,a) ==
|
|
1478
|
14 |
transrec2(i, 0,
|
|
11317
|
15 |
%g r. if(\\<exists>y \\<in> r. fa`g \\<subseteq> y, r,
|
|
|
16 |
r Un {f`(LEAST i. fa`g \\<subseteq> f`i &
|
|
|
17 |
(\\<forall>b<a. (fa`b \\<subseteq> f`i --> (\\<forall>t \\<in> r. ~ fa`b \\<subseteq> t))))}))"
|
|
1196
|
18 |
|
|
|
19 |
end
|