theorem Th11:
for
n being
natural non
empty number for
X being non
empty set for
J being
Signature ex
S being non
empty non
void strict AlgLangSignature over
X st
(
S is
n PC-correct &
S is
QC-correct &
S is
n AL-correct &
S is
J -extension & ( for
i being
natural number st not not
i = 0 & ... & not
i = 8 holds
the
connectives of
S . (n + i) = (sup the carrier' of J) +^ i ) & ( for
x being
Element of
X holds
( the
quantifiers of
S . (1,
x)
= [ the carrier' of J,1,x] & the
quantifiers of
S . (2,
x)
= [ the carrier' of J,2,x] ) ) & the
formula-sort of
S = sup the
carrier of
J & the
program-sort of
S = (sup the carrier of J) +^ 1 & the
carrier of
S = the
carrier of
J \/ { the formula-sort of S, the program-sort of S} & ( for
w being
Ordinal st
w = sup the
carrier' of
J holds
the
carrier' of
S = ( the carrier' of J \/ {(w +^ 0),(w +^ 1),(w +^ 2),(w +^ 3),(w +^ 4),(w +^ 5),(w +^ 6),(w +^ 7),(w +^ 8)}) \/ [:{ the carrier' of J},{1,2},X:] ) )