--- a/provsec/paper.tex	Fri May 21 13:44:20 2010 +0200
+++ b/provsec/paper.tex	Thu May 27 16:10:15 2010 +0200
@@ -595,7 +595,7 @@
     and nothing needs to be changes, so we leave it in place.
   \item Otherwise, if we have not assigned to this variable before; we
     suffix the assigned variable name with a fresh \KWD{\_thenx} (or
-    \KWD{_elsex}) and remember this renaming.
+    \KWD{\_elsex}) and remember this renaming.
   \item If we have assigned to this variable before in the same branch
     we reuse the same name as last time.
   \item All variables on the right-hand side that have been renamed in
@@ -632,6 +632,8 @@
 this up to the programmer, as we do not have the infrastructure for
 forbidding side-effects, but function-calls are nice to be able to
 make in the branches.
+
+
 %TODO: Maybe it is better to emit an error, and suggest the function call is moved before the assignment?
 \subsection{Output and Timing of Operations}
 We compile PySMCL into VIFF programs. VIFF uses a system of
@@ -683,7 +685,9 @@
 Any if-statement with a secret condition will be rewritten, and
 looping is not allowed with a secret condition, so the programs will
 never branch on secret values and the players will never have to
-disagree, or be uncertain on what to do next.
+disagree, or be uncertain on what to do next. The correctness of the
+protocol thus relies on the correctness of the if-rewriting, so the
+computation of $F_P$ is equivalent to that of $P$.
 
 Now we define a functionality $F_P$, working just as $F$, but it has a
 new command $P$ that, when called, makes the functionality run the