% state of a program
  % represented as values of a finite set of integer variables
  State[varCount: nat] : THEORY
  BEGIN
    state : TYPE = [ below(varCount) -> int ]      
  END State