equal
deleted
inserted
replaced
19 univ :: "i=>i" |
19 univ :: "i=>i" |
20 |
20 |
21 translations |
21 translations |
22 "Vset(x)" == "Vfrom(0,x)" |
22 "Vset(x)" == "Vfrom(0,x)" |
23 |
23 |
24 rules |
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" |