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