CONSTANTS
  N = 3
  Input = {2,3,5}
  RtnVal <- MCRtnVal

SPECIFICATION PCSpec
INVARIANT PCTypeOK