%
% Implements a "mathematical machine" with configuration
% set C.
% The transition function is delta.
% The initial configurtion is provided as initialconf.
%

mathm[C: TYPE, 
      delta: [C->C],
      initialconf: C]: THEORY
  BEGIN
    IMPORTING mathmtimet

    T: VAR mathmtimet

    mathm(T): RECURSIVE C = (
      %
      % initialization
      %
      IF T=0 THEN
        initialconf
      ELSE
        delta(mathm(T-1))
      ENDIF) MEASURE T

  END mathm