trace_consistent_rel(rho;daa;tr.proj;r) tc(r;ds1;da1;de)
[[r]] rho ds2 da2 de e s a tr25. [[r]] rho ds1 da1 de e s a tr
[[r]] rho ds2 da2 de e s a tr [[r]] rho ds1 da1 de e s a tr
r
p1.trace_consistent_rel(rho;daa;tr.proj;r))
r:rel(). r p1 tc(r;ds1;da1;de)
{[[ds2]] rho}
r:rel(). r p2 [[r]] rho ds2 da2 de e s a tr
p1
[[r]] rho ds1 da1 de e s a tr
r:rel(), ds1,ds2,da:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds1]] rho}, a:[[da1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds1;da1;de) ds1 = ds2 da1 = da2 ([[r]] rho ds1 da1 de e s a tr [[r]] rho ds2 da2 de e s a tr)
[r;ds1;ds2;daa;da1;da2;de;rho;e;s;a;tr]
| 1 | trace_consistent_rel(rho;daa;tr.proj;r) |
| 2 | tc(r;ds1;da1;de) |
| 3 | 24. [[r]] rho ds1 da1 de e s a tr [[r]] rho ds2 da2 de e s a tr 25. [[r]] rho ds1 da1 de e s a tr [[r]] rho ds2 da2 de e s a tr [[r]] rho ds1 da1 de e s a tr |
About:
 |  |  |