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} ; :: thesis: 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; :: thesis: verum
end;
{1,2,3,4} misses {0} \/ [:{1,2},X:]
proof
assume {1,2,3,4} meets {0} \/ [:{1,2},X:] ; :: thesis: 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; :: thesis: 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} ; :: thesis: 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; :: thesis: 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 p = the n -' 1 -element FinSequence of {0,1,2,3,4,5};
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;
n > 0 ;
then A7: n >= 0 + 1 by NAT_1:13;
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 ; :: thesis: ( not not i = 0 & ... & not i = 5 implies c . (n + i) = i )
assume not not i = 0 & ... & not i = 5 ; :: thesis: 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) ) ;
hence c . (n + i) = i by AOFA_A00:20; :: thesis: 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:]))) #); :: thesis: ( 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 ; :: according to STRUCT_0:def 13 :: thesis: ( not L is empty & L is n PC-correct & L is QC-correct )
thus not the carrier of L is empty ; :: according to STRUCT_0:def 1 :: thesis: ( 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; :: according to AOFA_L00:def 4 :: thesis: ( 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 :: thesis: ( 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 ; :: according to FUNCT_1:def 4 :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum
end;
thus the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L :: thesis: ( 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
not not 0 = 0 & ... & not 0 = 5 ;
then A15: c . (n + 0) = 0 by A8;
( 00 in {0} \/ [:{1,2},X:] & <*0*> in {<*0*>} ) by XBOOLE_0:def 3, TARSKI:def 1;
then [0,<*0*>] in ({0} \/ [:{1,2},X:]) --> <*0*> by ZFMISC_1:106;
then [0,<*0*>] in aa by XBOOLE_0:def 3;
then [0,<*0*>] in a by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . n) = <*00*> by A15, FUNCT_1:1
.= <* the formula-sort of L*> ;
:: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . n) = the formula-sort of L
thus the ResultSort of L . ( the connectives of L . n) = 00
.= the formula-sort of L ; :: thesis: verum
end;
thus the connectives of L . (n + 5) is_of_type {} , the formula-sort of L :: thesis: ( 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
not not 0 = 5 & ... & not 5 = 5 ;
then A16: c . (n + 5) = 5 by A8;
( 5 in {5} & {} in {{}} ) by TARSKI:def 1;
then [5,{}] in {5} --> {} by ZFMISC_1:106;
then [5,{}] in a by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . (n + 5)) = {} by A16, FUNCT_1:1; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . (n + 5)) = the formula-sort of L
thus the ResultSort of L . ( the connectives of L . (n + 5)) = 00
.= the formula-sort of L ; :: thesis: verum
end;
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 :: thesis: L is QC-correct
proof
let i be natural number ; :: thesis: ( 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 ) ; :: thesis: 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 A17: not not i = 1 & ... & not i = 4 ;
not ( not i = 1 or not c . (n + 1) = 1 ) & ... & ( not i = 4 or not c . (n + 4) = 4 ) by A17;
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*> ;
:: according to AOFA_A00:def 8 :: thesis: 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 ; :: thesis: verum
end;
thus the quant-sort of L = {1,2} ; :: according to AOFA_L00:def 5 :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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 :: thesis: verum
let q, x be object ; :: thesis: ( 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 ) ; :: thesis: the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L
then 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 :: thesis: verum
proof
thus the Arity of L . ( the quantifiers of L . (q,x)) = <*00*> by A21, FUNCT_1:1
.= <* the formula-sort of L*> ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the quantifiers of L . (q,x)) = the formula-sort of L
thus the ResultSort of L . ( the quantifiers of L . (q,x)) = 00
.= the formula-sort of L ; :: thesis: verum
end;
end;