Nuprl - mb automata 4 LEMMAs for rel mng wf closed

Rank	Theorem	Name
3			Thm* rho:Decl, ds,daa:Collection(dec()), da1:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, tr:trace_env([[daa]] rho), r:rel(). closed_rel(r) tc(r;ds;da1;de) trace_consistent_rel(rho;daa;tr.proj;r) [[r]] rho ds da1 de e s tr Prop	[rel_mng_wf_closed]
cites
0			Thm* v:Top, rho:Decl. v [[ < > ]] rho	[empty_sts_mng]
2			Thm* r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de)	[tc_closed_rel]