%{ In this article, we will take a presentation of a logic very close to 
that of Fairtlough and Mendler's lax logic<ref>{{bibtex:fm97lax}}</ref> and
show a translation into a polarized version of Pfenning and Davies' judgmental
reconstruction of lax logic.<ref>{{bibtex:pd01modal}}</ref> We will refer to
the non-judgmental, non-polarized system as the ''source logic'' and to the
judgmentally reconstructed, polarized system as the ''target logic.''
While we tend to see ''judgmentally reconstructed'' logics as Good 
Things<sup>TM</sup>, there's nothing inherently interesting about
''polarization'' of the the target
logic on its own -- the target logic is polarized because it will make the
proof of completeness for [[focused lax logic]] clearer.

Therefore, we have three separate things that are happening simultaneously. 
* First, we are formally establishing the connection between Fairtlough and Mendler's system and Pfenning and Davies' system. 
* Second, because the source logic has a cut rule and the target logic does not, we prove the [[admissibility of cut]] in the target logic and use it to eliminate instances of the cut rule during translation. Alternatively, we could have (presumably) proven cut elimination within Fairtlough and Mendler's system, or we could have left a cut rule in the target logic and then proven cut elimination there.
* Third, we are showing the connection between a non-polarized system and a polarized one. 
All three of these things could be done separately, but we did not find that
it added to the overall complexity to do them all together.

The third point above, translation into a non-polarized system, 
is where most of the 
technical difficulty of the completeness proof happens, because a general
translation from a non-polarized logic to a polarized one may add an 
arbitrary number of shift operations. 

<references/> 

<br/>}%

%{ == Preliminaries == }%

%{ We will be [[using a metric]] to make certain arguments about translation
simpler - we can think of this metric as a tree <tt>T</tt> that is either
a leaf (<tt>o</tt>), a parent with one child tree (<tt>x T</tt>), or a parent
with two child trees (<tt>T1 | T2</tt>). 
}%

metric : type.                          %name metric T.
o : metric.
x : metric -> metric.
| : metric -> metric -> metric.         %infix right 10 |.

id : metric -> metric -> type.          %name id ID.
id/refl : id M M.

%{ We will also be, throughout, working in a universe of atomic propositions.
Each atomic proposition has a defined polarity (<tt>pos</tt> or <tt>neg</tt>), 
though this is mostly irrelevant in the target logic and totally irrelevant in 
the source logic. Every theorem we prove will assume a universe of arbitrary
atomic propositions of both polarities, so every <tt>[[%worlds]]</tt> 
declaration will include at least the blocks <tt>bl_atmpos</tt> (positive
atomic propositions) and <tt>bl_atmneg</tt> (negative atomic propositions). }%

polarity : type.			%name polarity S.
pos : polarity.
neg : polarity.
atm : polarity -> type.                 %name atm Q q.
%block bl_atmpos : block {qp:atm pos}.
%block bl_atmneg : block {qn:atm neg}.

%{ == Fairtlough and Mendler's lax logic == }%

%{ Fairtlough and Mendler's presentation of lax logic has a slight 
inconsistancy: the logic's syntax is defined as 

<math>M ::= Q \mid \mathsf{true} \mid \mathsf{false} \mid M \wedge M \mid M \vee M \mid M \supset M \mid \neg M \mid {\bigcirc}M</math>

However, rules are given for neither <math>\mathsf{true}</math> nor 
<math>\mathsf{false}</math>. A reasonable approach seemed to be to define
<math>\mathsf{false}</math> as <math>\neg \mathsf{true}</math>. }%

prop' : type.                           %name prop' M.

atom'  : atm S -> prop'. 
tt'    : prop'.
/\     : prop' -> prop' -> prop'.       %infix right 9 /\.
\/     : prop' -> prop' -> prop'.       %infix right 8 \/.
=>     : prop' -> prop' -> prop'.       %infix right 7 =>.
not'   : prop' -> prop'.
circ'  : prop' -> prop'.
ff'    : prop' = not' tt'.

%{ === Sequent calculus === }%

%{ Fairtlough and Mendler present a Genzen-style intuitionstic sequent
calculus for propositional lax logic in terms of sequents
<math>\Gamma \vdash \Delta</math>, where <math>\Gamma</math> is a finite
list of ''hypotheses'' and <math>\Delta</math> is either 0 or 1 
''assertions''. To prove <math>\Gamma \vdash</math> is to say that the
hypotheses in <math>\Gamma</math> are contradictory, to prove
<math>\Gamma \vdash M</math> is to say that the hypotheses in 
<math>\Gamma</math> establish the proposition <math>M</math>. 

We represent the hypotheses using the LF context; each 
<math>M \in \Gamma</math> becomes an LF variable of type <tt>hyp' M</tt>, and
we use the world <tt>bl_hyp'</tt> to describe all such contexts. }%

hyp' : prop' -> type.
%block bl_hyp' : some {M: prop'} block {h: hyp' M}.

%{ We represent the conclusion as <tt>conc' T D</tt>, where 
* <tt>T</tt> is a metric capturing the shape of the derivation
* <tt>D</tt> = <tt>conc-#'</tt> represents proving a contradiction <math>\Gamma \vdash </math>; we abbreviate <tt>conc' T conc-#'</tt> as <tt># T</tt>.
* <tt>D</tt> = <tt>conc-true' M</tt> represents proving <math>\Gamma \vdash M</math>; we abbreviate <tt>conc' T (conc-true' M)</tt> as <tt>true' T M</tt>. }%

conseq' : type.                         %name conseq' D.
conc-# : conseq'.                       % Contradiction, length 0
conc-true' : prop' -> conseq'.          % Conclusion, length 1
conc' : metric -> conseq' -> type.

%abbrev # = [m] conc' m conc-#.
%abbrev true' = [m][x] conc' m (conc-true' x). 

%{ While our use of a [[structural metric]] embedded into the conclusion of
a sequent needs to be justified by [[adequacy]], it is less of an issue than
other changes we have made to the system. 

As previously mentioned, 
Fairtlough and Mendler's system had no rule for <math>\mathsf{true}</math>,
and we need no rule for <math>\mathsf{false}</math> as we defined it in terms
of <math>\mathsf{true}</math>. We do not write rules for
weakening on the left or exchange on the left, as those are provided "for free"
by the encoding into LF. In addition, we embed contraction into every
left rule:

<center>F&amp;M left conjunction rule: <math>\frac{\Gamma, A, B \vdash \Delta}{\Gamma, A \wedge B \vdash \Delta}</math>
&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; 
Our left conjunction rule: <math>\frac{\Gamma, A \wedge B, A, B \vdash \Delta}{\Gamma, A \wedge B \vdash \Delta}</math></center>

With those caveats, we will continue to consider our source logic, presented
here, to have the essential character of Fairtlough and Mendler's. 

==== Rules on paper ====

<center><math>\frac
{~~~}
{\Gamma \vdash \mathsf{true}}
{\mathsf{true}}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash M \qquad \Gamma \vdash N}
{\Gamma \vdash M \wedge N}
{\wedge}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, M \wedge N, M, N \vdash \Delta}
{\Gamma, M \wedge N \vdash \Delta}
{\wedge}L</math></center>

<br/>

<center><math>\frac
{\Gamma \vdash M}
{\Gamma \vdash M \vee N}
{\vee}R_1</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash N}
{\Gamma \vdash M \vee N}
{\vee}R_2</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, M \vee N, M \vdash \Delta \qquad \Gamma, M \vee N, N \vdash \Delta}
{\Gamma \vdash \Delta}
{\vee}L</math></center>

<br/>

<center><math>\frac
{\Gamma, M \vdash N}
{\Gamma \vdash M \supset N}
{\supset}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, M \supset N \vdash M \qquad \Gamma, M \supset N, N \vdash \Delta}
{\Gamma, M \supset N \vdash \Delta}
{\supset}L</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, M \vdash}
{\Gamma \vdash \neg M}
{\neg}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, \neg M \vdash M}
{\Gamma, \neg M \vdash}
{\neg}L</math></center>

<br/>

<center><math>\frac
{\Gamma \vdash M}
{\Gamma \vdash {\bigcirc} M}
{\bigcirc}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, {\bigcirc} M, M \vdash {\bigcirc} N}
{\Gamma, {\bigcirc} M \vdash {\bigcirc} N}
{\bigcirc}L</math></center>

<br/>

<center><math>\frac
{~~~}
{\Gamma, M \vdash M}
{id}</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash M \qquad \Gamma, M \vdash \Delta}
{\Gamma \vdash \Delta}
{cut}</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash}
{\Gamma \vdash M}
{weakR}</math></center>}%

%{ ==== Rules in Twelf ==== }%

trueR' : true' o tt'.
% no trueL'

/\R' : true' Tm M
       -> true' Tn N
       -> true' (Tm | Tn) (M /\ N).
/\L'  : (hyp' M -> hyp' N -> conc' T D)
         -> (hyp' (M /\ N) -> conc' (x (x T)) D).

\/R1' : true' T M
        -> true' (x T) (M \/ N).
\/R2' : true' T N
        -> true' (x T) (M \/ N).
\/L' : (hyp' M -> conc' Tm D)
       -> (hyp' N -> conc' Tn D)
       -> (hyp' (M \/ N) -> conc' (x (Tm | Tn)) D).

