← Back to branch summary

~ohad-kammar/ohads-thesis/trunk

« back to all changes in this revision

Viewing changes to operationwise.tex

  • Committer: Ohad Kammar
  • Date: 2014-04-01 11:55:55 UTC
  • Revision ID: ohad.kammar@cl.cam.ac.uk-20140401115555-n2sx48xcj2vudmon
proofread the combination chapter.

Show diffs side-by-side

added added

removed removed

Lines of Context:
operationwise.tex
97
97
$\tx$ in the same environment.
98
98
\end{counterexample}
99
99
 
100
 
We do now know any reasonable condition to act as an operation-wise
 
100
We do now know any reasonable condition that can act as an operation-wise
101
101
validity condition for the Unique optimisation.
102
102
 
103
103
\begin{theorem}\theoremlabel{operationwise pure hoist}
215
215
  The Swap optimisation is operation-wise valid: for every
216
216
  triple of presentations $\Ax_1 = \pair{\uaSignature_1}{\uaEq_1}$,
217
217
  $\Ax_2 = \pair{\uaSignature_2}{\uaEq_2}$, and $\Ax =
218
 
  \pair{\uaSignature}{\uaEq}$ and translations $\Ax_1
 
218
  \pair{\uaSignature}{\uaEq}$ and for every pair of translations $\Ax_1
219
219
  \xto{\Translation_1} \Ax \xfrom{\Translation_2} \Ax_2$:
220
220
  \begin{itemize}
221
221
  \item
262
262
  \pair{\uaSignature_2}{\uaEq_2}$, and $\Ax =
263
263
  \pair{\uaSignature}{\uaEq}$ and translations $\Ax_1
264
264
  \xto{\Translation_1} \Ax \xfrom{\Translation_2} \Ax_2$. In all three
265
 
  statements, the `only if' implications are immediate, and it remain to
 
265
  statements, the `only if' implications are immediate, and it remains to
266
266
  establish the converse implications. We begin with Swap, and assume
267
267
  the first condition.
268
268