Let u, v, w ∈ Z4m be such that α ∈ [u]m, β ∈ [v]m and γ ∈ [w]m. By Proposition 3, trianglem(*u, v, w*). At the corners of the triangle pApBpC , the following complete turns can be formed:
- (φAB − φAC ) − (φAB − φA) + (φAC − φA), corresponding to turnm(u, −*i, s*)
by Proposition 2,
- (φBC −φBA)−(φBC −φB)+ (φBA −φB), corresponding to turnm(v, −*k, j*), - (φCA −φCB)−(φCA −φC ) + (φCB −φC ), corresponding to turnm(w, −*t, l*).

This shows (∗∗). Conversely, assume (∗∗). By trianglem(*u, v, w*) and Proposition 3, we can choose pA, pB and pC such that φAB − φAC ∈ [u]m φBC − φBA ∈ [v]m φCA − φCB ∈ [w]m Since turnm(u, −*i, s*), by Proposition 2, we can find αA, βA and γA such that αA +
βA + γA = 0 and αA ∈ [−i]m, βA ∈ [s]m and γA ∈ [u]m. From Proposition 2(2), we obtain that it is possible to choose γA = φAB − φAC (note that the latter angle is also in [u]m). Put φA := φAB + αA, then φAB − φA = −αA ∈ [i]m, and φAC − φA =
(φAB − φA) − (φAB − φAC ) = −αA − γA = βA ∈ [s]m. φB and φC can be chosen similarly, fulfilling the constraints given by j and k resp. l and t. ✷
Using Algorithm 1, a composition table for *OPRA*m can be computed by enumerating all possible triples and only keeping those for which the predicate *opra* holds. Moreover, given a pair of *OPRA*m relations, by enumerating all possible third OPRAm relations and testing with the predicate *opra*, also the composition of two relations can be computed.

The run time of the predicate *opra* is O(m3), since the algorithm contains an existential quantification over the variables u, v, w ranging from 0 to 4m − 1. However, the existential quantification can be replaced by a constant number of case distinctions:
e.g. we look for u such that turnm(u, −*i, s*). But since u − i + s must add up to −1, 0 or 1, it is clear that u must be taken from the set {i − s − 1, i − *s, i* − s + 1}. As a result, we get an improved run time that is constant. This holds only when assuming a register machine with arithmetic operations executed in constant time. For a Turing machine with binary representations of numbers, basic arithmetic operations take time log m. Then the run time is O(log m).

The computation of the composition of two relations needs to enumerate all possible third relations, and then check each triple in constant time. Since there are
(4m)
2 + 4m relations, this takes O(m2) time, which is the same time as in [8]. Again, for Turing machines, this multiplies by a factor of log n, hence we get an overall running time of O(m2log m). Of course, the same remark applies to the algorithm of
[8].

A Haskell version of the *opra* algorithm (also implementing the above optimization of the existential quantification) can be downloaded at http://quail.rsise.

anu.edu.au.

The *OPRA* calculus can be used to express many other qualitative position calculi
[4].