Processed feedback

1 files changed, 9 insertions, 6 deletions

diff --git a/paper/interp.tex b/paper/interp.tex
index 5b8db03..f5101e5 100644
--- a/paper/interp.tex
+++ b/paper/interp.tex
@@ -15,9 +15,10 @@ $$
 \end{prooftree}
 $$
 
-This specifies nothing else than the intuition: if the execution of statement
-$S_1$ in state $s$ yields state $s'$, and $S_2$ in $s'$ yields $s''$, then
-$\whcomp{S_1}{S_2}$ in $s$ yields $s''$.
+This derivation rule consists of two premises, above the line, and one
+conclusion, beneath the line. It specifies nothing else than the intuition: if
+the execution of statement $S_1$ in state $s$ yields state $s'$, and $S_2$ in
+$s'$ yields $s''$, then $\whcomp{S_1}{S_2}$ in $s$ yields $s''$.
 
 The translation of this rule in a functional program looks as follows:
 
@@ -50,7 +51,8 @@ $$
 	\end{cases}
 $$
 
-This gives the assignment rule:
+This gives the assignment axiom\footnote{An axiom, in this context, is nothing
+else than a derivation rule with zero premises.}:
 
 $$
 \begin{prooftree}
@@ -106,8 +108,9 @@ $$
 \end{prooftree}
 $$
 
-A similar rule exists for $S_2$ in the case that $\mathcal B\llbracket
-b\rrbracket s$ does not hold.
+This derivation rule has one premise, but can only be applied when the
+condition $\mathcal B\llbracket b\rrbracket s$ holds. A similar rule exists
+for $S_2$ in the case that the condition does not hold.
 
 The problem with these rules is that they can only be applied when some
 condition is met. In this case, the condition is still relatively easy. In