積スター公式と和スター公式

コンウェイ半環（Conway半環）で次が成立する。

1. (ab)^* = 1 + a(ba)^*b
2. (a + b)^* = (b + a)^* = (a^*b)^*a^*

これをトレース付き双デカルト圏に持ってくると、

1. (f;g)^* = 1 + f;(g;f)^*;g
2. (f∨g)^* = (g∨f)^* = (f^*;g)^*;f^*

これらを示す。まずは積スター公式：fが黒丸、gが黒四角とする。

スターの定義としては 1∨f⁺を採用する。f^* = 1∨f⁺ の計算でむずかしい部分は既に終わっている。∇、Δに沿ってコピースライディング（重複化）して、その後右下のgをループに沿ってスライディングする。ワイヤーの長さをタイトニングとシフトで調整しておしまい。

---

次は和スター公式：

1. f^* = Tr[(1+f)∇;Δ] を箱（xとする）に入れておく。
2. (f^*;g)^*;f^* = (x;g)^*;x からスタート。
3. 左のxをループに沿ってスライディング。
4. コピースライディングの逆でxを1つにまとめる。
5. 箱xを開く。
6. 加法∇と対角Δの結合律。
7. 左下のΔをループに沿ってスライディング。
8. (g∨f)^* = (f∨g)^*の出来上がり。

図の描き方によってはもっと簡単になる、それは後述する。