%%%%%%%%%%%%%%%% CODE FOR IMAGE 1 RIGHT COLUMN %%%%%%%%%%%%%%%%%%%%%%
The above proposition shows that if $ab=bb$ and $cb ge 0$ then by setting
$bE = rp cap B(ab, ||ab||)$ we can satisfy the above constraints.
Unfortunately, we were not able to drive suitable constraints for models C and
D. tabref{tab:proptrans} summarizes our proposed constraints.
begin{table}[htbp]
  setlength{tabcolsep}{1.2pt}
  centering
  begin{tabular}{c | l}
    Model & multicolumn{1}{c}{Constraints}\hline
    A & $begin{aligned}
      &r_1'' ge lambda r_1, lambda r_2 + (1-lambda)r'_1 le Z\
      & ip{e''}{r_2''} ge (1-lambda)ip{e'}{r_2'}end{aligned}$\[1ex]hline
    B & $begin{aligned}
      &r_1'' + e'' + (1-lambda)(r_1' + e')=0,\
      &{ip{r_2''}{e''} ge (1-lambda)ip{r_2'}{e'}}, text{and}\
      &ab ge Z, forall x in cE, x in rp cap B(ab, ||ab||)end{aligned}$\
  end{tabular}
  caption{Sufficient constraints for enforcing $proptrans(r, r', e', r'',
    e'')$. $ab = frac{r_1'' - lambda r_1 + e''}{lambda}$.}
  label{tab:proptrans}
end{table}



subsubsection{Type Implication}

%%%%%%%%%%%%%%%% CODE FOR IMAGE 2 %%%%%%%%%%%%%%%%
tabref{tab:impl} summarizes the constraints for
different scoring functions.
begin{table}[htbp]
  %centering
  begin{tabular}{r | l}
    Model & multicolumn{1}{c}{Constraints}\hline
    A, AR , B &  $r le r'$\
    C, D &  $r le r' le -r$
    end{tabular}
  caption{Constraints sufficient for enforcing $implication(r, r')$ under different
  score models and composition functions. The constraint that $e ge Z forall
  e in cE$ applies in all rows.}
  label{tab:impl}
end{table}

subsubsection{Reverse Relational Implication}

%%%%%%%%%%%%%%%%%% CODE FOR PREAMBLE %%%%%%%%%%%%%%%
documentclass[11pt,a4paper]{article}
usepackage[hyperref]{acl2017}
usepackage{times}
usepackage{latexsym}
usepackage{url}
usepackage[]{enumitem}
usepackage{mfirstuc}
usepackage{adjustbox}
usepackage{lipsum}
usepackage[font=small,skip=2pt]{caption}
usepackage{subcaption}
usepackage[disable]{todonotes} % insert [disable] to disable all notes.
usepackage{xcolor}
usepackage{amssymb,amsmath,amsthm,mathtools,graphicx,url,xspace,booktabs,microtype}
usepackage{bm}
usepackage[]{breqn}
usepackage{dcolumn}
newcolumntype{H}{>{setbox0=hboxbgroup}c<{egroup}@{}}
newtheorem{proposition}{Proposition}
% ------------- listings -------------- %
usepackage{listings}
usepackage[]{changepage}
lstset{basicstyle=ttfamily,linewidth=10cm}
% ------------- algorithmicx --------------- %
% The package algorithmicx itself doesn’t define any algorithmic commands
% algpseudocode is the predefined command set that must be used.
usepackage{algorithm}
PassOptionsToPackage{noend}{algpseudocode}
usepackage{algpseudocode}
algnewcommand{LeftComment}[1]{(triangleright) #1}%
algrenewcommandalgorithmicindent{0.6em}%
usepackage{xpatch}
makeatletter%
xpatchcmd{algorithmic}{ALG@tlmz@}{leftmarginz@ALG@tlmz@}{}{}%
makeatother
% Set skips to very low values
newcommand{zerodisplayskips}{%
setlength{abovedisplayskip}{0pt}%
setlength{belowdisplayskip}{0pt}%
setlength{abovedisplayshortskip}{0pt}%
setlength{belowdisplayshortskip}{0pt}}
appto{normalsize}{zerodisplayskips}