equal
deleted
inserted
replaced
10 NOTE: univ(A) could be a translation; would simplify many proofs! |
10 NOTE: univ(A) could be a translation; would simplify many proofs! |
11 But Ind_Syntax.univ refers to the constant "univ" |
11 But Ind_Syntax.univ refers to the constant "univ" |
12 *) |
12 *) |
13 |
13 |
14 Univ = Arith + Sum + Finite + mono + |
14 Univ = Arith + Sum + Finite + mono + |
|
15 |
|
16 global |
|
17 |
15 consts |
18 consts |
16 Vfrom :: [i,i]=>i |
19 Vfrom :: [i,i]=>i |
17 Vset :: i=>i |
20 Vset :: i=>i |
18 Vrec :: [i, [i,i]=>i] =>i |
21 Vrec :: [i, [i,i]=>i] =>i |
19 univ :: i=>i |
22 univ :: i=>i |
20 |
23 |
21 translations |
24 translations |
22 "Vset(x)" == "Vfrom(0,x)" |
25 "Vset(x)" == "Vfrom(0,x)" |
|
26 |
|
27 path Univ |
23 |
28 |
24 defs |
29 defs |
25 Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))" |
30 Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))" |
26 |
31 |
27 Vrec_def |
32 Vrec_def |