\myheading{Branchless abs()}

Prove that branchless abs() function from the Henry Warren 2ed, "2-4 Absolute Value Function" is correct:

\lstinputlisting[style=customsmt]{proofs/abs.smt}