equal
deleted
inserted
replaced
74 (*Injections of the "disjoint sum"*) |
74 (*Injections of the "disjoint sum"*) |
75 In0_def: "In0(M) == Scons (Numb 0) M" |
75 In0_def: "In0(M) == Scons (Numb 0) M" |
76 In1_def: "In1(M) == Scons (Numb 1) M" |
76 In1_def: "In1(M) == Scons (Numb 1) M" |
77 |
77 |
78 (*Function spaces*) |
78 (*Function spaces*) |
79 Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}" |
79 Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}" |
80 |
80 |
81 (*the set of nodes with depth less than k*) |
81 (*the set of nodes with depth less than k*) |
82 ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" |
82 ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" |
83 ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}" |
83 ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}" |
84 |
84 |