Thm* A:ioa{i:l}(), as:(Label Term) List, k:Label.
ioa_mentions_trace(A) 
( i: . i < ||as||  2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))) 
subst_mentions_trace(as) | [effect_subst_mentions_trace] |
Thm* ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType)
, e1:{1of([[de]] rho)}, s:{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho), l:Term List.
( i: ||l||. trace_consistent(rho;da;tr.proj;l[i])) 
( ls:SimpleType List, f:reduce( s,m. [[s]] rho m;Prop;ls).
||ls|| = ||l|| & ( i: . i < ||l||  ls[i] term_types(ds;st1;de;l[i])) 
list_accum(x,t.x([[t]] e1 s a tr);f;l) Prop) | [rel_mng_lemma] |
Thm* ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType)
, e1:{1of([[de]] rho)}, s,s':{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho), l:Term List.
( i: ||l||. trace_consistent(rho;da;tr.proj;l[i])) 
( ls:SimpleType List, f:reduce( s,m. [[s]] rho m;Prop;ls).
||ls|| = ||l|| & ( i: . i < ||l||  ls[i] term_types(ds;st1;de;l[i])) 
list_accum(x,t.x([[t]] e1 s s' a tr);f;l) Prop) | [rel_mng_2_lemma] |
Thm* c:(Label Collection(Term)), r,r':rel().
r' col_subst2(c;r)

( as:(Label Term) List.
1of(unzip(as)) = rel_primed_vars(r)
& ( i: . i < ||as||  2of(as[i]) c(1of(as[i])))
& r' = rel_subst2(as;r)) | [member_col_subst2] |
Thm* c:(Label Collection(Term)), r,r':rel().
r' col_subst(c;r)

( as:(Label Term) List.
1of(unzip(as)) = rel_vars(r)
& ( i: . i < ||as||  2of(as[i]) c(1of(as[i])))
& r' = rel_subst(as;r)) | [member_col_subst] |
Thm* r:rel().
rel_mentions_trace(r)  ( i: . i < ||r.args|| & mentions_trace(r.args[i])) | [rel_mentions_trace_iff] |
Thm* r:rel(), i: . closed_rel(r)  i < ||r.args||  closed_term(r.args[i]) | [closed_rel_args] |
Thm* x:Label, r:rel().
(x rel_primed_vars(r))  ( i: . i < ||r.args|| & (x term_primed_vars(r.args[i]))) | [member_rel_primed_vars] |
Thm* as:(Label Term) List.
subst_mentions_trace(as)  ( i: ||as||. mentions_trace(2of(as[i]))) | [assert_subst_mentions_trace] |
Def trace_consistent_rel(rho;da;R;r)
== i: ||r.args||. trace_consistent(rho;da;R;r.args[i]) | [trace_consistent_rel] |
Def tc(r;ds;da;de)
== Case(r.name)
Case eq(Q) = >
||r.args|| = 2 & Q term_types(ds;da;de;r.args[0]) & Q term_types(ds;da;de;r.args[1])
Case R = >
||de.rel(R)|| = ||r.args||
& ( i: . i < ||r.args||  (de.rel(R))[i] term_types(ds;da;de;r.args[i]))
Default = > False | [tc] |