%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Interpreter for focused linear logic (LLF) %
% %
% Examples Linear Nested systems: K %
% %
% Author: Elaine Pimentel (2015) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
module k.
accumulate llf.
theory k
(
(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\ sigma Z\ (perp (r X (box A))),(perp (Z rel X)),pi Y\ (r Y A) @ (X rel Y)) ::
(sigma A\ sigma X\ sigma Y\ (perp (l X (box A))),(perp (X rel Y)), ((l Y A) @ (X rel Y))) ::
(sigma A\ sigma X\ (perp (r X A)) , (perp (l X A))) ::
( perp (l X cfalse) , top) :: nil
).
%%%% Tests
%llf 100 k (r x ((box a) cimp (box a))).
%llf 100 k (r x (a cimp (box a))).
%llf 100 k (r x ((box a) cimp a)).
%llf 100 k (r x ((box (a cimp b)) cimp ((box a) cimp (box b)))).