diff --git a/testcases/proof/proba/Coins.scala b/testcases/proof/proba/Coins.scala index a2421115451166f68413a02c62e66fb222483fad..c351153725b7c500203167484d392e68dd8c67ac 100644 --- a/testcases/proof/proba/Coins.scala +++ b/testcases/proof/proba/Coins.scala @@ -100,6 +100,19 @@ object Coins { !isUniform(dist) } //holds + def sumNonUniformWithIndependence(dist: CoinsJoinDist): Boolean = { + require(isDist(dist) && isIndependent(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist))) + val res = sum(dist) + !isUniform(res) + } holds + + //independence is required + def sumNonUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = { + require(isDist(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist))) + val res = sum(dist) + !isUniform(res) + } holds + def sumIsCommutative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = { require(isDist(coin1) && isDist(coin2))