liy_...@encs.concordia.ca wrote: > 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 > I can't guess what bern and events mean, but if prob and indep have a usual meaning, then it's not true.
eg let 3 coins, X, Y, Z be tossed independently. Let event A be coins X and Y fall the same way Let event B be coins X and Z fall the same way Let event C be coins Z and Y fall the same way Then each two of the three events A,B,C are independent. But A & B is not independent of C (which is what, I understand, the last line of your conclusion says) Regards, Jeremy ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
