# Focusing

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

Focusing for polarized logic and focalization (the completeness of focusing). This proof has been de-unicoded by a sed script, the original is here.

## Syntax

```pol: type. %name pol P.
+: pol.
-: pol.```

We define propositions in an environment with free atoms.

```atom: pol -> type. %name atom Q q.
%block atom+: block {Q+: atom +}.
%block atom-: block {Q-: atom -}.

typ: pol -> type. %name typ A.
c: atom P -> typ P.

dn: typ - -> typ +.
bot: typ +.
\/: typ + -> typ + -> typ +. %infix none 5 \/.
top+: typ +.
*: typ + -> typ + -> typ +. %infix none 5 *.

up: typ + -> typ -.
=>: typ + -> typ - -> typ -. %infix none 5 =>.
top-: typ -.
/\: typ - -> typ - -> typ -. %infix none 5 /\.```

Succedents are things that come to the right of the turnstile.

```suc: type. %name suc Suc jmt.
inv: typ - -> suc. %postfix 3 inv.
true: typ + -> suc. %postfix 3 true.
susp: typ - -> suc. %postfix 3 susp.```

Right-stable judgments are ones that are either positive or suspended.

```stable: suc -> type. %name stable St.
sp: stable (A+ true).
sn: stable (A- susp).```

An inversion context Inv is a list of positive propositions.

```pos: type. %name pos Inv.
#: pos.
,: typ + -> pos -> pos. %infix right 3 ,.```

## Sequent calculus

```seqform: type. %name seqform Form.
exp: seqform -> type. %name exp E z.

rfoc: typ + -> seqform.
%abbrev value: typ + -> type = [A+] exp (rfoc A+).

leftform: type.
hasleft: leftform -> suc -> seqform.

ininv: pos -> leftform.
%abbrev term: pos -> suc -> type = [Inv][U] exp (hasleft (ininv Inv) U).

infoc: typ - -> leftform.
%abbrev spine: typ - -> suc -> type = [A-][U] exp (hasleft (infoc A-) U).

hyp: typ - -> type. %name hyp X x.
%block nprop : some {A-: typ -} block {x: hyp A-}.
%block aprop : some {Q+: atom +} block {z: value (c Q+)}.
%block pprop : some {A+: typ +} block {z: value A+}.
%worlds (atom+ | atom- | nprop) (hyp _).

%block gamma_suspnormal = (atom+ | atom- | nprop | aprop). % World for cut
%block gamma = (atom+ | atom- | nprop | pprop).            % World for identity

suspnormal: suc -> type.
snn: suspnormal (A- inv).
snp: suspnormal (A+ true).
sna: suspnormal ((c Q-) susp).

suspstable: suc -> type.
ss: stable U -> suspnormal U -> suspstable U.

suspnormalF: seqform -> type.
snr: suspnormalF (rfoc A+).
snl: suspnormalF (hasleft _ U) <- suspnormal U.```

#### Values

V ::= z | thunk N | inl V | inr V | ⟨⟩+ | ⟨V1,V2⟩+

The rule id+ corresponding to the proof term z comes for free from LF.

```dnR: term # (A- inv) -> value (dn A-).
\/R1: value A+ -> value (A+ \/ B+).
\/R2: value B+ -> value (A+ \/ B+).
top+R: value top+.
*R: value A+ -> value B+ -> value (A+ * B+).```

#### Terms

M ::= ret V | x • Sp | ⟨z⟩.N | x.N | abort | [N1, N2] | ⟨⟩.N | ×N | ⟨N⟩ | {N} | λN | ⟨⟩- | ⟨N1,N2⟩-

```focR: value A+ -> term # (A+ true).
focL: stable Suc -> hyp A- -> spine A- Suc -> term # Suc.
η+: (value (c Q+) -> term Inv Suc) -> term (c Q+ , Inv) Suc.
dnL: (hyp A- -> term Inv Suc) -> term (dn A- , Inv) Suc.
botL: term (bot , Inv) Suc.
\/L: term (A+ , Inv) Suc -> term (B+ , Inv) Suc -> term (A+ \/ B+ , Inv) Suc.
top+L: term Inv Suc -> term (top+ , Inv) Suc.
*L: term (A+ , B+ , Inv) Suc -> term (A+ * B+ , Inv) Suc.
η-: term # ((c Q-) susp) -> term # ((c Q-) inv).
upR: term # (A+ true) -> term # (up A+ inv).
=>R: term (A+ , #) (B- inv) -> term # (A+ => B- inv).
top-R: term # (top- inv).
/\R: term # (A- inv) -> term # (B- inv) -> term # (A- /\ B- inv).```

#### Spines

Sp ::= nil | pm N | V;Sp | π1;Sp | π2;Sp

```id-: spine A- (A- susp).
upL: stable Suc -> term (A+ , #) Suc -> spine (up A+) Suc.
=>L: value A+ -> spine B- Suc -> spine (A+ => B-) Suc.
/\L1: spine A- Suc -> spine (A- /\ B-) Suc.
/\L2: spine B- Suc -> spine (A- /\ B-) Suc.```

#### Negative focal substitution

Our encoding gives us positive focal substitution for free - it's very natural to describe suspended propsitions ⟨A+⟩ in the hypothetical context as variables of type rfoc A+, which is adequate and gives us the id+ rule for free. By chosing a more traditional way of describing negative suspended propositions (instead of the complicated encoding that gives us id- for free), we have forced ourselves to prove a theorem, negative focal substitution, that we could have avoided. The partial "NoNil" development avoids proving subst-.

```subst-: stable U
-> exp (hasleft L (A- susp))
-> spine A- U
-> exp (hasleft L U)
-> type.
%mode subst- +Pf +E +Sp -Sp'.

/: subst- Pf (focL _ X Sp0) Sp (focL Pf X Sp0')
<- subst- Pf Sp0 Sp Sp0'.
/: subst- Pf (η+ [z] N z) Sp (η+ [z] N' z)
<- {z} subst- Pf (N z) Sp (N' z).
/: subst- Pf (dnL [x] N x) Sp (dnL [x] N' x)
<- {x} subst- Pf (N x) Sp (N' x).
/: subst- Pf botL Sp botL.
/: subst- Pf (\/L N1 N2) Sp (\/L N1' N2')
<- subst- Pf N1 Sp N1'
<- subst- Pf N2 Sp N2'.
/: subst- Pf (top+L N) Sp (top+L N')
<- subst- Pf N Sp N'.
/: subst- Pf (*L N) Sp (*L N')
<- subst- Pf N Sp N'.

/: subst- Pf id- Sp Sp.
/: subst- Pf (upL _ N) Sp (upL Pf N')
<- subst- Pf N Sp N'.
/: subst- Pf (=>L V Sp0) Sp (=>L V Sp0')
<- subst- Pf Sp0 Sp Sp0'.
/: subst- Pf (/\L1 Sp0) Sp (/\L1 Sp0')
<- subst- Pf Sp0 Sp Sp0'.
/: subst- Pf (/\L2 Sp0) Sp (/\L2 Sp0')
<- subst- Pf Sp0 Sp Sp0'.

%worlds (gamma) (subst- _ _ _ _).
%total E (subst- _ E _ _).```

Cut admissibility has a couple of mutually inductive theorems, but no more than is absolutely necessary given the syntactic classes we're dealing with. Furthermore, the different theorems we use neatly sort out the informal division of cases that we are used to dealing with when proving cut admissibility theorems. The "principal" substitutions capture the principal cuts:

• V • Ni - positive cut formula, and
• N • Sp - negative cut formula.
```cut+: {A+} small
-> suspnormal U
-> value A+
-> term (A+ , Inv) U
-> term Inv U
-> type.

cut-: {A-} small
-> suspstable U
-> term # (A- inv)
-> spine A- U
-> term # U
-> type.

%mode cut+ +A +S +Pf +V +N -N'.
%mode cut- +A +S +Pf +N +Sp -N'.```

The "rightist" substitution [[N/x]]E captures all right commutative cuts. Each inductive call within this group decreases the size of the expression E that we are substituting into.

```rsubst:  {A-} big
-> suspnormalF Form
-> term # (A- inv)
-> (hyp A- -> exp Form)
-> exp Form
-> type.

%mode rsubst  +A +S +Pf +N +E -E'.```

The "leftist" substitution <<E>>N captures all left commutative cuts. Each inductive call within this group decreases the size of the expression E that we are substituting in, hence "leftist."

```lsubst: {A+} big
-> suspstable U
-> exp (hasleft L (A+ true))
-> term (A+ , #) U
-> exp (hasleft L U)
-> type.

%mode lsubst +A +S +Pf +E +N -E'.```

#### Principal substitution/cuts

(V • N) = N'

