Given a hidden theory T=(,E) where is a hidden signature and E is a set of -equations, we say that two -terms t,t' of hidden sort h over a variable set X are attribute equal iff for all attributes a(Y,S) where S has sort h and Y is some variables, we have
E (X)(Y) a(Y,t) = a(Y,t') ,where (as is usual) we call the hidden sort valued operations methods and the visible sort valued operations attributes. Let us write attribute equality as t =A= t'; this just means that t,t' have exactly the same attribute values. Although in general this is far short of behavioral equivalence, it can still be a useful relation on terms.
Now for the main definition: A theory T is attribute coherent iff for any method f: v1...vj h1...hk -> h in with k > 0, if S1,...,Sk and S'1,...,S'k are new variables of sorts h1,...,hk, and if T' is T with the addition of the assertions Si =A= S'i for i=1,...,k, then we have
T' implies f(Z,S1,...Sk) =A= f(Z,S'1,...,S'k) ,where Z is a set of new variables of sorts v1,...,vj. Let's denote the assertion that T is attribute coherent by ACoh(T). The definition of coherence above can be considered a proof rule for establishing the goal ACoh(T).
Now we are in position to state the attribute coinduction proof rule. To prove
T (X)t = t' ,it is sufficient to prove that T is attribute coherent and that
T implies t =A= t' .The connection of this to the full coinduction proof rule is that =A= is just a particularly simple candidate relation on terms, and showing a theory attribute coherent shows that attribute equality is behavioral equivalence.