1 The cvt conversion

1.1 Basics of classes

Mathelia specializes in treating c-Forms (classes) as collections of s-Forms (things).
"Belonging" is the basis.
word(sc,p) … \(\in\)
\(x \in X\) is a p-Form. It is good to read it as "the thing \(x\) is in the class \(X\)".
\(=\) is also given a definition.
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

〇. naturally generates a rule cvt(〇.). For example, cvt(=_.) is
cvt … \(X = Y\) ≃ \(\forall x \, ( x \in X \Leftrightarrow x \in Y )\)

1.2 Comprehension notation

Comprehension notation is the standard tool for generating classes. We make it usable in a natural form.
word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)

The following rule cvt(cls.) is important (there is no cls. itself).
cvt … \(t \in \{ x \mid P \}\) ≃ substitution(\(P\), \(x\) ↦ \(t\))
Example　 \(\mathrm{a} \in \{ x \mid x \subset X \}\) ≃ \(\mathrm{a} \subset X\)

1.3 Arrow functions

\(\in\) and \(\mathsf{cls}\) were tools for substituting s-Forms into p-Forms; we also make it possible to substitute s-Forms into s-Forms.
word(vs,(s,s))F … \(\mathsf{fn}\)
abbr … \(\lceil x \mapsto X \rfloor\) ≈ \(\mathsf{fn} ( x , X )\)
The following rule cvt(fn.) is important (there is no fn. itself). The ｢ ｣ in the source are half-width corner brackets.
cvt … \(\lceil x \mapsto X \rfloor ( t )\) ≃ substitution(\(X\), \(x\) ↦ \(t\))
Example　 \(\lceil x \mapsto x + a \rfloor ( b )\) ≃ \(b + a\)

The v-Form before \(\mapsto\) can be replaced by \(\bullet\). In that case \(\bullet \mapsto\) is omitted.
Example　 \(\lceil \bullet + a \rfloor\) ≈ \(\lceil x \mapsto x + a \rfloor\)
\(\lceil \bullet \rfloor\) is the identity map.
\(\bullet\) should not be used in nesting, but it is always computed from the inside.
Example　 \(\lceil \bullet + \lceil \bullet + a \rfloor ( x ) \rfloor\) ≈ \(\lceil \bullet + ( x + a ) \rfloor\)

1.4 The cvt conversion

The automatic variable \(\mathbb{W}_\mathrm{c}.\) in a Book is "the sequence of all props of the form 〇. (where the gram of 〇 contains c)". At this point \(\mathbb{W}_\mathrm{c}.\) is only =_. .
|cvt is defined as "the result of repeatedly applying cvt(〇.) (〇 being \(\mathbb{W}_\mathrm{c}.\), cls., fn.) as much as possible".
Example　 \(X = \{ x \mid x \in X \}\) |cvt … \(\forall x \, ( x \in X \Leftrightarrow x \in X )\)