equal
deleted
inserted
replaced
6 Epsilon induction and recursion |
6 Epsilon induction and recursion |
7 *) |
7 *) |
8 |
8 |
9 Epsilon = Nat + "mono" + |
9 Epsilon = Nat + "mono" + |
10 consts |
10 consts |
11 eclose,rank :: "i=>i" |
11 eclose,rank :: i=>i |
12 transrec :: "[i, [i,i]=>i] =>i" |
12 transrec :: [i, [i,i]=>i] =>i |
13 |
13 |
14 defs |
14 defs |
15 eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))" |
15 eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))" |
16 transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" |
16 transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" |
17 rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))" |
17 rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))" |