| Rank | Theorem | Name |
| 3 | | | Thm*  A:ioa{i:l}(), rho:Decl, de:sig(), act:( [[A.da]] rho), r,r0:rel(). tc_ioa(A;de)   r  smts_eff_rel(action_effect(kind(act);A.eff;A.frame);r0)  rel_eq(rel_unprime(r);rel_unprime(r0)) ( t:dec(). t A.da & t.lbl = kind(act)) | [rel_effect_lemma] |
| cites |
| 2 | | | Thm* r:rel(), as:(Label Term) List. (x:Label. unprime(apply_alist(as;x;x)) = x) rel_unprime(rel_subst(as;r)) = rel_unprime(r) | [trivial_rel_subst] |
| 1 | | | Thm* as:(LabelT) List, d:T, x:Label. (x 1of(unzip(as))) ( < x,apply_alist(as;x;d) > as) | [apply_alist_member] |
| 1 | | | Thm* as:(LabelT) List, d:T, x:Label. (x 1of(unzip(as))) apply_alist(as;x;d) = d | [apply_alist_non_member] |
| 0 | | | Thm* a,b:Term List. a = b ||a|| = ||b||  (i:. i < ||a|| & a[i] = b[i]) | [unequal_termlists] |
| 1 | | | Thm* f:(A  B), as:A List, n:||as||. map(f;as)[n] = f(as[n]) | [map_select] |