Extended non-negative reals

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

Highlights

Major theorems

Theorem	Location	PVS Name	Contributors

Contributors

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

Maintainer

• César Muñoz, NASA, USA

Dependencies