ds1,ds2:Collection(dec()), rho:Decl, r:(
[[ds1]] rho).
ds1 = ds2 
r 
([[ds2]] rho)ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x).
(d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x)| Theorem | Name |
|
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:([[ds1]] rho).
ds1 = ds2 r ([[ds2]] rho) | [decls_mng_functionality_sigma] |
| cites | |
|
Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x).
(d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x) | [decls_mng_member] |