```/: cut+ (c Q+) S _ X (η+ [z] N z) (N X).

/: cut+ (dn A-) s Pf (dnR M) (dnL N) N'
<- rsubst A- (b s) (snl Pf) M N (N': term Inv U).

/: cut+ (A+ \/ B+) S Pf (\/R1 V) (\/L N1 N2) N'
<- cut+ A+ S Pf V N1 (N': term Inv U).

/: cut+ (A+ \/ B+) S Pf (\/R2 V) (\/L N1 N2) N'
<- cut+ B+ S Pf V N2 (N': term Inv U).

/: cut+ top+ S Pf top+R (top+L N) N.

/: cut+ (A+ * B+) S Pf (*R V1 V2) (*L N) N'
<- cut+ A+ S Pf V1 N (NB: term (B+ , Inv) U)
<- cut+ B+ S Pf V2 NB (N': term Inv U).```

(M • Sp) = N'

```/: cut- (c Q-) S Pf (η- N) id- N.

/: cut- (up A+) s Pf (upR N) (upL _ M) N'
<- lsubst A+ (b s) Pf N M N'.

/: cut- (A+ => B-) S (ss Pf1 Pf2) (=>R N) (=>L V Sp) N'
<- cut+ A+ S snn V N (NB: term # (B- inv))
<- cut- B- S (ss Pf1 Pf2) NB Sp (N': term # U).

/: cut- (A- /\ B-) S Pf (/\R N1 N2) (/\L1 Sp) N'
<- cut- A- S Pf N1 Sp (N': term # U).

/: cut- (A- /\ B-) S Pf (/\R N1 N2) (/\L2 Sp) N'
<- cut- B- S Pf N2 Sp (N': term # U).```

#### Rightist substitution (right commutative cuts)

[[M/x]]V = V'

```/: rsubst A- S snr M ([x] V) (V: value (c Q+)).

/: rsubst A- S snr M ([x] dnR (N x)) (dnR N')
<- rsubst A- S (snl snn) M ([x] N x) (N': term # (C- inv)).

/: rsubst A- S snr M ([x] \/R1 (V x)) (\/R1 V')
<- rsubst A- S snr M ([x] V x) (V': value C1+).

/: rsubst A- S snr M ([x] \/R2 (V x)) (\/R2 V')
<- rsubst A- S snr M ([x] V x) (V': value C2+).

/: rsubst A- S snr M ([x] top+R) top+R.

/: rsubst A- S snr M ([x] *R (V1 x) (V2 x)) (*R V1' V2')
<- rsubst A- S snr M ([x] V1 x) (V1': value C1+)
<- rsubst A- S snr M ([x] V2 x) (V2': value C2+).```

[[M/x]]N = N'

```% Entering principal substitution (cut-)
/: rsubst A- (b s) (snl Pf) M ([x] focR (V x)) (focR V')
<- rsubst A- (b s) snr M ([x] V x) V'.

/: rsubst A- (b s) (snl Pf) M ([x] focL Pf' x (Sp x)) N'
<- rsubst A- (b s) (snl Pf) M ([x] Sp x) (Sp': spine A- U)
<- cut- A- s (ss Pf' Pf) M Sp' (N': term # U).

/: rsubst A- S (snl Pf) M ([x] focL Pf' X' (Sp x)) (focL Pf' X' Sp')
<- rsubst A- S (snl Pf) M ([x] Sp x) (Sp': spine B- U).

/: rsubst A- S (snl Pf) M ([x] η+ [z] N x z) (η+ [z] N' z)
<- ({z: value (c Q+)} rsubst A- S (snl Pf) M ([x] N x z) (N' z: term Inv U)).

/: rsubst A- S (snl Pf) M ([x] dnL [x'] N x x') (dnL [x'] N' x')
<- ({x': hyp B-} rsubst A- S (snl Pf) M ([x] N x x') (N' x': term Inv U)).

/: rsubst A- S (snl Pf) M ([x] botL) botL.

/: rsubst A- S (snl Pf) M ([x] \/L (N1 x) (N2 x)) (\/L N1' N2')
<- rsubst A- S (snl Pf) M ([x] N1 x) (N1': term (B1 , Inv) U)
<- rsubst A- S (snl Pf) M ([x] N2 x) (N2': term (B2 , Inv) U).

/: rsubst A- S (snl Pf) M ([x] top+L (N x)) (top+L N')
<- rsubst A- S (snl Pf) M ([x] N x) (N': term Inv U).

/: rsubst A- S (snl Pf) M ([x] *L (N x)) (*L N')
<- rsubst A- S (snl Pf) M ([x] N x) (N': term (A+ , B+ , Inv) U).

/: rsubst A- S (snl snn) M ([x] η- (N x)) (η- N')
<- rsubst A- S (snl sna) M ([x] N x) (N': term # ((c Q-) susp)).

/: rsubst A- S (snl snn) M ([x] upR (N x)) (upR N')
<- rsubst A- S (snl snp) M ([x] N x) (N': term # (C+ true)).

/: rsubst A- S (snl snn) M ([x] =>R (N x)) (=>R N')
<- rsubst A- S (snl snn) M ([x] N x) (N': term (C1+ , #) (C2- inv)).

/: rsubst A- S (snl snn) M ([x] top-R) top-R.

/: rsubst A- S (snl snn) M ([x] /\R (N1 x) (N2 x)) (/\R N1' N2')
<- rsubst A- S (snl snn) M ([x] N1 x) (N1': term # (C1- inv))
<- rsubst A- S (snl snn) M ([x] N2 x) (N2': term # (C2- inv)).```

[[M/x]]Sp = Sp'

```/: rsubst A- S (snl sna) M ([x] id-) id-.

/: rsubst A- S (snl Pf) M ([x] upL Pf' (N x)) (upL Pf' N')
<- rsubst A- S (snl Pf) M ([x] N x) (N': term (B+ , #) U).

/: rsubst A- S (snl Pf) M ([x] =>L (V x) (Sp x)) (=>L V' Sp')
<- rsubst A- S snr M ([x] V x) (V': value B1+)
<- rsubst A- S (snl Pf) M ([x] Sp x) (Sp': spine B2- U).

/: rsubst A- S (snl Pf) M ([x] /\L1 (Sp x)) (/\L1 Sp')
<- rsubst A- S (snl Pf) M ([x] Sp x) (Sp': spine B1- U).

/: rsubst A- S (snl Pf) M ([x] /\L2 (Sp x)) (/\L2 Sp')
<- rsubst A- S (snl Pf) M ([x] Sp x) (Sp': spine B2- U).```

#### Leftist substitution (left commutative cuts)

<<M>>N = M'

```% Entering principal substitution (cut+)
/: lsubst A+ (b s) (ss Pf Pf') (focR V) N N'
<- cut+ A+ s Pf' V N N'.

/: lsubst A+ S (ss Pf Pf') (focL _ X Sp) N (focL Pf X Sp')
<- lsubst A+ S (ss Pf Pf') Sp N (Sp': spine B- U).

/: lsubst A+ S Pf (η+ [z] M z) N (η+ [z] M' z)
<- ({z: value (c Q+)} lsubst A+ S Pf (M z) N (M' z: term Inv U)).

/: lsubst A+ S (ss Pf Pf') (dnL [x'] M x') N (dnL [x'] M' x')
<- ({x': hyp B-} lsubst A+ S (ss Pf Pf') (M x') N (M' x': term Inv U)).

/: lsubst A+ S Pf botL N botL.

/: lsubst A+ S Pf (\/L M1 M2) N (\/L M1' M2')
<- lsubst A+ S Pf M1 N (M1': term (B1+ , Inv) U)
<- lsubst A+ S Pf M2 N (M2': term (B2+ , Inv) U).

/: lsubst A+ S Pf (top+L M) N (top+L M')
<- lsubst A+ S Pf M N (M': term Inv U).

/: lsubst A+ S Pf (*L M) N (*L M')
<- lsubst A+ S Pf M N (M': term (B1+ , B2+ , Inv) U).```

<<Sp>>N = Sp'

```/: lsubst A+ S (ss Pf Pf') (upL _ M) N (upL Pf M')
<- lsubst A+ S (ss Pf Pf') M N (M': term (B+ , #) U).

/: lsubst A+ S Pf (=>L V Sp) N (=>L V Sp')
<- lsubst A+ S Pf Sp N (Sp': spine B2- U).

/: lsubst A+ S Pf (/\L1 Sp) N (/\L1 Sp')
<- lsubst A+ S Pf Sp N (Sp': spine B1- U).

/: lsubst A+ S Pf (/\L2 Sp) N (/\L2 Sp')
<- lsubst A+ S Pf Sp N (Sp': spine B2- U).```

#### Wrap-up

```%worlds (gamma_suspnormal)
(cut+ _ _ _ _ _ _)
(cut- _ _ _ _ _ _)
(rsubst _ _ _ _ _ _ )
(lsubst _ _ _ _ _ _).```

