equal
deleted
inserted
replaced
1 (* Title: ZF/AC/recfunAC16.thy |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Grabczewski |
|
4 |
|
5 A recursive definition used in the proof of WO2 ==> AC16 |
|
6 *) |
|
7 |
|
8 recfunAC16 = Cardinal + Epsilon + |
|
9 |
|
10 constdefs |
|
11 recfunAC16 :: [i, i, i, i] => i |
|
12 |
|
13 "recfunAC16(f,fa,i,a) == |
|
14 transrec2(i, 0, |
|
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))))}))" |
|
18 |
|
19 end |
|