Adv_O2H_Game2FO'.qrhl

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

# Autogenerated file (by replacing game1FO' -> game2FO', decapsQuery1 -> decapsQuery2 in Adv_O2H_Game1FO'.qrhl)

include "ClassicalQueryG.qrhl".
include "queryH_Hq.qrhl".
include "decapsQuery2_G.qrhl".
include "Adv_INDCCA_encFO.qrhl".

program Adv_O2H_Game2FO'(query) := {
  (pk,sk) <- z';
  Hr <$ uniform UNIV;
  H0 <$ uniform UNIV;
  Hq <$ uniform UNIV;
  prfk <$ keygenPRF;
  mstar <$ uniform (msg_spaceT undefined);
  gin <- mstar;
  call ClassicalQueryG(query);
  cstar <- encr () pk mstar gout;
  Kstar <$ uniform UNIV;
  in_pk <- pk;
  in_cstar <- cstar;
  gin <- undefined;
  gout <- undefined;
  call Adv_INDCCA_encFO(query,queryH_Hq(query),decapsQuery2_G(query));
}.