With the exception of the "big/small" metric that allows the leftist and rightist substitutions to call principal substitutions at the same type, this is the usual induction metric for structrual cut elimination arguments.

```%total
{(A1 A2 A3 A4)
{(S1 S2 S3 S4)
[(V N- MR EL)
(N+ S ER NL)]}}
(cut+   A1 S1 _ V  N+ _)
(cut-   A2 S2 _ N- S  _)
(rsubst A3 S3 _ MR ER _)
(lsubst A4 S4 _ EL NL _).```

The following simpler induction metric also works, emphasizing that the "derivation" metric matters not at all in the principal cases, that the rightist substitutions are structurally inductive over the second given derivation (the "right" derivation) and that the leftist substitutions are structurally inductive over the first given derivation (the "left" derivation).

```%total
{(A1 A2 A3 A4)
{(S1 S2 S3 S4)
(S1 S2 ER EL)}}
(cut-   A1 S1 _ _  _  _)
(cut+   A2 S2 _ _  _  _)
(rsubst A3 S3 _ _  ER _)
(lsubst A4 S4 _ EL _  _).```

## Expansion

```expand+: {A+} (value A+ -> term Inv U) -> term (A+ , Inv) U -> type.
expand-: {A-} term # (A- susp) -> term # (A- inv) -> type.

%mode expand+ +A+ +N -Ni.
%mode expand- +A- +Sp -N.```

η(z.N) = N'

```/: expand+ (c Q+) ([z: value (c Q+)] N z) (η+ [z: value (c Q+)] N z).

/: expand+ (dn A-) ([z: value (dn A-)] N z) (dnL [x: hyp A-] N (dnR (N' x)))
<- ({x: hyp A-} expand- A- (focL sn x id-) (N' x: term # (A- inv))).

/: expand+ bot ([z: value bot] N z) botL.

/: expand+ (A+ \/ B+) ([z: value (A+ \/ B+)] N z) (\/L N1 N2)
<- expand+ A+ ([z1: value A+] N (\/R1 z1)) (N1: term (A+ , Inv) U)
<- expand+ B+ ([z2: value B+] N (\/R2 z2)) (N2: term (B+ , Inv) U).

/: expand+ top+ ([z: value top+] N z) (top+L (N top+R)).

/: expand+ (A+ * B+) ([z: value (A+ * B+)] N z) (*L N2)
<- ({z1: value A+}
expand+ B+ ([z2: value B+] N (*R z1 z2)) (N1 z1: term (B+ , Inv) U))
<- expand+ A+ ([z1: value A+] N1 z1) (N2: term (A+ , B+ , Inv) U).```

η(s.N) = N'

```/: expand- (c Q-) N (η- N).

/: expand- (up A+) N (upR N)
<- expand+ A+ ([z: value A+] focR z) (N': term (A+ , #) (A+ true))
<- subst- sp N (upL sp N') (N: term # (A+ true)).

/: expand- (A+ => B-) N (=>R N3)
<- ({z: value A+} subst- sn N (=>L z id-) (N1 z: term # (B- susp)))
<- ({z: value A+} expand- B- (N1 z) (N2 z: term # (B- inv)))
<- expand+ A+ N2 (N3: term (A+ , #) (B- inv)).

/: expand- top- N top-R.

/: expand- (A- /\ B-) N (/\R N1' N2')
<- subst- sn N (/\L1 id-) (N1: term # (A- susp))
<- expand- A- N1 (N1': term # (A- inv))
<- subst- sn N (/\L2 id-) (N2: term # (B- susp))
<- expand- B- N2 (N2': term # (B- inv)).

%worlds (gamma) (expand+ _ _ _) (expand- _ _ _).
%total (A+ A-) (expand+ A+ _ _) (expand- A- _ _).```

Identity is a corollary, though we'll only use it at the very end when we prove the identity principle for the unfocused sequent calculus:

```identity-: (hyp A- -> term # (A- inv)) -> type.
%mode +{A-} -{N: hyp A- -> term # (A- inv)} identity- N.

/: identity- N
<- ({x: hyp A-} expand- A- (focL sn x id-) (N x: term # (A- inv))).

%worlds (gamma) (identity- _).
%total [] (identity- _).

identity+: term (A+ , #) (A+ true) -> type.
%mode +{A+} -{N: term (A+ , #) (A+ true)} identity+ N.

/: identity+ N
<- expand+ A+ ([z: value A+] focR z) (N: term (A+ , #) (A+ true)).

%worlds (gamma) (identity+ _).
%total [] (identity+ _).```

The key lemmas for establishing the completeness of the focused sequent calculus are the "unfocused admissibility" lemmas, which establish that the normal rules of the sequent calculus are usable in the context of the focused calculus.

These lemmas are all provable by use of the cut and identity principles; while the proofs are hardly straightforward, they share a certain high-level structure.

#### Initial rules

