| Rank | Theorem | Name |
| 4 | | | Thm*  A:ioa{i:l}(), Q:Fmla, de:sig(), a:Label. tc_ioa(A;de)   single_valued_decls(A.ds) tc_pred(Q;A.ds;dec_lookup(A.da;a);de) tc_pred(wp(A;a;Q);A.ds;dec_lookup(A.da;a);de) | [tc_wp] |
| cites |
| 0 | | | Thm* c:Collection(T), f:(T  Collection(T')), y:T'. y  ( xc.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] |
| 3 | | | Thm* as:(LabelTerm) 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] |