| Rank | Theorem | Name |
| 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] |
| cites |
| 0 | | | Thm* as:(LabelT) List, p:(LabelT), l:Label, d:T. apply_alist([p / as];l;d) ~ if 1of(p) = l 2of(p) else apply_alist(as;l;d) fi | [apply_alist_cons] |
| 2 | | | 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] |
| 1 | | | Thm* c1:Collection(T). c1 c1 | [col_le_reflexive] |