From 59e61dfbca88dd7c761ee90f71fd56ba4f1dc0bb Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 8 Jul 2015 14:44:57 +0200
Subject: [PATCH] more independence results
---
testcases/proof/proba/Coins.scala | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/testcases/proof/proba/Coins.scala b/testcases/proof/proba/Coins.scala
index a24211154..c35115372 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))
--
GitLab