6 高レベルの表現
6.1 穴
数学は記号列を変形していくゲームです。「記号列の変形の規則」もまた表現されます。
規則を使うときに Form が代入される場所を「Formの穴」と言い、次の綴りを使います。
Formの穴 …
$[lDP]。例：「or の前後をひっくり返す」規則は
$P or $Q →
$Q or $P v-Formの穴 … 全角の
[ｌDP]（[Ａ-Ｚａ-ｚ][0-9]*'*）
v_-Formの穴 …
[ｌDP]_ wordの列の穴 …
$_[lDP]6.2 tex計算とFCL変換
Formel は入力された Form を2通りに処理します。tex 表記の計算と、
FCL（Formel Core Language）への変換です。
FCL は略記などを処理し終えた形で、証明器に渡す式は
FCL から翻訳して作られます。CLI の結果（前置記法）は
FCL です。
default.formel では \, \; \! !, _ ^ が
word tex_only に登録されています。空白で区切られた1つの word として書いたときだけ、表示のためだけに使われ、
FCL 変換では無視されます。例 ソース
x \; ∈ X（CLI の結果は
x ∈ X と同じ
[∈ x X]）。X_ や P^ の末尾の _ ^ は綴りの一部で、これとは別です。
{ } は見えない括弧です。
FCL 変換では
( ) と同じで、tex 表示では TeX のまとまり
{ } になります（括弧は表示されない）。例
m ↑ { n + 1 } は \(m^{n+1}\) と表示され、
m ↑ (n + 1) と同じ。
{ } は対で書きます（対でなければ拒否）。
word+ として紹介される word は高度な表現のためのもので、
FCL 変換では
lower という規則で処理されます。
最も簡単な例が
alias word（
FCL 変換では同じ word になる別の word）です。次は結合の強さだけが違う論理記号です。
word+(pp,p) …
\({\bf ,}\,\) \(\Longrightarrow\) \(\Longleftrightarrow\)lower …
\(P {\bf ,}\, Q\) ≃
\(P , Q\) lower …
\(P \Longrightarrow Q\) ≃
\(P \Rightarrow Q\) lower …
\(P \Longleftrightarrow Q\) ≃
\(P \Leftrightarrow Q\) word には precedence（preced）というデータもあり、上の「結合の強さ」はこれで決まります（preced が大きいほど弱い）。例：
\(P \Rightarrow Q \Longleftrightarrow \neg P \mathbin{\rm o\!r} Q\) は
\(( P \Rightarrow Q ) \Leftrightarrow ( \neg P \mathbin{\rm o\!r} Q )\) （CLI の結果
[⇔ [⇒ P^ Q^] [or [¬ P^] Q^]]。⟺ は
FCL では ⇔ になる）
6.3 省略表現
省略表現も使えます。
FCL 変換では
abbr という規則で処理されます。abbr も word と同じように紹介してから使います。紹介すると、規則が表示されます（
\({\tt n}\) は自然数が代入されるもの。
\({\tt n\,{\text -}\,1}\) なども使えます）。
abbr …
\(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈
\(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\) col は「並べたものすべてについて同じことを言う」省略です。ソース
[ x ; y col ∈ A ] は
x ∈ A and y ∈ A になります（表示では and が「,」になるので、ソースで読んでください）。CLI の結果は
[and [∈ x A] [∈ y A]] です。
量化子の省略表現もあります。
abbr …
\(\forall x_{1} , \cdots , x_{\tt n} P\) ≈
\(\forall x_{1} \cdots \forall x_{\tt n} ( P )\) abbr …
\(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈
\(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} \Longrightarrow ( P ) )\) ソース
[ ∀ x ∈ A . x ∈ B ] は
∀ x (x ∈ A ⇒ x ∈ B)（③と同じ）になります。CLI の結果は
[∀ x [⇒ [∈ x A] [∈ x B]]] で、③ の結果と一致します。
省略表現を使った式は、このように CLI で展開後の形を確かめられます。
col と ∀ などの abbr は
import /common/word_logic で紹介済みなので、その Book を import すれば書かずに使えます。