%------------------------------------------------------------------------------
% The Equivalence of a Direct and Structural Operational Semantics
%
% All references are to HR and F Nielson "Semantics with Applications:
% A Formal Introduction", John Wiley & Sons, 1992. (revised edition
% available: http://www.daimi.au.dk/~hrn )
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

direct_sos[V:TYPE+]: THEORY

BEGIN

  IMPORTING direct[V], sos[V], Cont[V], continuation[V]

  S: VAR Stm

  sos_le_direct: LEMMA sq_le(sos.SS(S),direct.SS(S))                 % N&N 4.56

  direct_le_sos: LEMMA sq_le(direct.SS(S),sos.SS(S))                 % N&N 4.57

  direct_eq_sos: LEMMA direct.SS(S) = sos.SS(S)                      % N&N 4.55

END direct_sos