type Z [large,bounded,nonuniform].
type G [large,bounded,nonuniform].

fun exp(G,Z): G.
fun exp'(G,Z): G.
const g:G.

fun mult(Z,Z): Z. 
equation builtin commut(mult).

(* GDH assumption *)
proba pGDH.
proba pDistRerandom.
expand GDH_RSR(G, Z, g, exp, exp', mult, pGDH, pDistRerandom).

process 0