is mentioned by

Def wp2(A;a;Q) == (rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))	[wp2]
Def (P)' == (rP. < (r)' > )	[pred_addprime]

In prior sections: mb collection mb automata 2

Try larger context: GenAutomata