I have to prove a goal in HOL4 as following:
g `!a b c. (indep bern a c) /\ (indep bern b c) ==>
(a IN events bern) /\ (b IN events bern) /\ (c IN events bern) /\
(prob bern (a INTER b INTER c) = prob bern (a INTER b) * prob bern c)`;
Here, a and c are independant, also b and c are independant. However,
a depends b.
Could anybody give me some hints? I really appreciate!
Regards,
Liya
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
