$`\newcommand{\LLambda}{\mathrm{L}\Lambda}
\newcommand{\Llambda}{\mathrm{L}\lambda}
\newcommand{\RLambda}{\mathrm{R}\Lambda}
\newcommand{\Rlambda}{\mathrm{R}\lambda}
\newcommand{\Dia}{\diamondsuit}
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\conc}{\mathop{\#} }
\newcommand{\Subst}[1]{ \begin{bmatrix} #1 \end{bmatrix} }
%`$
次のオペレーターを考える。$`\alpha, \beta\in \mrm{TypeCtx}`$
- $`\Dia_\alpha^\beta : \mrm{Prop}[\alpha]\to \mrm{Prop}[\alpha\conc\beta]`$
- $`\forall_\alpha^\beta : \mrm{Prop}[\alpha\conc\beta]\to \mrm{Prop}[\alpha]`$
- $`\exists_\alpha^\beta : \mrm{Prop}[\alpha\conc\beta]\to \mrm{Prop}[\alpha]`$
命題レベルの左右カリー化。$`\Gamma, \Delta \in \mrm{PropCtx}, Q\in \mrm{Prop}`$
- $`\LLambda_{\Gamma, Q}^\Delta: \mrm{MultiDeriv}(\Delta\conc\Gamma, Q) \to \mrm{MultiDeriv}(\Gamma, [\Delta\triangleright Q])`$
- $`\RLambda_{\Gamma, Q}^\Delta: \mrm{MultiDeriv}(\Gamma\conc\Delta, Q) \to \mrm{MultiDeriv}(\Gamma, [Q \triangleleft \Delta])`$
関数レベルの左右カリー化。$`\alpha, \beta \in \mrm{TypeCtx}, Y\in \mrm{Type}`$
- $`\Llambda_{\alpha, Y}^\beta: \mrm{MultiFunc}(\beta\conc\alpha, Y) \to \mrm{MultiFunc}(\alpha, [\beta \triangleright Y])`$
- $`\Rlambda_{\alpha, Y}^\beta: \mrm{MultiFunc}(\alpha\conc\beta) \to \mrm{MultiFunc}(\alpha, [Y\triangleleft \beta])`$
多関数 $`f:\alpha \to \beta`$ による置換
- $`f^*: \mrm{Prop}[\beta] \to \mrm{Prop}[\alpha]`$
- $`f^* Q = Q\Subst{f}`$
これに加えて:
- 連言の濃縮・希釈 バンチ演算
- 選言の濃縮・希釈 バンチ演算
- 全称命題の濃縮・希釈 拡大バンチ演算
- 存在命題の濃縮・希釈 拡大バンチ演算
- 同値置換 プレポスト結合 知識ベース使用 バンチ演算
- 各種のマージ 導出への演算
- ド・モルガン双対移動 導出への演算
- プレ結合 知識ベース使用 導出への演算
- ポスト結合 知識ベース使用 導出への演算
- カット