\newchapter{Proofs}

\leveldown{}

\renewcommand{\CURPATH}{proofs}

SAT/SMT solvers can't prove \emph{correctness} of something, or if the model behaves as the author wanted.

However, it can prove equivalence of two expressions or models.

\input{proofs/XOR_EN}
\input{proofs/XOR_SAT/main_EN}
\input{proofs/Dietz_EN}
\input{proofs/XOR_swap_EN}
\input{proofs/simplify1}
\input{proofs/simplify2}
\input{proofs/bitrev/main_EN}
\input{proofs/sorting_network/main_EN}
\input{proofs/ITE_equiv_EN}
\input{proofs/abs_EN}
\input{proofs/minmax_EN}
\input{proofs/nozerobytes_EN}
\input{proofs/bvashr_EN}
\input{proofs/floor_ceiling}
\input{proofs/isXML/main}

\levelup{}