**Go backward to** 2.3.3.3 Definedness

**Go up to** 2.3.3 Atomic Formulae

#### 2.3.3.4 Equations

EXISTL-EQUATION ::= existl-equation TERM TERM
STRONG-EQUATION ::= strong-equation TERM TERM

An existential equation `EXISTL-EQUATION` is written:

*T*_{1} =^{e}= *T*_{2}

The sign displayed as an `*e*' over a `*=*' in LaTeX
is input as ``=e=`'.
A strong equation is written:

*T*_{1} = *T*_{2}

An existential equation holds when the values of the terms are both
defined and equal; a strong equation holds also when the values of
both terms are undefined (thus the two forms of equation are
equivalent when the values of both terms are always defined).

An equation is well-sorted if there is a sort such that both terms
are well-sorted for that sort. It then expands to the corresponding
existential or strong equation on the fully-qualified expansions of
the terms for that sort.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk