Dear Jeremy, I really appreciate your reply. However, the following sentence in my question email is not my conclusion.
>> Here, a and c are independant, also b and c are independant. >> However, a depends b. It is the assumption. As I wrote in the goal, (indep bern a c) /\ (indep bern b c) means "a and c are independant, also b and c are independant", and a depends b; With this assumption, I tried to prove (prob bern (a INTER b INTER c) = prob bern (a INTER b) * prob bern c)`; I think it doesn't contradict with the case that a, b, c are independant, since "prob bern (a INTER b) = prob bern a * prob bern b" in this case. And "prob bern (a INTER b INTER c) = prob bern a * prob bern b * prob bern c" is true. ----------------------------------------------------------- For sure, your example is very instructive, though events A, B, C are independant there and this is not the case that I wanted to prove. I'm not sure if I got your point or not. If not, please give me some more explanation. Thanks again! Liya Quoting Jeremy Dawson <[email protected]>: > > [email protected] 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 ----- End forwarded message ----- ------------------------------------------------------------------------------ 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
