%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Interpreter for focused linear logic (LLF) %
% %
% Examples Linear Nested systems: EC %
% %
% Author: Elaine Pimentel (2015) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
module EC.
accumulate llf.
theory ec
(
(sigma A\ sigma B\ sigma X\ (perp (l X (A cimp B))) , ((r X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cimp B))) , ((l X A) @ (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cand B))) , ((l X A) @ (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cand B))) , ((r X A) & (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cor B))) , ((l X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cor B))) , ((r X A) @ (l X B))) ::
(sigma A\ sigma X\ (perp (r X A)) , (perp (l X A))) ::
(sigma A\ sigma X\ sigma Z\ (perp (r X (box A))),(perp (rel Z X)),pi Y\ pi W\ (r Y A) @ (l W A) @ (relE X Y W)) ::
(sigma A\ sigma X\ sigma Y\ sigma Z\ (perp (l X (box A))),(perp (relE X Y Z)), ((l Y (box A)) @ (rel X Y)) , ((r Z (box A)) @ (rel X Z))) ::
(sigma A\ sigma X\ sigma Y\ sigma Z\ (perp (l X (box A))),(perp (relE X Y Z)), ((l Y (box A)) @ (relE X Y Z)) , ((r Z (box A)) @ (rel X Z))) ::
( perp (l X cfalse) , top) :: nil
).