%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Interpreter for focused linear logic (LLF) %
% %
% Examples Linear Nested systems: G3cp %
% %
% Author: Elaine Pimentel (2015) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
module g3cp.
accumulate llf.
theory g3cp
(
(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))) ::
( perp (l X cfalse) , top) :: nil
).
%%%% Tests
%llf 100 g3cp (r x (a cimp a)).
%llf 100 g3cp (r x ((a cand b) cimp (a cand b))).