type cleartext.
type ciphertext.
type key [bounded].
type enc_seed [bounded].

fun enc(cleartext, key, enc_seed): ciphertext.
fun Z(cleartext):cleartext.

param N.
proba Penc.

equiv(ind_cpa(enc))
  k <-R key; 
  foreach i <= N do 
    r <-R enc_seed; 
    Oenc(x:cleartext) :=  return(enc(x, k, r)) 
<=(Penc(time, N, maxlength(x)))=> 
  k <-R key;
  foreach i <= N do 
  r <-R enc_seed; 
  Oenc(x:cleartext) := return(enc(Z(x), k, r)).

process 0