eq

eq [ <label-exp> ] <term> = <term> .

Declares an axiom, or equation.

Spaces around the = are necessary to separate the left from the right hand side. The terms given must belong to the same connected component in the graph defined by the sort ordering.

In simple words, the objects determined by the terms must be interpretable as of the same sort.

The optional part <label-exp> serves two purposes, one is to give an axiom an identifier, and one is to modify its behavior. The <label-exp> is of the form:

[ <modifier> <label> ] :

Warning: The square brackets here are not specifying optional components, but syntactical elements. Thus, a labeled axiom can look like:

eq[foobar] : foo = bar .

The <modifier> part is used to change the rewriting behavior of the axiom. There are at the moment two possible modifiers, namely :m-and (:m-and-also) and :m-or (:m-or-else). Both make sense only for operators where the arguments come from an associative sort. In this case both modifiers create all possible permutations of the arguments and rewrite the original term to the conjunction in case of :m-and or to the disjunction in case of :m-or of all the generated terms.

Assume that NatSet is a sort with associative constructor modeling a set of natural number, and let

  pred p1: Nat .
  ops q1 q2 : NatSet -> Bool .
  eq [:m-and]: q1(N1:Nat NS:NatSet) = p1(N1) .
  eq [:m-or]:  q2(N1:Nat NS:NatSet) = p1(N1) .

In this case an expression like q1(1 2 3) would reduce to p1(1) and p1(2) and p1(3) (modulo AC), and q2(1 2 3) into the same term with or instead.

Related: bceq, beq, ceq