Skip to content

Commit 6d48cc1

Browse files
alleystoughtonstrub
authored andcommitted
remove stray printing of lemma
1 parent 042456e commit 6d48cc1

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

theories/modules/EventPartitioning.ec

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,6 @@ theory ResultPartitioning.
128128
= big predT (fun a=> Pr[M.f(i) @ &m: E i (glob M) res /\ res = a]) (undup (X i))
129129
+ Pr[M.f(i) @ &m: E i (glob M) res /\ !mem (X i) res].
130130
proof.
131-
print mem_undup.
132131
have->:Pr[M.f(i) @ &m : E i (glob M){hr} res{hr} /\ ! (res{hr} \in X i)]=
133132
Pr[M.f(i) @ &m : E i (glob M){hr} res{hr} /\ ! (res{hr} \in undup (X i))].
134133
- smt(mem_undup).

0 commit comments

Comments
 (0)