=>R' : (hyp' M -> true' T N)
       -> true' (x T) (M => N).
=>L' : true' Tm M
       -> (hyp' N -> conc' Tn D)
       -> (hyp' (M => N) -> conc' (x (Tm | Tn)) D).

notR' : (hyp' M -> # T)
        -> (true' (x T) (not' M)).
notL' : true' T M
        -> (hyp' (not' M) -> # (x (x T))).

circR' : true' T M 
         -> true' (x T) (circ' M).
circL' : (hyp' M -> true' T (circ' N))
         -> (hyp' (circ' M) -> true' (x (x T)) (circ' N)).

id' : hyp' M -> true' o M.

cut' : true' Ta M 
        -> (hyp' M -> conc' T D)
        -> conc' (Ta | T) D.

weakR' : # T -> true' (x T) M.

%worlds (bl_atmpos | bl_atmneg | bl_hyp') 
 (hyp' M) 
 (conc' T M). % = (# T) (true' T A)


%{ == Polarized judgmental lax logic == }% 

%{ Polarized lax logic loses the <math>\neg</math> but distinguishes
between two different kinds of conjunction, <math>\wedge^+</math> and 
<math>\wedge^-</math>, and two variants of <math>\mathsf{true}</math>
which are the units of the two kinds of conjunction.

''Every'' proposition has a polarity, not just atomic propositions, and
this limits what we can write down. For instance, we cannot
write <math>\top \vee 0</math>, because <math>\vee</math> expectes two
positive things and <math>\top</math> is negative. We could either write
<math>1 \vee 0</math>, or else we could write 
<math>({\downarrow}\top) \vee 0</math>.

The full language of propositions is:

<math>A ::= P \mid N</math>

<math>P ::= Q^+ \mid {\downarrow}N \mid 1 \mid 0 \mid P \wedge^+ P \mid P \vee P</math>

<math>N ::= Q^- \mid {\uparrow}P \mid \top \mid N \wedge^- N \mid P \supset N \mid {\bigcirc}P</math>

The Twelf versions of the the connectives resemble ones from linear logic, 
but we mean unrestricted implication <math>P \supset N</math>
when we write <tt>P -o N</tt>, not linear implication. }%

prop : polarity -> type.                %name prop A.

atom : atm S -> prop S.
up : prop pos -> prop neg.
down : prop neg -> prop pos.
top : prop neg.
1 : prop pos.
0 : prop pos.
* : prop pos -> prop pos -> prop pos.   %infix right 9 *.
& : prop neg -> prop neg -> prop neg.   %infix right 8 &.
+ : prop pos -> prop pos -> prop pos.   %infix right 7 +.
-o : prop pos -> prop neg -> prop neg.  %infix right 6 -o.
circ : prop pos -> prop neg.

%{ === Sequent calculus === }%

%{ Our assumptions are, as before, represented by LF variables, this time
of type <tt>hyp A</tt>. }%

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

%{ We are always trying to prove one of two ''judgments,'' and so our 
sequents either take the form <math>\Gamma \vdash A~true</math> (<math>A</math>
is true) or <math>\Gamma \vdash A~lax</math> (<math>A</math> is true
under a constraint). }%

conseq : type.                          %name conseq J.
conc-lax : prop S -> conseq.            % A lax
conc-true : prop S -> conseq.           % A true
conc : conseq -> type.

%abbrev lax = [x] conc (conc-lax x).
%abbrev true = [x] conc (conc-true x).

%{ Later on in the proof of soundness we will use identity of ''derivations''
in order to make a termination argument work; with this one trick, we avoid
any need for a [[structural metric]] like we used before. }%

idconc : conc C -> conc C' -> type.
idconc/refl : idconc D D.

%{ ==== Rules on paper ==== 

<center><math>\frac
{~~~}
{\Gamma, Q^+ \vdash Q^+~true}
{init}^+</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{~~~}
{\Gamma, Q^- \vdash Q^-~true}
{init}^-</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash A~true}
{\Gamma \vdash A~lax}
{lax}R</math></center>

<br/>

<center><math>\frac
{\Gamma \vdash P~true}
{\Gamma \vdash {\uparrow}P~true}
{\uparrow}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, {\uparrow}P, P \vdash J}
{\Gamma, {\uparrow}P \vdash J}
{\uparrow}L</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash N~true}
{\Gamma \vdash {\downarrow}N~true}
{\downarrow}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, {\downarrow}N, N \vdash J}
{\Gamma, {\downarrow}N \vdash J}
{\downarrow}L</math></center>

<br/>

<center><math>\frac
{~~~}
{\Gamma \vdash 1~true}
{1}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash P_1~true \qquad \Gamma \vdash P_2~true}
{\Gamma \vdash P_1 \wedge^+ P_2~true}
{\wedge^+}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, P_1 \wedge^+ P_2, P_1, P_2 \vdash J}
{\Gamma, P_1 \wedge^+ P_2 \vdash J}
{\wedge^+}L</math></center>

<br/>

<center><math>\frac
{~~~}
{\Gamma \vdash \top~true}
{\top}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash N_1~true \qquad \Gamma \vdash N_2~true}
{\Gamma \vdash N_1 \wedge^- N_2~true}
{\wedge^-}R</math></center>

<br/>

<center><math>\frac
{\Gamma, N_1 \wedge^+ N_2, N_1 \vdash J}
{\Gamma, N_1 \wedge^+ N_2 \vdash J}
{\wedge^-}L_1</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, N_1 \wedge^+ N_2, N_2 \vdash J}
{\Gamma, N_1 \wedge^+ N_2 \vdash J}
{\wedge^-}L_2</math></center>

<br/>

<center><math>\frac
{\Gamma \vdash P_1~true}
{\Gamma \vdash P_1 \vee P_2~true}
{\vee}R_1</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma \vdash P_2~true}
{\Gamma \vdash P_1 \vee P_2~true}
{\vee}R_2</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, P_1 \vee P_2, P_1 \vdash J \qquad \Gamma, P_1 \vee P_2, P_2 \vdash J}
{\Gamma, P_1 \vee P_2 \vdash J}
{\vee}R</math></center>

<br/>

<center><math>\frac
{\Gamma, P \vdash N~true}
{\Gamma \vdash P \supset N~true}
{\supset}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, P_1 \supset P_2 \vdash P_1 \qquad \Gamma, P_1 \supset P_2, P_2 \vdash J}
{\Gamma, P_1 \supset P_2 \vdash J}
{\supset}L</math></center>

<br/>

<center><math>\frac
{\Gamma \vdash P~lax}
{\Gamma \vdash {\bigcirc}P~true}
{\bigcirc}R</math>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;<math>\frac
{\Gamma, {\bigcirc}P, P \vdash A~lax}
{\Gamma, {\bigcirc}P \vdash A~lax}
{\bigcirc}L</math></center>}%

%{ ==== Rules in Twelf ==== }%

init+ : hyp (atom Qp) -> true (atom (Qp: atm pos)).
init- : hyp (atom Qn) -> true (atom (Qn: atm neg)).

laxR : true A
        -> lax A.

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

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

1R : true 1.
% no 1L

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

topR : true top.
% no topL

&R : true N1
      -> true N2
      -> true (N1 & N2).
&L1 : (hyp N1 -> conc J)
       -> (hyp (N1 & N2) -> conc J).
&L2 : (hyp N2 -> conc J)
       -> (hyp (N1 & N2) -> conc J).

% no 0R
0L : (hyp 0 -> conc J).

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

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

circR : lax P
         -> true (circ P).
circL : (hyp P -> lax A)
         -> (hyp (circ P) -> lax A).

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

%{ == Translation == }%

%{ Now we can define a nondeterminstic translation between our variant of
Fairtlough and Mendler's propositional lax logic and our target logic,
polarized, judgmental lax logic. We will use a metric that essentially
captures the structure of the term in the target logic (in fact, it would
be worth seeing if we could use the term in the target logic in lieu of
the metric.) }%

%{ === Propositions === }%

%{ The intent of the first relation we define is to be maximally general, which
means that the <tt>t+-</tt> and <tt>t-+</tt> rules can add an arbitrary 
number of shifts. Read in the reverse direction, the translation is not 
very nondeterminstic; however "<tt>P -o up 0</tt>" can still be translated
to either "<tt>not M</tt>" or "<tt>M => (not' tt')</tt>," which are different
source logic expressions. }%

trans : metric -> prop' -> {S} prop S -> type. %name trans TR.

t+- : trans T M pos P -> trans (x T) M neg (up P).
t-+ : trans T M neg N -> trans (x T) M pos (down N).

