:: deftheorem DEF2 defines invariant ABSRED_0:def 30 :
for S being non empty non-empty TRSStr holds
( S is invariant iff for o being OperSymbol of S
for a, b being Element of dom (Den (o,S))
for i being Nat st i in dom a holds
for x, y being Element of S st x = a . i & b = a +* (i,y) & x ==> y holds
(Den (o,S)) . a ==> (Den (o,S)) . b );