equal
deleted
inserted
replaced
23 |
23 |
24 defs |
24 defs |
25 Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))" |
25 Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))" |
26 |
26 |
27 Vrec_def |
27 Vrec_def |
28 "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). \ |
28 "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). |
29 \ H(z, lam w:Vset(x). g`rank(w)`w)) ` a" |
29 H(z, lam w:Vset(x). g`rank(w)`w)) ` a" |
30 |
30 |
31 univ_def "univ(A) == Vfrom(A,nat)" |
31 univ_def "univ(A) == Vfrom(A,nat)" |
32 |
32 |
33 end |
33 end |