ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}.
ds2 
ds1 
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}.
ds2 ds1 r {[[ds2]] rho} | [decls_mng_monotone] |
| 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] |