文書の集合と環境

文書の集合 $K$ とは、次のデータである。

• 文書の識別子の有限集合 $\mathrm{Doc}$。
• 各文書 $d \in \mathrm{Doc}$ に、環境の有限列 $\mathrm{env}(d) = (e_1, \ldots, e_m)$（出現順）。
• 各環境 $e$ に、種類 $\mathrm{kind}(e)$（定義・公理・定理・命題・補題・系など）と、局所的な識別子 $\iota(e)$（記号 # を含まない文字列）。
• 種類が定理・命題・補題・系である環境（定理類）には、証明があるかないかの別と、証明がある場合はその中に書かれた参照の文字列の有限列 $\mathrm{ref}(e)$。

対 $(d, \iota)$ を鍵と呼び、$d\,\texttt{\#}\,\iota$ とも書く。