Lines Matching refs:random
110 `unif_prog_dist high low random =
111 (\s. if s IN (high CROSS low) CROSS random then
112 1/(&(CARD ((high CROSS low) CROSS random))) else 0)`;
116 `unif_prog_space high low random =
117 ((high CROSS low) CROSS random,
118 POW ((high CROSS low) CROSS random),
119 (\s. SIGMA (unif_prog_dist high low random) s))`;
136 ``!high low random. FINITE high /\ FINITE low /\ FINITE random /\
137 ~((high CROSS low) CROSS random={}) ==>
138 prob_space (unif_prog_space high low random)``,
155 >> `(\s. (if s IN high CROSS low CROSS random then
156 1 / & (CARD (high CROSS low CROSS random)) else 0)) =
157 (\s. inv (& (CARD (high CROSS low CROSS random))) *
158 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)`
167 ``!high low random P. FINITE high /\ FINITE low /\ FINITE random /\
168 ~((high CROSS low) CROSS random={}) /\
169 P SUBSET ((high CROSS low) CROSS random) ==>
170 (prob (unif_prog_space high low random) P =
171 (&(CARD P))/(&((CARD high)*(CARD low)*(CARD random))))``,
173 >> `(\s. (if s IN high CROSS low CROSS random then
174 1 / & (CARD (high CROSS low CROSS random)) else 0)) =
175 (\s. inv (& (CARD (high CROSS low CROSS random))) *
176 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)`
182 (\s. (if s IN high CROSS low CROSS random then 1 else 0)) x else 0)) =
191 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
192 ~((high CROSS low) CROSS random={}) ==>
193 (!l. l IN low ==> (distribution(unif_prog_space high low random) L {l} =
196 >> `p_space (unif_prog_space high low random) =
197 (high CROSS low CROSS random)`
200 >> `(PREIMAGE L {l} INTER (high CROSS low CROSS random)) SUBSET
201 (high CROSS low CROSS random)`
204 >> `(PREIMAGE L {l} INTER (high CROSS low CROSS random)) =
205 (IMAGE (\x. ((FST x, l),SND x)) (high CROSS random))`
212 >> `INJ (\x. ((FST x,l),SND x)) (high CROSS random)
213 (IMAGE (\x. ((FST x,l),SND x)) (high CROSS random))`
217 `((high :'a state -> bool) CROSS (random :'c state -> bool))`,
219 (high CROSS random))`] o
223 >> Suff `((& (CARD high) * & (CARD random)) * 1) / ((& (CARD high) * & (CARD random)) * & (CARD low)) =
234 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
235 ~((high CROSS low) CROSS random={}) ==>
237 (distribution (unif_prog_space high low random) (\x. (H x,L x)) {(h,l)} =
240 >> `p_space (unif_prog_space high low random) =
241 (high CROSS low CROSS random)`
244 >> `(PREIMAGE (\x. (H x,L x)) {(h,l)} INTER (high CROSS low CROSS random)) SUBSET
245 (high CROSS low CROSS random)`
248 >> `(PREIMAGE (\x. (H x,L x)) {(h,l)} INTER (high CROSS low CROSS random)) =
249 (IMAGE (\x. ((h, l), x)) random)`
256 >> `INJ (\x. ((h,l),x)) random
257 (IMAGE (\x. ((h,l),x)) random)`
261 `(random :'c state -> bool)`,
263 random)`] o
267 >> Suff `((& (CARD random)) * 1) / ((& (CARD random)) * (& (CARD high) * & (CARD low))) =
278 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
279 ~((high CROSS low) CROSS random={}) ==>
280 (!l r. l IN low /\ r IN random ==>
281 (distribution (unif_prog_space high low random) (\x. (L x,R x)) {(l,r)} =
282 ((1:real)/(&((CARD low)*(CARD random))))))``,
284 >> `p_space (unif_prog_space high low random) =
285 (high CROSS low CROSS random)`
288 >> `(PREIMAGE (\x. (L x,R x)) {(l,r)} INTER (high CROSS low CROSS random)) SUBSET
289 (high CROSS low CROSS random)`
292 >> `(PREIMAGE (\x. (L x,R x)) {(l,r)} INTER (high CROSS low CROSS random)) =
311 >> Suff `((& (CARD high)) * 1) / ((& (CARD high)) * (& (CARD low) * & (CARD random))) =
312 1 / (& (CARD low) * & (CARD random))`
322 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
323 ~((high CROSS low) CROSS random={}) ==>
324 (!h l r. h IN high /\ l IN low /\ r IN random ==>
325 (distribution (unif_prog_space high low random) (\x. (H x, L x,R x)) {(h,l,r)} =
326 ((1:real)/(&((CARD high)*(CARD low)*(CARD random))))))``,
328 >> `p_space (unif_prog_space high low random) =
329 (high CROSS low CROSS random)`
332 >> `(PREIMAGE (\x. (H x,L x,R x)) {(h,l,r)} INTER (high CROSS low CROSS random)) SUBSET
333 (high CROSS low CROSS random)`
336 >> `(PREIMAGE (\x. (H x,L x,R x)) {(h,l,r)} INTER (high CROSS low CROSS random)) =
347 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
348 ~((high CROSS low) CROSS random={}) ==>
349 (leakage (unif_prog_space high low random) f =
351 joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
352 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
354 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) -
356 joint_distribution (unif_prog_space high low random) f L {(x,z)} *
357 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} *
359 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))``,
363 joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
364 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
366 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) -
368 joint_distribution (unif_prog_space high low random) f L {(x,z)} *
369 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} *
371 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))`
372 >> `random_variable (f :('a, 'b, 'c, 'd) prog) (unif_prog_space high low random)
373 (IMAGE (f :('a, 'b, 'c, 'd) prog) (p_space (unif_prog_space high low random)),
374 POW (IMAGE (f :('a, 'b, 'c, 'd) prog) (p_space (unif_prog_space high low random))))`
380 >> `random_variable (H :('a, 'b, 'c, 'a) prog) (unif_prog_space high low random)
381 (IMAGE (H :('a, 'b, 'c, 'a) prog) (p_space (unif_prog_space high low random)),
382 POW (IMAGE (H :('a, 'b, 'c, 'a) prog) (p_space (unif_prog_space high low random))))`
388 >> `random_variable (L :('a, 'b, 'c, 'b) prog) (unif_prog_space high low random)
389 (IMAGE (L :('a, 'b, 'c, 'b) prog) (p_space (unif_prog_space high low random)),
390 POW (IMAGE (L :('a, 'b, 'c, 'b) prog) (p_space (unif_prog_space high low random))))`
396 >> `FINITE (p_space (unif_prog_space high low random))`
398 >> `POW (p_space (unif_prog_space high low random)) = events (unif_prog_space high low random)`
401 >> `p_space (unif_prog_space high low random) =
402 (high CROSS low CROSS random)`
405 >> `IMAGE L (high CROSS low CROSS random) = low`
409 >> `?x t. (high CROSS low CROSS random = x INSERT t) /\
411 >> Know `x' IN (high CROSS low CROSS random)` >- METIS_TAC [EXTENSION, IN_INSERT]
416 >> `IMAGE (\x. (H x,L x)) (high CROSS low CROSS random) = high CROSS low`
420 >> `?x t. (high CROSS low CROSS random = x INSERT t) /\
422 >> Know `x' IN (high CROSS low CROSS random)` >- METIS_TAC [EXTENSION, IN_INSERT]
427 >> `(IMAGE f (high CROSS low CROSS random) CROSS low) =
428 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)) UNION
429 ((IMAGE f (high CROSS low CROSS random) CROSS low) DIFF
430 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))`
437 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))
438 ((IMAGE f (high CROSS low CROSS random) CROSS low) DIFF
439 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))`
441 >> `FINITE (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)) /\
442 FINITE ((IMAGE f (high CROSS low CROSS random) CROSS low) DIFF
443 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))`
450 (low :'b state -> bool) CROSS (random :'c state -> bool)))`,
454 (random :'c state -> bool)) CROSS low DIFF
456 (high CROSS low CROSS random))`])
461 (random :'c state -> bool)) CROSS low DIFF
463 (high CROSS low CROSS random))`) REAL_SUM_IMAGE_IN_IF]
467 IMAGE f (high CROSS low CROSS random) CROSS low DIFF
468 IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)
471 joint_distribution (unif_prog_space high low random) f L
474 (joint_distribution (unif_prog_space high low random) f L
476 distribution (unif_prog_space high low random) L {z})) x
483 >> Suff `joint_distribution (unif_prog_space high low random) f L {x} = 0`
486 >> Suff `PREIMAGE (\x. (f x,L x)) {x} INTER (high CROSS low CROSS random) = {}`
495 >> `(IMAGE f (high CROSS low CROSS random) CROSS (high CROSS low)) =
496 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) UNION
497 ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS low)) DIFF
498 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))`
505 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))
506 ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS low)) DIFF
507 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))`
509 >> `FINITE (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) /\
510 FINITE ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS low)) DIFF
511 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))`
518 (low :'b state -> bool) CROSS (random :'c state -> bool)))`,
522 (random :'c state -> bool)) CROSS (high CROSS low) DIFF
524 (high CROSS low CROSS random))`])
531 (random :'c state -> bool)) CROSS (high CROSS low) DIFF
533 (high CROSS low CROSS random))`) REAL_SUM_IMAGE_IN_IF]
537 IMAGE f (high CROSS low CROSS random) CROSS
539 IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)
542 joint_distribution (unif_prog_space high low random) f
545 (joint_distribution (unif_prog_space high low random) f
547 distribution (unif_prog_space high low random)
555 >> Suff `joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(f x',SND x)} = 0`
558 >> Suff `PREIMAGE (\x. (f x,H x,L x)) {(f x',SND x)} INTER (high CROSS low CROSS random) = {}`
573 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
574 >> `(\x. (if x IN IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) then
575 (\(x,z). joint_distribution (unif_prog_space high low random) f L {(x,z)} *
576 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} /
577 distribution (unif_prog_space high low random) L {z})) x else 0)) =
578 (\x. (if x IN IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) then
579 (\(x,z). joint_distribution (unif_prog_space high low random) f L {(x,z)} *
580 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} *
590 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
591 >> `(\x. (if x IN IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) then
592 (\(x,y,z). joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
593 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} /
594 distribution (unif_prog_space high low random) (\x. (H x,L x)) {(y,z)})) x else 0)) =
595 (\x. (if x IN IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) then
596 (\(x,y,z). joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
597 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
609 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
610 ~((high CROSS low) CROSS random={}) ==>
611 (visible_leakage (unif_prog_space high low random) f =
615 joint_distribution (unif_prog_space high low random) f
618 (joint_distribution (unif_prog_space high low random) f
620 & (CARD high * CARD low * CARD random))) x)
622 (high CROSS low CROSS random)) -
626 joint_distribution (unif_prog_space high low random) f (\s. (L s,R s))
629 (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s))
630 {(x,z)} * & (CARD low * CARD random))) x)
631 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)))``,
636 joint_distribution (unif_prog_space high low random) f
639 (joint_distribution (unif_prog_space high low random) f
641 & (CARD high * CARD low * CARD random))) x)
643 (high CROSS low CROSS random)) -
647 joint_distribution (unif_prog_space high low random) f (\s. (L s,R s))
650 (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s))
651 {(x,z)} * & (CARD low * CARD random))) x)
652 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))`
654 >> `random_variable (f :('a, 'b, 'c, 'd) prog) (unif_prog_space high low random)
655 (IMAGE (f :('a, 'b, 'c, 'd) prog) (p_space (unif_prog_space high low random)),
656 POW (IMAGE (f :('a, 'b, 'c, 'd) prog) (p_space (unif_prog_space high low random))))`
662 >> `random_variable (H :('a, 'b, 'c, 'a) prog) (unif_prog_space high low random)
663 (IMAGE (H :('a, 'b, 'c, 'a) prog) (p_space (unif_prog_space high low random)),
664 POW (IMAGE (H :('a, 'b, 'c, 'a) prog) (p_space (unif_prog_space high low random))))`
671 (unif_prog_space high low random)
673 (p_space (unif_prog_space high low random)),
675 (p_space (unif_prog_space high low random))))`
683 >> `FINITE (p_space (unif_prog_space high low random))`
685 >> `POW (p_space (unif_prog_space high low random)) = events (unif_prog_space high low random)`
688 >> `p_space (unif_prog_space high low random) =
689 (high CROSS low CROSS random)`
692 >> `IMAGE (\s. (L s,R s)) (high CROSS low CROSS random) = low CROSS random`
696 >> `?x t. (high CROSS low CROSS random = x INSERT t) /\
698 >> Know `x' IN (high CROSS low CROSS random)` >- METIS_TAC [EXTENSION, IN_INSERT]
703 >> `IMAGE (\s. (H s,L s,R s)) (high CROSS low CROSS random) = (high CROSS (low CROSS random))`
711 >> `(IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random)) =
712 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)) UNION
713 ((IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random)) DIFF
714 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)))`
721 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random))
722 ((IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random)) DIFF
723 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)))`
725 >> `FINITE (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)) /\
726 FINITE ((IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random)) DIFF
727 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)))`
734 (low :'b state -> bool) CROSS (random :'c state -> bool)))`,
738 (random :'c state -> bool)) CROSS (low CROSS random) DIFF
741 (high CROSS low CROSS random))`])
746 (random :'c state -> bool)) CROSS (low CROSS random) DIFF
749 (high CROSS low CROSS random))`) REAL_SUM_IMAGE_IN_IF]
753 IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random) DIFF
754 IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)
757 joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} *
759 (joint_distribution (unif_prog_space high low random) f
761 distribution (unif_prog_space high low random)
769 >> Suff `joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {x} = 0`
773 (high CROSS low CROSS random) = {}`
782 >> `(IMAGE f (high CROSS low CROSS random) CROSS (high CROSS (low CROSS random))) =
783 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)) UNION
784 ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS (low CROSS random))) DIFF
785 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)))`
792 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random))
793 ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS (low CROSS random))) DIFF
794 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)))`
796 >> `FINITE (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)) /\
797 FINITE ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS (low CROSS random))) DIFF
798 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)))`
806 (low :'b state -> bool) CROSS (random :'c state -> bool)))`,
810 (random :'c state -> bool)) CROSS (high CROSS (low CROSS random)) DIFF
814 (high CROSS low CROSS random))`])
821 (random :'c state -> bool)) CROSS (high CROSS (low CROSS random)) DIFF
825 (high CROSS low CROSS random))`) REAL_SUM_IMAGE_IN_IF]
829 IMAGE f (high CROSS low CROSS random) CROSS
830 (high CROSS (low CROSS random)) DIFF
831 IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random)
834 joint_distribution (unif_prog_space high low random) f
837 (joint_distribution (unif_prog_space high low random) f
839 distribution (unif_prog_space high low random)
847 >> Suff `joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(f x',SND x)} = 0`
851 (high CROSS low CROSS random) = {}`
866 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
867 >> `(\x. (if x IN IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) then
868 (\(x,z). joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} *
869 lg (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} /
870 distribution (unif_prog_space high low random) (\s. (L s,R s)) {z})) x else 0)) =
871 (\x. (if x IN IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) then
872 (\(x,z). joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} *
873 lg (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} *
874 (&(CARD low * CARD random)))) x else 0))`
884 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
885 >> `(\x. (if x IN IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) then
886 (\(x,y,z). joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} *
887 lg (joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} /
888 distribution (unif_prog_space high low random) (\s. (H s,L s,R s)) {(y,z)})) x else 0)) =
889 (\x. (if x IN IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) then
890 (\(x,y,z). joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} *
891 lg (joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} *
892 (&((CARD high)*(CARD low)*(CARD random))))) x else 0))`
904 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\
905 ~((high CROSS low) CROSS random={}) ==>
907 joint_distribution (unif_prog_space high low random) f L {(x,z)} *
908 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} *
910 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))=
912 ((1/(&(CARD high * CARD low * CARD random)))*
914 (high CROSS random))) *
915 lg (((1/(&(CARD high * CARD low * CARD random)))*
917 (high CROSS random))) *
919 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))``,
921 >> `p_space (unif_prog_space high low random) =
922 (high CROSS low CROSS random)`
924 >> `FINITE (IMAGE (\s. (f s,SND(FST s))) (high CROSS low CROSS random))`
930 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
931 >> Suff `(\x. (if x IN IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) then
932 (\x. (\(x,z). joint_distribution (unif_prog_space high low random) f L {(x,z)} *
933 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} * & (CARD low))) x) x
935 (\x. (if x IN IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) then
936 (\x. (\(x,z). 1 / & (CARD high * CARD low * CARD random) *
937 SIGMA (\(h,r). (if f ((h,z),r) = x then 1 else 0)) (high CROSS random) *
938 lg (1 / & (CARD high * CARD low * CARD random) *
939 SIGMA (\(h,r). (if f ((h,z),r) = x then 1 else 0)) (high CROSS random) *
944 >> Q.ABBREV_TAC `j = joint_distribution (unif_prog_space high low random) f L {(f s',SND (FST s'))}`
945 >> Q.ABBREV_TAC `s = 1 / & (CARD high * CARD low * CARD random) *
947 (high CROSS random)`
953 >> `(\s. (if s IN high CROSS low CROSS random then
954 1 / & (CARD high * CARD low * CARD random) else 0)) =
955 (\s. (1 / & (CARD high * CARD low * CARD random)) *
956 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)`
961 >> Cases_on `(1 / & (CARD high * CARD low * CARD random) = 0)`
967 >> `FINITE (PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')} INTER (high CROSS low CROSS random))`
973 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
974 >> `(\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')} INTER (high CROSS low CROSS random)
975 then (\s. (if s IN high CROSS low CROSS random then 1 else 0)) x else 0)) =
976 (\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')} INTER (high CROSS low CROSS random)
981 >> `high CROSS random = IMAGE (\x. (FST (FST x),SND x)) (high CROSS {SND (FST s')} CROSS random)`
987 >> `(PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')} INTER (high CROSS low CROSS random)) =
988 (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random))`
992 >> `INJ (\x. (FST (FST x),SND x)) (high CROSS {SND (FST s')} CROSS random)
993 (IMAGE (\x. (FST (FST x),SND x)) (high CROSS {SND (FST s')} CROSS random))`
996 >> Q.ABBREV_TAC `c = & (CARD (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random)))`
997 >> `(high CROSS {SND (FST s')} CROSS random) =
999 (high CROSS {SND (FST s')} CROSS random)) UNION
1000 ((high CROSS {SND (FST s')} CROSS random) DIFF
1002 (high CROSS {SND (FST s')} CROSS random)))`
1006 (high CROSS {SND (FST s')} CROSS random))
1007 ((high CROSS {SND (FST s')} CROSS random) DIFF
1009 (high CROSS {SND (FST s')} CROSS random)))`
1012 >> `FINITE (high CROSS {SND (FST s')} CROSS random DIFF
1014 (high CROSS {SND (FST s')} CROSS random))`
1018 (random :'c state -> bool) DIFF
1020 (high CROSS {SND (FST s')} CROSS random))`) REAL_SUM_IMAGE_IN_IF]
1021 >> `(\x. (if x IN high CROSS {SND (FST s')} CROSS random DIFF
1022 PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random) then
1029 >> `FINITE (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random))`
1034 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
1035 >> `(\x. (if x IN PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random) then
1038 (\x. (if x IN PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random) then
1050 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\
1051 ~((high CROSS low) CROSS random={}) ==>
1053 joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} *
1054 lg (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} *
1055 & (CARD low * CARD random))) x)
1056 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))=
1058 ((1/(&(CARD high * CARD low * CARD random)))*
1060 lg (((1/(&(CARD high * CARD low * CARD random)))*
1062 & (CARD low * CARD random))) x)
1063 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)))``,
1065 >> `p_space (unif_prog_space high low random) =
1066 (high CROSS low CROSS random)`
1068 >> `FINITE (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))`
1074 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
1075 >> Suff `(\x. (if x IN IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) then
1076 (\x. (\(x,z). joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} *
1077 lg (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * & (CARD low * CARD random))) x) x
1079 (\x. (if x IN IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) then
1080 (\x. (\(x,z). 1 / & (CARD high * CARD low * CARD random) *
1082 lg (1 / & (CARD high * CARD low * CARD random) *
1084 & (CARD low * CARD random))) x) x else 0))`
1088 >> Q.ABBREV_TAC `j = joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(f s',(SND (FST s'),SND s'))}`
1089 >> Q.ABBREV_TAC `s = 1 / & (CARD high * CARD low * CARD random) *
1096 >> `(\s. (if s IN high CROSS low CROSS random then
1097 1 / & (CARD high * CARD low * CARD random) else 0)) =
1098 (\s. (1 / & (CARD high * CARD low * CARD random)) *
1099 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)`
1104 >> Cases_on `(1 / & (CARD high * CARD low * CARD random) = 0)`
1110 >> `FINITE (PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')} INTER (high CROSS low CROSS random))`
1116 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
1117 >> `(\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')} INTER (high CROSS low CROSS random)
1118 then (\s. (if s IN high CROSS low CROSS random then 1 else 0)) x else 0)) =
1119 (\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')} INTER (high CROSS low CROSS random)
1124 >> `(PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')} INTER (high CROSS low CROSS random)) =
1195 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\
1196 ~((high CROSS low) CROSS random={}) ==>
1198 joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
1199 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
1201 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))=
1203 ((1/(&(CARD high * CARD low * CARD random)))*
1204 (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) *
1205 lg (((1/(&(CARD high * CARD low * CARD random)))*
1206 (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) *
1208 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))``,
1210 >> `p_space (unif_prog_space high low random) =
1211 (high CROSS low CROSS random)`
1213 >> `FINITE (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))`
1219 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
1220 >> Suff `(\x. (if x IN IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) then
1221 (\x. (\(x,y,z). joint_distribution (unif_prog_space high low random) f
1223 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
1225 (\x. (if x IN IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) then
1227 1 / & (CARD high * CARD low * CARD random) *
1228 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random *
1229 lg (1 / & (CARD high * CARD low * CARD random) *
1231 random * & (CARD high * CARD low))) x) x else 0))`
1236 >> Q.ABBREV_TAC `j = joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(f s',FST s')}`
1237 >> Q.ABBREV_TAC `s = 1 / & (CARD high * CARD low * CARD random) *
1238 SIGMA (\r. (if f (FST s',r) = f s' then 1 else 0)) random`
1244 >> `(\s. (if s IN high CROSS low CROSS random then
1245 1 / & (CARD high * CARD low * CARD random) else 0)) =
1246 (\s. (1 / & (CARD high * CARD low * CARD random)) *
1247 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)`
1252 >> Cases_on `(1 / & (CARD high * CARD low * CARD random) = 0)`
1258 >> `FINITE (PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER (high CROSS low CROSS random))`
1265 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
1267 (high CROSS low CROSS random)
1268 then (\s. (if s IN high CROSS low CROSS random then 1 else 0)) x else 0)) =
1270 (high CROSS low CROSS random)
1275 >> `random = IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)`
1281 >> `(PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER (high CROSS low CROSS random)) =
1282 (PREIMAGE f {f s'} INTER ({FST (FST s')} CROSS {SND (FST s')} CROSS random))`
1287 >> `INJ SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)
1288 (IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random))`
1293 IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random))))`
1294 >> `({FST (FST s')} CROSS {SND (FST s')} CROSS random) =
1300 random))) UNION
1301 (({FST (FST s')} CROSS {SND (FST s')} CROSS random) DIFF
1307 random))))`
1317 random)))
1318 (({FST (FST s')} CROSS {SND (FST s')} CROSS random) DIFF
1324 random))))`
1330 ({FST (FST s')} CROSS {SND (FST s')} CROSS random)))`
1332 >> `FINITE ({FST (FST s')} CROSS {SND (FST s')} CROSS random DIFF
1337 ({FST (FST s')} CROSS {SND (FST s')} CROSS random)))`
1341 {SND (FST s')} CROSS (random :'c state -> bool) DIFF
1347 ({FST (FST s')} CROSS {SND (FST s')} CROSS random)))`) REAL_SUM_IMAGE_IN_IF]
1348 >> `(\x. (if x IN {FST (FST s')} CROSS {SND (FST s')} CROSS random DIFF
1351 IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)) then
1366 (random :'c state -> bool))))`) REAL_SUM_IMAGE_IN_IF]
1369 IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)) then
1374 IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)) then
1387 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\
1388 ~((high CROSS low) CROSS random={}) ==>
1390 joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} *
1391 lg (joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} *
1392 & (CARD high * CARD low * CARD random))) x)
1393 (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random))=
1395 ((1/(&(CARD high * CARD low * CARD random)))*
1397 lg (((1/(&(CARD high * CARD low * CARD random)))*
1399 & (CARD high * CARD low * CARD random))) x)
1400 (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random)))``,
1402 >> `p_space (unif_prog_space high low random) =
1403 (high CROSS low CROSS random)`
1405 >> `FINITE (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random))`
1412 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF]
1413 >> Suff `(\x. (if x IN IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) then
1414 (\x. (\(x,y,z). joint_distribution (unif_prog_space high low random) f
1416 lg (joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} *
1417 & (CARD high * CARD low * CARD random))) x) x else 0)) =
1418 (\x. (if x IN IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) then
1420 1 / & (CARD high * CARD low * CARD random) *
1422 lg (1 / & (CARD high * CARD low * CARD random) *
1423 (if f ((h,l),r) = out then 1 else 0) * & (CARD high * CARD low * CARD random))) x) x else 0))`
1428 >> Suff `joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(f s',FST (FST s'),SND (FST s'),SND s')} =
1429 1 / & (CARD high * CARD low * CARD random)`
1433 >> `(\s. (if s IN high CROSS low CROSS random then
1434 1 / & (CARD high * CARD low * CARD random) else 0)) =
1435 (\s. (1 / & (CARD high * CARD low * CARD random)) *
1436 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)`
1447 >> Q.ABBREV_TAC `foo = 1 / & (CARD high * CARD low * CARD random) *
1448 SIGMA (\s. (if s IN high CROSS low CROSS random then 1 else 0))
1452 (high CROSS low CROSS random))`
1453 >> `1 / & (CARD high * CARD low * CARD random) = 1 / & (CARD high * CARD low * CARD random) * 1`
1457 >> Cases_on `(1 / & (CARD high * CARD low * CARD random) = 0)`
1460 (high CROSS low CROSS random)) = {s'}`
1469 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\
1470 ~((high CROSS low) CROSS random={}) ==>
1472 joint_distribution (unif_prog_space high low random) f L {(x,z)} *
1473 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} *
1475 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))=
1476 (1/(&(CARD high * CARD low * CARD random)))*
1479 (high CROSS random))) *
1480 lg (((1/(&(CARD high * CARD random)))*
1482 (high CROSS random))))) x)
1483 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))``,
1485 >> `1 / & (CARD high * CARD low * CARD random) *
1489 (high CROSS random) *
1491 (1 / & (CARD high * CARD random) *
1493 (high CROSS random))) x)
1494 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)) =
1495 SIGMA (\x. 1 / & (CARD high * CARD low * CARD random) *
1498 (high CROSS random) *
1500 (1 / & (CARD high * CARD random) *
1502 (high CROSS random))) x)
1503 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))`
1508 1 / & (CARD high * CARD low * CARD random) *
1510 (high CROSS random) *
1512 (1 / & (CARD high * CARD low * CARD random) *
1514 (high CROSS random) * & (CARD low))) x) =
1516 1 / & (CARD high * CARD low * CARD random) *
1519 (high CROSS random) *
1521 (1 / & (CARD high * CARD random) *
1523 (high CROSS random))) x)`
1528 >> Suff `1 / & (CARD high * CARD low * CARD random) *
1530 (high CROSS random) * & (CARD low) =
1531 1 / & (CARD high * CARD random) *
1533 (high CROSS random)`
1535 >> Suff `1 / & (CARD high * CARD random) =
1536 & (CARD low) * (1 / & (CARD high * CARD low * CARD random))`
1540 >> `& (CARD high) * & (CARD low) * & (CARD random) =
1541 (& (CARD high) * & (CARD random)) * & (CARD low)`
1544 >> `inv (& (CARD high) * & (CARD random) * & (CARD low)) =
1545 inv (& (CARD high) * & (CARD random)) * inv (& (CARD low))`
1551 >> `& (CARD low) * (inv (& (CARD high) * & (CARD random)) * inv (& (CARD low))) =
1552 ((inv (& (CARD low))) * ((& (CARD low)))) * (inv (& (CARD high) * & (CARD random)))`
1564 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\
1565 ~((high CROSS low) CROSS random={}) ==>
1569 joint_distribution (unif_prog_space high low random) f
1572 (joint_distribution (unif_prog_space high low random) f
1574 & (CARD low * CARD random))) x)
1576 (high CROSS low CROSS random)) =
1577 (1/(&(CARD high * CARD low * CARD random)))*
1582 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)))``,
1584 >> `1 / & (CARD high * CARD low * CARD random) *
1592 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)) =
1594 (\x. 1 / & (CARD high * CARD low * CARD random) *
1600 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))`
1605 1 / & (CARD high * CARD low * CARD random) *
1608 (1 / & (CARD high * CARD low * CARD random) *
1610 & (CARD low * CARD random))) x) =
1612 1 / & (CARD high * CARD low * CARD random) *
1624 >> Suff `1 / & (CARD high * CARD low * CARD random) *
1627 high * & (CARD low * CARD random) =
1634 & (CARD low * CARD random) * (1 / & (CARD high * CARD low * CARD random))`
1638 >> `& (CARD high) * & (CARD low) * & (CARD random) =
1639 & (CARD high) * (& (CARD low) * & (CARD random))`
1642 >> `inv (& (CARD high) * (& (CARD low) * & (CARD random))) =
1643 inv (& (CARD high)) * inv(& (CARD low) * & (CARD random))`
1649 >> `& (CARD low) * & (CARD random) *
1650 (inv (& (CARD high)) * inv (& (CARD low) * & (CARD random))) =
1651 inv (& (CARD high)) * (inv (& (CARD low) * & (CARD random) ) * (& (CARD low) * & (CARD random)) )`
1654 >> Suff `(inv (& (CARD low) * & (CARD random)) *
1655 (& (CARD low) * & (CARD random))) = 1` >- RW_TAC real_ss []
1656 >> `inv (& (CARD low) * & (CARD random)) * & (CARD low) * & (CARD random) =
1657 (inv (& (CARD low) * & (CARD random))) * (& (CARD low) * & (CARD random))`
1668 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\
1669 ~((high CROSS low) CROSS random={}) ==>
1671 joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
1672 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} *
1674 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))=
1675 (1/(&(CARD high * CARD low * CARD random)))*
1677 ((SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) *
1678 lg (((1/(&(CARD random)))*
1679 (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)))) x)
1680 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))``,
1682 >> `1 / & (CARD high * CARD low * CARD random) *
1685 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random *
1687 (1 / & (CARD random) *
1688 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random)) x)
1689 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) =
1691 (\x. (1 / & (CARD high * CARD low * CARD random)) * (\(out,h,l).
1692 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random *
1694 (1 / & (CARD random) *
1695 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random)) x)
1696 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))`
1701 1 / & (CARD high * CARD low * CARD random) *
1702 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random *
1704 (1 / & (CARD high * CARD low * CARD random) *
1705 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random *
1708 1 / & (CARD high * CARD low * CARD random) *
1710 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random *
1712 (1 / & (CARD random) *
1713 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random)) x)`
1718 >> Suff `1 / & (CARD high * CARD low * CARD random) *
1719 SIGMA (\r. (if f (SND x,r) = FST x then 1 else 0)) random *
1721 1 / & (CARD random) *
1722 SIGMA (\r. (if f (SND x,r) = FST x then 1 else 0)) random`
1724 >> Suff `1 / & (CARD random) =
1725 & (CARD high * CARD low) * (1 / & (CARD high * CARD low * CARD random))`
1729 >> `& (CARD high) * & (CARD low) * & (CARD random) =
1730 (& (CARD high) * & (CARD low)) * & (CARD random)`
1733 >> `inv (& (CARD high) * & (CARD low) * & (CARD random)) =
1734 inv (& (CARD high) * & (CARD low)) * inv (& (CARD random))`
1750 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\
1751 ~((high CROSS low) CROSS random={}) ==>
1755 joint_distribution (unif_prog_space high low random) f
1758 (joint_distribution (unif_prog_space high low random) f
1760 & (CARD high * CARD low * CARD random))) x)
1762 (high CROSS low CROSS random)) =
1767 1 / & (CARD high * CARD low * CARD random) *
1770 (1 / & (CARD high * CARD low * CARD random) *
1772 & (CARD high * CARD low * CARD random))) x) = (\x. 0)`
1777 >> Suff `inv (& (CARD high * CARD low * CARD random)) *
1778 & (CARD high * CARD low * CARD random) = 1`
1788 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
1789 ~((high CROSS low) CROSS random={}) ==>
1790 (leakage (unif_prog_space high low random) f =
1791 (1/(&(CARD high * CARD low * CARD random)))*
1793 ((SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) *
1794 lg (((1/(&(CARD random)))*
1795 (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)))) x)
1796 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) -
1799 (high CROSS random))) *
1800 lg (((1/(&(CARD high * CARD random)))*
1802 (high CROSS random))))) x)
1803 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))))``,
1810 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
1811 ~((high CROSS low) CROSS random={}) ==>
1812 (visible_leakage (unif_prog_space high low random) f =
1813 ~(1 / & (CARD high * CARD low * CARD random) *
1823 (high CROSS low CROSS random))))``,
1830 ``!high low random f. ALL_DISTINCT high /\ ALL_DISTINCT low /\ ALL_DISTINCT random /\
1831 ~(high = []) /\ ~(low = []) /\ ~(random = []) ==>
1832 (leakage (unif_prog_space (LIST_TO_SET high) (LIST_TO_SET low) (LIST_TO_SET random)) f =
1833 (1/(&(LENGTH high * LENGTH low * LENGTH random)))*
1834 ((REAL_SUM (MAP (\x. (\(out,h,l). (\s. s * lg ((1/(&(LENGTH random)))*s))
1835 (REAL_SUM (MAP (\r. if (f((h,l),r)=out) then 1 else 0) random))) x)
1837 (MAP (\s. (f s,FST s)) (LIST_COMBS (LIST_COMBS high low) random))))) -
1838 (REAL_SUM (MAP (\x. (\(out,l). (\s. s * lg ((1/(&(LENGTH high * LENGTH random)))*s))
1840 (LIST_COMBS high random)))) x)
1843 (LIST_COMBS (LIST_COMBS high low) random)))))))``,
1845 >> (MP_TAC o Q.SPECL [`LIST_TO_SET high`,`LIST_TO_SET low`,`LIST_TO_SET random`,`f`])
1848 >> `~(set (LIST_COMBS (LIST_COMBS high low) random) = {})`
1850 >> Cases_on `high` >> Cases_on `low` >> Cases_on `random`
1855 >> Cases_on `(1 / & (LENGTH high * LENGTH low * LENGTH random) = 0)`
1859 (LIST_COMBS (LIST_COMBS high low) random))) =
1862 (LIST_COMBS (LIST_COMBS high low) random))))`
1867 (LIST_COMBS (LIST_COMBS high low) random))) =
1870 (LIST_COMBS (LIST_COMBS high low) random))))`
1879 ``!high low random f. ALL_DISTINCT high /\ ALL_DISTINCT low /\ ALL_DISTINCT random /\
1880 ~(high = []) /\ ~(low = []) /\ ~(random = []) ==>
1881 (visible_leakage (unif_prog_space (LIST_TO_SET high) (LIST_TO_SET low) (LIST_TO_SET random)) f =
1882 ~(1/(&(LENGTH high * LENGTH low * LENGTH random)))*
1886 (MAP (\s. (f s,SND (FST s),SND s)) (LIST_COMBS (LIST_COMBS high low) random)))))))``,
1888 >> (MP_TAC o Q.SPECL [`LIST_TO_SET high`,`LIST_TO_SET low`,`LIST_TO_SET random`,`f`])
1891 >> `~(set (LIST_COMBS (LIST_COMBS high low) random) = {})`
1893 >> Cases_on `high` >> Cases_on `low` >> Cases_on `random`
1899 >> Cases_on `(& (LENGTH high * LENGTH low * LENGTH random) = 0)` >> ASM_REWRITE_TAC []
1903 (LIST_COMBS (LIST_COMBS high low) random))) =
1906 (LIST_COMBS (LIST_COMBS high low) random))))`