VARIABLES T P E FIX_VARIABLES Int <: T Successor <: P P <: My