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)
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
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
