Rank | Theorem | Name |
4 | | | Thm* A:ioa{i:l}(), I:Fmla, de:sig(). tc_ioa(A;de)  tc_pred(I;A.ds; < > ;de)  covers_pred(A;I)  closed_pred(I)  single_valued_decls(A.ds)  tc_vcs{i}(VCs(A;I);A.ds;A.da;de) | [tc_ioa_inv_vc] |
cites |
1 | | | Thm* A:ioa{i:l}(). A ioa{i':l} | [ioa_univ_lemma] |
0 | | | Thm* c:Collection(T), f:(T Collection(T')), y:T'. y ( x c.f(x))  ( x:T. x c & y f(x)) | [member_col_accum] |
1 | | | 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] |
2 | | | 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] |
3 | | | Thm* as:(Label Term) List, A:ioa{i:l}(), de:sig(), x:Label, t:SimpleType, k:Label. single_valued_decls(A.ds)  tc_ioa(A;de)  ( i: . i < ||as||  2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i])))  mk_dec(x, t) A.ds  t term_types(A.ds;dec_lookup(A.da;k);de;apply_alist(as;x;x)) | [tc_ioa_lemma] |