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