diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index ccfa163fab3115bbba599a47fe2170ce4c30ad4d..816b0a17eda13c7edf6e7ff27fa125eeb0a9fd33 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -557,14 +557,15 @@ We propose to generalise this concept to encompass other sorts of information wh
 For example, we would develop a system which specifies both how to represent logical operations in a particular error correcting code, and how the operations are constrained in order to satisfy basic precautions to keep the realisation fault-tolerant (\ref{task:ECC}).
 We may then attempt to re-write procedures, to minimise the number of operations subject to the constraints described by those annotations.
 We may further elaborate such a system of annotations by a description of the constraints and the costs involved for operations within a particular hardware platform (\ref{task:runnable}).
-For example, in
+%%For example, in
 % Other
 %examples of annotations might include paths in the graph corresponding
 %to the trajectories of physical qubits, or subgraphs corresponding to
 %the primitive hardware operations and the time required to execute
 %them.  For
-hybrid architectures like NQIT, the annotations will also
-indicate the differing behaviour of the subsystems.  Augmented
+%%hybrid architectures like NQIT, the annotations will also
+%%indicate the differing behaviour of the subsystems.
+Augmented
 rewrites will be used to find a runnable implementation of the
 abstract tensor for the target platform, and to optimise resource use.
 The development
@@ -693,30 +694,15 @@ analyse how information and requirements from the back-end flow upward
 in a meaningful way, and how this can be translated into compilation
 flags and assertions/hints to the compiler within HLL programs. 
 
-A key research challenge of this work package consists in the
-management of the {\em classical computation} and {\em classical
-  information} within quantum algorithms: What computation should
-occur at the \azx-generation phase, and which classical parameters are
-passed on to the \azx terms? To help answer this question we will
-design a test suite (\ref{task:testBench}) to compare possible
-solutions.
-
 The open database of tests developed in \ref{task:testBench} will
 serve as a measuring tool for the quality of the output. The database
 will also be made available to the community for rating and testing
 future compilers or optimisation techniques.  To encourage interaction
 from other research groups, and to support other languages, both our
 interface and the \azx language will be made
-public.}
+public.
 
-
-
-\subsubsection{Representation, reasoning, and resources}
-\label{sec:machines-models}
-
-\REM{stuff about WP 2 here}
-
-\oldt{Proposed and existing quantum devices differ along a variety of axes.
+Proposed and existing quantum devices differ along a variety of axes.
 At the most abstract level, the quantum circuit model and the
 1-way model \cite{Raussendorf-2001} have different execution
 concepts and primitive operations, despite their computational
@@ -742,7 +728,24 @@ characteristics and architectural constraints of various idealised and
 realistic machines, and develop language features of \azx to express
 these properties.  The goal is two-fold: to facilitate
 \emph{code-generation} for a given machine from an \azx term; and to
-expose information needed by the \emph{optimiser}.
+expose information needed by the \emph{optimiser}.}
+
+
+
+\subsubsection{Representation, reasoning, and resources}
+\label{sec:machines-models}
+
+\REM{stuff about WP 2 here}
+
+\oldt{
+A key research challenge of this work package consists in the
+management of the {\em classical computation} and {\em classical
+  information} within quantum algorithms: What computation should
+occur at the \azx-generation phase, and which classical parameters are
+passed on to the \azx terms? To help answer this question we will
+design a test suite (\ref{task:testBench}) to compare possible
+solutions.
+
 
 Due to its novelty, we adopt an exploratory approach.  Initially, and
 in parallel, we study the circuit model (\ref{task:circuit-model}) and
@@ -757,20 +760,15 @@ transforming the tensor network into an equivalent runnable version.
 This experience will inform the later work in \ref{wp:theory} and
 \ref{wp:usefulstuff}.
 
-In the second phase we switch attention to real computers.  The first
-target is a classical simulator running on HPC hardware provided by
-our industrial partner Bull.  This will leverage existing expertise in
-simulation, combined with new techniques for symbolic evaluation of
-\azx terms.  \ROUGH{Finally we study two concrete quantum computers
-  based on different technologies: superconducting circuits (Delft)
-  and optically linked ion traps (NQIT).}  In both cases we will
-interact strongly with the experimental groups working on these
-models, who are either members of our consortium (S. Benjamin and
-N. de Beaudrap for NQIT) or our advisory board (L. DiCarlo in Delft).
-Since these architectures are dissimilar, tackling both is an ideal
-demonstration of our approach.  The completion of this phase will
-allow quantum programs represented as \azx terms to be run on real
-hardware.}
+While in the early stages of the project, it will already be quite
+useful to study concrete diagrams of fixed size (e.g. a quantum
+circuit on $N$ qubits for a previously-fixed $N$), in task
+\ref{task:betterboxes}, we will extend \azx to support parametrised
+families of diagrams (e.g. quantum circuits with $N$ qubits where $N$
+can vary) mirroring the control structures present in a quantum
+HLL. This will enable more sophisticated, generic optimisations to be
+run in advance of needing any particular computational procedure.
+}
 
 
 \subsubsection{Machine-independent optimisation}
@@ -805,8 +803,6 @@ systems, and the second is to gain a deeper understanding of the role
 played by W-type tensors as they interact with the generators of the
 \zx-calculus, which are themselves of GHZ-type. 
 
-While in the early stages of the project, it will already be quite useful to study concrete diagrams of fixed size (e.g. a quantum circuit on $N$ qubits for a previously-fixed $N$), in task \ref{task:betterboxes}, we will extend \azx to support parametrised families of diagrams (e.g. quantum circuits with $N$ qubits where $N$ can vary) mirroring the control structures present in a quantum HLL. This will enable more sophisticated, generic optimisations to be run in advance of needing any particular computational procedure.
-
 Finally, we will construct a theoretical framework which mediates the
 abstract rewrite theory of \zx-diagrams and real-world constraints
 coming from quantum hardware. In task \ref{task:annotate1}, we will
@@ -828,7 +824,23 @@ modes.}
 \subsubsection{Machine-dependent optimisation}
 \label{sec:comp-quant-softw}
 
-\oldt{An \azx term produced by the compiler front-end is, by design, an
+\oldt{
+In the second phase we switch attention to real computers.  The first
+target is a classical simulator running on HPC hardware provided by
+our industrial partner Bull.  This will leverage existing expertise in
+simulation, combined with new techniques for symbolic evaluation of
+\azx terms.  \ROUGH{Finally we study two concrete quantum computers
+  based on different technologies: superconducting circuits (Delft)
+  and optically linked ion traps (NQIT).}  In both cases we will
+interact strongly with the experimental groups working on these
+models, who are either members of our consortium (S. Benjamin and
+N. de Beaudrap for NQIT) or our advisory board (L. DiCarlo in Delft).
+Since these architectures are dissimilar, tackling both is an ideal
+demonstration of our approach.  The completion of this phase will
+allow quantum programs represented as \azx terms to be run on real
+hardware.
+
+  An \azx term produced by the compiler front-end is, by design, an
 abstract tensor network, perhaps annotated with some useful
 information, but generally without any preconception of how it should
 be executed on any particular machine.  Translating such