# This file contains the implication pattern of the irreducable modalities
# of the Modal Logic system S3.

=duals       # we take advantage of dualism to only specify half of them.
=beckersrule # and Becker's rule.

    Lp  =>      p
   LLp  =>     Lp

    Lp  =>   LMLp
   LLp  =>  LLMLp

   LMp  =>   LMMp
  LLMp  => LMLLMp
  LMLp  =>    MLp
  LMLp  =>  LMMLp

  LMLp  =>    LMp
 LLMLp  =>   LLMp

 LLMLp  =>  LMLLp

 LMLLp  => LMLLMp
 LMLLp  =>   MLLp
 LMLLp  =>   LMLp

 LMMLp  =>   LMMp
 LMMLp  => MLMMLp

LMLLMp =>     LMp

# end of definition of S3.