Proof of correctness of high-performance 3-1 interlock collapsing ALUs. - James E. Phillips; Stamatis Vassiliadis (IBM J. Res. Dev., 1993)