The NuPrl4 term structure and editor display mechanism are used to provide unambiguous notations for use in the the development of computer supported mathematical arguments. These notations are used to provide a natural statment of a theorem in Hamiltonian dynamics, anchored in a computationally unambiguous representation, that can be made explicit if required.