2 書いた通りに読まれる

{/} は2項記号の否定です。{/} は import した word_logic.book で紹介済みなので、word 行を書かなくても使えます（{*}・{**} は下で紹介します）。ここで word・lower の行を書いているのは、表示に gram と lower 規則を出すためです（紹介し直しても構いません）。
word+(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)
表示の lower の行は、その word が FCL で何に置き換わるかです。𝗉（ソースでは $..p）は2項記号の穴で、ここに = などが入ります。ソース x {/}= y（{/} と = の間に空白を入れない）は x ≠ y と表示され、FCL では ¬ (x = y) です。

次の Thm は査読を通ります。
\({\perp}\) \(\blacktriangleleft\) \(x \neq y\)

査読器は \({\perp}\) ◁ \(\neg ( x = y )\) を prover+ に投げ（3.book の |0）、入力はコレで、length:2 の証明が見つかります。
査読器に疑念を持つのは正しい姿勢です。その健全性は最重要視されています。

3 [ ] word：word を対象にする

3.1 関係の性質

= のような2項記号について「反射的」「推移的」を書きたいとき、[=] と括弧で囲んで1つの対象として扱います。
何が嬉しいか：「反射律」の中身（∀ x (x = x)）を記号ごとに書き直さずに済み、同じ性質を = にも ⊂ にも、さらに ??p^ のような2項の変数（すべての2項関係）にも一度に言えます（下の [??p^] :R の例）。
:R :T :X は word_logic に無いので紹介します。
word+([ss,p],p)R … \(:\mathsf{R}\)  \(:\mathsf{T}\)  \(:\mathsf{X}\)
lower … \([\mathbin{{\sf p}}] :\mathsf{R}\) ≃ \(\forall x ( x \mathbin{{\sf p}} x )\)
lower … \([\mathbin{{\sf p}}] :\mathsf{T}\) ≃ \(\forall x , y , z ( x \mathbin{{\sf p}} y \mathbin{{\sf p}} z \Longrightarrow x \mathbin{{\sf p}} z )\)
lower … \([\mathbin{{\sf p}}] :\mathsf{X}\) ≃ \(\forall x , y ( x \mathbin{{\sf p}} y \Longrightarrow y \mathbin{{\sf p}} x )\)
　[=] :R … 反射律（すべての x で x = x）
　[=] :T … 推移律（x = y かつ y = z なら x = z）
　[=] :X … 対称律（x = y なら y = x）
:R&:T のように & でつないだ word は自動で作られ、両方の性質の and になります。
lower … \([\mathbin{{\sf p}}] :\mathsf{R}\mathsf{T}\) ≃ \([\mathbin{{\sf p}}] :\mathsf{R} , [\mathbin{{\sf p}}] :\mathsf{T}\)
\([=] :\mathsf{R}\mathsf{T}\mathsf{X}\) \(\blacktriangleleft\) O
ソース `[=] :R&:T&:X`（「= は同値関係」）。FCL では [and [and [∀ z1 [= z1 z1]] [∀ z1 [∀ z2 [∀ z3 [⇒ [and [= z1 z2] [= z2 z3]] [= z1 z3]]]]]] [∀ z1 [∀ z2 [⇒ [= z1 z2] [= z2 z1]]]]] です（slash_cli で確認できます）。= は一階論理の等号なので、前提なしで示せます。
表示の lower にある x 𝗉 y 𝗉 z や =.. の X ⊂ Y ⊂ X は chain で、x 𝗉 y and y 𝗉 z の意味です（左から結合するのではない。slash_cli で [ chain X ⊂ Y ⊂ X ] → [and [⊂ X Y] [⊂ Y X]]）。
[ ] には ⊂ なども入ります。lower が先に働くので、/ W. の1回で :T も ⊂ も開きます。
\([\subset] :\mathsf{R}\mathsf{T}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
ソース `[⊂] :R&:T`（⊂ は反射的かつ推移的）。

3.2 2項記号の関数化

2項記号 a（= や ⇒）を「関数どうし」「関係どうし」に広げる word です。
word+(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[s,\({\tt x}\)][s,\({\tt x}\)],\({\tt y}\)) … \(\star\)
lower … \([\mathbin{{\sf f}}] \stackrel{\star}{\mathbin{{\sf a}}} [\mathbin{{\sf g}}]\) ≃ \(\forall x ( ( \mathbin{{\sf f}} x ) \mathbin{{\sf a}} ( \mathbin{{\sf g}} x ) )\)
ソース [?f] {*}= [?g] は「?f と ?g が恒等的に等しい」＝ [∀ z1 [= [?f z1] [?g z1]]] です。?f, ?g は1引数の関数変数で、[ ] で囲みます（囲まずに ?f {*}= ?g と書くと「wordの引数が不足しています」になります）。{*}= は and より強く結合します（[?f] {*}= [?g] and [?g] {*}= [?h] ⟹ [?f] {*}= [?h] は括弧なしでよい）。
word+(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[ss,\({\tt x}\)][ss,\({\tt x}\)],\({\tt y}\)) … \(\star\!\star\)
lower … \([\mathbin{{\sf f}}] \stackrel{\star\!\star}{\mathbin{{\sf a}}} [\mathbin{{\sf g}}]\) ≃ \(\forall x , y ( ( x \mathbin{{\sf f}} y ) \mathbin{{\sf a}} ( x \mathbin{{\sf g}} y ) )\)
{**} は2引数版です。ソース [=] {**}⇒ [⊂] は [∀ z1 [∀ z2 [⇒ [= z1 z2] [⊂ z1 z2]]]]（x = y ならば x ⊂ y）。
\([ \mathbin{p} ] :\mathsf{R} \Longleftrightarrow [=] \stackrel{\star\!\star}{\Rightarrow} [ \mathbin{p} ]\) \(\blacktriangleleft\) O
ソース `[??p^] :R ⟺ [=] {**}⇒ [??p^]`。??p^ は2引数の述語変数で、「??p^ が反射的 ⟺ x = y ならいつも x ??p^ y」と読みます。FCL は [⇔ [∀ z1 [??p^ z1 z1]] [∀ z1 [∀ z2 [⇒ [= z1 z2] [??p^ z1 z2]]]]]。