open Preamble

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Extralib

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

type ('output, 'input, 't) iO =
| Interact of 'output * ('input -> ('output, 'input, 't) iO)
| Value of 't
| Wrong of Errors.errmsg

val iO_rect_Type4 :
  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4

val iO_rect_Type3 :
  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4

val iO_rect_Type2 :
  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4

val iO_rect_Type1 :
  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4

val iO_rect_Type0 :
  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4

val iO_inv_rect_Type4 :
  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  'a4

val iO_inv_rect_Type3 :
  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  'a4

val iO_inv_rect_Type2 :
  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  'a4

val iO_inv_rect_Type1 :
  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  'a4

val iO_inv_rect_Type0 :
  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  'a4

val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __

val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __

open Proper

val bindIO :
  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO

val iOMonad : Monad.monadProps

val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __

val iORel : Monad.monadRel

val pred_io_inject : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO

val iOPred : Monad.injMonadPred

val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO

val dpi1__o__err_to_io__o__inject :
  ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO Types.sig0

val eject__o__err_to_io__o__inject :
  'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0

val err_to_io__o__inject : 'a2 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0

val dpi1__o__err_to_io :
  ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO

val eject__o__err_to_io : 'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO

val err_to_io_sig :
  'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO

val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO

val io_inject :
  ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO

val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO

val dpi1__o__io_inject__o__inject :
  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
  Types.sig0) iO Types.sig0

val eject__o__io_inject__o__inject :
  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0) iO
  Types.sig0

val io_inject__o__inject :
  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0

val dpi1__o__io_inject :
  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
  Types.sig0) iO

val eject__o__io_inject :
  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0) iO

val io_inject__o__io_eject__o__inject :
  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO Types.sig0

val dpi1__o__err_to_io__o__io_eject__o__inject :
  ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
  Types.sig0

val dpi1__o__io_inject__o__io_eject__o__inject :
  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
  Types.sig0

val eject__o__err_to_io__o__io_eject__o__inject :
  'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0

val eject__o__io_inject__o__io_eject__o__inject :
  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0

val err_to_io__o__io_eject__o__inject :
  'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0

val dpi1__o__io_eject__o__inject :
  (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
  Types.sig0

val eject__o__io_eject__o__inject :
  ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0

val io_eject__o__inject :
  ('a1, 'a3, 'a2 Types.sig0) iO -> ('a1, 'a3, 'a2) iO Types.sig0

val io_inject__o__io_eject :
  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO

val dpi1__o__err_to_io__o__io_eject :
  ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO

val dpi1__o__io_inject__o__io_eject :
  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO

val eject__o__err_to_io__o__io_eject :
  'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO

val eject__o__io_inject__o__io_eject :
  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO

val err_to_io__o__io_eject : 'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO

val dpi1__o__io_eject :
  (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO

val eject__o__io_eject :
  ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO

val opt_to_io : Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO

val bind_res_value :
  'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
  'a5) -> 'a5

val bindIO_value :
  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
  __ -> 'a5) -> 'a5

val bindIO_res_interact :
  'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1, 'a2,
  'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5

val bindIO_opt_interact :
  Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 ->
  ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5

val eq_to_rel_io__o__io_eq_from_res__o__inject :
  'a2 Errors.res -> 'a2 -> __ Types.sig0

val eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0

val jmeq_to_eq__o__io_eq_from_res__o__inject :
  'a2 Errors.res -> 'a2 -> __ Types.sig0

val jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0

val dpi1__o__io_eq_from_res__o__inject :
  'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0

val dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
  Types.sig0

val eject__o__io_eq_from_res__o__inject :
  'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0

val eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0

val io_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0

val io_eq_from_res__o__inject : 'a2 Errors.res -> 'a2 -> __ Types.sig0

val jmeq_to_eq__o__io_monad_eq_from_res__o__inject :
  'a2 Errors.res -> 'a2 -> __ Types.sig0

val jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0

val dpi1__o__io_monad_eq_from_res__o__inject :
  'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0

val dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
  Types.sig0

val eject__o__io_monad_eq_from_res__o__inject :
  'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0

val eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0

val io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0

val io_monad_eq_from_res__o__inject : 'a2 Errors.res -> 'a2 -> __ Types.sig0

val eq_to_rel_io__o__io_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0

val jmeq_to_eq__o__io_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0

val dpi1__o__io_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
  Types.sig0

val eject__o__io_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __ Types.sig0

val io_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0

val jmeq_to_eq__o__io_monad_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0

val dpi1__o__io_monad_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
  Types.sig0

val eject__o__io_monad_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __ Types.sig0

val io_monad_eq_from_opt__o__inject :
  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0