Main contributions include:
- A coding for diagonalizing a sequence
- Double and single indexing for sequences
- Convergence properties of doubly indexed sequences of non-negative reals
Theorem | Location | PVS Name | Contributors |
---|
- David Lester, Manchester University, UK
- César Muñoz, NASA, USA
- Sam Owre, SRI, USA
- Mariano Moscato, NIA & NASA, USA
- César Muñoz, NASA, USA