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)
| Theorem | Location | PVS Name | 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
- César Muñoz, NASA, USA
