Lines Matching refs:random
73 val unif_prog_space_leakage_computation_reduce_COMPUTE = prove (``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ ~((high CROSS low) CROSS random={}) ==> (leakage (unif_prog_space high low random) f = (1/(&(CARD high * CARD low * CARD random)))* (SIGMA (\(out,h,l). (\x. x * lg (((1/(&(CARD random)))* x))) (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random))
74 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) -
75 SIGMA (\(out,l). (\x. x * lg (((1/(&(CARD high * CARD random)))* x)))
76 (SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) (high CROSS random)))
77 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))))``, METIS_TAC [unif_prog_space_leakage_computation_reduce]);