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)

1

1. r: rel() 2. ds1: Collection(dec()) 3. ds2: Collection(dec()) 4. da: Collection(dec()) 5. da1: Collection(SimpleType) 6. da2: Collection(SimpleType) 7. de: sig() 8. rho: Decl 9. e: {[[de]] rho} 10. s: {[[ds1]] rho} 11. a: [[da1]] rho 12. tr: trace_env([[da]] rho) 13. trace_consistent_rel(rho;da;tr.proj;r) 14. tc(r;ds1;da1;de) 15. ds1 = ds2 16. da1 = da2 [[r]] rho ds1 da1 de e s a tr [[r]] rho ds2 da2 de e s a tr

2

1. r: rel() 2. ds1: Collection{i}(dec()) 3. ds2: Collection{i}(dec()) 4. da: Collection{i}(dec()) 5. da1: Collection{i}(SimpleType) 6. da2: Collection{i}(SimpleType) 7. de: sig() 8. rho: Decl{i} 9. sig_mng{i:l}(de; rho) = sig_mng{i:l}(de; rho) 10. zzz: Decl{i}Decl{i'} Decl{i} Decl{i'}

About: