3-way マージ

定義 5.1（「バージョン管理システム Git」§5）

有限集合 $I$ （行やファイルパスなどの「位置」の集合）と集合 $V$ （その位置に入りうる値の集合）を固定し、写像 $x : I \to V$ を版と呼ぶ。版 $b$ （ベース）と版 $x, y$ に対し、各 $i \in I$ で

D_i \;=\; \{\, x(i),\, y(i) \,\} \setminus \{\, b(i) \,\}

とおく。すべての $i \in I$ で $|D_i| \le 1$ が成り立つとき、 $x$ と $y$ は $b$ を基準として衝突しないといい、マージ結果 $m_b(x,y) : I \to V$ を

m_b(x,y)(i) \;=\; \begin{cases} v & (D_i = \{v\} \text{ のとき}) \\ b(i) & (D_i = \emptyset \text{ のとき}) \end{cases}

で定める。ある $i$ で $|D_i| = 2$ となるとき、位置 $i$ で衝突が起きたという。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。