// host performs both send1 and send2 only finitely many times
Pmax
=?[
G
F
(
t
=
1
) ]