```adm-initsusp-: (hyp (c Q) -> term # (c Q susp)) -> type.
%mode +{Q} -{N: hyp (c Q) -> term # (c Q susp)} adm-initsusp- N.

/: adm-initsusp- ([x: hyp (c Q)] focL sn x id-).

adm-init-: (hyp (c Q) -> term # (dn (c Q) true)) -> type.
%mode +{Q} -{N: hyp (c Q) -> term # (dn (c Q) true)} adm-init- N.

/: adm-init- ([x: hyp (c Q)] focR (dnR (η- (focL sn x id-)))).

adm-initsusp+: (value (c Q) -> term # (c Q true)) -> type.
%mode +{Q} -{N: value (c Q) -> term # (c Q true)} adm-initsusp+ N.

/: adm-initsusp+ ([z: value (c Q)] focR z).

adm-init+: (hyp (up (c Q)) -> term # (c Q true)) -> type.
%mode +{Q} -{N: hyp (up (c Q)) -> term # (c Q true)} adm-init+ N.

/: adm-init+ ([x: hyp (up (c Q))] focL sp x (upL sp (η+ [z] focR z))).

#### Disjunction

```adm-botL: stable U -> (hyp (up bot) -> term # U) -> type.

/: adm-botL Pf ([x: hyp (up bot)] focL Pf x (upL Pf botL)).

-> term # ((A+ \/ B+) true)
-> type.
%mode +{A+} +{B+} +{N1} -{N': term # ((A+ \/ B+) true)} adm-\/R1 N1 N'.

/: adm-\/R1 (N1: term # (A+ true)) N'
<- expand+ A+ ([z: value A+] focR (\/R1 z))
(NId1: term (A+ , #) ((A+ \/ B+) true))
<- lsubst A+ (b s) (ss sp snp) N1 NId1 (N': term # ((A+ \/ B+) true)).

-> term # (A+ \/ B+ true)
-> type.
%mode +{A+} +{B+} +{N2} -{N': term # ((A+ \/ B+) true)} adm-\/R2 N2 N'.

/: adm-\/R2 (N2: term # (B+ true)) N'
<- expand+ B+ ([z: value B+] focR (\/R2 z))
(NId2: term (B+ , #) ((A+ \/ B+) true))
<- lsubst B+ (b s) (ss sp snp) N2 NId2 (N': term # ((A+ \/ B+) true)).

-> (hyp (up A+) -> term # U)
-> (hyp (up B+) -> term # U)
-> (hyp (up (A+ \/ B+)) -> term # U)
-> type.
%mode adm-\/L +Pf +N1 +N2 -N'.

/: adm-\/L (ss Pf Pf') (N1: hyp (up A+) -> term # U)
(N2: hyp (up B+) -> term # U) ([x: hyp (up (A+ \/ B+))] focL Pf x (upL Pf N'))
<- expand+ A+ ([z1: value A+] focR (\/R1 (dnR (upR (focR z1)))))
(NId1: term (A+ , #) (dn (up A+) \/ dn (up B+) true))
<- expand+ B+ ([z2: value B+] focR (\/R2 (dnR (upR (focR z2)))))
(NId2: term (B+ , #) (dn (up A+) \/ dn (up B+) true))
<- lsubst (dn (up A+) \/ dn (up B+)) (b s) (ss Pf Pf')
(\/L NId1 NId2)
(\/L (dnL N1) (dnL N2))
(N': term (A+ \/ B+ , #) U).

%worlds (gamma_suspnormal) (adm-\/L _ _ _ _).
%total [] (adm-\/L _ _ _ _).```

#### Positive conjunction

```adm-top+R: term # (top+ true) -> type.

-> term # U
-> (hyp (up top+) -> term # U)
-> type.

/: adm-top+L Pf N1 ([x: hyp (up top+)] focL Pf x (upL Pf (top+L N1))).

%worlds (gamma_suspnormal) (adm-top+L _ _ _).
%total [] (adm-top+L _ _ _).

-> term # (B+ true)
-> term # (A+ * B+ true)
-> type.

/: adm-*R (N1: term # (A+ true)) (N2: term # (B+ true)) N'
<- ({v2: value B+}
expand+ A+ ([v1: value A+] (focR (*R v1 v2)))
(NIdB v2: term (A+ , #) (A+ * B+ true)))
<- ({x: hyp (up A+)}
expand+ B+ ([z2: value B+] focL sp x (upL sp (NIdB z2)))
(NId x: term (B+ , #) (A+ * B+ true)))
<- ({x: hyp (up A+)}
lsubst B+ (b s) (ss sp snp) N2 (NId x)
(NA x: term # (A+ * B+ true)))
<- rsubst (up A+) (b s) (snl snp) (upR N1) ([x: hyp (up A+)] NA x) N'.

%worlds (gamma_suspnormal) (adm-*R _ _ _).
%total [] (adm-*R _ _ _).

-> (hyp (up A+) -> hyp (up B+) -> term # U)
-> (hyp (up (A+ * B+)) -> term # U)
-> type.

/: adm-*L (ss Pf Pf') (N1: hyp (up A+) -> hyp (up B+) -> term # U)
([x: hyp (up (A+ * B+))] focL Pf x (upL Pf N'))
<- ({z1: value A+}
expand+ B+
([z2: value B+] focR (*R (dnR (upR (focR z1))) (dnR (upR (focR z2)))))
(NIdA z1: term (B+ , #) (dn (up A+) * dn (up B+) true)))
<- expand+ A+ ([z1: value A+] NIdA z1)
(NId: term (A+ , B+ , #) (dn (up A+) * dn (up B+) true))
<- lsubst (dn (up A+) * dn (up B+)) (b s) (ss Pf Pf') (*L NId)
(*L (dnL [x1: hyp (up A+)] dnL [x2: hyp (up B+)] N1 x1 x2))
(N': term (A+ * B+ , #) U).

%worlds (gamma_suspnormal) (adm-*L _ _ _).
%total [] (adm-*L _ _ _).```

#### Implication

```adm-=>R: (hyp (up A+) -> term # (dn B- true))
-> term # (dn (A+ => B-) true)
-> type.

/: adm-=>R (N1: hyp (up A+) -> term # (dn B- true)) (focR (dnR N'))
<- ({x: hyp (dn (up A+) => up (dn B-))}
{z: value A+}
expand- B-
(focL sn x (=>L (dnR (upR (focR z)))
(upL sn (dnL [x': hyp B-] focL sn x' id-))))
(NIdA x z: term # (B- inv)))
<- ({x: hyp (dn (up A+) => up (dn B-))}
expand+ A+ ([z: value A+] (NIdA x z))
(NId x: term (A+ , #) (B- inv)))
<- rsubst (dn (up A+) => up (dn B-)) (b s) (snl snn)
(=>R (dnL [x1: hyp (up A+)] upR (N1 x1)))
([x: hyp (dn (up A+) => up (dn B-))] =>R (NId x))
(N': term # (A+ => B- inv)).

-> term # (A+ true)
-> (hyp B- -> term # U)
-> (hyp (A+ => B-) -> term # U)
-> type.
%mode adm-=>L +Pf +N1 +N2 -N'.

/: adm-=>L (ss Pf Pf') (N1: term # (A+ true)) (N2: hyp B- -> term # U) N'
<- ({x: hyp (A+ => B-)}
{z: value A+}
expand- B- (focL sn x (=>L z id-))
(NIdB x z: term # (B- inv)))
<- ({x: hyp (A+ => B-)}
expand+ A+ ([z: value A+] focR (dnR (NIdB x z)))
(NId x: term (A+ , #) (dn B- true)))
<- ({x: hyp (A+ => B-)}
lsubst A+ (b s) (ss sp snp) N1 (NId x)
(NB x: term # (dn B- true)))
<- ({x: hyp (A+ => B-)}
lsubst (dn B-) (b s) (ss Pf Pf') (NB x) (dnL [x2: hyp B-] N2 x2)
(N' x: term # U)).

%worlds (gamma_suspnormal) (adm-=>L _ _ _ _).
%total [] (adm-=>L _ _ _ _).```

#### Negative conjunction

```adm-top-R: term # (dn top- true) -> type.

adm-/\R: term # (dn A- true)
-> term # (dn B- true)
-> term # (dn (A- /\ B-) true)
-> type.

/: adm-/\R N1 N2 (focR (dnR N'))
<- ({x: hyp (up (dn A-) /\ up (dn B-))}
expand- A- (focL sn x (/\L1 (upL sn (dnL [y] focL sn y id-))))
(NId1 x: term # (A- inv)))
<- ({x: hyp (up (dn A-) /\ up (dn B-))}
expand- B- (focL sn x (/\L2 (upL sn (dnL [y] focL sn y id-))))
(NId2 x: term # (B- inv)))
<- rsubst (up (dn A-) /\ up (dn B-)) (b s) (snl snn)
(/\R (upR N1) (upR N2))
([x: hyp (up (dn A-) /\ up (dn B-))] /\R (NId1 x) (NId2 x))
(N': term # (A- /\ B- inv)).

%worlds (gamma_suspnormal) (adm-/\R _ _ _).
%total [] (adm-/\R _ _ _).

-> (hyp A- -> term # U)
-> (hyp (A- /\ B-) -> term # U)
-> type.
%mode +{A-} +{B-} +{U} +{Pf} +{N1} -{N': hyp (A- /\ B-) -> term # U}

/: adm-/\L1 Pf (N1: hyp A- -> term # U) N'
<- ({x: hyp (A- /\ B-)}
expand- A- (focL sn x (/\L1 id-))
(NId x: term # (A- inv)))
<- ({x: hyp (A- /\ B-)}
rsubst A- (b s) (snl Pf) (NId x) N1
(N' x: term # U)).

%worlds (gamma_suspnormal) (adm-/\L1 _ _ _).
%total [] (adm-/\L1 _ _ _).

-> (hyp B- -> term # U)
-> (hyp (A- /\ B-) -> term # U)
-> type.
%mode +{A-} +{B-} +{U} +{Pf} +{N2} -{N': hyp (A- /\ B-) -> term # U}

/: adm-/\L2 Pf (N2: hyp B- -> term # U) N'
<- ({x: hyp (A- /\ B-)}
expand- B- (focL sn x (/\L2 id-))
(NId x: term # (B- inv)))
<- ({x: hyp (A- /\ B-)}
rsubst B- (b s) (snl Pf) (NId x) N2
(N' x: term # U)).

%worlds (gamma_suspnormal) (adm-/\L2 _ _ _).
%total [] (adm-/\L2 _ _ _).```

## Unfocused system

#### Syntax

```prop: type. %name prop P.
a: atom P -> prop.
ff: prop.
or: prop -> prop -> prop.
tt: prop.
and: prop -> prop -> prop.
imp: prop -> prop -> prop.

props: type. %name props Psi.
##: props.
;: prop -> props -> props. %infix right 3 ;.```

#### Erasure

The judgment t P A relates unpolarized propositions P and polarized propositions A. The judgment can be effectively run as an erasure function from polarized to unpolarized propositions.

```t: typ P -> prop -> type. %name t Trans.

tQ: t (c Q) (a Q).

tup: t A+ P -> t (up A+) P.
tbot: t bot ff.
t\/: t A+ P1 -> t B+ P2 -> t (A+ \/ B+) (or P1 P2).
ttop+: t top+ tt.
t*: t A+ P1 -> t B+ P2 -> t (A+ * B+) (and P1 P2).

tdn: t A- P -> t (dn A-) P.
t=>: t A+ P1 -> t B- P2 -> t (A+ => B-) (imp P1 P2).
ttop-: t top- tt.
t/\: t A- P1 -> t B- P2 -> t (A- /\ B-) (and P1 P2).

%mode t +A -P.
%worlds (atom+ | atom-) (t _ _).
%total A (t A _).

tInv: pos -> props -> type. %name tInv TransInv.
t#: tInv # ##.
t,: t A+ P -> tInv Inv Psi -> tInv (A+ , Inv) (P ; Psi).

%mode tInv +A -P.
%worlds (gamma) (tInv _ _).
%total Inv (tInv Inv _).

tU: suc -> prop -> type. %name tU TransU.
tp: tU (A+ true) P <- t A+ P.
tn: tU (A- inv) P <- t A- P.
ta: tU ((c Q-) susp) (a Q-).

tseq: seqform -> props -> prop -> type.
tV: tseq (rfoc A+) ## P <- t A+ P.
tN: tseq (hasleft (ininv Inv) U) Psi Q <- tU U Q <- tInv Inv Psi.
tS: tseq (hasleft (infoc A-) U) (P ; ##) Q <- tU U Q <- t A- P.```

#### Shift removal

There may be a more elegant way to do this, but the last missing piece of our unfocused admissibility lemma - the last thing we need to know about the polarized calculus - is that if we need to prove (or use) a deeply-shifted proposition, then it suffices to prove (or use) a non-deeply-shifted proposition that erases to the same thing.

```not-doubleshifted: typ Pol -> type.
ndQ:   not-doubleshifted (c Q).
ndQ+:  not-doubleshifted (dn (c Q)).
ndQ-:  not-doubleshifted (up (c Q)).
ndbot+:  not-doubleshifted bot.
ndbot-:  not-doubleshifted (up bot).
nd\/+:  not-doubleshifted (A+ \/ B+).
nd\/-:  not-doubleshifted (up (A+ \/ B+)).
ndtop++: not-doubleshifted top+.
ndtop+-: not-doubleshifted (up top+).
nd*+: not-doubleshifted (A+ * B+).
nd*-: not-doubleshifted (up (A+ * B+)).
nd=>+:  not-doubleshifted (dn (A+ => B-)).
nd=>-:  not-doubleshifted (A+ => B-).
ndtop-+: not-doubleshifted (dn top-).
ndtop--: not-doubleshifted top-.
nd/\+: not-doubleshifted (dn (A- /\ B-)).
nd/\-: not-doubleshifted (A- /\ B-).

rshifty: t A P
-> t A' P
-> not-doubleshifted A'
-> (term # (A' true)
-> term # (A true))
-> type.

%mode rshifty +T -T' -ND -N.

/: rshifty (tdn (tup T)) T' ND ([n] (focR (dnR (upR (N n)))))
<- rshifty T T' ND N.
/: rshifty tQ tQ ndQ ([n] n).
/: rshifty tbot tbot ndbot+ ([n] n).
/: rshifty (t\/ T1 T2) (t\/ T1 T2) nd\/+ ([n] n).
/: rshifty ttop+ ttop+ ndtop++ ([n] n).
/: rshifty (t* T1 T2) (t* T1 T2) nd*+ ([n] n).
/: rshifty (tdn tQ) (tdn tQ) ndQ+ ([n] n).
/: rshifty (tdn (t=> T1 T2)) (tdn (t=> T1 T2)) nd=>+ ([n] n).
/: rshifty (tdn ttop-) (tdn ttop-) ndtop-+ ([n] n).
/: rshifty (tdn (t/\ T1 T2)) (tdn (t/\ T1 T2)) nd/\+ ([n] n).

%worlds (gamma_suspnormal) (rshifty _ _ _ _).
%total T (rshifty T _ _ _).

lshifty: t A P
-> t A' P
-> not-doubleshifted A'
-> ({U} stable U
-> (hyp A' -> term # U)
-> (hyp A -> term # U))
-> type.
%mode lshifty +T -T' -ND -N.

/: lshifty (tup (tdn T)) T' ND ([u][pf][n][x] focL pf x (upL pf (dnL (N u pf n))))
<- lshifty T T' ND N.
/: lshifty (tup tQ) (tup tQ) ndQ- ([u][pf][n] n).
/: lshifty (tup tbot) (tup tbot) ndbot- ([u][pf][n] n).
/: lshifty (tup (t\/ T1 T2)) (tup (t\/ T1 T2)) nd\/- ([u][pf][n] n).
/: lshifty (tup ttop+) (tup ttop+) ndtop+- ([u][pf][n] n).
/: lshifty (tup (t* T1 T2)) (tup (t* T1 T2)) nd*- ([u][pf][n] n).
/: lshifty tQ tQ ndQ ([u][pf][n] n).
/: lshifty (t=> T1 T2) (t=> T1 T2) nd=>- ([u][pf][n] n).
/: lshifty ttop- ttop- ndtop-- ([u][pf][n] n).
/: lshifty (t/\ T1 T2) (t/\ T1 T2) nd/\- ([u][pf][n] n).

%worlds (gamma_suspnormal) (lshifty _ _ _ _).
%total T (lshifty T _ _ _).```

#### Sequent rules

```left: prop -> type. %name left H.
right: prop -> type. %name right D.
right': props -> prop -> type. %name right' D.
%block h: some {P} block {h: left P}.

init: left (a Q) -> right (a Q).

ffL: left ff -> right P.

orR1: right P1 -> right (or P1 P2).

orR2: right P2 -> right (or P1 P2).

orL: (left P1 -> right Q)
-> (left P2 -> right Q)
-> (left (or P1 P2) -> right Q).

ttR: right tt.

andR: right P1 -> right P2 -> right (and P1 P2).

andL1: (left P1 -> right Q)
-> (left (and P1 P2) -> right Q).

andL2: (left P2 -> right Q)
-> (left (and P1 P2) -> right Q).

impR: (left P1 -> right P2)
-> right (imp P1 P2).

impL: right P1
-> (left P2 -> right Q)
-> (left (imp P1 P2) -> right Q).

nil: right P -> right' ## P.

cons: (left P -> right' Psi Q) -> right' (P ; Psi) Q.```

Syntactic identity on derivations is used for completeness -- it keeps the derivation size the same when we do case analysis.

```id: right P -> right P -> type.
refl: id D D.```

## De-focalization (soundness)

Soundness is established in a context where each polarized hypothesis is mapped to its erasure.

```soundhyp: hyp A- -> t A- P -> left P -> type.
%block soundhyps: some {A-}{P}{T: t A- P}
block {x: hyp A-}{h: left P}{_: soundhyp x T h}.

soundsusp: value (c Q+) -> left (a Q+) -> type.
%block soundsusps: some {Q+}
block {z: value (c Q+)}{h: left (a Q+)}{_: soundsusp z h}.

%block soundctx = (atom+ | atom- | soundhyps | soundsusps).

%mode +{A-} -{P} +{X: hyp A-} -{T: t A- P} -{H: left P} soundhyp X T H.
%worlds (soundctx) (soundhyp _ _ _).
%total [] (soundhyp _ _ _).

%mode +{Q+} +{Z: value (c Q+)} -{H: left (a Q+)} soundsusp Z H.
%worlds (soundctx) (soundsusp _ _).
%total [] (soundsusp _ _).

sound: exp Form -> tseq Form Psi P -> right' Psi P -> type.
%mode sound +E +T -D.

/: sound (Z: value (c Q+)) (tV tQ) (nil (init H))
<- soundsusp Z H.

/: sound (dnR N) (tV (tdn T)) (nil D)
<- sound N (tN t# (tn T)) (nil D).

/: sound (\/R1 V) (tV (t\/ T1 _)) (nil (orR1 D))
<- sound V (tV T1) (nil D).

/: sound (\/R2 V) (tV (t\/ _ T2)) (nil (orR2 D))
<- sound V (tV T2) (nil D).

/: sound top+R (tV ttop+) (nil ttR).

/: sound (*R V1 V2) (tV (t* T1 T2)) (nil (andR D1 D2))
<- sound V1 (tV T1) (nil D1)
<- sound V2 (tV T2) (nil D2).

/: sound (focR V) (tN t# (tp T)) D
<- sound V (tV T) D.

/: sound (focL _ X Sp) (tN t# (TCQ: tU U Q)) (nil (D H))
<- soundhyp X (TAP: t A- P) (H: left P)
<- sound Sp (tS TAP TCQ) (cons [x: left P] (nil (D x: right Q))).

/: sound (η+ [z: value (c Q+)] N z) (tN (t, tQ TInv) TCQ) (cons D)
<- ({z: value (c Q+)}{h: left (a Q+)}
soundsusp z h ->
sound (N z) (tN TInv TCQ) (D h: right' Psi Q)).

/: sound (dnL [x: hyp A-] N x) (tN (t, (tdn T) TInv) TCQ) (cons D)
<- ({x: hyp A-}{h: left P}
soundhyp x T h ->
sound (N x) (tN TInv TCQ) (D h: right' Psi Q)).

sound-ffL: {Psi} left ff
-> right' Psi Q -> type.
/: sound-ffL _ H (nil (ffL H)).
/: sound-ffL _ H (cons D)
<- {h} sound-ffL _ H (D h).
%mode +{Psi} +{Q} +{H: left ff} -{D: right' Psi Q} sound-ffL Psi H D.
%worlds (atom+ | atom- | h) (sound-ffL _ _ _).
%total Psi (sound-ffL Psi _ _).

/: sound botL (tN TInv TCQ) (cons D)
<- ({h: left ff} sound-ffL _ h (D h)).

sound-orL: {Psi} left (or P1 P2)
-> (left P1 -> right' Psi Q)
-> (left P2 -> right' Psi Q)
-> right' Psi Q -> type.
/: sound-orL _ H ([h1] nil (D1 h1)) ([h2] nil (D2 h2)) (nil (orL D1 D2 H)).
/: sound-orL _ H ([h1] cons (D1 h1)) ([h2] cons (D2 h2)) (cons D)
<- {h} sound-orL _ H ([h1] D1 h1 h) ([h2] D2 h2 h) (D h).
%mode sound-orL +Psi +H +D1 +D2 -D.
%worlds (atom+ | atom- | h) (sound-orL _ _ _ _ _).
%total Psi (sound-orL Psi _ _ _ _).

/: sound (\/L N1 N2) (tN (t, (t\/ T1 T2) TInv) TCQ) (cons D)
<- sound N1 (tN (t, T1 TInv) TCQ) (cons (D1: left P1 -> right' Psi Q))
<- sound N2 (tN (t, T2 TInv) TCQ) (cons (D2: left P2 -> right' Psi Q))
<- ({h: left (or P1 P2)} sound-orL _ h D1 D2 (D h)).

/: sound (top+L N) (tN (t, ttop+ TInv) TCQ) (cons [h: left tt] D)
<- sound N (tN TInv TCQ) (D: right' Psi Q).

sound-andL: {Psi} left (and P1 P2)
-> (left P1 -> left P2 -> right' Psi Q)
-> right' Psi Q -> type.
/: sound-andL _ H ([h1] [h2] nil (D1 h1 h2))
(nil (andL1 ([h1] andL2 ([h2] D1 h1 h2) H) H)).
/: sound-andL _ H ([h1] [h2] cons (D1 h1 h2)) (cons D)
<- {h} sound-andL _ H ([h1] [h2] D1 h1 h2 h) (D h).
%mode sound-andL +Psi +H +D1 -D.
%worlds (atom+ | atom- | h) (sound-andL _ _ _ _).
%total Psi (sound-andL Psi _ _ _).

/: sound (*L N) (tN (t, (t* T1 T2) TInv) TCQ) (cons D)
<- sound N (tN (t, T1 (t, T2 TInv)) TCQ) (cons [h1] cons [h2] D1 h1 h2)
<- ({h: left (and P1 P2)} sound-andL _ h D1 (D h: right' Psi Q)).

/: sound (η- N) (tN t# (tn tQ)) (nil D)
<- sound N (tN t# ta) (nil D).

/: sound (upR N) (tN t# (tn (tup T))) (nil D)
<- sound N (tN t# (tp T)) (nil D).

/: sound (=>R N) (tN t# (tn (t=> T1 T2))) (nil (impR D))
<- sound N (tN (t, T1 t#) (tn T2)) (cons [h: left P1] (nil (D h: right P2))).

/: sound top-R (tN t# (tn ttop-)) (nil ttR).

/: sound (/\R N1 N2) (tN t# (tn (t/\ T1 T2))) (nil (andR D1 D2))
<- sound N1 (tN t# (tn T1)) (nil D1)
<- sound N2 (tN t# (tn T2)) (nil D2).

/: sound id- (tS tQ ta) (cons [h] nil (init h)).

/: sound (upL _ N) (tS (tup T1) TCQ) D
<- sound N (tN (t, T1 t#) TCQ) (D: right' (P ; ##) Q).

/: sound (=>L V Sp) (tS (t=> T1 T2) TCQ) (cons [h] nil (impL D1 D2 h))
<- sound V (tV T1) (nil (D1: right P1))
<- sound Sp (tS T2 TCQ) (cons [h: left P2] nil (D2 h: right Q)).

/: sound (/\L1 Sp) (tS (t/\ T1 T2) TCQ)
(cons [h: left (and P1 P2)] nil (andL1 D h))
<- sound Sp (tS T1 TCQ) (cons [h1: left P1] nil (D h1: right Q)).

/: sound (/\L2 Sp) (tS (t/\ T1 T2) TCQ)
(cons [h: left (and P1 P2)] nil (andL2 D h))
<- sound Sp (tS T2 TCQ) (cons [h2: left P2] nil (D h2: right Q)).

%worlds (soundctx) (sound _ _ _).
%total (E) (sound E _ _).```

## Focalization (completeness)

Completeness is established in a context where each erased hypothesis is mapped to some polarization. This is the almost same, type-wise, as the context for soundness, but the computational interpretation runs the opposite way 'round.

```completehyp_res: typ Pol -> type.
cn: hyp A- -> completehyp_res (A-).
ca: value (c Q+) -> completehyp_res (c Q+).

completehyp: left P -> t A P -> completehyp_res A -> type.
%block completehypn: some {A-: typ -}{P}{T: t A- P}
block {x: hyp A-}{h: left P}{_: completehyp h T (cn x)}.
%block completehypa: some {Q+: atom +}{P}{T: t (c Q+) P}
block {z: value (c Q+)}{h: left P}{_: completehyp h T (ca z)}.

%block completectx = (gamma_suspnormal | completehypn | completehypa).

transnormal: tU U P -> suspnormal U -> type.
%mode transnormal +T -Pf.

/: transnormal (tp _) snp.
/: transnormal (tn _) snn.
/: transnormal ta sna.

%worlds (atom+ | atom-) (transnormal _ _).
%total [] (transnormal _ _).

%mode completehyp +H -T -X.
%worlds (completectx) (completehyp _ _ _).
%total [] (completehyp _ _ _).

complete: stable U -> right P -> tU U P -> term # U -> type.
%mode complete +S +D +T -N.```

#### Initial rules

```comp-init-susp:
not-doubleshifted A'
-> t A' (a Q)
-> (hyp A' -> term # (c Q susp))
-> type.

/: comp-init-susp _ tQ M

%mode comp-init-susp +ND +TH' -E.
%worlds (completectx) (comp-init-susp _ _ _).
%total [] (comp-init-susp _ _ _).

/: complete Pf (init H) ta (NS _ sn M X)
<- completehyp H (TH: t A (a Q)) (cn (X: hyp A))
<- lshifty TH (TH': t A' (a Q))
(ND: not-doubleshifted A')
(NS: {U} stable U -> (hyp A' -> term # U) -> (hyp A -> term # U))
<- comp-init-susp ND TH' M.

comp-init-case:
not-doubleshifted Aleft'
-> t Aleft' (a Q)
-> not-doubleshifted Aright'
-> t Aright' (a Q)
-> (hyp Aleft' -> term # (Aright' true))
-> type.
%mode comp-init-case +NDH +TH' +ND +T' -M.

/: comp-init-case ndQ tQ ndQ+ (tdn tQ) M <- adm-init- M.

/: comp-init-case ndQ- (tup tQ) ndQ tQ M <- adm-init+ M.

%worlds (completectx) (comp-init-case _ _ _ _ _).
%total [] (comp-init-case _ _ _ _ _).

comp-init:
t Aleft (a Q)
-> completehyp_res Aleft
-> not-doubleshifted Aright'
-> t Aright' (a Q)
-> term # (Aright' true)
-> type.

/: comp-init tQ (ca Z) ndQ tQ (M Z)

/: comp-init TH (cn X) ND T' (NS _ sp M X)
<- lshifty TH (TH': t Aleft' (a Q))
(NDH: not-doubleshifted Aleft')
(NS: {U} stable U -> (hyp Aleft' -> term # U)
-> (hyp Aleft -> term # U))
<- comp-init-case NDH TH' ND T' M.

%mode comp-init +TH +HypRes +NDright +T' -M.
%worlds (completectx) (comp-init _ _ _ _ _).
%total [] (comp-init _ _ _ _ _).

/: complete Pf (init H) (tp (T: t Aright (a Q))) (NSright M)
<- rshifty T (T': t Aright' (a Q))
(NDright: not-doubleshifted Aright')
(NSright: term # (Aright' true) -> term # (Aright true))
<- completehyp H (TH: t Aleft (a Q)) (HypRes: completehyp_res Aleft)
<- comp-init TH HypRes NDright T' M.```

#### Disjunction

```comp-ffL: stable U
-> not-doubleshifted A'
-> t A' ff
-> (hyp A' -> term # U) -> type.
/: comp-ffL Pf ndbot- (tup tbot) M <- adm-botL Pf M.
%mode comp-ffL +Pf +ND +T -M.
%worlds (completectx) (comp-ffL _ _ _ _).
%total [] (comp-ffL _ _ _ _).

/: complete Pf (ffL H) T (NS _ Pf M X)
<- completehyp H (TH: t A ff) (cn (X: hyp A))
<- lshifty TH (TH': t A' ff)
(ND: not-doubleshifted A')
(NS: {U} stable U -> (hyp A' -> term # U) -> (hyp A -> term # U))
<- comp-ffL Pf ND TH' M.

comp-orR1: {D: right (or P1 P2)} id D (orR1 D1)
-> not-doubleshifted A'
-> t A' (or P1 P2)
-> term # (A' true)
-> type.
%mode comp-orR1 +D +Id +ND +T -M.
/: comp-orR1 (orR1 D1) refl nd\/+ (t\/ (T1: t A+ P1) (T2: t B+ P2)) M
<- complete sp D1 (tp T1) (N1: term # (A+ true))
<- adm-\/R1 N1 (M: term # (A+ \/ B+ true)).

/: complete Pf (orR1 D1) (tp T) (NS M)
<- rshifty T (T': t A' (or P1 P2))
(ND: not-doubleshifted A')
(NS: term # (A' true) -> term # (A true))
<- comp-orR1 (orR1 D1) refl ND T' M.

comp-orR2: {D: right (or P1 P2)} id D (orR2 D2)
-> not-doubleshifted A'
-> t A' (or P1 P2)
-> term # (A' true)
-> type.
%mode comp-orR2 +D +Id +ND +T' -M.
/: comp-orR2 (orR2 D2) refl nd\/+ (t\/ (T1: t A+ P1) (T2: t B+ P2)) M
<- complete sp D2 (tp T2) (N2: term # (B+ true))
<- adm-\/R2 N2 (M: term # (A+ \/ B+ true)).

/: complete Pf (orR2 D2) (tp T) (NS M)
<- rshifty T (T': t A' (or P1 P2))
(ND: not-doubleshifted A')
(NS: term # (A' true) -> term # (A true))
<- comp-orR2 (orR2 D2) refl ND T' M.

comp-orL: stable U
-> {D: right Q} id D (orL D1 D2 (H: left (or P1 P2)))
-> not-doubleshifted A'
-> t A' (or P1 P2)
-> tU U Q
-> (hyp A' -> term # U)
-> type.
%mode comp-orL +Pf +D +Id +ND +TH +T -M.
/: comp-orL Pf (orL D1 D2 H) refl nd\/- (tup (t\/ T1 T2)) T M
<- ({x1: hyp (up B1+)} {h1: left P1}
completehyp h1 (tup T1) (cn x1) ->
complete Pf (D1 h1) T (N1 x1: term # U))
<- ({x2: hyp (up B2+)} {h2: left P2}
completehyp h2 (tup T2) (cn x2) ->
complete Pf (D2 h2) T (N2 x2: term # U))
<- transnormal T Pf'
<- adm-\/L (ss Pf Pf') N1 N2 (M: hyp (up (B1+ \/ B2+)) -> term # U).

/: complete Pf (orL D1 D2 H) (T: tU U Q) (NS _ Pf M X)
<- completehyp H (TH: t A (or P1 P2)) (cn (X: hyp A))
<- lshifty TH TH' ND NS
<- comp-orL Pf (orL D1 D2 H) refl ND TH' T M.```

#### Conjunction

```comp-ttR: {D: right tt} id D ttR
-> not-doubleshifted A'
-> t A' tt
-> term # (A' true)
-> type.
/: comp-ttR ttR refl ndtop++ ttop+ M
/: comp-ttR ttR refl ndtop-+ (tdn ttop-) M
%mode comp-ttR +D +Id +ND +T' -M.
%worlds (completectx) (comp-ttR _ _ _ _ _).
%total [] (comp-ttR _ _ _ _ _).

/: complete Pf ttR (tp T) (NS M)
<- rshifty T (T': t A' tt)
(ND: not-doubleshifted A')
(NS: term # (A' true) -> term # (A true))
<- comp-ttR ttR refl ND T' M.

comp-andR: {D: right (and P1 P2)} id D (andR D1 D2)
-> not-doubleshifted A'
-> t A' (and P1 P2)
-> term # (A' true)
-> type.
%mode comp-andR +D +Id +ND +T' -M.
/: comp-andR (andR D1 D2) refl nd*+ (t* (T1: t A+ P1) (T2: t B+ P2)) M
<- complete sp D1 (tp T1) (N1: term # (A+ true))
<- complete sp D2 (tp T2) (N2: term # (B+ true))
/: comp-andR (andR D1 D2) refl nd/\+ (tdn (t/\ (T1: t A- P1) (T2: t B- P2))) M
<- complete sp D1 (tp (tdn T1)) (N1: term # (dn A- true))
<- complete sp D2 (tp (tdn T2)) (N2: term # (dn B- true))

/: complete Pf (andR D1 D2) (tp T) (NS M)
<- rshifty T (T': t A' (and P1 P2))
(ND: not-doubleshifted A')
(NS: term # (A' true) -> term # (A true))
<- comp-andR (andR D1 D2) refl ND T' M.

comp-andL1: stable U
-> {D: right Q} id D (andL1 D1 (H: left (and P1 P2)))
-> not-doubleshifted A'
-> t A' (and P1 P2)
-> tU U Q
-> (hyp A' -> term # U)
-> type.
%mode comp-andL1 +Pf +D +Id +ND +TH' +T -M.
/: comp-andL1 Pf (andL1 D1 H) refl nd*-
(tup (t* (T1: t A+ P1) (T2: t B+ P2))) T M
<- ({x: hyp (up A+)} {h: left P1}
completehyp h (tup T1) (cn x) ->
complete Pf (D1 h) T (N1 x: term # U))
<- transnormal T Pf'
<- adm-*L (ss Pf Pf') ([x][y] N1 x) M.
/: comp-andL1 Pf (andL1 D1 H) refl nd/\- (t/\ (T1: t A- P1) (T2: t B- P2)) T M
<- ({x: hyp A-} {h: left P1}
completehyp h T1 (cn x) ->
complete Pf (D1 h) T (N1 x: term # U))
<- transnormal T Pf'

/: complete Pf (andL1 D1 H) (T: tU U Q) (NS _ Pf M X)
<- completehyp H (TH: t A (and P1 P2)) (cn (X: hyp A))
<- lshifty TH TH' ND NS
<- comp-andL1 Pf (andL1 D1 H) refl ND TH' T M.

comp-andL2: stable U
-> {D: right Q} id D (andL2 D1 (H: left (and P1 P2)))
-> not-doubleshifted A'
-> t A' (and P1 P2)
-> tU U Q
-> (hyp A' -> term # U)
-> type.
%mode comp-andL2 +Pf +D +Id +ND +TH' +T -M.
/: comp-andL2 Pf (andL2 D2 H) refl nd*-
(tup (t* (T1: t A+ P1) (T2: t B+ P2))) T M
<- ({x: hyp (up B+)} {h: left P2}
completehyp h (tup T2) (cn x) ->
complete Pf (D2 h) T (N2 x: term # U))
<- transnormal T Pf'
<- adm-*L (ss Pf Pf') ([x][y] N2 y) M.
/: comp-andL2 Pf (andL2 D2 H) refl nd/\- (t/\ (T1: t A- P1) (T2: t B- P2)) T M
<- ({x: hyp B-} {h: left P2}
completehyp h T2 (cn x) ->
complete Pf (D2 h) T (N2 x: term # U))
<- transnormal T Pf'

/: complete Pf (andL2 D2 H) (T: tU U Q) (NS _ Pf M X)
<- completehyp H (TH: t A (and P1 P2)) (cn (X: hyp A))
<- lshifty TH TH' ND NS
<- comp-andL2 Pf (andL2 D2 H) refl ND TH' T M.```

#### Implication

```comp-impR: {D: right (imp P1 P2)} id D (impR D1)
-> not-doubleshifted A'
-> t A' (imp P1 P2)
-> term # (A' true)
-> type.
%mode comp-impR +D +Id +ND +T' -M.
/: comp-impR (impR D1) refl nd=>+ (tdn (t=> (T1: t A+ P1) (T2: t B- P2))) M
<- ({x: hyp (up A+)} {h: left P1}
completehyp h (tup T1) (cn x) ->
complete sp (D1 h) (tp (tdn T2)) (N1 x))

/: complete Pf (impR D1) (tp T) (NS M)
<- rshifty T (T': t A' (imp P1 P2))
(ND: not-doubleshifted A')
(NS: term # (A' true) -> term # (A true))
<- comp-impR (impR D1) refl ND T' M.

comp-impL: stable U
-> {D: right Q} id D (impL D1 D2 (H: left (imp P1 P2)))
-> not-doubleshifted A'
-> t A' (imp P1 P2)
-> tU U Q
-> (hyp A' -> term # U)
-> type.
%mode comp-impL +Pf +D +Id +ND +TH' +T -M.
/: comp-impL Pf (impL D1 D2 _) refl nd=>- (t=> (T1: t A+ P1) (T2: t B- P2)) T M
<- complete sp D1 (tp T1) (N1: term # (A+ true))
<- ({x: hyp B-} {h: left P2}
completehyp h T2 (cn x) ->
complete Pf (D2 h) T (N2 x))
<- transnormal T Pf'
<- adm-=>L (ss Pf Pf') N1 N2 M.

/: complete Pf (impL D1 D2 H) T (NS _ Pf M X)
<- completehyp H (TH: t A (imp P1 P2)) (cn (X: hyp A))
<- lshifty TH TH' ND NS
<- comp-impL Pf (impL D1 D2 H) refl ND TH' T M.

%worlds (completectx)
(comp-orR1 _ _ _ _ _)
(comp-orR2 _ _ _ _ _)
(comp-orL _ _ _ _ _ _ _)
(comp-andR _ _ _ _ _)
(comp-andL1 _ _ _ _ _ _ _)
(comp-andL2 _ _ _ _ _ _ _)
(comp-impR _ _ _ _ _)
(comp-impL _ _ _ _ _ _ _)
(complete _ _ _ _).
%total (D D1 D2 D3 D4 D5 D6 D7 D8)
(comp-orR1 D1 _ _ _ _)
(comp-orR2 D2 _ _ _ _)
(comp-orL _ D3 _ _ _ _ _)
(comp-andR D4 _ _ _ _)
(comp-andL1 _ D5 _ _ _ _ _)
(comp-andL2 _ D6 _ _ _ _ _)
(comp-impR D7 _ _ _ _)
(comp-impL _ D8 _ _ _ _ _)
(complete _ D _ _).```

## Inheriting the focused calculus's metatheory

We need the existance of some polarization strategy; we intentionally pick a middling, undistinghished sort of translation that translates everything as a negative proposition. It will work great on hereditary Harrop formulas and not so good if you have lots of disjunction and positive propositions; the only interesting thing about it is that it's results are reminiscent of Howe's semi-focused lax logic..

```polarize: {P} t (A-: typ -) P -> type.
%mode polarize +P -T.

/: polarize (a Q) tQ.
/: polarize (a Q) (tup tQ).
/: polarize ff (tup tbot).
/: polarize (or P1 P2) (tup (t\/ (tdn T1) (tdn T2)))
<- polarize P1 T1
<- polarize P2 T2.
/: polarize tt ttop-.
/: polarize (and P1 P2) (t/\ T1 T2)
<- polarize P1 T1
<- polarize P2 T2.
/: polarize (imp P1 P2) (t=> (tdn T1) T2)
<- polarize P1 T1
<- polarize P2 T2.

%worlds (atom+ | atom-) (polarize _ _).
%total P (polarize P _).

%block translate: some {A}{P}{TH: t A P}
block {x: hyp A}{h: left P}{_: soundhyp x TH h}{_: completehyp h TH (cn x)}.

unfocused-cut: right P -> (left P -> right Q) -> right Q -> type.
%mode unfocused-cut +D +E -F.

/: unfocused-cut (D: right P) (E: left P -> right Q) F
<- polarize P (TP: t A- P)
<- complete sp D (tp (tdn TP)) (M: term # ((dn A-) true))
<- polarize Q (TQ: t C- Q)
<- ({x: hyp A-}{h: left P}
completehyp h TP (cn x) ->
complete sp (E h) (tp (tdn TQ)) (N x: term # (dn C- true)))
<- lsubst _ (b s) (ss sp snp) M (dnL N) N'
<- sound N' (tN t# (tp (tdn TQ))) (nil (F: right Q)).

%worlds (translate) (unfocused-cut _ _ _).
%total [] (unfocused-cut _ _ _).

unfocused-identity: (left P -> right P) -> type.
%mode +{P} -{D: left P -> right P} unfocused-identity D.

/: unfocused-identity D
<- polarize P (TP: t A- P)
<- identity- (N: hyp A- -> term # (A- inv))
<- ({x: hyp A-}{h: left P}
soundhyp x TP h ->
sound (N x) (tN t# (tn TP)) (nil (D h: right P))).

%worlds (translate) (unfocused-identity _).
%total [] (unfocused-identity _).```

## Running the theorems

Here are two unfocused derivations of (p /\ q) => (r /\ s) => (p /\ t).

```d1: {P}{p: atom P}{q: atom P}{r: atom P}{s: atom P}
right (imp (and (a p) (a q))
(imp (and (a r) (a s))
(and (a p) (a r))))
= [P][p][q][r][s]
impR [h1: left (and (a p) (a q))]
impR [h2: left (and (a r) (a s))]
andR
(andL1 ([h1': left (a p)] init h1') h1)
(andL1 ([h2': left (a r)] init h2') h2).

d2: {P}{p: atom P}{q: atom P}{r: atom P}{s: atom P}
right (imp (and (a p) (a q))
(imp (and (a r) (a s))
(and (a p) (a r))))
= [P][p][q][r][s]
impR [h1: left (and (a p) (a q))]
impR [h2: left (and (a r) (a s))]
andL1 ([h1': left (a p)]
andR
(andL2 ([_] (andL2 ([_] (init h1')) h1)) h1)
(andL1 ([h2': left (a r)] init h2') h2))
h1.```

Here are three different polarizations.

```%solve t-: {p}{q}{r}{s} t (dn(c p /\ c q) => (dn(c r /\ c s) => (c p /\ c r))) _.
%solve t+: {p}{q}{r}{s} t ((c p * c q) => ((c r * c s) => up(c p * c r))) _.
%solve te: {p}{q}{r}{s} t (dn(up(c p) /\ up(c q))
=> up(dn(dn(up(c r) /\ up(c s))
=> up(dn(up(c p) /\ up(c r)))))) _.```

Under the same "good" polarization, different derivations translate to a single unique proof.

```%query 1 * {p}{q}{r}{s} complete _ (d1 - p q r s) (tp (tdn (t- p q r s)))
(N p q r s).
%query 1 * {p}{q}{r}{s} complete _ (d2 - p q r s) (tp (tdn (t- p q r s)))
(N p q r s).```
```Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)
%query 1 *

{p:atom -} {q:atom -} {r:atom -} {s1:atom -}
complete (St1 p q r s1) (d1 - p q r s1) (tp (tdn (t- p q r s1))) (N p q r s1).
---------- Solution 1 ----------
N =
[q:atom -] [q1:atom -] [q2:atom -] [q3:atom -]
focR
(dnR
(=>R
(dnL
([x':hyp (c q /\ c q1)]
=>R
(dnL
([x'14:hyp (c q2 /\ c q3)]
/\R (&eta;- (focL sn x' (/\L1 id-)))
(&eta;- (focL sn x'14 (/\L1 id-))))))))).
____________________________________________

%query 1 *

{p:atom -} {q:atom -} {r:atom -} {s1:atom -}
complete (St1 p q r s1) (d2 - p q r s1) (tp (tdn (t- p q r s1))) (N p q r s1).
---------- Solution 1 ----------
N =
[q:atom -] [q1:atom -] [q2:atom -] [q3:atom -]
focR
(dnR
(=>R
(dnL
([x':hyp (c q /\ c q1)]
=>R
(dnL
([x'28:hyp (c q2 /\ c q3)]
/\R (&eta;- (focL sn x' (/\L1 id-)))
(&eta;- (focL sn x'28 (/\L1 id-))))))))).
____________________________________________

%% OK %%```

Different polarizations may lead to very differently shaped derivations.

```%query 1 * {p}{q}{r}{s} complete _ (d2 + p q r s)
(tp (tdn (t+ p q r s)))
(N p q r s).
%query 1 * {p}{q}{r}{s} complete _ (d2 + p q r s)
(tp (tdn (te p q r s)))
(N p q r s).```
```Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)
%query 1 *

{p:atom +} {q:atom +} {r:atom +} {s1:atom +}
complete (St1 p q r s1) (d2 + p q r s1) (tp (tdn (t+ p q r s1))) (N p q r s1).
---------- Solution 1 ----------
N =
[q:atom +] [q1:atom +] [q2:atom +] [q3:atom +]
focR
(dnR
(=>R
(*L
(&eta;+
([z:exp (rfoc (c q))]
&eta;+
([z71:exp (rfoc (c q1))]
=>R
(*L
(&eta;+
([z72:exp (rfoc (c q2))]
&eta;+
([z73:exp (rfoc (c q3))]
upR (focR (*R z z72)))))))))))).
____________________________________________

%query 1 *

{p:atom +} {q:atom +} {r:atom +} {s1:atom +}
complete (St1 p q r s1) (d2 + p q r s1) (tp (tdn (te p q r s1))) (N p q r s1).
---------- Solution 1 ----------
N =
[q:atom +] [q1:atom +] [q2:atom +] [q3:atom +]
focR
(dnR
(=>R
(dnL
([x':hyp (up (c q) /\ up (c q1))]
upR
(focR
(dnR
(=>R

(dnL
([x'26:hyp (up (c q2) /\ up (c q3))]
upR
(focR
(dnR
(/\R
(upR
(focL sp x'
(/\L1
(upL sp
(&eta;+ ([z:exp (rfoc (c q))] focR z))))))
(upR
(focL sp x'26
(/\L1
(upL sp
(&eta;+ ([z:exp (rfoc (c q2))] focR z)))))))))))))))))).
____________________________________________

%% OK %%```