r:rel(), rho:Decl, ds,daa:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, a1,a2:Top, tr:trace_env([[daa]] rho). trace_consistent_rel(rho;daa;tr.proj;r) tc(r;ds;da1;de) closed_rel(r) ([[r]] rho ds da1 de e s a1 tr [[r]] rho ds da2 de e s a2 tr)

1	1. r: rel() 2. rho: Decl 3. ds: Collection(dec()) 4. daa: Collection(dec()) 5. da1: Collection(SimpleType) 6. da2: Collection(SimpleType) 7. de: sig() 8. s: {[[ds]] rho} 9. e: {[[de]] rho} 10. a1: Top 11. a2: Top 12. tr: trace_env([[daa]] rho) 13. trace_consistent_rel(rho;daa;tr.proj;r) 14. tc(r;ds;da1;de) 15. closed_rel(r) [[r]] rho ds da1 de e s a1 tr [[r]] rho ds da2 de e s a2 tr
2	1. r: rel() 2. rho: Decl{i} 3. ds: Collection{i}(dec()) 4. daa: Collection{i}(dec()) 5. da1: Collection{i}(SimpleType) 6. da2: Collection{i}(SimpleType) 7. de: sig() 8. s: {[[ds]] rho} 9. sig_mng{i:l}(de; rho) = sig_mng{i:l}(de; rho) 10. zzz: Decl{i}Decl{i'} Decl{i} Decl{i'}

About: