%{ == Polarized logic == }% 

polarity : type.			%name polarity S.
pos : polarity.
neg : polarity.

atm : polarity -> type.                 %name atm Q q.
prop : polarity -> type.                %name prop A.

atom : atm S -> prop S.
up : prop pos -> prop neg.
down : prop neg -> prop pos.
* : prop pos -> prop pos -> prop pos.   %infix right 10 *.
+ : prop pos -> prop pos -> prop pos.   %infix right 9 +.
-o : prop pos -> prop neg -> prop neg.  %infix right 8 -o.

%block bl_atmpos : block {qp:atm pos}.
%block bl_atmneg : block {qn:atm neg}.



%{ == Sequent calculus for polarized logic == }%

%{ === Logic definition === }%

%{ 
A sequent is written
 h1: hyp A1, ..., hn: hyp An |- conc A 
 A1, ..., An |- A
}%

hyp : prop S -> type.                   %name hyp H h.
conc : prop S -> type.                  %name conc D.

%block bl_hyp : some {S:polarity} {A:prop S} block {h:hyp A}.

init : hyp (atom Q) -> conc (atom Q).

upR : conc P
       -> conc (up P).
upL : (hyp P -> conc C)
       -> (hyp (up P) -> conc C).

downL : (hyp N -> conc C)
	    -> (hyp (down N) -> conc C).
downR : conc N
	 -> conc (down N).

*R : conc P1 -> conc P2 -> conc (P1 * P2).
*L : (hyp P1 -> hyp P2 -> conc C)
      -> (hyp (P1 * P2) -> conc C).

+R1 : conc P1 -> conc (P1 + P2).
+R2 : conc P2 -> conc (P1 + P2).
+L : (hyp P1 -> conc C)
      -> (hyp P2 -> conc C)
      -> (hyp (P1 + P2) -> conc C).

-oR : (hyp P -> conc N)
       -> (conc (P -o N)).
-oL : conc P
       -> (hyp N -> conc C)
       -> (hyp (P -o N) -> conc C).

%worlds (bl_atmpos | bl_atmneg | bl_hyp)
  (hyp A) (conc C).

%{ == Focused sequent calculus == }%

%{ === Logic definition === }%

%{ 
Neutral sequent:
 l1:left P1, ..., ln:left Pn |- right N
 P1, ..., Pn |- N

Left-focused sequent:
 l1:left P1, ..., ln:left Pn |- lfoc N1 N2
 P1, ..., Pn [N1] |- N2

Right-focused sequent:
 l1:left P1, ..., ln:left Pn |- rfoc P
 P1, ..., Pn |- [P]

These can be generically expressed as:
 l1:left P1, ..., ln:left Pn |- conseq C
 P1, ..., Pn |- C
}%

left : prop pos -> type.                %name left L l.

conclusion : type.                      %name conclusion C.
conseq : conclusion -> type.            %name conseq R.
conc-lfoc : prop neg -> prop neg -> conclusion.
conc-rfoc : prop pos -> conclusion.
conc-right : prop neg -> conclusion.

%abbrev rfoc = [P] conseq (conc-rfoc P).
%abbrev lfoc = [N][N'] conseq (conc-lfoc N N').
%abbrev right = [N] conseq (conc-right N).

%block bl_left : some {P:prop pos} block {l:left P}.

initR' : left (atom Qp) -> rfoc (atom Qp).
initL' : lfoc (atom Qn) (atom Qn).

upR' : rfoc P
        -> right (up P).
upL' : (left P -> right N)
        -> (lfoc (up P) N).

downR' : right N
          -> rfoc (down N).
