theorem Th26:
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 b2 -extension b1 PC-correct QC-correct QCLangSignature over
Union X for
Y being
empty-yielding b4 -tolerating ManySortedSet of the
carrier of
S for
L being
non-empty Language of
Y,
S for
x being
Element of
Union Y for
t being
Element of
Union the
Sorts of
L for
s being
SortSymbol of
S st
x in Y . s &
t in the
Sorts of
L . s holds
( ( for
a being
Element of
Args (
(In (( the connectives of S . (n + 5)), the carrier' of S)),
L) st
a = {} holds
a / (
x,
t)
= {} ) & ( for
A being
Formula of
L holds
( ( for
a being
Element of
Args (
(In (( the connectives of S . n), the carrier' of S)),
L) st
<*A*> = a holds
a / (
x,
t)
= <*(A / (x,t))*> ) & ( for
B being
Formula of
L holds
( ( for
a being
Element of
Args (
(In (( the connectives of S . (n + 1)), the carrier' of S)),
L) st
<*A,B*> = a holds
a / (
x,
t)
= <*(A / (x,t)),(B / (x,t))*> ) & ... & ( for
a being
Element of
Args (
(In (( the connectives of S . (n + 4)), the carrier' of S)),
L) st
<*A,B*> = a holds
a / (
x,
t)
= <*(A / (x,t)),(B / (x,t))*> ) & ( for
z being
Element of
Union X holds
( ( for
a being
Element of
Args (
(In (( the quantifiers of S . (1,z)), the carrier' of S)),
L) st
<*A*> = a holds
a / (
x,
t)
= <*(A / (x,t))*> ) & ( for
a being
Element of
Args (
(In (( the quantifiers of S . (2,z)), the carrier' of S)),
L) st
<*A*> = a holds
a / (
x,
t)
= <*(A / (x,t))*> ) ) ) ) ) ) ) )