等式

指標 (Signature; ソート宣言とオペレータ宣言の組) から作られる項の集合を T とする。等式は 2つの項 t1, t2 ∈ T 間の等価関係を宣言する。仕様中に記述された等式は、公理として推論の際に使用される。

等式は eq を使って宣言する:

eq <lhs> = <rhs> .

<lhs> と <rhs> は同じソート上の項である。これらの項には変数を含めることができる。変数は特定のソート上に宣言され、そのソート上の任意の項を代入できる。

例として、自然数の仕様に現れる次の等式を例に考える:

eq 0 + M:Nat = M .

M は Nat 上の変数である。M には Nat 上の任意の項を代入できるので、0 + 0 という項は、M に 0 を代入すると、この等式を用いて 0 と等しいと推論できる。同様に、以下のような推論がすべて成り立つ:

条件付き等式

条件付き等式は ceq を使って宣言する:

ceq <lhs> = <rhs> if <condition> .

<condition> は内蔵モジュール BOOL で宣言されているソート Bool 上の項である。