is mentioned by

Thm* rho:Decl, r:rel(), da:Collection(dec()) , R:(LabelLabel). 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:(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)	[effect_subst_mentions_trace]
Thm* Q:Fmla. closed_pred((Q)') closed_pred(Q)	[closed_pred_addprime]
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]] 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)	[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]] 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)	[rel_mng_2_lemma]
Thm* 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	[term_typing]
Thm* 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)	[tc_monotone]
Thm* 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	[term_typing2]
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:(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)	[rel_subst_tc]
Thm* 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)	[rel_subst2_tc]
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc(rel_unprime(r);ds;da;de)	[tc_unprime]
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc((r)';ds;da;de)	[tc_addprime]
Thm* r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de)	[tc_closed_rel]
Thm* 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))	[tc_functionality]
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(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) Prop	[tc_wf]
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:(LabelLabel). trace_consistent(rho;da;R;t) Prop	[trace_consistent_wf]
Thm* rho:Decl, t:Term, da:Collection(dec()) , R:(LabelLabel). mentions_trace(t) trace_consistent(rho;da;R;t)	[no_mention_implies_consistent_term]
Thm* 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))	[member_col_subst2]
Thm* 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))	[closed_rel_mng2]
Thm* 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	[rel_mng_2_unprime]
Thm* 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	[rel_mng_2_addprime]
Thm* Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') covers_pred(A;Q)	[covers_pred_addprime]
Thm* c:(LabelCollection(Term)), r:rel(). col_subst(c;r) Collection(rel())	[col_subst_wf_2]
Thm* 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))	[member_col_subst]
Thm* A:ioa{i:l}(), I:Fmla, r:rel(). r I covers_pred(A;I) covers_rel(A;r)	[covers_pred_rel_member]
Thm* 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)	[rel_mng_tappend]
Thm* 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)	[rel_mng_static]
Thm* 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)	[closed_rel_mng_sq]
Thm* r:rel(). rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i]))	[rel_mentions_trace_iff]
Thm* r:rel(), x:Label. (x rel_primed_vars(r)) (x rel_vars(r))	[rel_primed_vars_rel_vars]
Thm* r:rel(), i:. closed_rel(r) i < ||r.args|| closed_term(r.args[i])	[closed_rel_args]
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* d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d1 = d2 u ([[d2]] rho)	[sigma_decls_mng_functionality]
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* ds:Collection(dec()), rho:Decl, a:([[ds]] rho). value(a) [[dec_lookup(ds;kind(a))]] rho	[sigma_decls_mng_value]
Thm* da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho. < k,w > ([[da]] rho)	[sigma_decls_mng2]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho}	[decls_mng_monotone]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho}	[decls_mng_record_subtype]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:([[ds1]] rho). ds1 = ds2 r ([[ds2]] rho)	[decls_mng_functionality_sigma]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds1 = ds2 r {[[ds2]] rho}	[decls_mng_functionality]
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* d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d2 d1 u ([[d2]] rho)	[sigma_decls_mng_monotone]
Thm* 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	[rel_mng_unprime]
Thm* r:rel(), te:(LabelLabel), 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()), 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))	[term_types_monotone_member]
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* d:dec(), rho:Decl, s:{[[d]] rho}. s {[[ < d > ]] rho}	[decls_mng_singleton]
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:(LabelTerm) 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:(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))	[term_subst2_tc]
Thm* 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))	[term_subst_tc]
Thm* 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)	[term_types_closed]
Thm* 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)	[term_types_monotone]
Thm* 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)	[term_types_functionality]
Thm* t:Term, as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) unprime(term_subst(as;t)) = unprime(t)	[trivial_term_subst]
Thm* t:ioa{i:l}(). t.frame Collection(frame())	[ioa_frame_wf]
Thm* t:ioa{i:l}(). t.eff Collection(eff())	[ioa_eff_wf]
Thm* t:ioa{i:l}(). t.pre Collection(pre())	[ioa_pre_wf]
Thm* t:ioa{i:l}(). t.init Collection(rel())	[ioa_init_wf]
Thm* t:ioa{i:l}(). t.da Collection(dec())	[ioa_da_wf]
Thm* t:ioa{i:l}(). t.ds Collection(dec())	[ioa_ds_wf]
Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t)	[term_types_unprime]
Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)	[term_types_addprime]
Thm* A:ioa{i:l}(). A ioa{i':l}	[ioa_univ_lemma]
Thm* t:pre(). t.rel rel()	[pre_rel_wf]
Thm* t:pre(). t.kind Label	[pre_kind_wf]
Thm* as:(LabelTerm) 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:(LabelTerm) 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:(LabelTerm) List. subst_mentions_trace(as) (i:||as||. mentions_trace(2of(as[i])))	[assert_subst_mentions_trace]
Thm* a,b:rel(). rel_eq(a;b) a = b	[assert_rel_eq]
Def trace_consistent_rel(rho;da;R;r) == i:||r.args||. trace_consistent(rho;da;R;r.args[i])	[trace_consistent_rel]
Def 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)	[pred_mng_2]
Def closed_pred(p) == r:rel(). r p closed_rel(r)	[closed_pred]
Def [[p]] rho ds da de e s a tr == r:rel(). r p [[r]] rho ds da de e s a tr	[pred_mng]
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 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]
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 covers_pred(A;p) == x:Label. pred_mentions(p;x) covers_var(A;x)	[covers_pred]

In prior sections: core fun 1 well fnd int 1 bool 1 sqequal 1 int 2 list 1 prog 1 rel 1 mb basic mb nat union num thy 1 mb list 1 mb label mb declaration mb record mb events mb collection mb tree mb list 2 mb automata 1 mb automata 2 mb state machine

Try larger context: GenAutomata