game1FO'_goodbad_scs_right1.qrhl

# Autogenerated file (by replacing game0FO -> game0FO', game1FO -> game1FO', etc. etc. in game1FO_goodbad_scs_right1.qrhl)

include "Adv_O2H_Game1FO'.qrhl".
include "queryGmeasured.qrhl".
include "Count.qrhl".
include "queryGmeasured.qrhl".

program game1FO'_goodbad_scs_right1 := {
  count <- 0;
  stop_at <$ uniform {..<qG+2*qH+qD+1};
  z' <$ keygenT undefined;
  G <$ uniform {G. ∀m. G m ∈ Rgood' (fst z') (snd z') m};
  call Adv_O2H_Game1FO'(Count(queryGmeasured));
  b <$ bernoulli (correctness_pksk enc dec msg_space () (fst z') (snd z'));
}.