TRC abstraction and notation conversion utility

See text for an explanation of the various notations. The dropdown list allows you to insert the definition of any term used in defining push. Each term in the list is defined in terms of earlier terms in the list together with primitive constants p1, p2, eq and abst.