Sequences of countable length defined as co-algebraic datatypes.
| Theorem | Location | PVS Name | Contributors |
|---|
- Jerry James, Utah State University, USA
- César Muñoz, NASA, USA
- Aaron Dutle, NASA, USA
- Mariano Moscato, NIA & NASA, USA
- Sam Owre, SRI, USA
- César Muñoz, NASA, USA
This library does not depend on any external theory.