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))r:rel(), x:Label. (x rel_primed_vars(r)) (x rel_vars(r))| Rank | Theorem | Name |
| 2 |
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] |
| cites | ||
| 1 |
Thm* r:rel(), x:Label. (x rel_primed_vars(r)) (x rel_vars(r)) | [rel_primed_vars_rel_vars] |