:: deftheorem defines vf-qc-correct AOFA_L00:def 35 :
for n being natural non empty number
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 Y being empty-yielding b₄ -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S holds
( L is vf-qc-correct iff for A, B being Formula of L holds
( vf (\not A) = vf A & vf (A \and B) = (vf A) (\/) (vf B) & vf (A \or B) = (vf A) (\/) (vf B) & vf (A \imp B) = (vf A) (\/) (vf B) & vf (A \iff B) = (vf A) (\/) (vf B) & vf (\true_ L) = EmptyMS the carrier of S & ( for x being Element of Union X
for a being SortSymbol of S st x in X . a holds
( vf (\for (x,A)) = (vf A) (\) (a -singleton x) & vf (\ex (x,A)) = (vf A) (\) (a -singleton x) ) ) ) );