Skip to content

Commit

Permalink
Tap
Browse files Browse the repository at this point in the history
  • Loading branch information
imbrem committed Aug 12, 2024
1 parent 4e21dbd commit de0cf13
Showing 1 changed file with 14 additions and 13 deletions.
27 changes: 14 additions & 13 deletions paper.tex
Original file line number Diff line number Diff line change
Expand Up @@ -1309,24 +1309,25 @@ \subsection{Regions}
: \ms{L}}
}
\\
% % TODO: derivable, but prove this!
% % TODO: derivable from ucfg, but prove this!
% \prftree[r]{\rle{cfg$_0$}}
% {\haslb{\Gamma}{r}{\ms{L}}}
% {\lbeq{\Gamma}{\where{r}{}}{r}{\ms{L}}}
% \\
% TODO: derivable from dinaturality?
\prftree[r]{\rle{wk-cfg}}
{\haslb{\Gamma}{[\ell_i \mapsto \ell_{\rho\;i}]r}{\ms{L}, (\lhyp{\ell_i}{A_i},)_i}}
{\forall i, \haslb{\Gamma, \bhyp{x_i}{A_i}}
{[\ell_i \mapsto \ell_{\rho\;i}]t_i}
{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\lbeq{\Gamma}
{\where{[\ell_i \mapsto \ell_{\rho i}]r}
{(\lwbranch{\ell_i}{x_i}{[\ell_i \mapsto \ell_{\rho\;i}]r})_i}}
{\where{r}{(\lwbranch{\ell_{\rho\;i}}{x_i}{r})_i}}
{\ms{L}}}
\\
% TODO: probably derivable from dinaturality? but prove...
% \prftree[r]{\rle{wk-cfg}}
% {\haslb{\Gamma}{[\ell_i \mapsto \ell_{\rho\;i}]r}{\ms{L}, (\lhyp{\ell_i}{A_i},)_i}}
% {\forall i, \haslb{\Gamma, \bhyp{x_i}{A_i}}
% {[\ell_i \mapsto \ell_{\rho\;i}]t_i}
% {\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
% {\lbeq{\Gamma}
% {\where{[\ell_i \mapsto \ell_{\rho i}]r}
% {(\lwbranch{\ell_i}{x_i}{[\ell_i \mapsto \ell_{\rho\;i}]r})_i}}
% {\where{r}{(\lwbranch{\ell_{\rho\;i}}{x_i}{r})_i}}
% {\ms{L}}}
% \\
% TODO: note difference between this and wk-cfg
% TODO: think about whether _this_ is derivable... maybe from dinaturality too?
\prftree[r]{\rle{dead-cfg}}
{\haslb{\Gamma}{r}{\ms{L}, (\lhyp{\ell_i}{A_i},)_i}}
{\forall i, \haslb{\Gamma, \bhyp{x_i}{A_i}}{t_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
Expand Down

0 comments on commit de0cf13

Please sign in to comment.