# Equations

A term is constructed from operators and variables. An equation consists of a pair of terms (with or without a term of condition).

An equation is declared with the keyword `eq`

as follows:

`eq `

*<lhs>*` = `

*<rhs>*` .`

Terms *<lhs>* and *<rhs>* should be of the same sort. Those terms can include variables.

Example (the first equation of NAT+)

eq 0 + M:Nat = M .

The symbol `M`

stands for a variable of Sort `Nat`

. The following equations can be deduced from the above equation:

`0 + 0 = 0`

`0 + s(0) = s(0)`

`0 + s(s(0)) = s(s(0))`

- ...
`0 + s(s(s(s(s(s(s(s(s(s(0)))))))))) = s(s(s(s(s(s(s(s(s(s(0))))))))))`

- ...

## Conditional equations

A conditional equation is declared with `ceq`

as follows:

`ceq `

*<lhs>*` = `

*<rhs>*` if `

*<condition>*` .`

A condition (*<condition>*) is a term of Sort `Bool`

which is declared in the built-in module `BOOL`

[Next] Variables

Original Copyright © Takahiro Seino, all rights reserved.