Term) List
subst_mentions_trace(as)
x:Label.
(x 
rel_primed_vars(r))
(t:SimpleType.
mk_dec(x, t) ds
t term_types(ds;da;de;apply_alist(as;x;x))
& s'.x = [[apply_alist(as;x;x)]] 1of(e) s a tr [[t]] rho)
[[rel_subst2(as;r)]] rho ds da de e s a tr 
rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)
r1,r2:rel(), ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s1,s2:{[[ds]] rho}, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_rel(rho;daa;tr.proj;r1) trace_consistent_rel(rho;daa;tr.proj;r2) tc(r1;ds;da;de) tc(r2;ds;da;de) r1.name = r2.name ||r1.args|| = ||r2.args|| 
(i:. i < ||r1.args|| [[r1.args[i]]] 1of(e) s1 a tr = [[r2.args[i]]] 1of(e) s1 s2 a tr [[rel_arg_typ(r1.name;i;de)]] rho) ([[r1]] rho ds da de e s1 a tr rel_mng_2(r2; rho; ds; da; de; e; s1; s2; a; tr))
[rel_subst2(as;r);r;ds;daa;da;de;rho;e;s;s';a;tr]
| 1 | 18. tc(rel_subst2(as;r);ds;da;de) 19. trace_consistent_rel(rho;daa;tr.proj;rel_subst2(as;r)) 20. ||rel_subst2(as;r).args|| = ||r.args|| 21. i: 22. i < ||rel_subst2(as;r).args|| [[rel_subst2(as;r).args[i]]] 1of(e) s a tr = [[r.args[i]]] 1of(e) s s' a tr [[rel_arg_typ(rel_subst2(as;r).name;i;de)]] rho |
About:
 |  |  |  |  |  |  |  |