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 jer...@rsise.anu.edu.au:
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
- End forwarded message -
--
Download Intel#174; 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
