set O = {0,1,2,3,4,5} \/ [:{1,2},X:];
set a = (({1,2,3,4} --> <*0,0*>) \/ (({0} \/ [:{1,2},X:]) --> <*0*>)) \/ ({5} --> {});
set r = ({0,1,2,3,4,5} \/ [:{1,2},X:]) --> 0;
A1:
( dom ({1,2,3,4} --> <*0,0*>) = {1,2,3,4} & dom ({5} --> {}) = {5} & dom (({0} \/ [:{1,2},X:]) --> <*0*>) = {0} \/ [:{1,2},X:] )
;
B1:
[:{1,2},X:] misses {0,1,2,3,4,5}
proof
assume
[:{1,2},X:] meets {0,1,2,3,4,5}
;
contradiction
then consider x being
object such that A2:
(
x in {0,1,2,3,4,5} &
x in [:{1,2},X:] )
by XBOOLE_0:3;
thus
contradiction
by A2, ENUMSET1:def 4;
verum
end;
{1,2,3,4} misses {0} \/ [:{1,2},X:]
proof
assume
{1,2,3,4} meets {0} \/ [:{1,2},X:]
;
contradiction
then consider x being
object such that A2:
(
x in {1,2,3,4} &
x in {0} \/ [:{1,2},X:] )
by XBOOLE_0:3;
(
x in {0} or
x in [:{1,2},X:] )
by A2, XBOOLE_0:def 3;
then consider y,
z being
object such that A3:
(
y in {1,2} &
z in X &
x = [y,z] )
by A2, ENUMSET1:def 2;
thus
contradiction
by A2, A3, ENUMSET1:def 2;
verum
end;
then reconsider aa = ({1,2,3,4} --> <*0,0*>) \/ (({0} \/ [:{1,2},X:]) --> <*0*>) as Function by A1, GRFUNC_1:13;
A4: dom aa =
{1,2,3,4} \/ ({0} \/ [:{1,2},X:])
by A1, XTUPLE_0:23
.=
({0} \/ {1,2,3,4}) \/ [:{1,2},X:]
by XBOOLE_1:4
.=
{0,1,2,3,4} \/ [:{1,2},X:]
by ENUMSET1:7
;
{0,1,2,3,4} \/ [:{1,2},X:] misses {5}
proof
assume
{0,1,2,3,4} \/ [:{1,2},X:] meets {5}
;
contradiction
then consider x being
object such that A5:
(
x in {0,1,2,3,4} \/ [:{1,2},X:] &
x in {5} )
by XBOOLE_0:3;
x = 5
by A5, TARSKI:def 1;
then
( 5
in {0,1,2,3,4} or 5
in [:{1,2},X:] )
by A5, XBOOLE_0:def 3;
hence
contradiction
by ENUMSET1:def 3;
verum
end;
then reconsider a = (({1,2,3,4} --> <*0,0*>) \/ (({0} \/ [:{1,2},X:]) --> <*0*>)) \/ ({5} --> {}) as Function by A1, A4, GRFUNC_1:13;
A6: dom a =
({0,1,2,3,4} \/ [:{1,2},X:]) \/ {5}
by A1, A4, XTUPLE_0:23
.=
({5} \/ {0,1,2,3,4}) \/ [:{1,2},X:]
by XBOOLE_1:4
.=
{0,1,2,3,4,5} \/ [:{1,2},X:]
by ENUMSET1:15
;
reconsider 00 = 0 as Element of {0} by TARSKI:def 1;
( <*00*> in {0} * & <*00,00*> in {0} * )
by FINSEQ_1:def 11;
then
( rng ({1,2,3,4} --> <*0,0*>) c= {0} * & rng (({0} \/ [:{1,2},X:]) --> <*0*>) c= {0} * )
by ZFMISC_1:31;
then
( (rng ({1,2,3,4} --> <*0,0*>)) \/ (rng (({0} \/ [:{1,2},X:]) --> <*0*>)) c= {0} * & <*> {0} in {0} * )
by FINSEQ_1:def 11, XBOOLE_1:8;
then
( rng aa c= {0} * & rng ({5} --> {}) c= {0} * )
by RELAT_1:12;
then
(rng aa) \/ (rng ({5} --> {})) c= {0} *
by XBOOLE_1:8;
then
rng a c= {0} *
by RELAT_1:12;
then reconsider a = a as Function of ({0,1,2,3,4,5} \/ [:{1,2},X:]),({0} *) by A6, FUNCT_2:2;
reconsider r = ({0,1,2,3,4,5} \/ [:{1,2},X:]) --> 0 as Function of ({0,1,2,3,4,5} \/ [:{1,2},X:]),{0} ;
( 0 in {0,1,2,3,4,5} & 1 in {0,1,2,3,4,5} & 2 in {0,1,2,3,4,5} & 3 in {0,1,2,3,4,5} & 4 in {0,1,2,3,4,5} & 5 in {0,1,2,3,4,5} )
by ENUMSET1:def 4;
then reconsider o0 = 0 , o1 = 1, o2 = 2, o3 = 3, o4 = 4, o5 = 5 as Element of {0,1,2,3,4,5} \/ [:{1,2},X:] by XBOOLE_0:def 3;
set m = n -' 1;
set p = the n -' 1 -element FinSequence of {0,1,2,3,4,5};
n > 0
;
then A7:
n >= 0 + 1
by NAT_1:13;
then
n - 1 >= 1 - 1
by XREAL_1:9;
then bb:
n -' 1 = n - 1
by XREAL_0:def 2;
B2:
( rng the n -' 1 -element FinSequence of {0,1,2,3,4,5} c= {0,1,2,3,4,5} & {0,1,2,3,4,5} c= {0,1,2,3,4,5} \/ [:{1,2},X:] )
by XBOOLE_1:7;
then reconsider p = the n -' 1 -element FinSequence of {0,1,2,3,4,5} as FinSequence of {0,1,2,3,4,5} \/ [:{1,2},X:] by XBOOLE_1:1, FINSEQ_1:def 4;
set c6 = <*o0,o1,o2,o3,o4,o5*>;
reconsider c = p ^ <*o0,o1,o2,o3,o4,o5*> as FinSequence of {0,1,2,3,4,5} \/ [:{1,2},X:] ;
rng <*o0,o1,o2,o3,o4,o5*> = {0,1,2,3,4,5}
by AOFA_A00:21;
then B3:
( rng c = (rng p) \/ (rng <*o0,o1,o2,o3,o4,o5*>) & (rng p) \/ (rng <*o0,o1,o2,o3,o4,o5*>) c= {0,1,2,3,4,5} \/ {0,1,2,3,4,5} & {0,1,2,3,4,5} \/ {0,1,2,3,4,5} = {0,1,2,3,4,5} )
by B2, XBOOLE_1:13, FINSEQ_1:31;
aa:
c . ((n -' 1) + 1) = <*o0,o1,o2,o3,o4,o5*> . 1 & ... & c . ((n -' 1) + 6) = <*o0,o1,o2,o3,o4,o5*> . 6
by FINSEQ_3:155;
A8:
for i being natural number st not not i = 0 & ... & not i = 5 holds
c . (n + i) = i
proof
let i be
natural number ;
( not not i = 0 & ... & not i = 5 implies c . (n + i) = i )
assume
not not
i = 0 & ... & not
i = 5
;
c . (n + i) = i
then
not ( not
i = 0 or not
c . (n + 0) = <*o0,o1,o2,o3,o4,o5*> . (0 + 1) ) & ... & ( not
i = 5 or not
c . (n + 5) = <*o0,o1,o2,o3,o4,o5*> . (5 + 1) )
by aa, bb;
hence
c . (n + i) = i
;
verum
end;
take L = QCLangSignature(# {0},({0,1,2,3,4,5} \/ [:{1,2},X:]),a,r,(In (0,{0})),c,{1,2},(incl ([:{1,2},X:],({0,1,2,3,4,5} \/ [:{1,2},X:]))) #); ( not L is void & not L is empty & L is n PC-correct & L is QC-correct )
thus
not the carrier' of L is empty
; STRUCT_0:def 13 ( not L is empty & L is n PC-correct & L is QC-correct )
thus
not the carrier of L is empty
; STRUCT_0:def 1 ( L is n PC-correct & L is QC-correct )
( len <*o0,o1,o2,o3,o4,o5*> = 5 + 1 & len p = n -' 1 )
by CARD_1:def 7;
then
( (len p) + (len <*o0,o1,o2,o3,o4,o5*>) = (n -' 1) + (1 + 5) & (n -' 1) + (1 + 5) = ((n -' 1) + 1) + 5 & n is Real & 1 is Real )
;
then
(len p) + (len <*o0,o1,o2,o3,o4,o5*>) = n + 5
by A7, XREAL_1:235;
hence
len the connectives of L >= n + 5
by FINSEQ_1:22; AOFA_L00:def 4 ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one & the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L & the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct )
set N = {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)};
thus
the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one
( the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L & the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct )proof
let x be
object ;
FUNCT_1:def 4 for b1 being object holds
( not x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not b1 in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . b1 or x = b1 )let y be
object ;
( not x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not y in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . y or x = y )
assume A9:
(
x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) &
y in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) &
( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . y )
;
x = y
then A10:
(
x in {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} &
y in {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} )
by RELAT_1:57;
then A11:
(
c . x = (c | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x &
(c | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = c . y )
by A9, FUNCT_1:49;
A12:
( not not
x = n + 0 & ... & not
x = n + 5 & not not
y = n + 0 & ... & not
y = n + 5 )
by A10, ENUMSET1:def 4;
then consider i being
Nat such that A13:
(
0 <= i &
i <= 5 &
x = n + i )
;
consider j being
Nat such that A14:
(
0 <= j &
j <= 5 &
y = n + j )
by A12;
( not not
i = 0 & ... & not
i = 5 & not not
j = 0 & ... & not
j = 5 )
by A13, A14;
then
(
c . x = i &
c . y = j )
by A8, A13, A14;
hence
x = y
by A11, A13, A14;
verum
end;
thus
the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L
( the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct )
thus
the connectives of L . (n + 5) is_of_type {} , the formula-sort of L
( the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct )
thus
the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L
L is QC-correct proof
let i be
natural number ;
( not 1 <= i or not i <= 4 or the connectives of L . (n + i) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L )
assume
( 1
<= i &
i <= 4 )
;
the connectives of L . (n + i) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L
then
not not
i = 1 & ... & not
i = 4
;
then
not ( not
i = 1 or not
c . (n + 1) = 1 ) & ... & ( not
i = 4 or not
c . (n + 4) = 4 )
by aa, bb;
then
(
c . (n + i) in {1,2,3,4} &
<*0,0*> in {<*0,0*>} )
by TARSKI:def 1, ENUMSET1:def 2;
then
[(c . (n + i)),<*0,0*>] in {1,2,3,4} --> <*0,0*>
by ZFMISC_1:106;
then
[(c . (n + i)),<*0,0*>] in aa
by XBOOLE_0:def 3;
then
[(c . (n + i)),<*0,0*>] in a
by XBOOLE_0:def 3;
hence the
Arity of
L . ( the connectives of L . (n + i)) =
<*00,0*>
by FUNCT_1:1
.=
<* the formula-sort of L,00*>
.=
<* the formula-sort of L, the formula-sort of L*>
;
AOFA_A00:def 8 the ResultSort of L . ( the connectives of L . (n + i)) = the formula-sort of L
thus the
ResultSort of
L . ( the connectives of L . (n + i)) =
00
.=
the
formula-sort of
L
;
verum
end;
thus
the quant-sort of L = {1,2}
; AOFA_L00:def 5 ( the quantifiers of L is one-to-one & rng the quantifiers of L misses rng the connectives of L & ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) )
A18:
the quantifiers of L = id [:{1,2},X:]
by Def7, XBOOLE_1:7;
hence
the quantifiers of L is one-to-one
; ( rng the quantifiers of L misses rng the connectives of L & ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) )
rng the quantifiers of L c= [:{1,2},X:]
by A18;
hence
rng the quantifiers of L misses rng the connectives of L
by B1, B3, XBOOLE_1:64; for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L
hereby verum
let q,
x be
object ;
( q in the quant-sort of L & x in X implies the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L )assume A19:
(
q in the
quant-sort of
L &
x in X )
;
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of Lthen A20:
[q,x] in [: the quant-sort of L,X:]
by ZFMISC_1:87;
( the
quantifiers of
L . (
q,
x)
= [q,x] &
<*0*> in {<*0*>} )
by A19, A18, FUNCT_1:18, TARSKI:def 1, ZFMISC_1:87;
then
( the
quantifiers of
L . (
q,
x)
in {0} \/ [:{1,2},X:] &
<*0*> in {<*0*>} )
by A20, XBOOLE_0:def 3;
then
[( the quantifiers of L . (q,x)),<*0*>] in ({0} \/ [:{1,2},X:]) --> <*0*>
by ZFMISC_1:106;
then
[( the quantifiers of L . (q,x)),<*0*>] in aa
by XBOOLE_0:def 3;
then A21:
[( the quantifiers of L . (q,x)),<*0*>] in a
by XBOOLE_0:def 3;
thus
the
quantifiers of
L . (
q,
x)
is_of_type <* the formula-sort of L*>, the
formula-sort of
L
verum
end;