%
%  This is a file of properties which modify the behavior of both 
%  the unifier and the multi-line note checker.
%
$((\pvar \c \qvar) \And (\qvar \c \rvar) \c (\pvar \c \rvar))$
$((\pvar \And \qvar) \Iff (\qvar \And \pvar))$
$(((\pvar \And \qvar) \And \rvar) \Iff (\pvar \And (\qvar \And \rvar)))$
%$((\pvar \Or \qvar) \Iff (\qvar \Or \pvar))$
%$(((\pvar \Or \qvar) \Or \rvar) \Iff (\pvar \Or (\qvar \Or \rvar)))$
$((x < y \And y < z) \c (x < z))$
$((x > y \And y > z) \c (x > z))$
$((x \le  y \And y \le  z) \c (x \le  z))$
$((x \ge  y \And y \ge  z) \c (x \ge  z))$
$((x \i  y \And y \i  z) \c (x \i  z))$
$((x \j  y \And y \j  z) \c (x \j  z))$
$((x \i\ne  y \And y \i\ne  z) \c (x \i\ne  z))$
$((x \j\ne  y \And y \j\ne  z) \c (x \j\ne  z))$
$((x < y) \And (y \le z) \c (x < z))$
$((x \le y) \And (y < z) \c (x < z))$
$((x > y \And y \ge z) \c (x > z))$
$((x \ge y \And y > z) \c (x > z))$
$((x \i\ne  y \And y \i\ne  z) \c (x \i\ne  z))$
$((x \i  y \And y \i\ne  z) \c (x \i\ne  z))$
$((x \i\ne  y \And y \i  z) \c (x \i\ne  z))$
$((x \j  y \And y \j\ne  z) \c (x \j\ne  z))$
$((x \j\ne  y \And y \j\ne  z) \c (x \j\ne  z))$
$((x \j\ne  y \And y \j  z) \c (x \j\ne  z))$
%$((x + y) \ident (y + x))$ 
$(((x + y) + z) \ident (x + (y + z)))$ 
$((x + (y + z)) \ident ((x + y) + z))$ 
