:: deftheorem defines vf-eq-correct AOFA_L00:def 45 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being empty-yielding GeneratorSet of T
for S being non empty non void b₂ -extension b₁ PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S),S holds
( L is vf-eq-correct iff for s being SortSymbol of S holds
( ( for t1, t2 being Element of L,s holds vf (t1 '=' (t2,L)) = (vf t1) (\/) (vf t2) ) & ( for s being SortSymbol of S
for t being Element of L,s st t in X . s holds
vf t = s -singleton t ) ) );