Selected Objects
| def | subst_mentions_trace | subst_mentions_trace(as) == reduce( a,b. mentions_trace(2of(a))   b;false;as) |
| def | rel_eq | rel_eq(a;b) == eq_relname(a.name;b.name) termlist_eq(a.args;b.args) |
| THM | assert_rel_eq |  a,b:rel(). rel_eq(a;b)   a = b |
| THM | assert_subst_mentions_trace | as:(Label Term) List. subst_mentions_trace(as) ( i: ||as||. mentions_trace(2of(as[i]))) |
| def | pre | pre() == LabelLabelrel() |
| THM | term_subst_mentions_guard | as:(LabelTerm) List, g:Label, t:Term.
 subst_mentions_trace(as)  term_mentions_guard(g;term_subst(as;t)) term_mentions_guard(g;t) |
| THM | term_subst2_mentions_guard | as:(LabelTerm) List, g:Label, t:Term.
subst_mentions_trace(as) term_mentions_guard(g;term_subst2(as;t)) term_mentions_guard(g;t) |
| def | ioa | ioa{i:l}()
== Collection(dec())Collection(dec())Collection(rel())Collection(pre())Collection(eff())
Collection(frame()) |
| THM | ioa_univ_lemma | A:ioa{i:l}(). A  ioa{i':l} |
| def | term_types | term_types(ds;da;de;t)
== iterate(statevar x- > dec_lookup(ds;x)
statevar x'- > dec_lookup(ds;x)
funsymbol op- > < de.fun(op) >
freevar x- > da
trace(P)- > < lbl_pr( < Trace, P > ) >
c1(c2)- > st_app(c1;c2)
over t) |
| THM | term_types_addprime | t:Term, ds,da,de:Top. term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t) |
| THM | term_types_unprime | t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t) |
| THM | trivial_term_subst | t:Term, as:(LabelTerm) List.
(x:Label. unprime(apply_alist(as;x;x)) = x) unprime(term_subst(as;t)) = unprime(t) |
| def | sig_mng | [[s]] rho == < op.[[s.fun(op)]] rho,R.[[s.rel(R)]] rho > |
| THM | term_types_functionality | ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), t:Term.
ds1 = ds2 da1 = da2 term_types(ds1;da1;de;t) = term_types(ds2;da2;de;t) |
| THM | term_types_monotone | ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), t:Term.
ds1  ds2 da1 da2 term_types(ds1;da1;de;t) term_types(ds2;da2;de;t) |
| THM | term_types_closed | t:Term, ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig().
closed_term(t) term_types(ds;da1;de;t) = term_types(ds;da2;de;t) |
| THM | term_subst_tc | t:Term, s:SimpleType, as:(LabelTerm) 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)) |
| THM | term_subst2_tc | t:Term, s:SimpleType, as:(LabelTerm) 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)) |
| THM | trivial_rel_subst | r:rel(), as:(LabelTerm) List.
(x:Label. unprime(apply_alist(as;x;x)) = x) rel_unprime(rel_subst(as;r)) = rel_unprime(r) |
| def | decls_mng | [[ds]] rho == [[d]] rho for d {d:dec()| d ds } |
| THM | empty_decls_mng | v:Top, rho:Decl, x:Label. v [[ < > ]] rho(x) |
| THM | decls_mng_member | 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) |
| THM | decls_mng_subtype | ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x), a:SimpleType.
mk_dec(x, a) ds y [[a]] rho |
| THM | decls_mng_singleton | d:dec(), rho:Decl, s:{[[d]] rho}. s {[[ < d > ]] rho} |
| THM | decls_mng_rename_member | 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) |
| THM | term_types_monotone_member | ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), t:Term.
ds1 ds2
da1 da2 (a:SimpleType. a term_types(ds1;da1;de;t) a term_types(ds2;da2;de;t)) |
| def | rel_mng | [[r]] rho ds da de e s a tr == list_accum(x,t.x([[t]] 1of(e) s a tr);[[r.name]] rho 2of(e) ;r.args) |
| THM | rel_mng_nil | 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() |
| THM | rel_mng_unprime | 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 |
| THM | sigma_decls_mng_monotone | d1,d2:Collection(dec()), rho:Decl, u:( [[d1]] rho). d2 d1 u ([[d2]] rho) |
| THM | tproj_w_f | da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label.
tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List |
| THM | decls_mng_functionality | ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds1 = ds2 r {[[ds2]] rho} |
| THM | decls_mng_functionality_sigma | ds1,ds2:Collection(dec()), rho:Decl, r:([[ds1]] rho). ds1 = ds2 r ([[ds2]] rho) |
| THM | decls_mng_record_subtype | ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho} |
| THM | decls_mng_monotone | ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho} |
| THM | sigma_decls_mng2 | da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho. < k,w > ([[da]] rho) |
| THM | sigma_decls_mng_value | ds:Collection(dec()), rho:Decl, a:([[ds]] rho). value(a) [[dec_lookup(ds;kind(a))]] rho |
| def | pred_unprime | pred_unprime(P) == < rel_unprime(r) | r P > |
| THM | sigma_decls_mng_functionality | d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d1 = d2 u ([[d2]] rho) |
| THM | sigma_decls_mng_value2 | ds:Collection(dec()), rho:Decl, a:([[ds]] rho), x:Label.
mk_dec(kind(a), x) ds value(a) rho(x) |
| def | rel_primed_vars | rel_primed_vars(r) == reduce(t,vs. term_primed_vars(t) @ vs;nil;r.args) |
| THM | member_rel_primed_vars | x:Label, r:rel().
(x rel_primed_vars(r)) (i:. i < ||r.args|| & (x term_primed_vars(r.args[i]))) |
| THM | rel_vars_addprime | r:rel(). rel_primed_vars((r)') = rel_vars(r) |
| def | closed_rel | closed_rel(r) == rel_free_vars(r) = nil |
| THM | closed_rel_args | r:rel(), i:. closed_rel(r) i < ||r.args|| closed_term(r.args[i]) |
| THM | rel_primed_vars_rel_vars | r:rel(), x:Label. (x rel_primed_vars(r)) (x rel_vars(r)) |
| def | rel_mentions_trace | rel_mentions_trace(r) == reduce(x,y. mentions_trace(x) y;false;r.args) |
| THM | rel_mentions_trace_iff | r:rel(). rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i])) |
| THM | closed_rel_mng_sq | 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) |
| def | affects_trace_rel | affects_trace_rel(e;k;r) == reduce(x,y. affects_trace(e;k;x) y;false;r.args) |
| THM | rel_mng_static | 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) |
| def | covers_pred | covers_pred(A;p) == x:Label. pred_mentions(p;x) covers_var(A;x) |
| THM | rel_mng_tappend | 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) |
| THM | covers_pred_rel_member | A:ioa{i:l}(), I:Fmla, r:rel(). r I covers_pred(A;I) covers_rel(A;r) |
| def | col_subst | 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))) > ) |
| THM | member_col_subst | c:(LabelCollection(Term)), r,r':rel().
r' col_subst(c;r)
(as:(LabelTerm) List.
1of(unzip(as)) = rel_vars(r)
& (i:. i < ||as|| 2of(as[i]) c(1of(as[i])))
& r' = rel_subst(as;r)) |
| def | pred_addprime | (P)' == ( rP. < (r)' > ) |
| THM | covers_pred_addprime | Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') covers_pred(A;Q) |
| def | rel_mng_2 | rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)
== list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;r.args) |
| THM | rel_mng_2_addprime | 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 |
| THM | rel_mng_2_unprime | 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 |
| THM | closed_rel_mng2 | r:rel(), rho,ds,da1,da2,de,s,s',e,a1,a2,tr:Top.
closed_rel(r)
(rel_mng_2(r; rho; ds; da1; de; e; s; s'; a1; tr) ~ rel_mng_2
(r; rho; ds; da2; de; e; s; s'; a2; tr)) |
| def | col_subst2 | 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))) > ) |
| THM | member_col_subst2 | c:(LabelCollection(Term)), r,r':rel().
r' col_subst2(c;r)
(as:(LabelTerm) List.
1of(unzip(as)) = rel_primed_vars(r)
& (i:. i < ||as|| 2of(as[i]) c(1of(as[i])))
& r' = rel_subst2(as;r)) |
| def | trace_consistent | 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 > )))) |
| THM | no_mention_implies_consistent_term | rho:Decl, t:Term, da:Collection(dec()), R:(LabelLabel).
mentions_trace(t) trace_consistent(rho;da;R;t) |
| THM | covers_pred_lemma2 | 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)) |
| def | tc | 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 |
| THM | tproj_w_f2 | 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 |
| THM | tc_functionality | r:rel(), ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig().
ds1 = ds2 da1 = da2 (tc(r;ds1;da1;de) tc(r;ds2;da2;de)) |
| def | tc_smt | tc_smt(s;ds;da;de) == mk_dec(s.lbl, s.typ) ds & s.typ term_types(ds;da;de;s.term) |
| THM | tc_closed_rel | r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig().
closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de) |
| THM | tc_addprime | r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) tc((r)';ds;da;de) |
| THM | tc_unprime | r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) tc(rel_unprime(r);ds;da;de) |
| THM | rel_subst2_tc | r:rel(), as:(LabelTerm) 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) |
| THM | rel_subst_tc | r:rel(), as:(LabelTerm) 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) |
| THM | term_mng_equal | 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 |
| THM | term_typing2 | ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, t:Term, s,s':{[[ds]] rho}
, e:{1of([[de]] rho)}, a:SimpleType, v:[[da]] rho, tr:trace_env([[daa]] rho).
trace_consistent(rho;daa;tr.proj;t) a term_types(ds;da;de;t) [[t]] e s s' v tr [[a]] rho |
| THM | tc_monotone | r:rel(), de:sig(), ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType).
ds1 ds2 da1 da2 tc(r;ds1;da1;de) tc(r;ds2;da2;de) |
| def | guarded_trace | guarded_trace(da;e;I)
== r:rel(). r I (k:Label. affects_trace_rel(e;k;r) (t:dec(). t da & t.lbl = k)) |
| THM | term_typing | ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, t:Term, s:{[[ds]] rho}
, e:{1of([[de]] rho)}, a:SimpleType, v:[[st1]] rho, tr:trace_env([[da]] rho).
trace_consistent(rho;da;tr.proj;t) a term_types(ds;st1;de;t) [[t]] e s v tr [[a]] rho |
| THM | rel_mng_2_lemma | 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]] rhom;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) |
| def | pred_mng | [[p]] rho ds da de e s a tr == r:rel(). r p [[r]] rho ds da de e s a tr |
| THM | rel_mng_lemma | 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]] rhom;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) |
| def | closed_pred | closed_pred(p) == r:rel(). r p closed_rel(r) |
| THM | closed_pred_addprime | Q:Fmla. closed_pred((Q)') closed_pred(Q) |
| def | ioa_mentions_trace | ioa_mentions_trace(A)
== (e:eff(). e A.eff & mentions_trace(e.smt.term))
(p:pre(). p A.pre & rel_mentions_trace(p.rel))
(r:rel(). r A.init & rel_mentions_trace(r)) |
| def | smts_eff_rel | smts_eff_rel(ss;r) == col_subst(x.smts_eff(ss;x);r) |
| THM | effect_subst_mentions_trace | A:ioa{i:l}(), as:(LabelTerm) 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) |
| def | pred_mng_2 | pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr)
== r:rel(). r p rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr) |
| def | wp2 | wp2(A;a;Q) == (rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r)) |
| def | wp2_rel | wp2_rel(A;a;r) == col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r) |
| def | trace_consistent_rel | trace_consistent_rel(rho;da;R;r) == i:||r.args||. trace_consistent(rho;da;R;r.args[i]) |
| THM | no_mention_implies_consistent_rel | rho:Decl, r:rel(), da:Collection(dec()), R:(LabelLabel).
rel_mentions_trace(r) trace_consistent_rel(rho;da;R;r) |