Thm* rho:Decl, r:rel(), da:Collection(dec())
, R:(Label Label  ). rel_mentions_trace(r)  trace_consistent_rel(rho;da;R;r) | [no_mention_implies_consistent_rel] |
Thm* A:ioa{i:l}(), a:Label, Q:Fmla. wp2(A;a;Q) Fmla | [wp2_wf] |
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()), st:Collection(SimpleType), de:sig(), rho:Decl
, e1:{1of([[de]] rho)}, s1,s2:{[[ds]] rho}, a:[[st]] rho, tr:trace_env([[da]] rho), u:Term
, t:SimpleType.
trace_consistent(rho;da;tr.proj;u) 
( x:Label. (x term_vars(u))  s1.x = s2.x) 
t term_types(ds;st;de;u)  [[u]] e1 s1 a tr = [[u]] e1 s2 a tr [[t]] rho | [term_mng_equal] |
Thm* r:rel(), as:(Label Term) List, ds:Collection(dec())
, da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) 
( x:Label.
(x rel_vars(r)) 
( t:SimpleType. mk_dec(x, t) ds  t term_types(ds;da;de;apply_alist(as;x;x))))

tc(rel_subst(as;r);ds;da;de) | [rel_subst_tc] |
Thm* r:rel(), as:(Label Term) List, ds:Collection(dec())
, da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) 
( 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))))

tc(rel_subst2(as;r);ds;da;de) | [rel_subst2_tc] |
Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label.
trace_consistent(rho;da;tr.proj;trace(y1))  tr.y1 [[lbl_pr( < Trace, y1 > )]] rho | [tproj_w_f2] |
Thm* r:rel(), I:Fmla, A:ioa{i:l}(), a:Label.
covers_pred(A;I) 
r I  ( r':rel(). r' col_subst2( x.smts_eff(action_effect(a;A.eff;A.frame);x);r)) | [covers_pred_lemma2] |
Thm* rho:Decl, t:Term, da:Collection(dec()), R:(Label Label  ).
trace_consistent(rho;da;R;t) Prop | [trace_consistent_wf] |
Thm* rho:Decl, t:Term, da:Collection(dec())
, R:(Label Label  ). mentions_trace(t)  trace_consistent(rho;da;R;t) | [no_mention_implies_consistent_term] |
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:rel(). col_subst(c;r) Collection(rel()) | [col_subst_wf_2] |
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(), x:Label. (x rel_primed_vars(r))  (x rel_vars(r)) | [rel_primed_vars_rel_vars] |
Thm* r:rel(). rel_primed_vars((r)') = rel_vars(r) | [rel_vars_addprime] |
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* ds:Collection(dec()), rho:Decl, a:( [[ds]] rho), x:Label.
mk_dec(kind(a), x) ds  value(a) rho(x) | [sigma_decls_mng_value2] |
Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label
, t:SimpleType. t dec_lookup(ds;x)  s.x [[t]] rho | [record_select_wf_decls_mng2] |
Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label
, t:SimpleType. mk_dec(x, t) ds  s.x [[t]] rho | [record_select_wf_decls_mng] |
Thm* da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho.
< k,w > ( [[da]] rho) | [sigma_decls_mng2] |
Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label.
tr.y1 {a:( [[da]] rho)| tr.proj(y1,kind(a)) } List | [tproj_w_f] |
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] |
Thm* ds1,ds2:Collection(dec()), x,y:Label, rho:Decl
, v:[[ds1]] rho(x). ( d:dec(). d ds2  d.lbl = y  mk_dec(x, d.typ) ds1)  v [[ds2]] rho(y) | [decls_mng_rename_member] |
Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x)
, a:SimpleType. mk_dec(x, a) ds  y [[a]] rho | [decls_mng_subtype] |
Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x).
( d:dec(). d ds2  d.lbl = x  d ds1)  v [[ds2]] rho(x) | [decls_mng_member] |
Thm* v:Top, rho:Decl, x:Label. v [[ < > ]] rho(x) | [empty_decls_mng] |
Thm* r:rel(), as:(Label Term) List.
( x:Label. unprime(apply_alist(as;x;x)) = x)  rel_unprime(rel_subst(as;r)) = rel_unprime(r) | [trivial_rel_subst] |
Thm* t:Term, s:SimpleType, as:(Label Term) List, ds:Collection(dec())
, da:Collection(SimpleType), de:sig().
s term_types(ds;da;de;t) 
( x:Label.
(x term_primed_vars(t)) 
( t:SimpleType. mk_dec(x, t) ds  t term_types(ds;da;de;apply_alist(as;x;x))))

s term_types(ds;da;de;term_subst2(as;t)) | [term_subst2_tc] |
Thm* t:Term, s:SimpleType, as:(Label Term) List, ds:Collection(dec())
, da:Collection(SimpleType), de:sig().
s term_types(ds;da;de;t) 
( x:Label.
(x term_vars(t)) 
( t:SimpleType. mk_dec(x, t) ds  t term_types(ds;da;de;apply_alist(as;x;x))))

s term_types(ds;da;de;term_subst(as;t)) | [term_subst_tc] |
Thm* t:Term, as:(Label Term) List.
( x:Label. unprime(apply_alist(as;x;x)) = x)  unprime(term_subst(as;t)) = unprime(t) | [trivial_term_subst] |
Thm* t:pre(). t.kind Label | [pre_kind_wf] |
Thm* as:(Label Term) List, g:Label, t:Term.
subst_mentions_trace(as)  term_mentions_guard(g;term_subst2(as;t))  term_mentions_guard(g;t) | [term_subst2_mentions_guard] |
Thm* as:(Label Term) List, g:Label, t:Term.
subst_mentions_trace(as)  term_mentions_guard(g;term_subst(as;t))  term_mentions_guard(g;t) | [term_subst_mentions_guard] |
Thm* as:(Label Term) List.
subst_mentions_trace(as)  ( i: ||as||. mentions_trace(2of(as[i]))) | [assert_subst_mentions_trace] |
Def guarded_trace(da;e;I)
== r:rel(). r I  ( k:Label. affects_trace_rel(e;k;r)  ( t:dec(). t da & t.lbl = k)) | [guarded_trace] |
Def trace_consistent(rho;da;R;t)
== g:Label.
term_mentions_guard(g;t) 
subtype_rel(({a:( [[da]] rho)| (R(g,kind(a))) } List); (rho(lbl_pr( < Trace, g > )))) | [trace_consistent] |
Def col_subst2(c;r)
== col_map_subst(as.rel_subst2(as;r); < zip(rel_primed_vars(r);s) |
s col_list_prod(map(c;rel_primed_vars(r))) > ) | [col_subst2] |
Def col_subst(c;r)
== col_map_subst(as.rel_subst(as;r); < zip(rel_vars(r);s) | s col_list_prod(map(c;rel_vars(r))) > ) | [col_subst] |
Def covers_pred(A;p) == x:Label. pred_mentions(p;x)  covers_var(A;x) | [covers_pred] |
Def closed_rel(r) == rel_free_vars(r) = nil | [closed_rel] |
Def pre() == Label Label rel() | [pre] |