# Equality predicate `=`

The built-in equality predicate `_=_` takes terms of the same sort and returns `true` when they are reduced into a same term.

The equality predicate `_=_` is defined in the built-in module `EQL` as follows:

```sys:mod! EQL
{
imports {
protecting (TRUTH)
}
signature {
pred _ = _ : _ Cosmos _ _ Cosmos _  { comm prec: 51 }
}
axioms {
eq CUX = CUX = true .
}
}```

(*) The equality predicate `_=_` and the keyword `_=_` in the equation declaration are confusing. When using the equality predicate in an equation, it is recommended to put a term in brackets like `eq p(N:Nat, M:Nat) = (N = M) .`

The following is an example of equational reasoning with the equality predicate `_=_`:

```CafeOBJ> select NAT+ + EQL
NAT+ + EQL> red s(s(0)) + 0 = s(0) + s(0) .
-- reduce in NAT+ + EQL : s(s(0)) + 0 = s(0) + s(0)
true : Bool
(0.004 sec for parse, 6 rewrites(0.002 sec), 9 matches)
NAT+ + EQL> ```

The expression `NAT+ + EQL` is a module expression which stands for the sum of `NAT+` and `EQL`. In the first line, `NAT+ + EQL` is selected, and elements of both modules can be used hereafter. In the next line, try to reduce the equation of `s(s(0)) + 0` and `s(0) + s(0)`. Here, the symbol `_=_` is the equality predicate. In the fourth line, CafeOBJ system returns `true`, which means that the input terms are equivalent.

The equality predicate `_=_` (or reduction) does not give a complete equational reasoning. Only the output `true` is trustworthy. From syntactical and/or semantical reasons, it may fail to prove an equation even if it is true.

The following is an example of equational reasoning with `_=_` which fails to prove the equation `n + m = m + n` for arbitrary elements `n, m`, that is, the commutativity of `+`:

```CafeOBJ> open NAT+ + EQL .
-- opening module NAT+ + EQL.. done.
%NAT+ + EQL> ops n m : -> Nat .  -- arbitrarily choosen two naturals n and m
%NAT+ + EQL> red n + m = m + n . -- try to verify + is commutative
_*
-- reduce in %NAT+ + EQL : n + m = m + n
n + m = m + n : Bool
(0.003 sec for parse, 0 rewrites(0.010 sec), 9 matches)
%NAT+ + EQL> close
CafeOBJ> ```

The output term is not `true`, though the commutativity of `+` holds for `NAT+`.

```CafeOBJ> open NAT+ + EQL .
-- opening module NAT+ + EQL.. done.
%NAT+ + EQL> ops n m : -> Nat .
%NAT+ + EQL> op _+_ : Nat Nat -> Nat { comm } .
%NAT+ + EQL> red n + m = m + n .
-- reduce in %NAT+ + EQL : n + m = m + n
true : Bool
(0.002 sec for parse, 1 rewrites(0.003 sec), 9 matches)
%NAT+ + EQL> close
CafeOBJ> ```