Selected Objects
| def | covers_var | covers_var(A;x) ==  fr:frame(). fr  < fr A.frame | fr.var = x > & ( a:Label. (a fr.acts)   (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > )) |
| def | action_pre | action_pre(a;ps) == < p.rel | p < p ps | p.kind = a > > |
| def | imp_hyp | t.hyp == 1of(t) |
| def | imp_concl | t.concl == 2of(t) |
| def | mk_imp | mk_imp(hyp, concl) == < hyp,concl > |
| def | qimp_lbl | t.lbl == 1of(t) |
| def | qimp_hyp | t.hyp == 1of(2of(t)) |
| def | qimp_concl | t.concl == 2of(2of(t)) |
| def | mk_qimp | mk_qimp(lbl, hyp, concl) == < lbl,hyp,concl > |
| def | vc_imp | vc_imp(x) == inl(x) |
| def | case_vc_imp | Case vc_imp(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z)) |
| def | vc_qimp | vc_qimp(x) == inr(x) |
| def | case_vc_qimp | Case vc_qimp(x) = > body(x) cont(x1,z) == ( x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1]) |
| def | vc_hyp | vc_hyp(v) == Case(v) Case vc_imp(x) = > x.hyp Case vc_qimp(x) = > x.hyp Default = > False |
| def | vc_concl | vc_concl(v) == Case(v) Case vc_imp(x) = > x.concl Case vc_qimp(x) = > x.concl Default = > False |
| def | vcs | VCs{i} == Collection{i'}(vc{i:l}()) |
| def | vcs_singleton | < *v* > == < v > |
| def | vcs_add | a +* b == a + b |
| def | term_mng2 | [[t]] e s s' a tr
== iterate(statevar x- > s.x
statevar x'- > s'.x
funsymbol x- > e.x
freevar x- > a
trace(P)- > tr.P
x(y)- > x(y)
over t) |
| def | term_mentions_guard | term_mentions_guard(g;t) == term_iterate(x.false ;x.false;x.false;x.false;x.x = g;x,y. x  y;t) |
| def | term_eq | (rec) term_eq(a;b) == Case(a) Case x;y = > Case(b) Case x';y' = > term_eq(x;x') term_eq(y;y') Case tree_leaf(x) = > false Default = > True Case tree_leaf(x) = > Case(b) Case x';y' = > false Case tree_leaf(x') = > (x=x') Default = > True Default = > True |
| def | term_iter | iterate(statevar x- > v(x)
statevar x''- > v'(x')
funsymbol op- > opr(op)
freevar f- > fvar(f)
trace(tr)- > trace(tr)
a(b)- > comb(a;b)
over t)
== term_iterate(x.v(x);
x'.v'(x');
op.opr(op);
f.fvar(f);
tr.trace(tr);
a,b. comb(a;b);
t) |
| THM | assert_term_eq | a,b:Term. term_eq(a;b)  a = b |
| def | st_app1 | st_app1(s1;s2) == Case(s1) Case a;b = > if st_eq(a;s2) < b > else < > fi Default = > < > |
| THM | member_st_app1 | s1,s2,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2  s) |
| def | sig | sig() == (LabelSimpleType) (Label(SimpleType List)) |
| def | dec | dec() == LabelSimpleType |
| def | smt | smt() == LabelTermSimpleType |
| THM | smt_sq | SQType(smt()) |
| def | relname | relname() == SimpleType+Label |
| THM | relname_sq | SQType(relname()) |
| def | eq_relname | eq_relname(a;b) == Case(a) Case eq(x) = > Case(b) Case eq(x') = > st_eq(x;x') Case x' = > false Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x = x' Default = > false Default = > false |
| THM | assert_eq_relname | a,b:relname(). eq_relname(a;b) a = b |
| def | frame | frame() == LabelSimpleType(Label List) |
| def | dec_lookup | dec_lookup(ds;x) == < d.typ | d < d ds | d.lbl = x > > |
| THM | member_dec_lookup | ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds |
| def | single_valued_decls | single_valued_decls(c) == x:Label, t1,t2:SimpleType. mk_dec(x, t1) c mk_dec(x, t2) c t1 = t2 |
| THM | dec_lookup_functionality | ds1,ds2:Collection(dec()), x:Label. ds1 = ds2 dec_lookup(ds1;x) = dec_lookup(ds2;x) |
| THM | dec_lookup_monotone | x:Label, a1,a2:Collection(dec()). a1  a2 dec_lookup(a1;x) dec_lookup(a2;x) |
| def | st_mng | [[s]] rho == t_iterate(st_lift(rho);x,y. xy;s) |
| def | unprime | unprime(t) == term_iterate(x.x;x.x;op.op;f.f;P.trace(P);a,b. a b;t) |
| THM | term_mng_unprime | t:Term, e,a,s,tr:Top. [[t]] e s a tr ~ [[unprime(t)]] e s a tr |
| THM | term_mng2_unprime | t:Term, e,s,s',a,tr:Top. [[unprime(t)]] e s s' a tr ~ [[t]] e s a tr |
| def | term_subst | term_subst(as;t)
== iterate(statevar v- > apply_alist(as;v;v)
statevar v'- > apply_alist(as;v;v')
funsymbol f- > f
freevar f- > f
trace(P)- > trace(P)
x(y)- > x y
over t) |
| def | term_free_vars | term_free_vars(t) == term_iterate(f.nil;f.nil;f.nil;v.[v];P.nil;x,y. x @ y;t) |
| def | rel_vars | rel_vars(r) == reduce(t,vs. term_vars(t) @ vs;nil;r.args) |
| def | rel_mentions | rel_mentions(r;x) == i: . i < ||r.args|| & (x term_vars(r.args[i])) |
| def | col_map_subst | col_map_subst(x.f(x);c) == < f(x) | x c > |
| def | smt_terms | smt_terms(c) == < s.term | s c > |
| def | action_effect | action_effect(a;es;fs) == < e.smt | e < e es | e.kind = a > > + < mk_smt(f.var, f.var, f.typ) | f < f fs |  a f.acts > > |
| def | imp | imp{i:l}() == FmlaFmla |
| def | qimp | qimp{i:l}() == LabelFmlaFmla |
| def | addprime | (t)' == term_iterate(x.x';x.x';op.op;f.f;P.trace(P);a,b. a b;t) |
| THM | term_mng2_addprime | t:Term, e,s,s',a,tr:Top. [[(t)']] e s s' a tr ~ [[t]] e s' a tr |
| THM | term_free_vars_addprime | t:Term. term_free_vars((t)') ~ term_free_vars(t) |
| def | term_subst2 | term_subst2(as;t)
== iterate(statevar v- > v
statevar v'- > apply_alist(as;v;v')
funsymbol f- > f
freevar f- > f
trace(P)- > trace(P)
x(y)- > x y
over t) |
| THM | term_subst2_addprime | x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x) |
| def | termlist_eq | (rec) termlist_eq(a;b) == Case of a; nil Case of b; nil true ; x.xs false ; x.xs Case of b; nil false ; x'.xs' term_eq(x;x')termlist_eq(xs;xs') |
| def | mentions_trace | mentions_trace(t)
== iterate(statevar x- > false
statevar x'- > false
funsymbol x- > false
freevar x- > false
trace(P)- > true
x(y)- > x y
over t) |
| THM | assert_termlist_eq | a,b:Term List. termlist_eq(a;b) a = b |
| def | affects_trace | affects_trace(e;k;t)
== iterate(statevar x- > false
statevar x'- > false
funsymbol x- > false
freevar x- > false
trace(P)- > e(P,k)
x(y)- > x y
over t) |
| THM | mentions_guard_mentions_trace | g:Label, t:Term. term_mentions_guard(g;t) mentions_trace(t) |
| THM | term_mng_static | u:Term, e,s,a,tr,tr':Top. mentions_trace(u) ([[u]] e s a tr' ~ [[u]] e s a tr) |
| THM | unequal_termlists | a,b:Term List. a = b ||a|| = ||b|| (i:. i < ||a|| & a[i] = b[i]) |
| def | st_app | st_app(c1;c2) == ( s2c2.(s1c1.st_app1(s1;s2))) |
| THM | member_st_app | c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1) |
| THM | term_mng_tappend | u:Term, d:Decl, tr:trace_env(d), a:( d), e,s,v:Top. affects_trace(tr.proj;kind(a);u) ([[u]] e s v tappend(tr;a) ~ [[u]] e s v tr) |
| def | rel | rel() == relname()(Term List) |
| THM | rel_sq | SQType(rel()) |
| THM | st_app_monotone | a1,a2,b1,b2:Collection(SimpleType). a1 a2 b1 b2 st_app(a1;b1) st_app(a2;b2) |
| THM | st_app_functionality | a1,a2,b1,b2:Collection(SimpleType). a1 = a2 b1 = b2 st_app(a1;b1) = st_app(a2;b2) |
| def | eff | eff() == LabelLabelSimpleTypesmt() |
| def | sts_mng | [[sts]] rho ==  x:{x:SimpleType| x sts }. [[x]] rho |
| THM | empty_sts_mng | v:Top, rho:Decl. v [[ < > ]] rho |
| THM | sts_mng_subtype | sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho |
| THM | sts_mng_singleton | t:SimpleType, rho:Decl, v:[[t]] rho. v [[ < t > ]] rho |
| THM | sts_mng_functionality | sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho |
| THM | member_rel_vars | x:Label, r:rel(). (x rel_vars(r)) (i:. i < ||r.args|| & (x term_vars(r.args[i]))) |
| THM | rel_mentions_iff | r:rel(), x:Label. rel_mentions(r;x) (x rel_vars(r)) |
| def | st_list_mng | [[l]] rho == reduce(s,m. [[s]] rhom;Prop;l) |
| def | dec_mng | [[d]] rho == Case(d) Case x : s = > x:[[s]] rho |
| def | relname_mng | [[rn]] rho e == Case(rn) Case eq(Q) = > x,y. x = y [[Q]] rho Case R = > e.R Default = > True |
| def | rel_subst | rel_subst(as;r) == mk_rel(r.name, map(t.term_subst(as;t);r.args)) |
| def | rel_unprime | rel_unprime(r) == mk_rel(r.name, map(t.unprime(t);r.args)) |
| def | term_primed_vars | term_primed_vars(t)
== iterate(statevar v- > nil
statevar v'- > [v]
funsymbol f- > nil
freevar f- > nil
trace(P)- > nil
x(y)- > x @ y
over t) |
| THM | term_vars_addprime | t:Term. term_primed_vars((t)') ~ term_vars(t) |
| def | closed_term | closed_term(t) == term_free_vars(t) = nil |
| THM | closed_tapp | t1,t2:Term. closed_term(t1 t2) closed_term(t1) & closed_term(t2) |
| THM | term_primed_vars_term_vars | x:Label, u:Term. (x term_primed_vars(u)) (x term_vars(u)) |
| def | rel_free_vars | rel_free_vars(r) == reduce(t,vs. term_free_vars(t) @ vs;nil;r.args) |
| THM | closed_term_mng | t:Term, e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr) |
| THM | closed_term_mng2 | t:Term, e,s,s',a1,a2,tr:Top. closed_term(t) ([[t]] e s s' a1 tr ~ [[t]] e s s' a2 tr) |
| def | pred_mentions | pred_mentions(p;x) == r:rel(). r p & rel_mentions(r;x) |
| def | covers_rel | covers_rel(A;r) == x:Label. rel_mentions(r;x) covers_var(A;x) |
| def | smts_eff | smts_eff(ss;x) == smt_terms( < s ss | s.lbl = x > ) |
| def | vc | vc{i:l}() == imp{i:l}()+qimp{i:l}() |
| def | rel_addprime | (r)' == mk_rel(r.name, map(t.(t)';r.args)) |
| THM | rel_free_vars_addprime | r:rel(). rel_free_vars((r)') = rel_free_vars(r) |
| def | rel_subst2 | rel_subst2(as;r) == mk_rel(r.name, map(t.term_subst2(as;t);r.args)) |
| THM | rel_subst2_addprime | r:rel(), as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) rel_subst2(as;(r)') = rel_subst(as;r) |