downL' : (lfoc N N')
          -> (left (down N) -> right N').

*R' : rfoc P1
       -> rfoc P2
       -> rfoc (P1 * P2).
*L' : (left P1 -> left P2 -> right N')
       -> (left (P1 * P2) -> right N').

+R1' : rfoc P1
        -> rfoc (P1 + P2).
+R2' : rfoc P2 
        -> rfoc (P1 + P2).
+L' : (left P1 -> right N')
       -> (left P2 -> right N')
       -> (left (P1 + P2) -> right N').

-oR' : (left P -> right N) 
        -> (right (P -o N)).
-oL' : rfoc P
        -> (lfoc N N')
        -> (lfoc (P -o N) N').

%worlds (bl_atmpos | bl_atmneg | bl_left)
  (left P) (conseq C).  % = (right N) (left N N') (rfoc P).

%{ === Cut admissibility === }%

cut< : {N} lfoc N' N -> (lfoc N NC) -> lfoc N' NC -> type.
cut- : {N} right N -> (lfoc N NC) -> right NC -> type.
cut+ : {P} rfoc P -> (left P -> conseq C) -> conseq C -> type.
%mode cut< +N +D +E -F.
%mode cut- +N +D +E -F.
%mode cut+ +P +D +E -F.

%{ ==== Identity cuts ==== }% 

- : cut+ (atom Qp) (initR' D) ([l] initR' l) (initR' D).
- : cut< (atom Qn) (initL') (initL') (initL').

%{ ==== Principal cuts ==== }%

- : cut- (up P) (upR' (D : rfoc P)) (upL' (E : left P -> right N)) F
     <- cut+ P D E (F : right N).

- : cut+ (down N) (downR' (D : right N)) 
     ([l:left (down N)] downL' (E l : lfoc N NC) l) G
     <- cut+ (down N) (downR' D) E (F : lfoc N NC)
     <- cut- N D F (G : right NC).

- : cut+ (P1 * P2) (*R' (D1 : rfoc P1) (D2 : rfoc P2)) 
     ([l:left (P1 * P2)] *L' (E l : left P1 -> left P2 -> right N) l) G
     <- ({l1:left P1}{l2: left P2} 
           cut+ (P1 * P2) (*R' D1 D2) ([l:left (P1 * P2)] E l l1 l2)
           (F l1 l2 : right N))
     <- ({l1:left P1} cut+ P2 D2 ([l2:left P2] F l1 l2) (F' l1 : right N))
     <- cut+ P1 D1 F' (G : right N).

- : cut+ (P1 + P2) (+R1' (D1 : rfoc P1))
     ([l:left (P1 + P2)] +L' (E1 l : left P1 -> right N) (E2 l) l) F
     <- ({l1:left P1}
           cut+ (P1 + P2) (+R1' D1) ([l:left (P1 + P2)] E1 l l1)
           (E1' l1 : right N))
     <- cut+ P1 D1 E1' (F : right N).

- : cut+ (P1 + P2) (+R2' (D2 : rfoc P2))
     ([l:left (P1 + P2)] +L' (E1 l) (E2 l : left P2 -> right N) l) F
     <- ({l2:left P2}
           cut+ (P1 + P2) (+R2' D2) ([l:left (P1 + P2)] E2 l l2)
           (E2' l2 : right N))
     <- cut+ P2 D2 E2' (F : right N).

- : cut- (N -o P) (-oR' (D1 : left N -> right P))
     (-oL' (E1 : rfoc N) (E2 : lfoc P NC)) F
     <- cut+ N E1 D1 (F1 : right P)
     <- cut- P F1 E2 (F : right NC).

%{ ==== Left commutative cuts ==== }%

- : cut< N (upL' D) E (upL' F)
     <- ({l1} cut- N (D l1) E (F l1)).
- : cut- N (downL' D L) E (downL' F L)
     <- cut< N D E F.
- : cut- N (*L' D L) E (*L' F L)
     <- ({l1}{l2} cut- N (D l1 l2) E (F l1 l2)).
- : cut- N (+L' D1 D2 L) E (+L' F1 F2 L)
     <- ({l1} cut- N (D1 l1) E (F1 l1))
     <- ({l2} cut- N (D2 l2) E (F2 l2)).
- : cut< N (-oL' D1 D2) E (-oL' D1 F2)
     <- cut< N D2 E F2.

%{ ==== Right commutative cuts ==== }%

- : cut+ P D ([l] initR' L) (initR' L).
- : cut+ P D ([l] initL') (initL').
- : cut+ P D ([l] upR' (E l)) (upR' F)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] upL' [l1] E l l1) (upL' F)
     <- ({l1} cut+ P D ([l] E l l1) (F l1)).
- : cut+ P D ([l] downR' (E l)) (downR' F)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] downL' (E l) L) (downL' F L)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] *R' (E1 l) (E2 l)) (*R' F1 F2)
     <- cut+ P D ([l] E1 l) F1
     <- cut+ P D ([l] E2 l) F2.
- : cut+ P D ([l] *L' ([l1][l2] E l l1 l2) L)
     (*L' ([l1][l2] F l1 l2) L)
     <- ({l1}{l2} cut+ P D ([l] E l l1 l2) (F l1 l2)).
- : cut+ P D ([l] +R1' (E l)) (+R1' F)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] +R2' (E l)) (+R2' F)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] +L' ([l1] E1 l l1) ([l2] E2 l l2) L)
     (+L' F1 F2 L)
     <- ({l1} cut+ P D ([l] E1 l l1) (F1 l1))
     <- ({l2} cut+ P D ([l] E2 l l2) (F2 l2)).
- : cut+ P D ([l] -oR' (E l)) (-oR' F)
     <- {l1} cut+ P D ([l] E l l1) (F l1).
- : cut+ P D ([l] -oL' (E1 l) (E2 l)) (-oL' F1 F2)
     <- cut+ P D ([l] E1 l) F1
     <- cut+ P D ([l] E2 l) F2.

%worlds (bl_atmpos | bl_atmneg | bl_left)
(cut< _ _ _ _)
(cut- _ _ _ _)
(cut+ _ _ _ _).

%total {(N1 N2 P3) [(D1 D2 D3) (E1 E2 E3)]}
(cut< N1 D1 E1 _)
(cut+ N2 D2 E2 _)
(cut- P3 D3 E3 _).

%{ ==== Corollary - unfocused cut ==== }%

cut-unfoc+ : right (up P) -> (left P -> right N) -> right N -> type.
%mode cut-unfoc+ +D +E -F.

- : cut-unfoc+ D E F
     <- cut- (up P) D (upL' E) F.

%worlds (bl_atmpos | bl_atmneg | bl_left) (cut-unfoc+ _ _ _).
%total [] (cut-unfoc+ _ _ _).

cut-unfoc- : right A -> (left (down A) -> right C) -> right C -> type.
%mode cut-unfoc- +A +B -C.

- : cut-unfoc- D E F
     <- cut+ (down A) (downR' D) E F.

%worlds (bl_atmpos | bl_atmneg | bl_left) (cut-unfoc- _ _ _).
%total [] (cut-unfoc- _ _ _).



%{ === Identity === }%

%{ ==== Eta expansion lemmas ==== }%

eta- : {N:prop neg} ({N':prop neg} lfoc N N' -> right N') -> right N -> type.
eta+ : {P:prop pos} (rfoc P -> right N') -> (left P -> right N') -> type.
%mode eta- +N +R -R'.
%mode eta+ +P +R -R'.

%block bl_rfoc : some {P:prop pos} block {rf:rfoc P}.

- : eta+ (atom Qp) ([rf] R rf) ([l] R (initR' l)).

- : eta- (atom Qn) ([n'] [lf] R n' lf) (R (atom Qn) initL').

- : eta- (up P) ([n'] [lf] R n' lf) (R (up P) (upL' ([l] R' l)))
     <- eta+ P ([rf] upR' rf) ([l] R' l).

- : eta+ (down N) ([rf] R rf) ([l:left (down N)] R (downR' (R' l))) 
     <- ({l:left (down N)} eta- N ([n'] [lf] downL' lf l) (R' l)). 

- : eta+ (P1 * P2) ([rf] R rf) ([l] *L' ([l1] [l2] R'' l1 l2) l)
     <- ({rf1:rfoc P1} eta+ P2 ([rf2] R (*R' rf1 rf2)) ([l2] R' rf1 l2))
     <- ({l2:left P2} eta+ P1 ([rf1] R' rf1 l2) ([l1] R'' l1 l2)).

- : eta+ (P1 + P2) ([rf] R rf) (+L' R1 R2)
     <- eta+ P1 ([rf1] R (+R1' rf1)) ([l1:left P1] R1 l1 : right N)
     <- eta+ P2 ([rf1] R (+R2' rf1)) ([l2:left P2] R2 l2 : right N).

- : eta- (P1 -o N2) ([n'] [lf] R n' lf) (-oR' [l1] R1 l1)
     <- ({rf1:rfoc P1}
           eta- N2 ([n'] [lf2] R n' (-oL' rf1 lf2)) (R2  rf1))
     <- eta+ P1 ([rf1] R2 rf1) ([l1] R1 l1).

%worlds (bl_atmpos | bl_atmneg | bl_left | bl_rfoc)
  (eta- N R R') (eta+ P R R').

%total (N P) (eta- N _ _) (eta+ P _ _).


%{ ==== Identity corollaries ==== }%

idp : {P:prop pos} (left P -> right (up P)) -> type.
%mode idp +P -R.

- : idp P R <- eta+ P ([rf] upR' rf) R.

%worlds (bl_atmpos | bl_atmneg | bl_left | bl_rfoc) (idp _ _).
%total [] (idp _ _).

idn : {N:prop neg} (left (down N) -> right N) -> type.
%mode idn +N -R.

- : idn N ([l] R l)
     <- ({l:left (down N)} eta- N ([qn] [lf] downL' lf l) (R l)). 

%worlds (bl_atmpos | bl_atmneg | bl_left | bl_rfoc) (idn _ _).
%total [] (idn _ _).



%{ == Soundness == }%

sdR : right N -> conc N -> type.
sd+ : rfoc P -> conc P -> type.
sd- : lfoc N N' -> (hyp N -> conc N') -> type.
sdL : left P -> hyp P -> type.
%mode sdR +R -D.
%mode sd+ +R -D.
%mode sd- +R -D.
%mode sdL +L -H.

- : sd+ (initR' L) (init H)
     <- sdL L H.
- : sd- (initL') ([h] init h).
- : sdR (upR' R) (upR D)
     <- sd+ R D.
- : sd- (upL' [l] R l) ([h] upL ([hp] D hp) h)
     <- ({l} {hp} sdL l hp -> sdR (R l) (D hp)).
- : sd+ (downR' R) (downR D)
     <- sdR R D.
- : sdR (downL' R L) (downL ([hn] D hn) H)
     <- sd- R ([hn] D hn)
     <- sdL L H.
- : sd+ (*R' R1 R2) (*R D1 D2)
     <- sd+ R1 D1
     <- sd+ R2 D2.
- : sdR (*L' ([l1] [l2] R l1 l2) L12) (*L ([h1] [h2] D h1 h2) H12)
     <- ({l1} {h1} sdL l1 h1
           -> {l2} {h2} sdL l2 h2
           -> sdR (R l1 l2) (D h1 h2))
     <- sdL L12 H12.
- : sd+ (+R1' R1) (+R1 D1)
     <- sd+ R1 D1.
- : sd+ (+R2' R2) (+R2 D2)
     <- sd+ R2 D2.
- : sdR (+L' ([l1] R1 l1) ([l2] R2 l2) L) (+L ([h1] D1 h1) ([h2] D2 h2) H)
     <- ({l1} {h1} sdL l1 h1 -> sdR (R1 l1) (D1 h1))
     <- ({l2} {h2} sdL l2 h2 -> sdR (R2 l2) (D2 h2))
     <- sdL L H.
- : sdR (-oR' [l] R l) (-oR [h] D h)
     <- ({l} {h} sdL l h -> sdR (R l) (D h)).
- : sd- (-oL' R1 R2) ([h] -oL D1 ([h2] D2 h2) h)
     <- sd+ R1 D1
     <- sd- R2 ([h2] D2 h2).

%block bl_sdL : some {P:prop pos} block {l:left P} {h:hyp P} {_:sdL l h}.

%worlds (bl_atmpos | bl_atmneg | bl_sdL) (sdR _ _) (sd+ _ _) (sd- _ _) (sdL _ _).
%total [] (sdL _ _).
%total (R1 R2 R3) (sdR R1 _) (sd+ R2 _) (sd- R3 _).



%{ == Completeness == }%

%{ === Unfocused admissibility === }%

adm*R : right (up P1) -> right (up P2) -> right (up (P1 * P2)) -> type.
%mode adm*R +R1 +R2 -R.

- : adm*R (R1 : right (up P1)) (R2 : right (up P2)) R
     <- ({rf1:rfoc P1} eta+ P2 ([rf2:rfoc P2] upR' (*R' rf1 rf2)) 
           ([l2:left P2] R3 rf1 l2))
     <- ({l2:left P2} eta+ P1 ([rf1:rfoc P1] R3 rf1 l2) ([l1] R4 l1 l2))
     <- ({l2:left P2} cut-unfoc+ R1 ([l1:left P1] R4 l1 l2) (R5 l2))
     <- cut-unfoc+ R2 ([l2:left P2] R5 l2) R.

%worlds (bl_atmpos | bl_atmneg | bl_left) (adm*R _ _ _).
%total [] (adm*R _ _ _).

adm+R1 : right (up P1) -> right (up (P1 + P2)) -> type.
%mode +{P1:prop pos} +{P2:prop pos} +{R1:right (up P1)}
      -{R:right (up (P1 + P2))} (adm+R1 R1 R).

- : adm+R1 (R1 : right (up P1)) R
     <- eta+ P1 ([rf1:rfoc P1] upR' (+R1' rf1))
        (R1' : left P1 -> right (up (P1 + P2)))
     <- cut-unfoc+ R1 ([l1] R1' l1) R.

%worlds (bl_atmpos | bl_atmneg | bl_left) (adm+R1 _ _).
%total [] (adm+R1 _ _).

adm+R2 : right (up P2) -> right (up (P1 + P2)) -> type.
%mode +{P1:prop pos} +{P2:prop pos} +{R2:right (up P2)}
      -{R:right (up (P1 + P2))} (adm+R2 R2 R).

- : adm+R2 (R2 : right (up P2)) R
     <- eta+ P2 ([rf2:rfoc P2] upR' (+R2' rf2))
        (R2' : left P2 -> right (up (P1 + P2)))
     <- cut-unfoc+ R2 ([l2] R2' l2) R.

%worlds (bl_atmpos | bl_atmneg | bl_left) (adm+R2 _ _).
%total [] (adm+R2 _ _).

adm-oL : right (up P1)
	  -> (left (down N2) -> right N')
	  -> (left (down (P1 -o N2)) -> right N')
	  -> type.
%mode adm-oL +R1 +R2 -R.

- : adm-oL (R1 : right (up P1)) (R2 : left (down N2) -> right N')
     (R : left (down (P1 -o N2)) -> right N')
     <- ({l:left (down (P1 -o N2))} {rf1:rfoc P1}
           eta- N2 ([n][lf2] downL' (-oL' rf1 lf2) l) (R3 rf1 l : right N2))
     <- ({l} eta+ P1 ([rf1] R3 rf1 l) ([l1] R4 l l1))
     <- ({l} {l1} cut-unfoc- (R4 l l1) ([l2] R2 l2) (R5 l l1))
     <- ({l} cut-unfoc+ R1 ([l1] R5 l l1) (R l)).

%worlds (bl_atmpos | bl_atmneg | bl_left) (adm-oL _ _ _).
%total [] (adm-oL _ _ _).

%{ === Completeness === }%

cph+ : hyp P -> left P -> type.
cph- : hyp N -> left (down N) -> type.
cp- : conc N -> right N -> type.
cp+ : conc P -> right (up P) -> type.
%mode cph+ +Hp -L.
%mode cph- +Hn -L.
%mode cp- +Dn -R.
%mode cp+ +Dp -R.

- : cp+ (init Hp) (upR' (initR' L))
     <- cph+ Hp L.
- : cp- (init Hn) (downL' (initL') L)
     <- cph- Hn L.

- : cp- (upR Dp) R
     <- cp+ Dp R.
- : cp- (upL ([hp] Dn1 hp) Hn) (downL' (upL' ([l] R1 l)) L)
     <- cph- Hn L
     <- ({hp:hyp P} {l:left P}
           cph+ hp l -> cp- (Dn1 hp) (R1 l)).
- : cp+ (upL ([hp] Dp1 hp) Hn) (downL' (upL' ([l] R1 l)) L)
     <- cph- Hn L
     <- ({hp:hyp P} {l:left P}
	   cph+ hp l -> cp+ (Dp1 hp) (R1 l)).

- : cp+ (downR Dn) (upR' (downR' R))
     <- cp- Dn R.
- : cp- (downL ([hn] Dn hn) Hp) (R L)
     <- cph+ Hp L
     <- ({hn:hyp N} {l:left (down N)}
           cph- hn l -> cp- (Dn hn) (R l)).
- : cp+ (downL ([hn] Dp hn) Hp) (R L)
     <- cph+ Hp L
     <- ({hn:hyp N} {l:left (down N)}
           cph- hn l -> cp+ (Dp hn) (R l)).

- : cp+ (*R Dp1 Dp2) R12
     <- cp+ Dp1 R1
     <- cp+ Dp2 R2
     <- adm*R R1 R2 R12.
- : cp- (*L ([hp1] [hp2] Dn hp1 hp2) Hp) (*L' ([l1] [l2] R l1 l2) L)
     <- cph+ Hp L
     <- ({hp1:hyp P1} {l1:left P1} cph+ hp1 l1
           -> {hp2:hyp P2} {l2:left P2} cph+ hp2 l2
           -> cp- (Dn hp1 hp2) (R l1 l2)).
- : cp+ (*L ([hp1] [hp2] Dp hp1 hp2) Hp) (*L' ([l1] [l2] R l1 l2) L)
     <- cph+ Hp L
     <- ({hp1:hyp P1} {l1:left P1} cph+ hp1 l1
           -> {hp2:hyp P2} {l2:left P2} cph+ hp2 l2
           -> cp+ (Dp hp1 hp2) (R l1 l2)).

- : cp+ (+R1 Dp1) R12
     <- cp+ Dp1 R1
     <- adm+R1 R1 R12.
- : cp+ (+R2 Dp2) R12
     <- cp+ Dp2 R2
     <- adm+R2 R2 R12.
- : cp- (+L ([h1] D1 h1) ([h2] D2 h2) H) (+L' R1 R2 L)
     <- cph+ H L
     <- ({h1}{l1} cph+ h1 l1 -> cp- (D1 h1) (R1 l1))
     <- ({h2}{l2} cph+ h2 l2 -> cp- (D2 h2) (R2 l2)).
- : cp+ (+L ([h1] D1 h1) ([h2] D2 h2) H) (+L' R1 R2 L)
     <- cph+ H L
     <- ({h1}{l1} cph+ h1 l1 -> cp+ (D1 h1) (R1 l1))
     <- ({h2}{l2} cph+ h2 l2 -> cp+ (D2 h2) (R2 l2)).

- : cp- (-oR [hp] Dn hp) (-oR' [l] R l)
     <- ({hp:hyp P} {l:left P}
           cph+ hp l -> cp- (Dn hp) (R l)).
- : cp- (-oL Dp1 ([hn2] Dn2 hn2) Hn) (R12 L)
     <- cph- Hn L
     <- cp+ Dp1 R1
     <- ({hn2:hyp N2} {l2:left (down N2)}
           cph- hn2 l2 -> cp- (Dn2 hn2) (R2 l2))
     <- adm-oL R1 ([l2] R2 l2) ([l] R12 l).
- : cp+ (-oL Dp1 ([hn2] Dp2 hn2) Hn) (R12 L)
     <- cph- Hn L
     <- cp+ Dp1 R1
     <- ({hn2:hyp N2} {l2:left (down N2)}
           cph- hn2 l2 -> cp+ (Dp2 hn2) (R2 l2))
     <- adm-oL R1 ([l2] R2 l2) ([l] R12 l).

%block bl_cph+ : some {P:prop pos} block {hp:hyp P} {l:left P} {_:cph+ hp l}.
%block bl_cph- : some {N:prop neg} block {hn:hyp N} {l:left (down N)} {_:cph- hn l}.

%worlds (bl_atmpos | bl_atmneg | bl_cph+ | bl_cph-)
   (cp- _ _) (cp+ _ _) (cph- _ _) (cph+ _ _).

%total [] (cph+ Hp _).
%total [] (cph- Hn _).
%total (Dn Dp) (cp- Dn _) (cp+ Dp _).


%{ == Translating into focused logic == }%

%{ A simple proof which is isomorphic in the unfocused and
focused system, establishing <tt>|- a * b -o b * a</tt>
for positive a and b.}%

%abbrev ' = [q] atom q.
r0 : {a:atm pos} {b:atm pos} right (' a * ' b -o up (' b * ' a))
   = [a] [b] -oR' ([lab] *L' ([la] [lb] upR' (*R' (initR' lb) (initR' la))) lab).
d0 : {a:atm pos} {b:atm pos} conc (' a * ' b -o up (' b * ' a))
   = [a] [b] -oR ([hab] *L ([ha] [hb] upR (*R (init hb) (init ha))) hab).

%{|check=decl}%

%query 1 * {a}{b} sdR (r0 a b) (D0 a b).

%{|check=decl}%

%query 1 * {a}{b} cp- (d0 a b) (R0 a b).

%{ === Reducing the number of proofs === }%

%{ This first example is already in "focused form" - invertible rules
are applied only "before" upR is applied to prove 
<tt>|- (a + b) -> up (a + b)</tt> |check=decl}% 
%query 1 *
   {a: atm pos}{b: atm pos} 
   cp- (-oR ([h: hyp (atom a + atom b)]
		    +L ([ha: hyp (atom a)] upR (+R1 (init ha)))
		       ([hb: hyp (atom b)] upR (+R2 (init hb))) h))
            (D a b).

%{ This a proof of the same sequent, but upR is applied before +L, which
is fine in the unfocused system but not in the focused system, where upR
starts a focusing phase and makes it impossible to apply invertible rules like
+L. Translation produces the same focused proof from these two different
unfocused proofs. |check=decl}% 
%query 1 *
   {a: atm pos}{b: atm pos} 
   cp- (-oR ([h: hyp (atom a + atom b)] 
		    upR (+L ([ha: hyp (atom a)] +R1 (init ha))
			    ([hb: hyp (atom b)] +R2 (init hb)) h)))
            (D a b).



%{ === Forward and backward chaining === }%

%{ Finally, consder the following unfocused sequent proof. The proof
proceeds in what we generally consider a "forward-chaining" manner, using
the hypothesis (atom A) to obtain the hypothesis (atom B), which is then
used to obtain the hypothesis (atom C), which is then used to obtain
the hypothesis (atom D), which is finally used to finish. }%

implies-proof =
   [A: atm neg][B: atm neg][C: atm neg][D: atm neg]
   -oR (downL [ha: hyp (atom A)]
   -oR (downL [hab: hyp (down (atom A) -o (atom B))]
   -oR (downL [hbc: hyp (down (atom B) -o (atom C))]
   -oR (downL [hcd: hyp (down (atom C) -o (atom D))] 
    (-oL (downR (init ha)) 
     ([hb: hyp (atom B)]
      -oL (downR (init hb))
      ([hc: hyp (atom C)]
       -oL (downR (init hc))
       ([hd: hyp (atom D)] init hd) 
       hcd)
      hbc)
     hab))))).

%{ Because negative polarity forces search to be goal directed, translating
this proof into the focused system will flip the order in which the 
implications are considered, and no facts (beyond the four in the implication)
will ever be added to the context. | check=decl }%
   
%query 1 * 
   {a: atm neg}{b: atm neg}{c: atm neg}{d: atm neg}
   cp- (implies-proof a b c d) _.

%{ Finally, we can show the proof of a successful attempt to prove
<tt>right (A -o (A -o B) -o (B -o C) -o C)</tt> in the weakly focused system.
In general, this could cause an infinite loop as Twelf has no problem
with deriving multiple copies of the same fact, but here we use all
negative atoms, and the resulting backward-chaining semantics
corresponds nicely to Twelf's built-in backward-chaining semantics. 
|check=decl}%

%solve p : 
   {a: atm neg}{b: atm neg}{c: atm neg}
   right (down (' a)
          -o down (down (' a) -o ' b) 
            -o down (down (' b) -o ' c) -o ' c).