Lines Matching refs:high
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={}) ==>
236 (!h l. h IN high /\ l IN low ==>
237 (distribution (unif_prog_space high low random) (\x. (H x,L x)) {(h,l)} =
238 ((1:real)/(&((CARD high)*(CARD low))))))``,
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)) =
267 >> Suff `((& (CARD random)) * 1) / ((& (CARD random)) * (& (CARD high) * & (CARD low))) =
268 1 / (& (CARD high) * & (CARD low))`
278 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\
279 ~((high CROSS low) CROSS random={}) ==>
281 (distribution (unif_prog_space high low random) (\x. (L x,R x)) {(l,r)} =
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)) =
293 (IMAGE (\x. ((x, l), r)) high)`
300 >> `INJ (\x. ((x,l),r)) high
301 (IMAGE (\x. ((x,l),r)) high)`
305 `(high :'a state -> bool)`,
307 high)`] o
311 >> Suff `((& (CARD high)) * 1) / ((& (CARD high)) * (& (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)} *
353 & (CARD high * CARD low))) x)
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)} *
365 & (CARD high * CARD low))) x)
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)))`
449 ((high :'a state -> bool) CROSS
452 ((high :'a state -> bool) CROSS
456 (high CROSS low CROSS random))`])
459 ((high :'a state -> bool) CROSS
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)))`
517 ((high :'a state -> bool) CROSS
520 ((high :'a state -> bool) CROSS
522 (random :'c state -> bool)) CROSS (high CROSS low) DIFF
524 (high CROSS low CROSS random))`])
529 ((high :'a state -> bool) CROSS
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
538 (high CROSS low) DIFF
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) = {}`
572 ((high :'a state -> bool) CROSS
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)} *
589 ((high :'a state -> bool) CROSS
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)} *
598 (&((CARD high)*(CARD low))))) x else 0))`
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))
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))
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)))`
733 ((high :'a state -> bool) CROSS
736 ((high :'a state -> bool) CROSS
741 (high CROSS low CROSS random))`])
744 ((high :'a state -> bool) CROSS
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)))`
805 ((high :'a state -> bool) CROSS
808 ((high :'a state -> bool) CROSS
810 (random :'c state -> bool)) CROSS (high CROSS (low CROSS random)) DIFF
814 (high CROSS low CROSS random))`])
819 ((high :'a state -> bool) CROSS
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) = {}`
865 ((high :'a state -> bool) CROSS
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)} *
883 ((high :'a state -> bool) CROSS
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))`
929 ((high :'a state -> bool) CROSS
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))`
972 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS
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))`
1016 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `((high :'a state -> bool) CROSS
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))`
1033 ((high :'a state -> bool) CROSS {SND (FST s')} CROSS
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)} *
1056 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))=
1058 ((1/(&(CARD high * CARD low * CARD random)))*
1059 (SIGMA (\h. if (f((h,FST z),SND z)=x) then 1 else 0) high)) *
1060 lg (((1/(&(CARD high * CARD low * CARD random)))*
1061 (SIGMA (\h. if (f((h,FST z),SND z)=x) then 1 else 0) high)) *
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))`
1073 ((high :'a state -> bool) CROSS
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) *
1081 SIGMA (\h. (if f ((h,FST z),SND z) = x then 1 else 0)) high *
1082 lg (1 / & (CARD high * CARD low * CARD random) *
1083 SIGMA (\h. (if f ((h,FST z),SND z) = x then 1 else 0)) high *
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) *
1090 SIGMA (\h. (if f ((h,SND (FST s')),SND s') = f s' then 1 else 0)) high`
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))`
1115 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS
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)) =
1125 (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}))`
1131 (high CROSS {SND (FST s')} CROSS {SND s'}))`
1132 >> `high = IMAGE (FST o FST) (high CROSS {SND (FST s')} CROSS {SND s'})`
1138 >> `INJ (FST o FST) (high CROSS {SND (FST s')} CROSS {SND s'})
1139 (IMAGE (FST o FST) (high CROSS {SND (FST s')} CROSS {SND s'}))`
1142 >> `(high CROSS {SND (FST s')} CROSS {SND s'}) =
1144 (high CROSS {SND (FST s')} CROSS {SND s'})) UNION
1145 ((high CROSS {SND (FST s')} CROSS {SND s'}) DIFF
1147 (high CROSS {SND (FST s')} CROSS {SND s'})))`
1151 (high CROSS {SND (FST s')} CROSS {SND s'}))
1152 ((high CROSS {SND (FST s')} CROSS {SND s'}) DIFF
1154 (high CROSS {SND (FST s')} CROSS {SND s'})))`
1157 >> `FINITE (high CROSS {SND (FST s')} CROSS {SND s'} DIFF
1159 (high CROSS {SND (FST s')} CROSS {SND s'}))`
1161 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `((high :'a state -> bool) CROSS
1165 (high CROSS {SND (FST s')} CROSS {SND (s' :('a, 'b, 'c) prog_state)}))`) REAL_SUM_IMAGE_IN_IF]
1166 >> `(\x. (if x IN high CROSS {SND (FST s')} CROSS {SND s'} DIFF
1167 PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}) then
1174 >> `FINITE (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}))`
1178 ((high :'a state -> bool) CROSS {SND (FST s')} CROSS
1180 >> `(\x. (if x IN PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}) then
1183 (\x. (if x IN PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}) then
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)} *
1200 & (CARD high * CARD low))) x)
1201 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))=
1203 ((1/(&(CARD high * CARD low * CARD random)))*
1205 lg (((1/(&(CARD high * CARD low * CARD random)))*
1207 & (CARD high * CARD low))) x)
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))`
1218 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS
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)} *
1224 & (CARD high * CARD low))) x) x else 0)) =
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) *
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) *
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))`
1264 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS
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)
1281 >> `(PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER (high CROSS low CROSS random)) =
1292 (high CROSS low CROSS
1297 (high CROSS low CROSS
1304 (high CROSS low CROSS
1314 (high CROSS low CROSS
1321 (high CROSS low CROSS
1328 (high CROSS low CROSS
1335 (high CROSS low CROSS
1345 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS
1350 (high CROSS low CROSS
1363 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS
1368 (high CROSS low CROSS
1373 (high CROSS low CROSS
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))`
1411 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS
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
1576 (high CROSS low CROSS random)) =
1577 (1/(&(CARD high * CARD low * CARD random)))*
1579 ((SIGMA (\h. if (f((h,l),r)=out) then 1 else 0) high)) *
1580 lg (((1/(&(CARD high)))*
1581 (SIGMA (\h. if (f((h,l),r)=out) then 1 else 0) high)))) x)
1582 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)))``,
1584 >> `1 / & (CARD high * CARD low * CARD random) *
1588 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high *
1590 (1 / & (CARD high) *
1591 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high)) x)
1592 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)) =
1594 (\x. 1 / & (CARD high * CARD low * CARD random) *
1596 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high *
1598 (1 / & (CARD high) *
1599 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high)) x)
1600 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))`
1605 1 / & (CARD high * CARD low * CARD random) *
1606 SIGMA (\h. (if f ((h,FST z),SND z) = x then 1 else 0)) high *
1608 (1 / & (CARD high * CARD low * CARD random) *
1609 SIGMA (\h. (if f ((h,FST z),SND z) = x then 1 else 0)) high *
1612 1 / & (CARD high * CARD low * CARD random) *
1614 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high *
1616 (1 / & (CARD high) *
1617 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high)) x)`
1624 >> Suff `1 / & (CARD high * CARD low * CARD random) *
1627 high * & (CARD low * CARD random) =
1628 1 / & (CARD high) *
1631 high`
1633 >> Suff `1 / & (CARD high) =
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))`
1650 (inv (& (CARD high)) * inv (& (CARD low) * & (CARD random))) =
1651 inv (& (CARD high)) * (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)} *
1673 & (CARD high * CARD low))) x)
1674 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))=
1675 (1/(&(CARD high * CARD low * CARD random)))*
1680 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))``,
1682 >> `1 / & (CARD high * CARD low * CARD random) *
1689 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) =
1691 (\x. (1 / & (CARD high * CARD low * CARD random)) * (\(out,h,l).
1696 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))`
1701 1 / & (CARD high * CARD low * CARD random) *
1704 (1 / & (CARD high * CARD low * CARD random) *
1706 & (CARD high * CARD low))) x) =
1708 1 / & (CARD high * CARD low * CARD random) *
1718 >> Suff `1 / & (CARD high * CARD low * CARD random) *
1720 & (CARD high * CARD low) =
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))`
1740 >> Suff `(& (CARD high) * & (CARD low)) * inv (& (CARD high) * & (CARD low)) = 1`
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)))*
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) *
1817 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high *
1819 (1 / & (CARD high) *
1820 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high))
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)))*
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)))*
1883 ((REAL_SUM (MAP (\x. (\(out,l,r). (\s. s * lg ((1/(&(LENGTH high)))*s))
1884 (REAL_SUM (MAP (\h. if (f((h,l),r)=out) then 1 else 0) high))) x)
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))))`