tatom : trans o (atom' Q) S (atom Q). 
t+true : trans o tt' pos 1.
t-true : trans o tt' neg top.
t+false: trans o ff' pos 0.
t+and  : trans T1 M1 pos P1
          -> trans T2 M2 pos P2 
          -> trans (T1 | T2) (M1 /\ M2) pos (P1 * P2).
t-and  : trans T1 M1 neg N1 
          -> trans T2 M2 neg N2 
          -> trans (T1 | T2) (M1 /\ M2) neg (N1 & N2).
t+or   : trans T1 M1 pos P1 
          -> trans T2 M2 pos P2
          -> trans (T1 | T2) (M1 \/ M2) pos (P1 + P2).
t-imp  : trans T1 M1 pos P
          -> trans T2 M2 neg N 
          -> trans (T1 | T2) (M1 => M2) neg (P -o N).
t+not  : trans T M pos P -> trans (x T) (not' M) neg (P -o up 0).
t+circ : trans T M pos P -> trans (x T) (circ' M) neg (circ P).

%worlds (bl_atmpos | bl_atmneg) (trans _ _ _ _).

%{ === Conclusions === }%

%{ We additionally define translation between right-hand-sides 
<tt>D</tt> in the source logic and judgments <tt>J</tt> in the target 
logic. }%

trans-conc : metric -> conseq' -> conseq -> type. %name trans-conc TC.

tc : trans-conc T (conc-true' M) (conc-true A) <- trans T M S A.
tc# : trans-conc o conc-# (conc-true (up 0)).
tclax : trans-conc T (conc-true' (circ' M)) (conc-lax A) 
         <- trans T M S A.

%worlds (bl_atmpos | bl_atmneg) (trans-conc _ _ _).

%{ === Hypotheses === }%

%{ When we are showing soundness and completeness, we will need
to know that for every hypothesis in the {source, target} logic we have
a hypothesis in the {target, source} logic such that one is the translation
of the other. 

What we would like to do is define a single <tt>trans-hyp</tt> that allows us 
to translate from source logic hypotheses to target logic hypotheses, and
vice versa. However, because we cannot assign multiple modes to the same 
relation, we'll define two different relations, and use them to define two
different worlds.

* <tt>trans-soundhyp</tt> takes a target logic hypotheis <tt>H</tt> and obtains a translation <tt>TR</tt> and a source logic hypothesis <tt>H'</tt>.
* <tt>trans-complhyp</tt> takes a source logic hypothesis <tt>H'</tt> and obtains a translation <tt>TR</tt> and a target logic hypothesis <tt>H</tt>. }%

trans-soundhyp : hyp H -> trans Mh H' S H -> hyp' H' -> type.
%mode trans-soundhyp +H' -T -H.

%block bl_trans-soundhyp 
   : some {M: metric}{S: polarity}{A: prop S}{A': prop'}{T: trans M A' S A}
      block {h: hyp A}{h': hyp' A'}{t: trans-soundhyp h T h'}.

%worlds (bl_atmpos | bl_atmneg | bl_trans-soundhyp)  (trans-soundhyp _ _ _).
%total [] (trans-soundhyp _ _ _).

trans-complhyp : hyp' A -> trans Mt A S C -> hyp C -> type.
%mode trans-complhyp +H' -T -H.

%block bl_trans-complhyp 
   : some {M: metric}{A: prop'}{S: polarity}{C: prop S}{T: trans M A S C}
      block {h': hyp' A}{h: hyp C}{t: trans-complhyp h' T h}.

%worlds (bl_atmpos | bl_atmneg | bl_trans-complhyp)  (trans-complhyp _ _ _).
%total [] (trans-complhyp _ _ _).

%{ === Correspondence === }%

%{ A corollary to the  theorem we will state below will say "If 
<math>\vdash A~true</math> and <math>M~\texttt{trans}~A</math>, then 
<math>\vdash M</math>." However, if there is no <math>M</math> such that 
<math>M~\texttt{trans}~A</math>, then the theorem will be vacuously true, 
which is not our intent. Therefore, we need to establish that our translations
of propositions and conclusions are ''correspondences'' 
(left- and right-total). 

Twelf can verify that translation is ''right-total'', that there is an 
<tt>M</tt> for every <tt>A</tt> and a <tt>D</tt> for every <tt>J</tt>, without
any further work on our part: we just assign modes to the relation
and state a [[totality assertion]]. }%

%mode trans -T -M +S +A.
%mode trans-conc -T -D +J.
%total (A C) (trans _ _ _ A) (trans-conc _ _ C).

%{ However, in the forward direction, to show that the relation is 
''left-total'' we will need to write an 
[[effectiveness lemma]], which we will call <tt>can-trans</tt>.

The two lemmas <tt>can-switch</tt> are really just case analysis to 
establish that if you can translate something as a positive formula, you can
apply an up shift to make it a negative formula, and vice versa. }%

can-switch+ : trans M A S (C: prop S) -> trans N A pos C' -> type.
- : can-switch+ T T.
- : can-switch+ T (t-+ T).
%mode can-switch+ +A -B. 
%worlds (bl_atmpos | bl_atmneg) (can-switch+ _ _). 
%total [] (can-switch+ _ _).

can-switch- : trans M A S' C -> trans N A neg C' -> type.
- : can-switch- T T.
- : can-switch- T (t+- T).
%mode can-switch- +A -B. 
%worlds (bl_atmpos | bl_atmneg) (can-switch- _ _). 
%total [] (can-switch- _ _).

can-trans : {A} trans M A S (C: prop S) -> type. 
%mode can-trans +A -T.

- : can-trans (atom' Qp) tatom.
- : can-trans tt' t-true.
- : can-trans (A /\ B) (t-and T1' T2')
     <- can-trans A T1
     <- can-switch- T1 T1'
     <- can-trans B T2
     <- can-switch- T2 T2'.
- : can-trans (A \/ B) (t+or T1' T2')
     <- can-trans A T1
     <- can-switch+ T1 T1'
     <- can-trans B T2
     <- can-switch+ T2 T2'.
- : can-trans (A => B) (t-imp T1' T2')
     <- can-trans A T1
     <- can-switch+ T1 T1'
     <- can-trans B T2
     <- can-switch- T2 T2'.
- : can-trans (not' A) (t+not T')
     <- can-trans A T
     <- can-switch+ T T'.
- : can-trans (circ' A) (t+circ T')
     <- can-trans A T
     <- can-switch+ T T'.

%worlds (bl_atmpos | bl_atmneg) (can-trans _ _).
%total A (can-trans A _).

can-trans-conc : {D} trans-conc T D J -> type.
%mode can-trans-conc +D -T.

- : can-trans-conc conc-# tc#.
- : can-trans-conc (conc-true' M) (tc TR)
     <- can-trans M TR.

%worlds (bl_atmpos | bl_atmneg) (can-trans-conc _ _).
%total A (can-trans-conc A _).


%{ == Metatheory of the target logic == }%

%{ The correctness of translation will rest on the standard metatheoretic
results: the ''identity principle'' and the ''admissibility of cut''. Note 
that we could have added a <tt>cut</tt> and <tt>id</tt> rule to the target
logic, but we still would have eventually needed to do the work in this 
section in order to have confidence that our target logic was reasonable. }% 

%{ === Identity === }%

%{ For all propositions <math>A</math>, there exists a derivation of
<math>A \vdash A~true</math>. 

The proof is by induction on the formula <math>A</math>. }%

identity : {A} (hyp A -> true A) -> type.
%mode identity +A -D.

- : identity (atom Q) init+.
- : identity (atom Q) init-.
- : identity (up P) ([h] upL ([h'] upR (D h')) h)
     <- identity P (D: hyp P -> true P).
- : identity (down N) ([h] downL ([h'] downR (D h')) h)
     <- identity N (D: hyp N -> true N).
- : identity top ([_] topR).
- : identity 1 ([_] 1R).
- : identity 0 ([h] 0L h).
- : identity (P1 * P2) ([h] *L ([h1][h2] *R (D1 h1) (D2 h2)) h)
     <- identity P1 (D1: hyp P1 -> true P1)
     <- identity P2 (D2: hyp P2 -> true P2).
- : identity (N1 & N2) ([h] &L1 ([h1] &L2 ([h2] &R (D1 h1) (D2 h2)) h) h)
     <- identity N1 (D1: hyp N1 -> true N1)
     <- identity N2 (D2: hyp N2 -> true N2).
- : identity (P1 + P2) ([h] +L ([h1] +R1 (D1 h1)) ([h2] +R2 (D2 h2)) h)
     <- identity P1 (D1: hyp P1 -> true P1)
     <- identity P2 (D2: hyp P2 -> true P2).
- : identity (P -o N) ([h] -oR ([h1] -oL (D1 h1) ([h2] D2 h2) h))
     <- identity P (D1: hyp P -> true P)
     <- identity N (D2: hyp N -> true N).
- : identity (circ P) ([h] circR (circL ([h'] laxR (D1 h')) h))
     <- identity P (D1: hyp P -> true P).

%worlds (bl_atmpos | bl_atmneg | bl_hyp) (identity _ _).
%total T (identity T _).

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

%{ There are two cut principles which must be proven simultaneously; 
<tt>cut</tt> is the main theorem, and <tt>lcut</tt> is the cut principle
for lax truth.

* If <math>\Gamma \vdash A~true</math> and <math>\Gamma, A \vdash J</math>, then <math>\Gamma \vdash J</math> (<tt>cut</tt>)
* If <math>\Gamma \vdash A~lax</math> and <math>\Gamma, A \vdash C~lax</math>, then <math>\Gamma \vdash C~lax</math> (<tt>lcut</tt>)

The proofs are by mutual lexographic induction; either the principal cut 
formula <math>A</math> gets smaller, or else the principal cut formula
stays the same and one or both of the input derivations get smaller. The proof
is entirely standard other than the need for extra commutative cuts for
<tt>tlax</tt>; more explanation is available at the article on
the [[admissibility of cut]]. }%

cut : {A} true A -> (hyp A -> conc J) -> conc J -> type.
lcut : {A} lax A -> (hyp A -> lax C) -> lax C -> type.
%mode cut +A +D +E -F.
%mode lcut +A +D +E -F.

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

- : cut (atom Q) (init+ H) ([h] init+ h) (init+ H).
- : cut (atom Q) (init- H) ([h] init- h) (init- H).

- : cut (up P) (upR (D: true P)) ([h] upL (E h : hyp P -> conc J) h) G
     <- ({h': hyp P} cut (up P) (upR D) ([h] E h h') (F h'))
     <- cut P D ([h'] F h') (G: conc J).

- : cut (down N) (downR (D: true N)) ([h] downL (E h : hyp N -> conc J) h) G
     <- ({h': hyp N} cut (down N) (downR D) ([h] E h h') (F h'))
     <- cut N D ([h'] F h') (G: conc J).

- : cut (P1 * P2) (*R (D1: true P1) (D2: true P2))
     ([h] *L (E h : hyp P1 -> hyp P2 -> conc J) h) G
     <- ({h1: hyp P1}{h2: hyp P2} 
           cut (P1 * P2) (*R D1 D2) ([h] E h h1 h2) (F h1 h2))
     <- ({h2: hyp P2} cut P1 D1 ([h1] F h1 h2) (F1 h2))
     <- cut P2 D2 ([h2] F1 h2) (G: conc J).

- : cut (N1 & N2) (&R (D1: true N1) (D2: true N2)) 
     ([h] &L1 (E h : hyp N1 -> conc J) h) G
     <- ({h1: hyp N1} cut (N1 & N2) (&R D1 D2) ([h] E h h1) (F h1))
     <- cut N1 D1 ([h1] F h1) (G: conc J).

- : cut (N1 & N2) (&R (D1: true N1) (D2: true N2)) 
     ([h] &L2 (E h : hyp N2 -> conc J) h) G
     <- ({h2: hyp N2} cut (N1 & N2) (&R D1 D2) ([h] E h h2) (F h2))
     <- cut N2 D2 ([h2] F h2) (G: conc J).

- : cut (P1 + P2) (+R1 (D1: true P1)) ([h] +L (E1 h : hyp P1 -> conc J) _ h) G
     <- ({h1: hyp P1} cut (P1 + P2) (+R1 D1) ([h] E1 h h1) (F h1))
     <- cut P1 D1 ([h1] F h1) G. 

- : cut (P1 + P2) (+R2 (D2: true P2)) ([h] +L _ (E2 h : hyp P2 -> conc J) h) G
     <- ({h2: hyp P2} cut (P1 + P2) (+R2 D2) ([h] E2 h h2) (F h2))
     <- cut P2 D2 ([h2] F h2) G. 

- : cut (P -o N) (-oR (D: hyp P -> true N)) 
     ([h] -oL (E1 h: true P) (E2 h: hyp N -> conc J) h) G
     <- cut (P -o N) (-oR D) ([h] E1 h) (F1: true P)
     <- ({h': hyp N} cut (P -o N) (-oR D) ([h] E2 h h') (F2 h' : conc J))
     <- cut P F1 ([h'] D h') (G1: true N)
     <- cut N G1 ([h'] F2 h') (G: conc J).

- : cut (circ P) (circR (D: lax P)) ([h] circL (E h : hyp P -> lax C) h) G
     <- ({h': hyp P} cut (circ P) (circR D) ([h] E h h') (F h': lax C))
     <- lcut P D ([h'] F h') G.

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

- : lcut P (laxR (D: true P)) E F
     <- cut P D E F.
- : cut A (upL D H) E (upL F H)
     <- {h1} cut A (D h1) E (F h1).
- : cut A (downL D H) E (downL F H)
     <- {h1} cut A (D h1) E (F h1).
- : cut A (0L H) E (0L H).
- : cut A (*L D H) E (*L F H)
     <- {h1}{h2} cut A (D h1 h2) E (F h1 h2).
- : cut A (&L1 D H) E (&L1 F H)
     <- {h1} cut A (D h1) E (F h1).
- : cut A (&L2 D H) E (&L2 F H)
     <- {h2} cut A (D h2) E (F h2).
- : cut A (+L D1 D2 H) E (+L F1 F2 H)
     <- ({h1} cut A (D1 h1) E (F1 h1))
     <- ({h2} cut A (D2 h2) E (F2 h2)).
- : cut A (-oL D1 D2 H) E (-oL D1 F2 H)
     <- {h'} cut A (D2 h') E (F2 h').


%{ ==== Monadic left commutative cuts ==== }%

- : lcut A (circL ([h] D h) H) E (circL ([h] F h) H)
     <- {h'} lcut A (D h') E (F h').
- : lcut A (upL D H) E (upL F H)
     <- {h1} lcut A (D h1) E (F h1).
- : lcut A (downL D H) E (downL F H)
     <- {h1} lcut A (D h1) E (F h1).
- : lcut A (0L H) E (0L H).
- : lcut A (*L D H) E (*L F H)
     <- {h1}{h2} lcut A (D h1 h2) E (F h1 h2).
- : lcut A (&L1 D H) E (&L1 F H)
     <- {h1} lcut A (D h1) E (F h1).
- : lcut A (&L2 D H) E (&L2 F H)
     <- {h2} lcut A (D h2) E (F h2).
- : lcut A (+L D1 D2 H) E (+L F1 F2 H)
     <- ({h1} lcut A (D1 h1) E (F1 h1))
     <- ({h2} lcut A (D2 h2) E (F2 h2)).
- : lcut A (-oL D1 D2 H) E (-oL D1 F2 H)
     <- {h'} lcut A (D2 h') E (F2 h').

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

- : cut A D ([h] init+ H) (init+ H).
- : cut A D ([h] init- H) (init- H).
- : cut A D ([h] laxR (E h)) (laxR F)
     <- cut A D ([h] E h) F.
- : cut A D ([h] upR (E h)) (upR F)
     <- cut A D ([h] E h) F.
- : cut A D ([h] upL ([h'] E h h') H) (upL F H)
     <- {h'} cut A D ([h] E h h') (F h'). 
- : cut A D ([h] downR (E h)) (downR F)
     <- cut A D ([h] E h) F.
- : cut A D ([h] downL ([h'] E h h') H) (downL F H)
     <- {h'} cut A D ([h] E h h') (F h').
- : cut A D ([h] topR) topR.
- : cut A D ([h] 1R) 1R.
- : cut A D ([h] 0L H) (0L H).
- : cut A D ([h] *R (E1 h) (E2 h)) (*R F1 F2)
     <- cut A D ([h] E1 h) F1
     <- cut A D ([h] E2 h) F2.
- : cut A D ([h] *L ([h1][h2] E h h1 h2) H) (*L ([h1][h2] F h1 h2) H)
     <- {h1}{h2} cut A D ([h] E h h1 h2) (F h1 h2).
- : cut A D ([h] &R (E1 h) (E2 h)) (&R F1 F2)
     <- cut A D ([h] E1 h) F1
     <- cut A D ([h] E2 h) F2.
- : cut A D ([h] &L1 ([h1] E1 h h1) H) (&L1 ([h1] F1 h1) H)
     <- {h1} cut A D ([h] E1 h h1) (F1 h1).
- : cut A D ([h] &L2 ([h2] E2 h h2) H) (&L2 ([h2] F2 h2) H)
     <- {h2} cut A D ([h] E2 h h2) (F2 h2).
- : cut A D ([h] +R1 (E1 h)) (+R1 F1)
     <- cut A D ([h] E1 h) F1.
- : cut A D ([h] +R2 (E2 h)) (+R2 F2)
     <- cut A D ([h] E2 h) F2.
- : cut A D ([h] +L ([h1] E1 h h1) ([h2] E2 h h2) H) (+L F1 F2 H)
     <- ({h1} cut A D ([h] E1 h h1) (F1 h1))
     <- ({h2} cut A D ([h] E2 h h2) (F2 h2)).
- : cut A D ([h] -oR [h'] E h h') (-oR [h'] F h')
     <- {h'} cut A D ([h] E h h') (F h').
- : cut A D ([h] -oL (E1 h) ([h'] E2 h h') H) (-oL F1 ([h'] F2 h') H)
     <- cut A D ([h] E1 h) F1
     <- {h'} cut A D ([h] E2 h h') (F2 h').
- : cut A D ([h] circR (E h)) (circR F)
     <- cut A D ([h] E h) F.
- : cut A D ([h] circL ([h'] E h h') H) (circL ([h'] F h') H)
     <- {h'} cut A D ([h] E h h') (F h').

%{ ==== Monadic right commutive cuts ==== }%

- : lcut A D ([h] upL ([h'] E h h') H) (upL F H)
     <- {h'} lcut A D ([h] E h h') (F h'). 
- : lcut A D ([h] downL ([h'] E h h') H) (downL F H)
     <- {h'} lcut A D ([h] E h h') (F h').
- : lcut A D ([h] *L ([h1][h2] E h h1 h2) H) (*L ([h1][h2] F h1 h2) H)
     <- {h1}{h2} lcut A D ([h] E h h1 h2) (F h1 h2).
- : lcut A D ([h] &L1 ([h1] E1 h h1) H) (&L1 ([h1] F1 h1) H)
     <- {h1} lcut A D ([h] E1 h h1) (F1 h1).
- : lcut A D ([h] &L2 ([h2] E2 h h2) H) (&L2 ([h2] F2 h2) H)
     <- {h2} lcut A D ([h] E2 h h2) (F2 h2).
- : lcut A D ([h] +L ([h1] E1 h h1) ([h2] E2 h h2) H) (+L F1 F2 H)
     <- ({h1} lcut A D ([h] E1 h h1) (F1 h1))
     <- ({h2} lcut A D ([h] E2 h h2) (F2 h2)).

%worlds (bl_atmpos | bl_atmneg | bl_hyp) (cut _ _ _ _) (lcut _ _ _ _).
%total {(A1 A2) [(D1 D2) (E1 E2)]} (cut A1 D1 E1 F1) (lcut A2 D2 E2 F2).


%{ === Inversion lemmas === }%

%{ Proving invertability is an application of both cut and identity; it 
establishes that that for some rules, whenver the conclusion is true then
the premises are always true as well. 

In general, negative propositions are invertible on the right and positive
propositions are invertible on the left, though in unfocused intutionstic
logic <tt>up</tt> and <tt>down</tt> are invertible in both directions and
both variants of conjunction are invertible on the right. This is not the full
set of inversion lemmas, just the ones we needed. }%

invupR : true (up P) -> true P -> type.
- : invupR D F
     <- identity P (EP : hyp P -> true P)
     <- cut (up P) D (upL ([h] EP h)) F.
%mode invupR +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invupR _ _).
%total [] (invupR _ _).

invupL : (hyp (up P) -> conc J) -> (hyp P -> conc J) -> type.
- : invupL ([h] D h) ([h] F h)
     <- identity P (EP : hyp P -> true P)
     <- {h: hyp P} cut (up P) (upR (EP h)) D (F h).
%mode invupL +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invupL _ _).
%total [] (invupL _ _).

invdownR : true (down P) -> true P -> type.
- : invdownR D F
     <- identity P (EP : hyp P -> true P)
     <- cut (down P) D (downL ([h] EP h)) F.
%mode invdownR +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invdownR _ _).
%total [] (invdownR _ _).

invdownL : (hyp (down P) -> conc J) -> (hyp P -> conc J) -> type.
- : invdownL ([h] D h) ([h] F h)
     <- identity P (EP : hyp P -> true P)
     <- {h: hyp P} cut (down P) (downR (EP h)) D (F h).
%mode invdownL +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invdownL _ _).
%total [] (invdownL _ _).

inv*R : true (P1 * P2) -> true P1 -> true P2 -> type.
- : inv*R D F1 F2
     <- identity (P1 * P2) (E : hyp (P1 * P2) -> true (P1 * P2))
     <- identity P1 (E1 : hyp P1 -> true P1)
     <- identity P2 (E2 : hyp P2 -> true P2)
     <- cut (P1 * P2) D (*L [h1][h2] E1 h1) F1
     <- cut (P1 * P2) D (*L [h1][h2] E2 h2) F2.
%mode inv*R +D -F1 -F2.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (inv*R _ _ _).
%total [] (inv*R _ _ _).

inv&R : true (N1 & N2) -> true N1 -> true N2 -> type.
- : inv&R D F1 F2
     <- identity (N1 & N2) (E : hyp (N1 & N2) -> true (N1 & N2))
     <- identity N1 (E1 : hyp N1 -> true N1)
     <- identity N2 (E2 : hyp N2 -> true N2)
     <- cut (N1 & N2) D (&L1 [h1] E1 h1) F1
     <- cut (N1 & N2) D (&L2 [h2] E2 h2) F2.
%mode inv&R +D -F1 -F2.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (inv&R _ _ _).
%total [] (inv&R _ _ _).

inv-oR : true (P -o N) -> (hyp P -> true N) -> type.
- : inv-oR D ([h] F h)
     <- identity P (EP : hyp P -> true P)
     <- identity N (EN : hyp N -> true N)
     <- {h': hyp P} cut (P -o N) D (-oL (EP h') ([h] EN h)) (F h').
%mode inv-oR +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (inv-oR _ _).
%total [] (inv-oR _ _).

invcircR : true (circ P) -> lax P -> type.
- : invcircR D F
     <- identity P (E: hyp P -> true P)
     <- lcut (circ P) (laxR D) (circL ([h'] laxR (E h'))) F.
%mode invcircR +A -B.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invcircR _ _).
%total [] (invcircR _ _).

invcircL : (hyp (circ P) -> lax C) -> (hyp P -> lax C) -> type.
- : invcircL D F
     <- identity P (E: hyp P -> true P)
     <- {h': hyp P} cut (circ P) (circR (laxR (E h'))) ([h] D h) (F h').

%{ == Correctness of translation == }%

%{ === Equivalence === }%

%{ This is an interesting theorem, because it captures the idea that the
translation, while nondeterminstic (a single source logic proposition 
corresponds to many target logic propositions), is not significant
(all target logic propositions in the image of a single source logic
proposition are equivalent). Equivalence will be necessary for the completeness
theorem in order to translate the identity rule in the source logic into the 
target logic.

* If <math>M~\texttt{trans}~A_1</math> and <math>\Gamma \vdash A_1~true</math> and <math>M~\texttt{trans}~A_2</math>, then <math>\Gamma \vdash A_2~true</math>.

The theorem is proved by simultaneous induction on the unordered pair of the 
two translations, and therefore suffers from an annoying lack of expressivity
in the Twelf termination checker. There is no way to express the argument 
"the unordered pair of X and Y gets smaller," and so when we need to switch
the position of the arguments in the lambda case, we cannot convince Twelf
that something is getting smaller. The only way to do this seems to be to
cut and paste the lemma into two copies which then call each other at the
critical case; Twelf can handle the unordered pair as mutual induction. 

First we need a minor strenghtening lemma first, that expresses that if a 
hypothesis translated from true, then it isn't needed. }%

trans-equiv-str : (hyp A -> conc J) -> trans _ tt' pos A -> conc J -> type.

- : trans-equiv-str D (t-+ (t+- TR)) E
     <- invdownL D D'
     <- invupL D' D''
     <- trans-equiv-str D'' TR E.
- : trans-equiv-str D (t-+ t-true) E
     <- cut (down top) (downR topR) D E.
- : trans-equiv-str D t+true E
     <- cut 1 1R D E.

%mode trans-equiv-str +D +TR -F. 
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (trans-equiv-str _ _ _).
%total TR (trans-equiv-str _ TR _).

trans-equiv : trans _ M _ A1 -> true A1 -> trans _ M _ A2 -> true A2 -> type.
trans-equivX: trans _ M _ A1 -> true A1 -> trans _ M _ A2 -> true A2 -> type.
%mode trans-equiv +T1 +D1 +T2 -D2.
%mode trans-equivX +T1 +D1 +T2 -D2.

- : trans-equiv (t+- T1) D1 T2 D2
     <- invupR D1 D1'
     <- trans-equiv T1 D1' T2 D2.
- : trans-equiv (t-+ T1) D1 T2 D2
     <- invdownR D1 D1'
     <- trans-equiv T1 D1' T2 D2.
- : trans-equiv T1 D1 (t+- T2) (upR D2)
     <- trans-equiv T1 D1 T2 D2.
- : trans-equiv T1 D1 (t-+ T2) (downR D2)
     <- trans-equiv T1 D1 T2 D2.

- : trans-equiv tatom D tatom D.
- : trans-equiv t+true D t+true D.
- : trans-equiv t+true D t-true topR.
- : trans-equiv t-true D t+true 1R.
- : trans-equiv t-true D t-true D.
- : trans-equiv t+false D _ E
     <- cut 0 D ([h] 0L h) E.
- : trans-equiv (t+not T) D t+false E
     <- inv-oR D (Da : hyp P1 -> true (up 0))
     <- ({h} invupR (Da h) (Db h))
     <- trans-equiv-str Db T E.
- : trans-equiv (t+and Ta Tb) D (t+and Sa Sb) (*R Ea Eb)
     <- inv*R D Da Db
     <- trans-equiv Ta Da Sa Ea
     <- trans-equiv Tb Db Sb Eb.
- : trans-equiv (t-and Ta Tb) D (t+and Sa Sb) (*R Ea Eb)
     <- inv&R D Da Db
     <- trans-equiv Ta Da Sa Ea
     <- trans-equiv Tb Db Sb Eb.
- : trans-equiv (t+and Ta Tb) D (t-and Sa Sb) (&R Ea Eb)
     <- inv*R D Da Db
     <- trans-equiv Ta Da Sa Ea
     <- trans-equiv Tb Db Sb Eb.
- : trans-equiv (t-and Ta Tb) D (t-and Sa Sb) (&R Ea Eb)
     <- inv&R D Da Db
     <- trans-equiv Ta Da Sa Ea
     <- trans-equiv Tb Db Sb Eb.
- : trans-equiv (t+or Ta Tb) D (t+or Sa Sb) E
     <- identity P1 (D1 : hyp P1 -> true P1)
     <- ({h1} trans-equiv Ta (D1 h1) Sa (E1 h1))
     <- identity P2 (D2 : hyp P2 -> true P2)
     <- ({h2} trans-equiv Tb (D2 h2) Sb (E2 h2))
     <- cut (P1 + P2) D (+L ([h1] +R1 (E1 h1)) ([h2] +R2 (E2 h2))) E.
- : trans-equiv (t-imp Ta Tb) D (t-imp Sa Sb) (-oR E)
     <- identity P2 (D1 : hyp P2 -> true P2)
     <- ({h1} trans-equivX Sa (D1 h1) Ta (E1 h1))
     <- inv-oR D (D2 : hyp P1 -> true N1)
     <- ({h1} trans-equiv Tb (D2 h1) Sb (E2 h1))
     <- ({h2} cut P1 (E1 h2) ([h1] E2 h1) (E h2: true N2)).
- : trans-equiv (t+not T) D (t+not S) (-oR E)
     <- identity P2 (D1: hyp P2 -> true P2)
     <- ({h1} trans-equivX S (D1 h1) T (E1 h1))
     <- inv-oR D (D2 : hyp P1 -> true (up 0))
     <- ({h2} cut P1 (E1 h2) ([h1] D2 h1) (E h2: true (up 0))).
- : trans-equiv (t+circ T) (D: true (circ P)) (t+circ S) (circR F)
     <- invcircR D (D1 : lax P)
     <- identity P (D2 : hyp P -> true P)
     <- ({h1} trans-equiv T (D2 h1) S (E h1: true B))
     <- lcut P D1 ([h] laxR (E h)) F.

%% Cut and paste:

- : trans-equivX (t+- T1) D1 T2 D2
     <- invupR D1 D1'
     <- trans-equivX T1 D1' T2 D2.
- : trans-equivX (t-+ T1) D1 T2 D2
     <- invdownR D1 D1'
     <- trans-equivX T1 D1' T2 D2.
- : trans-equivX T1 D1 (t+- T2) (upR D2)
     <- trans-equivX T1 D1 T2 D2.
- : trans-equivX T1 D1 (t-+ T2) (downR D2)
     <- trans-equivX T1 D1 T2 D2.

- : trans-equivX tatom D tatom D.
- : trans-equivX t+true D t+true D.
- : trans-equivX t+true D t-true topR.
- : trans-equivX t-true D t+true 1R.
- : trans-equivX t-true D t-true D.
- : trans-equivX t+false D _ E
     <- cut 0 D ([h] 0L h) E.
- : trans-equivX (t+not T) D t+false E
     <- inv-oR D (Da : hyp P1 -> true (up 0))
     <- ({h} invupR (Da h) (Db h))
     <- trans-equiv-str Db T E.
- : trans-equivX (t+and Ta Tb) D (t+and Sa Sb) (*R Ea Eb)
     <- inv*R D Da Db
     <- trans-equivX Ta Da Sa Ea
     <- trans-equivX Tb Db Sb Eb.
- : trans-equivX (t-and Ta Tb) D (t+and Sa Sb) (*R Ea Eb)
     <- inv&R D Da Db
     <- trans-equivX Ta Da Sa Ea
     <- trans-equivX Tb Db Sb Eb.
- : trans-equivX (t+and Ta Tb) D (t-and Sa Sb) (&R Ea Eb)
     <- inv*R D Da Db
     <- trans-equivX Ta Da Sa Ea
     <- trans-equivX Tb Db Sb Eb.
- : trans-equivX (t-and Ta Tb) D (t-and Sa Sb) (&R Ea Eb)
     <- inv&R D Da Db
     <- trans-equivX Ta Da Sa Ea
     <- trans-equivX Tb Db Sb Eb.
- : trans-equivX (t+or Ta Tb) D (t+or Sa Sb) E
     <- identity P1 (D1 : hyp P1 -> true P1)
     <- ({h1} trans-equivX Ta (D1 h1) Sa (E1 h1))
     <- identity P2 (D2 : hyp P2 -> true P2)
     <- ({h2} trans-equivX Tb (D2 h2) Sb (E2 h2))
     <- cut (P1 + P2) D (+L ([h1] +R1 (E1 h1)) ([h2] +R2 (E2 h2))) E.
- : trans-equivX (t-imp Ta Tb) D (t-imp Sa Sb) (-oR E)
     <- identity P2 (D1 : hyp P2 -> true P2)
     <- ({h1} trans-equiv Sa (D1 h1) Ta (E1 h1))
     <- inv-oR D (D2 : hyp P1 -> true N1)
     <- ({h1} trans-equivX Tb (D2 h1) Sb (E2 h1))
     <- ({h2} cut P1 (E1 h2) ([h1] E2 h1) (E h2: true N2)).
- : trans-equivX (t+not T) D (t+not S) (-oR E)
     <- identity P2 (D1: hyp P2 -> true P2)
     <- ({h1} trans-equiv S (D1 h1) T (E1 h1))
     <- inv-oR D (D2 : hyp P1 -> true (up 0))
     <- ({h2} cut P1 (E1 h2) ([h1] D2 h1) (E h2: true (up 0))).
- : trans-equivX (t+circ T) (D: true (circ P)) (t+circ S) (circR F)
     <- invcircR D (D1 : lax P)
     <- identity P (D2 : hyp P -> true P)
     <- ({h1} trans-equivX T (D2 h1) S (E h1: true B))
     <- lcut P D1 ([h] laxR (E h)) F.

%worlds (bl_atmpos | bl_atmneg | bl_hyp)
  (trans-equiv _ _ _ _) (trans-equivX _ _ _ _).
%total [(T1 T2) (S1 S2)] (trans-equiv T1 _ S1 _) (trans-equivX S2 _ T2 _).

%{ === Soundness === }%

%{ * If <math>\Gamma \vdash J</math> and <math>\Gamma'~\texttt{trans}~\Gamma</math> and <math>\Delta~\texttt{trans}~J</math>, then <math>\Gamma' \vdash \Delta</math> (<tt>trans-sound</tt>)

Proved by induction on the target logic derivation <math>\Gamma \vdash J</math>.  }%

trans-sound : conc C -> trans-conc Mt C' C -> conc' Mc C' -> type.
%mode trans-sound +C +T -C'.

%{ Every case of translating a left rule needs to translate a hypothesis, 
and we can usefully predict the form of the output, except in the cases where
the reverse translation is not determinstic. The first lemma, 
<tt>trans-init</tt>, is essentally just an [[output factoring]] 
lemma because the case of translating
atomic formula really consists of two cases, the positive atoms and the
negative atoms, and this triggers Twelf's [[output freeness]] check. 

The second nondetermistic case is where we are translating an implication
in the target logic and may encounter either an implication or a 
negation in the source logic. This case (<tt>trans-imp</tt>)
becomes mutually inductive
with the main theorem, and establishes a pattern that will continue in the
completeness theorem. 

One case in particular is worth pointing out. We have
<math>\Gamma \vdash {\uparrow} 0~true</math> in the target logic using the
rule <tt>upR</tt>, which gives us a subderivation 
<math>\Gamma \vdash 0~true</math>, and we are
translating into a contradiction <math>\Gamma' \vdash</math> in the 
target logic (let <math>\Gamma'</math> be the translated 
<math>\Gamma</math>).  

By the induction hypothesis we have
<math>\Gamma' \vdash \mathsf{false}</math>, 
which we have defined to be <math>\Gamma' \vdash \neg \mathsf{true}</math>. 
We need to prove, however, <math>\Gamma' \vdash</math>. Let 
[[User:Rsimmons|me]] know if I'm wrong, but the only way I could figure out
how to do this was by using the cut rule in the source logic, which means
that we do ''not'' get cut elimination "for free" in the source logic by virtue
of cut admissibility in the target logic.

<math>
\frac
{\frac
 {~~~~}
 {\Gamma \vdash \neg\mathsf{true}}
 {i.h.}\qquad 
 \frac
 {\frac{}{\Gamma, \neg\mathsf{true}\vdash\mathsf{true}}{\mathsf{true}R}}
 {\Gamma, \neg\mathsf{true}\vdash}}
 {\neg}L
{\Gamma \vdash}
{cut}
</math>

This awkwardness is a result of the slight mismatch between falsehood in 
the target logic and contradiction in the source logic, and is part of
the reason we didn't include falsehood as a primitive in the source logic. 
}% 

trans-init : trans Mt A' S (atom Q) -> hyp' A' -> hyp' (atom' Q) -> type.
- : trans-init tatom H H.
%mode trans-init +T +H -H'.
%worlds (bl_atmpos | bl_atmneg | bl_trans-soundhyp)  (trans-init _ _ _).
%total [] (trans-init _ _ _).

- : trans-sound (init+ H) (tc tatom) (id' H'')
     <- trans-soundhyp H T H'
     <- trans-init T H' H''.
- : trans-sound (init- H) (tc tatom) (id' H'')
     <- trans-soundhyp H T H'
     <- trans-init T H' H''.
- : trans-sound (laxR D) (tclax T) (circR' E)
     <- trans-sound D (tc T) E.
- : trans-sound (upR D) (tc (t+- T)) E
     <- trans-sound D (tc T) E. 
- : trans-sound (upR D) tc# (cut' E ([h] notL' trueR' h))
     <- trans-sound D (tc t+false) E.
- : trans-sound (upL D H) T (E H')
     <- trans-soundhyp H (t+- Th) H'
     <- ({h}{h'} trans-soundhyp h Th h' 
           -> trans-sound (D h) T (E h' : conc' M C)).
- : trans-sound (downR D) (tc (t-+ T)) E
     <- trans-sound D (tc T) E.
- : trans-sound (downL D H) T (E H')
     <- trans-soundhyp H (t-+ Th) H'
     <- ({h}{h'} trans-soundhyp h Th h' 
           -> trans-sound (D h) T (E h' : conc' M C)).
- : trans-sound topR (tc t-true) trueR'.
- : trans-sound 1R (tc t+true) trueR'.
- : trans-sound (0L H) _ (notL' trueR' H')
     <- trans-soundhyp H t+false H'.
- : trans-sound (0L H) _ (weakR' (notL' trueR' H'))
     <- trans-soundhyp H t+false H'.
- : trans-sound (*R D1 D2) (tc (t+and T1 T2)) (/\R' E1 E2)
     <- trans-sound D1 (tc T1) E1
     <- trans-sound D2 (tc T2) E2.
- : trans-sound (*L D H) T (/\L' ([h1][h2] E h1 h2) H')
     <- trans-soundhyp H (t+and Th1 Th2) H'
     <- ({h1}{h1'} trans-soundhyp h1 Th1 h1'
           -> {h2}{h2'} trans-soundhyp h2 Th2 h2'
           -> trans-sound (D h1 h2) T (E h1' h2')).
- : trans-sound (&R D1 D2) (tc (t-and T1 T2)) (/\R' E1 E2)
     <- trans-sound D1 (tc T1) E1
     <- trans-sound D2 (tc T2) E2.
- : trans-sound (&L1 D H) T (/\L' ([h1][h2] E h1) H')
     <- trans-soundhyp H (t-and Th _) H'
     <- ({h}{h'} trans-soundhyp h Th h'
           -> trans-sound (D h) T (E h')).
- : trans-sound (&L2 D H) T (/\L' ([h1][h2] E h2) H')
     <- trans-soundhyp H (t-and _ Th) H'
     <- ({h}{h'} trans-soundhyp h Th h'
           -> trans-sound (D h) T (E h')).
- : trans-sound (+R1 D) (tc (t+or T _)) (\/R1' E)
     <- trans-sound D (tc T) E.
- : trans-sound (+R2 D) (tc (t+or _ T)) (\/R2' E)
     <- trans-sound D (tc T) E.
- : trans-sound (+L D1 D2 H) T (\/L' E1 E2 H')
     <- trans-soundhyp H (t+or Th1 Th2) H'
     <- ({h1}{h1'} trans-soundhyp h1 Th1 h1'
           -> trans-sound (D1 h1) T (E1 h1'))
     <- ({h2}{h2'} trans-soundhyp h2 Th2 h2'
           -> trans-sound (D2 h2) T (E2 h2')).
- : trans-sound (-oR D) (tc (t-imp T1 T2)) (=>R' E)
     <- ({h}{h'} trans-soundhyp h T1 h'
           -> trans-sound (D h) (tc T2) (E h')).
- : trans-sound (-oR D) (tc (t+not T)) (notR' E)
     <- ({h: hyp A}{h': hyp' A'} trans-soundhyp h T h'
           -> trans-sound (D h) tc# (E h')).

trans-imp : {D: conc C}
          idconc D (-oL (D1: true A1) (D2: hyp A2 -> conc C) H)
          -> trans-conc Mt C' C 
          -> trans Mh A' neg (A1 -o A2)
          -> hyp' A'
          -> conc' Md C'
          -> type.
%mode trans-imp +D +Id +T +Th +H -F.
- : trans-imp (-oL D1 D2 H) idconc/refl T (t-imp Th1 Th2) H' (=>L' E1 E2 H')
     <- trans-sound D1 (tc Th1) E1
     <- ({h}{h'} trans-soundhyp h Th2 h'
           -> trans-sound (D2 h) T (E2 h')).
- : trans-imp (-oL D1 D2 H) idconc/refl T (t+not Th) (H': hyp' (not' A')) 
     (weakR' (notL' E1 H'))
     <- trans-sound D1 (tc Th) (E1: true' Md A').
- : trans-imp (-oL D1 D2 H) idconc/refl tc# (t+not Th) (H': hyp' (not' A')) 
     (notL' E1 H')
     <- trans-sound D1 (tc Th) (E1: true' Md A').

- : trans-sound (-oL D1 D2 H) T F
     <- trans-soundhyp H Th H'
     <- trans-imp (-oL D1 D2 H) idconc/refl T Th H' F.
- : trans-sound (circR D) (tc (t+circ T)) E
     <- trans-sound D (tclax T) E.
- : trans-sound (circL D H) (tclax T) (circL' E H')
     <- trans-soundhyp H (t+circ Th) H'
     <- ({h}{h'} trans-soundhyp h Th h'
           -> trans-sound (D h) (tclax T) (E h')).

%worlds (bl_atmpos | bl_atmneg | bl_trans-soundhyp) 
  (trans-sound _ _ _) (trans-imp _ _ _ _ _ _).
%total (D E) (trans-imp E _ _ _ _ _) (trans-sound D _ _).

%{ === Completeness === }% 

%{ * If <math>\Gamma' \vdash \Delta</math> and <math>\Gamma'~\texttt{trans}~\Gamma</math> and <math>\Delta~\texttt{trans}~J</math>, then <math>\Gamma \vdash J</math>.

By lexographic induction on the first derivation's metric and then
the second derivation's metric. For every left rule, we need a mutually
inductive lemma that strips off any unnecessary shifts from the translation
of the hypothesis; within these lemmas, the first derivation will always
stay the same, but the derivation of the translation of the hypothesis
will get smaller. }%

trans-compl : {Td}{Tt}
               conc' Td D -> trans-conc Tt D J -> conc J -> type.
%mode trans-compl +Td +Tt +D +T -E.

%abbrev trans-compl'  
   = [d: conc' Td D][t: trans-conc Tt D J][e: conc J] 
      trans-compl Td Tt d t e.

%{ ==== Shifts ==== }%

- : trans-compl' D (tc (t+- T)) (upR E) 
     <- trans-compl' D (tc T) E.

- : trans-compl' D (tc (t-+ T)) (downR E)
     <- trans-compl' D (tc T) E.

%{ ==== Truth ==== }%

- : trans-compl' trueR' (tc t+true) 1R.
- : trans-compl' trueR' (tc t-true) topR.

%{ ==== Conjunction ==== }%

- : trans-compl' (/\R' D1 D2) (tc (t+and T1 T2)) (*R E1 E2)
     <- trans-compl' D1 (tc T1) E1
     <- trans-compl' D2 (tc T2) E2.

- : trans-compl' (/\R' D1 D2) (tc (t-and T1 T2)) (&R E1 E2)
     <- trans-compl' D1 (tc T1) E1
     <- trans-compl' D2 (tc T2) E2.

trans-andL : {TD}{Th} id TD (x Td)
              -> (hyp' M1 -> hyp' M2 -> conc' Td D)
              -> trans-conc Tt D J
              -> trans Th (M1 /\ M2) S A
              -> (hyp A -> conc J) -> type.
%mode trans-andL +TD +Th +Id +D +T +Th -E.
- : trans-andL _ _ id/refl (D : hyp' M1 -> hyp' M2 -> conc' Td D')
     (T: trans-conc Tt D' J) (t-and T1 T2) 
     ([h] (&L1 ([h1] &L2 ([h2] E h1 h2) h) h))
     <- ({h1'}{h1} trans-complhyp h1' T1 h1
           -> {h2'}{h2} trans-complhyp h2' T2 h2
           -> trans-compl' (D h1' h2') T (E h1 h2)).
- : trans-andL _ _ id/refl (D: hyp' M1 -> hyp' M2 -> conc' Td D') 
     (T: trans-conc Tt D' J) (t+and T1 T2) 
     ([h] (*L ([h1][h2] E h1 h2) h))
     <- ({h1'}{h1} trans-complhyp h1' T1 h1
           -> {h2'}{h2} trans-complhyp h2' T2 h2
           -> trans-compl' (D h1' h2') T (E h1 h2)).
- : trans-andL _ _ Id D T (t+- Th) (upL E)
     <- trans-andL _ _ Id D T Th E.
- : trans-andL _ _ Id D T (t-+ Th) (downL E)
     <- trans-andL _ _ Id D T Th E.

- : trans-compl' (/\L' D H') T (E H)
     <- trans-complhyp H' Th (H: hyp A)
     <- trans-andL _ _ id/refl D T Th (E: hyp A -> conc D').

%{ ==== Disjunction ==== }%

- : trans-compl' (\/R1' (D: true' Tt M1)) (tc (t+or T1 _)) (+R1 E)
     <- trans-compl' D (tc T1) E.
- : trans-compl' (\/R2' (D: true' Tt M2)) (tc (t+or _ T2)) (+R2 E)
     <- trans-compl' D (tc T2) E.

trans-orL : {TD}{Th} id (TD) (Td1 | Td2)
             -> (hyp' M1 -> conc' Td1 D')
             -> (hyp' M2 -> conc' Td2 D')
             -> trans-conc Tt D' J
             -> trans Th (M1 \/ M2) S A
             -> (hyp A -> conc J) -> type.
%mode trans-orL +TD +Th +Id +D1 +D2 +T +Th -E.
- : trans-orL _ _ id/refl D1 D2 T (t+or Th1 Th2) (+L ([h1] E1 h1) ([h2] E2 h2))
     <- ({h1': hyp' M1}{h1: hyp P1} trans-complhyp h1' Th1 h1
           -> trans-compl' (D1 h1') T (E1 h1: conc J))
     <- ({h2': hyp' M2}{h2: hyp P2} trans-complhyp h2' Th2 h2
           -> trans-compl' (D2 h2') T (E2 h2: conc J)).
- : trans-orL _ _ id/refl D1 D2 T (t+- Th) (upL E)
     <- trans-orL _ _ id/refl D1 D2 T Th E.
- : trans-orL _ _ id/refl D1 D2 T (t-+ Th) (downL E)
     <- trans-orL _ _ id/refl D1 D2 T Th E.

- : trans-compl' (\/L' D1 D2 H') T (E H)
     <- trans-complhyp H' Th H
     <- trans-orL _ _ id/refl D1 D2 T Th E.

%{ ==== Implication ==== }%

- : trans-compl' (=>R' (D: hyp' M1 -> true' Tt M2)) (tc (t-imp T1 T2)) (-oR E)
     <- ({h'}{h} trans-complhyp h' T1 h
           -> trans-compl' (D h') (tc T2) (E h)).

trans-impL : {TD}{Th} id TD (Td1 | Td2)
              -> true' Td1 M1
              -> (hyp' M2 -> conc' Td2 D')
              -> trans-conc Tt D' J
              -> trans Th (M1 => M2) S A
              -> (hyp A -> conc J) -> type.
%mode trans-impL +TD +Th +Id +D1 +D2 +T +Th -E.
- : trans-impL _ _ id/refl (D1: true' Td1 M1) (D2: hyp' M2 -> conc' Td2 D')
     (T: trans-conc Mt D' J) (t-imp T1 T2) (-oL E1 ([h] E2 h))
     <- trans-compl' D1 (tc T1) (E1: true P)
     <- ({h': hyp' M2}{h: hyp N}{t: trans-complhyp h' T2 h}
           trans-compl' (D2 h') T (E2 h: conc J)).
- : trans-impL _ _ id/refl D1 D2 T (t+- Th) (upL E)
     <- trans-impL _ _ id/refl D1 D2 T Th E.
- : trans-impL _ _ id/refl D1 D2 T (t-+ Th) (downL E)
     <- trans-impL _ _ id/refl D1 D2 T Th E.

- : trans-compl' (=>L' D1 D2 (H': hyp' (M1 => M2))) T (E H)
     <- trans-complhyp H' Th (H: hyp A)
     <- trans-impL _ _ id/refl D1 D2 T Th E.

%{ ==== Negation ==== }%

- : trans-compl' (notR' (D: hyp' tt' -> # _)) (tc t+false) G
     <- ({h'}{h} trans-complhyp h' t+true h
           -> trans-compl' (D h') tc# (E h))
     <- cut 1 1R ([h] E h) F
     <- invupR F G.

- : trans-compl' (notR' (D: hyp' M -> # _)) (tc (t+not T)) (-oR ([h] (E h)))
     <- ({h'}{h} trans-complhyp h' T h
           -> trans-compl' (D h') tc# (E h)).

trans-notL : {TD}{Tt} id TD (x Td)
              -> true' Td M
              -> trans Tt (not' M) S A
              -> (hyp A -> true (up 0)) -> type.
%mode trans-notL +TD +Tt +Id +D +Th -E.
- : trans-notL _ _ id/refl (D: true' Td M) (t+not T) (-oL E (upL 0L))
     <- trans-compl' D (tc T) (E: true P).
- : trans-notL _ _ id/refl D t+false 0L.
- : trans-notL _ _ Id D (t+- T) (upL E)
     <- trans-notL _ _ Id D T E.
- : trans-notL _ _ Id D (t-+ T) (downL E)
     <- trans-notL _ _ Id D T E.

- : trans-compl' (notL' (D: true' Td M) (H': hyp' (not' M))) tc# (E H)
     <- trans-complhyp H' Th (H: hyp A)
     <- trans-notL _ _ id/refl D Th E.

%{ ==== Lax modality ==== }%

- : trans-compl' (circR' D) (tc (t+circ T)) (circR (laxR E))
     <- trans-compl' D (tc T) E.
- : trans-compl' (circR' D) (tclax T) (laxR E)
     <- trans-compl' D (tc T) E.

trans-circL : {TD}{Th} id TD (x Td)
               -> (hyp' M -> true' Td (circ' D'))
               -> trans Tt D' S C
               -> trans Th (circ' M) Sh A
               -> (hyp A -> lax C) -> type.
%mode trans-circL +TD +Tt +Id +D +T +Th -E. 
- : trans-circL _ _ id/refl D T (t+circ Th) (circL E)
     <- ({h': hyp' M}{h: hyp P}{t: trans-complhyp h' Th h}
           trans-compl' (D h') (tclax T) (E h : lax C)).
- : trans-circL _ _ Id D T (t+- Th) (upL F)
     <- trans-circL _ _ Id D T Th F.
- : trans-circL _ _ Id D T (t-+ Th) (downL F)
     <- trans-circL _ _ Id D T Th F.

- : trans-compl' (circL' (D: hyp' M -> true' Td (circ' D')) H')
     (tc (t+circ (T: trans Tt D' pos J))) (circR (E H))
     <- trans-complhyp H' Th (H: hyp A)
     <- trans-circL _ _ id/refl D T Th E.

- : trans-compl' (circL' (D: hyp' M -> true' Td (circ' D')) H')
     (tclax (T: trans Tt D' S J)) (E H)
     <- trans-complhyp H' Th (H: hyp A)
     <- trans-circL _ _ id/refl D T Th E.

%{ ==== Structural Rules ==== }%

%{ For translating a cut, we need to come up with a translation of a source
logc expression to a target logic expression; we have already established
this was possible when we proved <tt>can-trans</tt> to show that translation
was left-total. }%

- : trans-compl' (cut' (Da: true' _ M) Dc) T F
     <- can-trans M (TRa: trans _ M S A)
     <- trans-compl' Da (tc TRa) (Ea: true A)
     <- ({h'}{h} trans-complhyp h' TRa h
           -> trans-compl' (Dc h') T (Ec h))
     <- cut A Ea Ec F.

%{ Due to the mismatch between
the lax judgment and the circle, we need three cases for translating identity. 
The first case is the most important one and is straightforward, however: we
are translating <math>\Gamma', M \vdash M</math> and need to show
<math>\Gamma, A_M \vdash A_M~true</math>, 
where <math>M~\texttt{trans}~A_M</math>. 

Identity is a terminal rule, so we will not use induction here. 
We know because <math>M</math> is a hypothesis that there is 
a hypothesis <math>A</math> such that 
<math>M~\texttt{trans}~A</math>, and so by the identity principle we can prove
<math>\Gamma, A \vdash A~true</math>; then, <tt>trans-equiv</tt> allows
us to prove <math>\Gamma, A_M \vdash A_M~true</math>, which is what we 
actually need. }%

- : trans-compl' (id' (H': hyp' M)) (tc (T: trans _ M S Am)) E
     <- trans-complhyp H' Th (H: hyp A)
     <- identity A (D2: hyp A -> true A)
     <- trans-equiv Th (D2 H) T (E: true Am).

%{ When we are translating to a lax judgment in the target language, what we
get out of the translation isn't exactly what we want, we need
<math>\Gamma \vdash A~lax</math> but the best we can get is 
<math>\Gamma \vdash {\bigcirc}P~true</math> or 
<math>\Gamma \vdash {\bigcirc}{\downarrow}N~true</math>. However, we can 
use inversion lemmas (and lax cut, in the second case) to get what we need.
}%

- : trans-compl' (id' (H': hyp' (circ' M))) (tclax (T: trans _ M pos Pm)) F
     <- trans-complhyp H' Th (H: hyp P)
     <- identity P (D2: hyp P -> true P)
     <- trans-equiv Th (D2 H) (t+circ T) (E: true (circ Pm))
     <- invcircR E (F: lax Pm).
- : trans-compl' (id' (H': hyp' (circ' M))) (tclax (T: trans _ M neg Nm)) G
     <- trans-complhyp H' Th (H: hyp N)
     <- identity N (D2: hyp N -> true N)
     <- trans-equiv Th (D2 H) (t+circ (t-+ T)) (E: true (circ (down Nm)))
     <- invcircR E (F: lax (down Nm))
     <- identity _ (Id: hyp Nm -> true Nm)
     <- lcut _ F ([h] laxR (downL ([h'] Id h') h)) (G: lax Nm).

- : trans-compl' (weakR' D) _ F
     <- trans-compl' D tc# E
     <- cut (up 0) E ([h] upL 0L h) F.

%worlds (bl_atmpos | bl_atmneg | bl_trans-complhyp) 
 (trans-compl _ _ _ _ _)
 (trans-andL _ _ _ _ _ _ _)
 (trans-impL _ _ _ _ _ _ _ _)
 (trans-orL _ _ _ _ _ _ _ _)
 (trans-notL _ _ _ _ _ _)
 (trans-circL _ _ _ _ _ _ _).

%total {(D1 D2 D3 D4 D5 D6) (T1 T2 T3 T4 T5 T6)}
 (trans-compl D1 T1 _ _ _)
 (trans-andL D2 T2 _ _ _ _ _)
 (trans-orL D3 T3 _ _ _ _ _ _)
 (trans-impL D4 T4 _ _ _ _ _ _)
 (trans-notL D5 T5 _ _ _ _)
 (trans-circL D6 T6 _ _ _ _ _).