is mentioned by

Thm* A:ioa{i:l}(), a:Label, Q:Fmla. wp2(A;a;Q) Fmla	[wp2_wf]
Thm* Q:Fmla. closed_pred((Q)') closed_pred(Q)	[closed_pred_addprime]
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]
Thm* Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') covers_pred(A;Q)	[covers_pred_addprime]
Thm* A:ioa{i:l}(), I:Fmla, r:rel(). r I covers_pred(A;I) covers_rel(A;r)	[covers_pred_rel_member]

In prior sections: mb automata 2

Try larger context: GenAutomata