enterleave_init : CONTEXT = BEGIN

T__B : TYPE = {T__1, T__2, T__3, T__BB};

T : TYPE = {g : T__B | g /= T__BB};

State : MODULE =
  BEGIN
    LOCAL s : set {T;} ! Set
    LOCAL l : sequence {T__B; T__BB, 3} ! Sequence                %%10
    INITIALIZATION [
        l = sequence {T__B; T__BB, 3} ! empty
      -->
    ]
    TRANSITION [
      Init__ :
          s' = set {T;} ! empty
        -->
          s' IN {x : set {T;} ! Set | TRUE}
    ]                                                             %%20
  END;

%% The following CTL theorem was added by hand

%% The initialisation theorem
  init : THEOREM State |- 
	EX (s = sequence {T__B; T__BB, 3} ! range(l)); 

END
%% The contexts sequence and set were used