Flexion unit4: gaxitの性質
前の記事
の記法を用いる. Bimould$A,B,C$に対し,
\begin{align}
\gaxit(B,C)(A)(\bw):=\sum_{\substack{0\leq s\\\ba_1b_1\bc_1\cdots \ba_sb_s\bc_s=\bw}}A({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_s}\lceil b_s\rceil_{\bc_s})\prod_{i=1}^sB(\ba_i\rfloor_{b_i})C({}_{b_i}\lfloor \bc_i)
\end{align}
と定義する. ただし, $\ba$のような太字は任意の長さのbiword, $b$のように太字でないものは長さ1のbiwordとする. この定義はEcalleの論文におけるものと一般には一致していないが, $B(\varnothing)=C(\varnothing)=1$の場合は一致しており, 扱いやすいこともあるので, 今回はこの定義を用いることにする.
$\gaxit$の性質
\begin{align}
\gaxit(B,C)(A_1\times A_2)=\gaxit(B,C)(A_1)\times \gaxit(B,C)(A_2)
\end{align}
が成り立つ.
\begin{align}
&\gaxit(B,C)(A_1\times A_2)(\bw)\\
&=\sum_{\substack{0\leq s\\\ba_1b_1\bc_1\cdots \ba_sb_s\bc_s=\bw}}(A_1\times A_2)({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_s}\lceil b_s\rceil_{\bc_s})\prod_{i=1}^sB(\ba_i\rfloor_{b_i})C({}_{b_i}\lfloor \bc_i)\\
&=\sum_{\substack{0\leq s\\\ba_1b_1\bc_1\cdots \ba_sb_s\bc_s=\bw}}\sum_{j=0}^sA_1({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_j}\lceil b_j\rceil_{\bc_j})A_2({}_{\ba_{j+1}}\lceil b_{j+1}\rceil_{\bc_{j+1}},\dots,{}_{\ba_s}\lceil b_s\rceil_{\bc_s})\prod_{i=1}^sB(\ba_i\rfloor_{b_i})C({}_{b_i}\lfloor \bc_i)\\
&=\sum_{\bx\by=\bw}\sum_{\substack{0\leq s\\\ba_1b_1\bc_1\cdots \ba_sb_s\bc_s=\bx}}A_1({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_s}\lceil b_s\rceil_{\bc_s})\prod_{i=1}^sB(\ba_i\rfloor_{b_i})C({}_{b_i}\lfloor \bc_i)\\
&\qquad\cdot\sum_{\substack{0\leq t\\\ba_1b_1\bc_1\cdots \ba_tb_t\bc_t=\by}}A_2({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_t}\lceil b_t\rceil_{\bc_t})\prod_{i=1}^tB(\ba_i\rfloor_{b_i})C({}_{b_i}\lfloor \bc_i)\\
&=(\gaxit(B,C)(A_1)\times \gaxit(B,C)(A_2))(\bw)
\end{align}
と示される.
\begin{align}
\gaxi((A,B),(C,D)):=(\gaxit(C,D)(A)\times C, D\times \gaxit(C,D)(B))
\end{align}
とする. このとき, 以下が成り立つ.
\begin{align}
\gaxit(C,D)\circ \gaxit(A,B)=\gaxit(\gaxi((A,B),(C,D)))
\end{align}
が成り立つ.
証明を見やすくするために, biwordの線形和を
\begin{align}
g_{A,B}(\bw)&:=\sum_{\substack{0\leq s\\\ba_1b_1\bc_1\cdots \ba_sb_s\bc_s=\bw}}({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_s}\lceil b_s\rceil_{\bc_s})\prod_{i=1}^sA(\ba_i\rfloor_{b_i})B({}_{b_i}\lfloor \bc_i)\\
\psi_{A,B}(\bw)&:=\sum_{\ba b\bc=\bw}A(\ba\rfloor_b){}_{\ba}\lceil b\rceil_{\bc}B({}_b\lfloor \bc)
\end{align}
とする. このとき, 定義から
\begin{align}
g_{A,B}(\bw)=\sum_{\substack{0\leq n\\\ba_1\cdots\ba_n=\bw}}\psi_{A,B}(\ba_1)\cdots \psi_{A,B}(\ba_n)
\end{align}
と表される. よって,
\begin{align}
(g_{A,B}\circ g_{C,D})(\bw)&=\sum_{\substack{0\leq n\\\ba_1\cdots\ba_n=\bw}}g_{A,B}(\psi_{C,D}(\ba_1)\cdots \psi_{C,D}(\ba_n))\\
&=\sum_{\substack{0\leq n\\\ba_1\cdots\ba_n=\bw}}\sum_{\substack{0\leq m\\0=i_0< i_1<\cdots< i_{m-1}< i_m=n}}\prod_{j=1}^m\psi_{A,B}(\psi_{C,D}(\ba_{i_{j-1}+1})\cdots \psi_{C,D}(\ba_{i_j}))\\
&=\sum_{\substack{0\leq m\\\bb_1\cdots\bb_m=\bw}}\prod_{j=1}^m\left(\sum_{\substack{0\leq n\\\ba_1\cdots\ba_n=\bb_i}}\psi_{A,B}(\psi_{C,D}(\ba_1)\cdots\psi_{C,D}(\ba_n))\right)
\end{align}
ここで,
\begin{align}
&\sum_{\substack{0\leq n\\\ba_1\cdots\ba_n=\bw}}\psi_{A,B}(\psi_{C,D}(\ba_1)\cdots\psi_{C,D}(\ba_n))\\
&=\sum_{\substack{0\leq n\\\ba_1b_1\bc_1\cdots \ba_nb_n\bc_n=\bw}}\psi_{A,B}({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_n}\lceil b_n\rceil_{\bc_n})\prod_{i=1}^nC(\ba_i\rfloor_{b_i})D({}_{b_i}\lfloor \bc_i)\\
&=\sum_{\substack{0\leq n\\\ba_1b_1\bc_1\cdots \ba_nb_n\bc_n=\bw}}\sum_{i=1}^nA(({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_{i-1}}\lceil b_{i-1}\rceil_{\bc_{i-1}})\rfloor_{b_i}) {}_{\ba_1b_1\bc_1\cdots \ba_{i}}\lceil b_i\rceil_{\bc_i\cdots \ba_nb_n\bc_n}\\
&\qquad\cdot B({}_{b_i}\lfloor({}_{\ba_{i+1}}\lceil b_{i+1}\rceil_{\bc_{i+1}},\dots,{}_{\ba_{n}}\lceil b_{n}\rceil_{\bc_{n}}))\prod_{i=1}^nC(\ba_i\rfloor_{b_i})D({}_{b_i}\lfloor \bc_i)\\
&=\sum_{\ba b\bc=\bw}{}_{\ba}\lceil b\rceil_{\bc}\sum_{\substack{0\leq n\\\ba_1b_1\bc_1\cdots\ba_nb_n\bc_n\ba_{n+1}=\ba}}A(({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_n}\lceil b_n\rceil_{\bc_n})\rfloor_{b})\left(\prod_{i=1}^nC(\ba_i\rfloor_{b_i})D({}_{b_i}\lfloor \bc_i)\right)C(\ba_{n+1}\rfloor_{b})\\
&\qquad\cdot\sum_{\substack{0\leq n\\\bc_0\ba_1b_1\bc_1\cdots\ba_nb_n\bc_n=\bb}}B({}_b\lfloor({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_n}\lceil b_n\rceil_{\bc_n}))D({}_b\lfloor\bc_0)\left(\prod_{i=1}^nC(\ba_i\rfloor_{b_i})D({}_{b_i}\lfloor \bc_i)\right)\\
&=\sum_{\ba b\bc=\bw}{}_{\ba}\lceil b\rceil_{\bc}(\gaxit(C,D)(A)\times C)(\ba\rfloor_b)(D\times\gaxit(C,D)(B))({}_b\lfloor\bc)\\
&=\psi_{\gaxi((A,B),(C,D))}(\bw)
\end{align}
となる. よって,
\begin{align}
(g_{A,B}\circ g_{C,D})(\bw)
&=\sum_{\substack{0\leq m\\\bb_1\cdots\bb_m=\bw}}\prod_{j=1}^m\psi_{\gaxi((A,B),(C,D))}(\bb_j)=g_{\gaxi((A,B),(C,D))}(\bw)
\end{align}
である. $\gaxit(A,B)(M)=M\circ g_{A,B}$であるから, これは
\begin{align}
(\gaxit(C,D)\circ \gaxit(A,B))(M)=\gaxit(\gaxi((A,B),(C,D)))(M)
\end{align}
と書き換えられ, 示すべき等式が得られる.
\begin{align} \swap(\gaxit(\swap(B),\swap(C))(\swap(A))\times \swap(B))=\gaxit(B,\push(C))(A)\times B \end{align}
命題2の証明における記法をここでも用いる.
\begin{align}
&\swap(\gaxit(\swap(B),\swap(C))(\swap(A))\times \swap(B))\left(w_1,\dots,w_r\right)\\
&=(\gaxit(\swap(B),\swap(C))(\swap(A))\times \swap(B))\left(\begin{matrix}v_r,v_{r-1}-v_r,\dots,v_1-v_2\\u_1+\cdots+u_r,\dots,u_1+u_2,u_1\end{matrix}\right)\\
&=\sum_{\substack{0\leq n\\\ba_1\cdots\ba_{n+1}=\left(\begin{matrix}v_r,v_{r-1}-v_r,\dots,v_1-v_2\\u_1+\cdots+u_r,\dots,u_1+u_2,u_1\end{matrix}\right)}}\swap(A)(\psi_{\swap(B),\swap(C)}(\ba_1)\cdots \psi_{\swap(B),\swap(C)}(\ba_n))\swap(B)(\ba_{n+1})
\end{align}
である. ここで, $j> i$に対し,
\begin{align}
&\psi_{\swap(B),\swap(C)}\left(\begin{matrix}v_{j-1}-v_{j},\dots,v_{i}-v_{i+1}\\u_1+\cdots+u_{j-1},\cdots,u_1+\cdots+u_{i}\end{matrix}\right)\\
&=\sum_{k=i}^{j-1}\left(v_i-v_{j}\atop u_1+\cdots+u_k\right)\swap(B)\left(\begin{matrix}v_{j-1}-v_{j},\dots,v_{k+1}-v_{k+2}\\u_{k+1}+\cdots+u_{j-1},\cdots,u_{k+1}\end{matrix}\right)\swap(C)\left(\begin{matrix}v_{k-1}-v_{k},\dots,v_{i}-v_{i+1}\\-u_k,\dots,-u_{i+1}-\cdots-u_{k}\end{matrix}\right)\\
&=\sum_{k=i}^{j-1}\left(v_i-v_{j}\atop u_1+\cdots+u_k\right)B\left(\begin{matrix}u_{k+1},\dots,u_{j-1}\\v_{k+1}-v_{j},\dots,v_{j-1}-v_{j}\end{matrix}\right)C\left(\begin{matrix}-u_{i+1}-\cdots-u_k,u_{i+1},\dots,u_{k-1}\\v_i-v_k,\dots,v_{k-1}-v_k\end{matrix}\right)\\
&=\sum_{k=i}^{j-1}\left(v_i-v_{j}\atop u_1+\cdots+u_k\right)B\left((w_{k+1}\cdots w_{j-1})\rfloor_{w_{j}}\right)\push(C)\left(\begin{matrix}u_{i+1},\dots,u_{k}\\v_{i+1}-v_i,\dots,v_k-v_i\end{matrix}\right)\\
&=\sum_{k=i}^{j-1}\left(v_i-v_{j}\atop u_1+\cdots+u_k\right)\push(C)({}_{w_i}\lfloor(w_{i+1}\cdots w_{k})))B\left((w_{k+1}\cdots w_{j-1})\rfloor_{w_{j}}\right)
\end{align}
となることを用いると(形式的に$w_{r+1}:=\left(0\atop 0\right)$と見なす),
\begin{align}
&\sum_{\substack{0\leq n\\\ba_1\cdots\ba_{n+1}=\left(\begin{matrix}v_r,v_{r-1}-v_r,\dots,v_1-v_2\\u_1+\cdots+u_r,\dots,u_1+u_2,u_1\end{matrix}\right)}}\swap(A)(\psi_{\swap(B),\swap(C)}(\ba_1)\cdots \psi_{\swap(B),\swap(C)}(\ba_n))\swap(B)(\ba_{n+1})\\
&=\sum_{\substack{0\leq n\\1\leq j_1<\cdots< j_n< j_{n+1}=r+1\\1\leq \forall l\leq n, j_l\leq k_l< j_{l+1}}}\swap(A)\left(\begin{matrix}v_{j_n},v_{j_{n-1}}-v_{j_n},\dots,v_{j_1}-v_{j_2}\\u_{1}+\cdots+u_{k_n},\dots,u_1+\cdots+u_{k_1}\end{matrix}\right)\\
&\qquad\cdot B((w_1\cdots w_{j_1-1})\rfloor_{w_{j_1}})\prod_{i=1}^n\push(C)({}_{w_{j_i}}\lfloor(w_{j_i+1}\cdots w_{k_i}))B((w_{k_i+1}\cdots w_{j_i-1})\rfloor_{w_{j_{i+1}}})\\
&=\sum_{\substack{0\leq n\\1\leq j_1<\cdots< j_n< j_{n+1}=r+1\\1\leq \forall l\leq n, j_l\leq k_l< j_{l+1}\\k_0=0}}A\left(\begin{matrix}u_1+\cdots+u_{k_1},u_{k_1+1}+\cdots+u_{k_2},\dots,u_{k_{n-1}+1}+\cdots+u_{k_n}\\v_{j_1},v_{j_2},\dots,v_{j_n}\end{matrix}\right)\\
&\qquad\cdot \left(\prod_{i=1}^nB((w_{k_{i-1}+1}\cdots w_{j_i-1})\rfloor_{w_{j_i}})\push(C)({}_{w_{j_i}}\lfloor(w_{j_i+1}\cdots w_{k_i}))\right)B(w_{k_n+1}\cdots w_r)\\
&=(\gaxit(B,\push(C))(A)\times B)(\bw)
\end{align}
となって示すべき等式が得られた.
群構造
$\gaxi$は結合的である. つまり,
\begin{align}
&\gaxi((A_1,A_2),\gaxi((B_1,B_2),(C_1,C_2)))\\
&=\gaxi(\gaxi((A_1,A_2),(B_1,B_2)),(C_1,C_2))
\end{align}
が成り立つ.
命題2を用いると,
\begin{align}
&\gaxi((A_1,A_2),\gaxi((B_1,B_2),(C_1,C_2)))\\
&=(\gaxit(\gaxi((B_1,B_2),(C_1,C_2)))(A_1)\times (\gaxit(C_1,C_2)(B_1)\times C_1),\\
&\qquad(C_2\times\gaxit(C_1,C_2)(B_2))\times\gaxit(\gaxi((B_1,B_2),(C_1,C_2))(A_2))\\
&=((\gaxit(C_1,C_2)\circ\gaxit(B_1,B_2))(A_1)\times \gaxit(C_1,C_2)(B_1)\times C_1,\\
&\qquad C_2\times\gaxit(C_1,C_2)(B_2)\times(\gaxit(C_1,C_2)\circ\gaxit(B_1,B_2))(A_2))\\
\end{align}
となる. ここで, 命題1を用いると,
\begin{align}
&\gaxi((A_1,A_2),\gaxi((B_1,B_2),(C_1,C_2)))\\
&=((\gaxit(C_1,C_2)(\gaxit(B_1,B_2)(A_1)\times B_1)\times C_1,\\
&\qquad C_2\times\gaxit(C_1,C_2)(B_2\times\gaxit(B_1,B_2)(A_2)))\\
&=\gaxi(\gaxi((A_1,A_2),(B_1,B_2)),(C_1,C_2))
\end{align}
となって示すべき等式を得る.
$M(\varnothing)=1$となるようなbimould全体を$\MU$と表す. $\gaxi((1,1),(A,B))=\gaxi((A,B),(1,1))=(A,B)$となるから, $(1,1)$は$\gaxi$に関する単位元になっている.
$\MU\times\MU$において, $\gaxi$に関する逆元が存在する.
$(A,B)\in\MU\times\MU$とする. 結合性が成り立つことと, 単位元を持つことから, 左逆元があることを示せば十分である.
\begin{align}
\gaxi((C,D),(A,B))=(\gaxit(A,B)(C)\times A, B\times\gaxit(A,B)(D))
\end{align}
である.
\begin{align}
\gaxit(A,B)(C)\times A=1
\end{align}
を満たす$C\in \MU$が存在することを示す. まず, 長さ$0$の値は$C(\varnothing):=1$とすればよい. $r\geq 1$として, 長さ$r-1$まで上の等式を満たす$C$が構成できたとする. そのとき, 上の式に$\bw=(w_1,\dots,w_r)$を代入したものは
\begin{align}
\sum_{\substack{0\leq s\\\ba_1b_1\bc_1\cdots \ba_sb_s\bc_s\ba_{s+1}=\bw}}C({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_s}\lceil b_s\rceil_{\bc_s})\left(\prod_{i=1}^sA(\ba_i\rfloor_{b_i})B({}_{b_i}\lfloor \bc_i)\right)A(\ba_{s+1})=0
\end{align}
となり,
\begin{align}
C(\bw)=-\sum_{\substack{0\leq s< r\\\ba_1b_1\bc_1\cdots \ba_sb_s\bc_s\ba_{s+1}=\bw}}C({}_{\ba_1}\lceil b_1\rceil_{\bc_1},\dots,{}_{\ba_s}\lceil b_s\rceil_{\bc_s})\left(\prod_{i=1}^sA(\ba_i\rfloor_{b_i})B({}_{b_i}\lfloor \bc_i)\right)A(\ba_{s+1})
\end{align}
と書きかえると, 右辺の$C$の引数は長さ$r-1$以下であることから, $C(\bw)$の値をこの右辺によって定めればよいことが分かる. $B\times\gaxit(A,B)(D)=1$を満たす$D\in\MU$についても全く同様に構成できる.
よって, $\MU\times \MU$は$\gaxi$を積とする群になることが分かる. $\gaxi$による$(A,B)$の逆元を$\invgaxi(A,B)$と表す.
Ecalleの基本等式
$A\times B$は$\mathrm{mu}(A,B)$とも書かれる. $A\in\MU$に対し, $B(\varnothing):=1$
\begin{align}
B(\bw)=-\sum_{\ba\bb=\bw, \ba\neq\varnothing }A(\ba)B(\bb)
\end{align}
によって帰納的に定めると, とすると, $B$は$\times$に関する$A$の逆元となる. これを$\invmu(A)$と表す.
\begin{align}
\gamit(B)&:=\gaxit(B,1)\\
\ganit(B)&:=\gaxit(1,B)\\
\garit(B)&:=\gaxit(B,\invmu(B))
\end{align}
として,
\begin{align}
\gari(A,B)&:=\garit(B)(A)\times B\\
\gira(A,B)&:=\swap(\gari(\swap(A),\swap(B)))
\end{align}
とする. このとき, 命題3より
\begin{align}
\gira(A,B)&=\swap(\gaxit(\swap(B),(\invmu\circ\swap)(B))(\swap(A))\times \swap(B))\\
&=\gaxit(B,(\push\circ\swap\circ\invmu\circ\swap)(B))(A)\times B
\end{align}
が成り立つ. $h(B):=(\push\circ\swap\circ\invmu\circ\swap)(B)$として, $\girat(B):=\gaxit(B,h(B))$とすると, 上の等式は
\begin{align}
\gira(A,B)&=\girat(B)(A)\times B
\end{align}
と書き換えられる.
$A,B\in \MU$に対し,
\begin{align}
\garit(B)\circ\garit(A)&=\garit(\gari(A,B))
\end{align}
が成り立つ.
命題2より,
\begin{align}
\garit(B)\circ\garit(A)&=\gaxit(\garit(B)(A)\times B,\invmu(B)\times \garit(B)(\invmu(A)))
\end{align}
ここで, $\garit$は$\gaxit$の特別な場合であるから, 特に$\times$を保つので, $\garit(B)(\invmu(A))=\invmu(\garit(B)(A))$となる. よって,
\begin{align}
\garit(B)\circ\garit(A)&=\gaxit(\garit(B)(A)\times B,\invmu(B)\times \invmu(\garit(B)(A)))\\
&=\gaxit(\gari(A,B),\invmu(\gari(A,B)))\\
&=\garit(\gari(A,B))
\end{align}
となる.
$\invgaxi(A,B)$の左側の成分を$\invgaxi_L(A,B)$と表すことにして,
\begin{align}
\invgari(A)&:=\invgaxi_L(A,\invmu(A))\\
\invgira(A)&:=\invgaxi_L(A,h(A))\\
\rash(B)&:=h(B)\times B\\
\ras(B)&:=(\invgari\circ\invgira)(B)
\end{align}
とする. このとき, 以下が成り立つ.
$B\in\MU$に対し,
\begin{align}
\gira(A,B)=\ganit(\rash(B))(\gari(A,\ras(B)))
\end{align}
が成り立つ.
これはEcalleの基本等式と呼ばれるものである.
まず,
\begin{align}
&\girat(B)\circ\garit(\invgira(B))\\
&=\gaxit(\girat(B)(\invgira(B))\times B, h(B)\times \girat(B)(\invmu(\invgira(B)))\\
&=\ganit(h(B)\times \invmu(\girat(B)(\invgira(B))))
\end{align}
である. ここで, $ \girat(B)(\invgira(B))=\invmu(B)$であるから, これを代入すると,
\begin{align}
\girat(B)\circ\garit(\invgira(B))=\ganit(h(B)\times B)=\ganit(\rash(B))
\end{align}
を得る. これより,
\begin{align}
\ganit(\rash(B))(\ras(B))&=\girat(B)(\garit(\invgira(B))(\invgari(\invgira(B))))\\
&=\girat(B)(\invmu(\invgira(B)))\\
&=\invmu(\girat(B)(\invgira(B)))\\
&=\invmu(\invmu(B))\\
&=B
\end{align}
である. 命題6より$\garit(A)^{-1}=\garit(\invgari(A))$であることから,
\begin{align}
\girat(B)&=\ganit(\rash(B))\circ \garit(\invgira(B))^{-1}\\
&=\ganit(\rash(B))\circ\garit(\invgari(\invgira(B)))\\
&=\ganit(\rash(B))\circ\garit(\ras(B))\\
\end{align}
を得る. よって, これらを用いると,
\begin{align}
\gira(A,B)&=\girat(B)(A)\times B\\
&=\ganit(\rash(B))(\garit(\ras(B))(A))\times\ganit(\rash(B))(\ras(B))\\
&=\ganit(\rash(B))(\garit(\ras(B))(A)\times \ras(B))\\
&=\ganit(\rash(B))(\gari(A,\ras(B)))
\end{align}
となって示すべき等式が得られる.
\begin{align}
\fragari(A,B)&:=\gari(A,\invgari(B))\\
\fragira(A,B)&:=\swap(\fragari(\swap(A),\swap(B)))=\gira(A,\invgira(B))\\
\crash(B)&:=\rash(\invgira(B))
\end{align}
とする. 定理7は以下のように書き換えられる.
\begin{align} \fragira(A,B)&=\ganit(\crash(B))(\fragari(A,B)) \end{align}
定理7の$B$を$\invgari(B)$に置き換えればよい.
$\adari(A)(B):=\fragari(\preari(A,B),A)$とする. このとき, 以下が成り立つ.
$B$が$\push$不変であるとき,
\begin{align}
\swap(\adari(A)(B))=\ganit(\crash(\swap(A)))(\adari(\swap(A))(\swap(B)))
\end{align}
が成り立つ.
これはEcalleの第二基本等式と呼ばれるものである.
前の記事
の定理2より, $B$が$\push$不変ならば,
\begin{align}
\swap(\preari(A,B))=\preari(\swap(A),\swap(B))
\end{align}
である($B$が$\push$不変なら$\swap(B)$も$\push$不変になる). よって, 系1より,
\begin{align}
\swap(\adari(A)(B))&=\swap(\fragari(\preari(A,B),\invgari(A)))\\
&=\fragira(\preari(\swap(A),\swap(B)),\swap(A))\\
&=\ganit(\crash(\swap(A)))(\fragari(\preari(\swap(A),\swap(B)),\swap(A)))\\
&=\ganit(\crash(\swap(A)))(\adari(\swap(A))(\swap(B)))
\end{align}
となる.
