This alternative formulation of the complex numbers integrates with the standard PVS decision procedures. The technique is to auto-rewrite complex equalities, such as z1 = z2 as the pair of rules:

• Re(z1) = Re(z2) & Im(Z1) = Im(z2)

Highlights

Major theorems

Theorem	Location	PVS Name	Contributors

Contributors

• David Lester, Manchester University, UK
• Anthony Narkawicz, NASA, USA
• César Muñoz, NASA, USA
• Sam Owre, SRI, USA
• Mariano Moscato, NIA & NASA, USA

Maintainer

• César Muñoz, NASA, USA

Dependencies