p:Fmla, 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_pred(rho;daa;tr.proj;p) tc_pred(p;ds;da1;de) closed_pred(p) ([[p]] rho ds da1 de e s a1 tr [[p]] rho ds da2 de e s a2 tr)

1	1. p: Fmla 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_pred(rho;daa;tr.proj;p) 14. tc_pred(p;ds;da1;de) 15. closed_pred(p) [[p]] rho ds da1 de e s a1 tr [[p]] rho ds da2 de e s a2 tr
2	1. p: Fmla{i} 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: