Thm* as:(Label Term) List, A:ioa{i:l}(), de:sig(), x:Label, t:SimpleType, k:Label. single_valued_decls(A.ds) ![](FONT/eq.png) tc_ioa(A;de) ![](FONT/eq.png) ( i: . i < ||as|| ![](FONT/eq.png) 2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))) ![](FONT/eq.png) mk_dec(x, t) A.ds ![](FONT/eq.png) t term_types(A.ds;dec_lookup(A.da;k);de;apply_alist(as;x;x)) | [tc_ioa_lemma] |
Thm* r:rel(), as:(Label Term) List, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s,s':{[[ds]] rho}, k:Label, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_rel(rho;daa;tr.proj;r) ![](FONT/eq.png) tc(r;ds;da;de) ![](FONT/eq.png) subst_mentions_trace(as) ![](FONT/eq.png) ( x:Label. (x rel_primed_vars(r)) ![](FONT/eq.png) ( t:SimpleType. mk_dec(x, t) ds ![](FONT/eq.png) 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)) ![](FONT/eq.png) tc(rel_subst2(as;r);ds;da;de) & trace_consistent_rel(rho;daa;tr.proj;rel_subst2(as;r)) & ([[rel_subst2(as;r)]] rho ds da de e s a tr ![](FONT/if_big.png) rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)) | [rel_subst_mng_2_iff] |
Thm* 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) ![](FONT/eq.png) trace_consistent_rel(rho;daa;tr.proj;r2) ![](FONT/eq.png) tc(r1;ds;da;de) ![](FONT/eq.png) tc(r2;ds;da;de) ![](FONT/eq.png) r1.name = r2.name ![](FONT/eq.png) ||r1.args|| = ||r2.args|| ![](FONT/eq.png) ( i: . i < ||r1.args|| ![](FONT/eq.png) [[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) ![](FONT/eq.png) ([[r1]] rho ds da de e s1 a tr ![](FONT/if_big.png) rel_mng_2(r2; rho; ds; da; de; e; s1; s2; a; tr)) | [rel_mng_2_iff] |
Thm* r:rel(), i: , ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) ![](FONT/eq.png) tc(r;ds;st1;de) ![](FONT/eq.png) i < ||r.args|| ![](FONT/eq.png) [[r.args[i]]] e s a tr [[rel_arg_typ(r.name;i;de)]] rho | [rel_arg_typing] |
Thm* r:rel(), i: , ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) ![](FONT/eq.png) tc(r;ds;st1;de) ![](FONT/eq.png) i < ||r.args|| ![](FONT/eq.png) [[r.args[i]]] e s s' a tr [[rel_arg_typ(r.name;i;de)]] rho | [rel_arg_typing2] |
Def [[A]] rho de e == mk_sm([[A.da]] rho, [[A.ds]] rho, s.[[A.init]] rho A.ds < > de e s niltrace(), s1,a,s2. ( p:pre(). p A.pre ![](FONT/eq.png) p.kind = kind(a) ![](FONT/eq.png) [[p.rel]] rho A.ds dec_lookup(A.da;kind(a)) de e s1 value(a) niltrace()) & ( ef:eff(). ef A.eff ![](FONT/eq.png) ef.kind = kind(a) ![](FONT/eq.png) s2.ef.smt.lbl = [[ef.smt.term]] 1of(e) s1 value(a) niltrace() [[ef.smt.typ]] rho) & ( fr:frame(). fr A.frame ![](FONT/eq.png) (kind(a) fr.acts) ![](FONT/eq.png) s2.fr.var = s1.fr.var [[fr.typ]] rho)) | [ioa_mng] |