diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index dad33547f1741f7a3213591873a0040c8e0b7f31..c833d7023fd82419185384286aad6c841392d765 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -229,7 +229,7 @@ easily run existing programs, and future programming languages automatically gai
   This means that one can formally prove every equality of quantum circuits in these gate models through the application of a small number of relatively simple rules for rewriting tensors.
 This stunning achievement opens the door to many
 new possibilities for optimisation and verification of quantum
-computations.
+computations. 
 
 %  and is complete for important subtheories such as the stablizer
 % fragment \cite{1367-2630-16-9-093021} and single qubit Clifford+T
@@ -255,7 +255,7 @@ An example of such a transformation is the following:}
     %\cnotv[0.6] \rTo^* 
     \cnotvi[0.7]
   \]~\\[-4mm]%
-Members of our consortium have demonstrated how to use these formal reasoning techniques in software, including the interactive theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which was used to formally verify quantum communication protocols and error correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr}) and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early demonstration of the capacity of the \zxcalculus to \newt{outperform other methods of circuit optimisation}.
+Members of our consortium have demonstrated how to use these formal reasoning techniques in software, including the interactive theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which was used to formally verify quantum communication protocols and error correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr}) and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early demonstration of the capacity of the \zxcalculus to \newt{outperform other methods of circuit optimisation,  in the sense that certain circuit metric (such as total size, tree-width, or number of non-Clifford subterms such as T-gates) can be minimised.}
 \TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
 %%% cutting because repeated later
 % It is strictly more powerful than the stabiliser