:: deftheorem defines is_Sep-closed_on CQC_SIM1:def 12 :
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds
( X is_Sep-closed_on p iff ( [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in X & ( for q being Element of CQC-WFF A
for t being QC-symbol of A
for K being Element of Fin (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in X holds
[q,t,K,f] in X ) & ( for q, r being Element of CQC-WFF A
for t being QC-symbol of A
for K being Element of Fin (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for t being QC-symbol of A
for K being Element of Fin (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) ) );