AlarisGP models and documentation

Theory associated with the interface to the Alaris GP.
This new release improves the PVS theory for the completeness template (refactored function name to improve readability and understanding of the model)