Thm* r:rel(), rho,ds,da,de,e,s,s',a,tr:Top.
rel_mng_2(rel_unprime(r); rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s a tr | [rel_mng_2_unprime] |
Thm* r:rel(), rho,ds,da,de,e,s,s',a,tr:Top.
rel_mng_2((r)'; rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s' a tr | [rel_mng_2_addprime] |
Thm* d:Decl, tr:trace_env(d), a:( d), r:rel(), rho,ds,da,de,e,s,v:Top.
affects_trace_rel(tr.proj;kind(a);r) 
([[r]] rho ds da de e s v tappend(tr;a) ~ [[r]] rho ds da de e s v tr) | [rel_mng_tappend] |
Thm* r:rel(), rho,ds,da,de,e,s,a,tr,tr':Top.
rel_mentions_trace(r)  ([[r]] rho ds da de e s a tr' ~ [[r]] rho ds da de e s a tr) | [rel_mng_static] |
Thm* r:rel(), rho,ds,da1,da2,de,s,e,a1,a2,tr:Top.
closed_rel(r)  ([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr) | [closed_rel_mng_sq] |
Thm* r:rel(), e,a,s,ds,da,de,rho,tr:Top.
[[r]] rho ds da de e s a tr ~ [[rel_unprime(r)]] rho ds da de e s a tr | [rel_mng_unprime] |
Thm* r:rel(), te:(Label Label  ), rho,ds,da,de,e,s,a:Top.
[[r]] rho ds da de e s a mk_trace_env(nil, te) ~ [[r]] rho ds da de e s a niltrace() | [rel_mng_nil] |
Def [[p]] rho ds da de e s a tr == r:rel(). r p  [[r]] rho ds da de e s a tr | [pred_mng] |