set X = {0,1};
set Y = {0,1,2,3,4,5,6,7,8,9};
reconsider 00 = 0 , x1 = 1 as Element of {0,1} by TARSKI:def 2;
reconsider y0 = 0 , 01 = 1, 02 = 2, 03 = 3, 04 = 4, 05 = 5, 06 = 6, 07 = 7, 08 = 8, 09 = 9 as Element of {0,1,2,3,4,5,6,7,8,9} by ENUMSET1:def 8;
set aa = <*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>;
set a = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {});
set r = ({0,1,2,9} --> 00) \/ ({3,4,5,6,7,8} --> x1);
( <*00*> in {0,1} * & <*00,00*> in {0,1} * & <*x1*> in {0,1} * & <*x1,x1*> in {0,1} * & <*> {0,1} in {0,1} * ) by FINSEQ_1:def 11;
then A1: ( {{},<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} c= {0,1} * & rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= (rng (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>)) \/ (rng ({0} --> {})) & dom ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) = (dom (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>)) \/ (dom ({0} --> {})) & dom ({0} --> {}) = {0} & rng ({0} --> {}) = {{}} ) by Th10, FUNCT_4:17, FUNCT_4:def 1;
then rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} \/ {{}} by Th21;
then ( rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {{},<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} & dom (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) = Seg 9 ) by Th12, FINSEQ_1:89;
then ( rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {0,1} * & dom ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) = {0,1,2,3,4,5,6,7,8,9} ) by A1, Th12, Th22;
then reconsider a = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {}) as Function of {0,1,2,3,4,5,6,7,8,9},({0,1} *) by FUNCT_2:2;
A2: ( dom ({0,1,2,9} --> 00) = {0,1,2,9} & dom ({3,4,5,6,7,8} --> x1) = {3,4,5,6,7,8} ) ;
{0,1,2,9} misses {3,4,5,6,7,8}
proof
assume {0,1,2,9} meets {3,4,5,6,7,8} ; :: thesis: contradiction
then consider x being object such that
A3: ( x in {0,1,2,9} & x in {3,4,5,6,7,8} ) by XBOOLE_0:3;
( ( x = 0 or x = 1 or x = 2 or x = 9 ) & ( x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 ) ) by A3, ENUMSET1:def 2, ENUMSET1:def 4;
hence contradiction ; :: thesis: verum
end;
then reconsider r = ({0,1,2,9} --> 00) \/ ({3,4,5,6,7,8} --> x1) as Function by A2, GRFUNC_1:13;
A4: dom r = {0,1,2,9} \/ {3,4,5,6,7,8} by A2, XTUPLE_0:23
.= ({0,1,2} \/ {9}) \/ {3,4,5,6,7,8} by ENUMSET1:6
.= ({0,1,2} \/ {3,4,5,6,7,8}) \/ {9} by XBOOLE_1:4
.= {0,1,2,3,4,5,6,7,8} \/ {9} by Th13
.= {0,1,2,3,4,5,6,7,8,9} by ENUMSET1:85 ;
rng r = (rng ({0,1,2,9} --> 00)) \/ (rng ({3,4,5,6,7,8} --> x1)) by RELAT_1:12
.= {00} \/ (rng ({3,4,5,6,7,8} --> x1))
.= {00} \/ {x1}
.= {0,1} by ENUMSET1:1 ;
then reconsider r = r as Function of {0,1,2,3,4,5,6,7,8,9},{0,1} by A4, FUNCT_2:2;
set B = BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #);
A5: len the connectives of BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) = (len <*y0,01,02,03,04,05,06,07*>) + (len <*08,09*>) by FINSEQ_1:22
.= 8 + (len <*08,09*>) by Th19
.= 8 + 2 by FINSEQ_1:44
.= 10 ;
( BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is 10 -connectives & not BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is empty & not BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is void ) by A5;
then reconsider B = BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) as non empty non void 10 -connectives strict BoolSignature ;
take B ; :: thesis: ( B is 1-1-connectives & B is 4,1 integer & B is bool-correct & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
thus the connectives of B is one-to-one :: according to AOFA_A00:def 28 :: thesis: ( B is 4,1 integer & B is bool-correct & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 the connectives of B or not y in proj1 the connectives of B or not the connectives of B . x = the connectives of B . y or x = y )
assume A6: ( x in dom the connectives of B & y in dom the connectives of B ) ; :: thesis: ( not the connectives of B . x = the connectives of B . y or x = y )
set c = the connectives of B;
A7: dom the connectives of B = Seg 10 by Th25;
A8: ( y = 1 or y = 2 or y = 3 or y = 4 or y = 5 or y = 6 or y = 7 or y = 8 or y = 9 or y = 10 ) by A6, A7, Th23, ENUMSET1:def 8;
( the connectives of B . 1 = y0 & the connectives of B . 2 = 01 & the connectives of B . 3 = 02 & the connectives of B . 4 = 03 & the connectives of B . 5 = 04 & the connectives of B . 6 = 05 & the connectives of B . 7 = 06 & the connectives of B . 8 = 07 & the connectives of B . 9 = 08 & the connectives of B . 10 = 09 ) by Th25;
hence ( not the connectives of B . x = the connectives of B . y or x = y ) by A7, A8, A6, Th23, ENUMSET1:def 8; :: thesis: verum
end;
thus B is 4,1 integer :: thesis: ( B is bool-correct & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
proof
thus len the connectives of B >= 4 + 6 by A5; :: according to AOFA_A00:def 38 :: thesis: ex I being Element of B st
( I = 1 & I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
reconsider I = x1 as Element of B ;
take I ; :: thesis: ( I = 1 & I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
thus I = 1 ; :: thesis: ( I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
thus I <> the bool-sort of B ; :: thesis: ( the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
A9: ( the connectives of B . 4 = 3 & 3 nin dom ({0} --> {}) ) by Th25;
hence the Arity of B . ( the connectives of B . 4) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 3 by FUNCT_4:11
.= {} by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 4) = I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
( 3 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;
then [3,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;
then [3,I] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . 4) = I by A9, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
A10: ( the connectives of B . 5 = 4 & 4 nin dom ({0} --> {}) ) by Th25;
hence the Arity of B . ( the connectives of B . (4 + 1)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 4 by FUNCT_4:11
.= {} by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 1)) = I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
( 4 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;
then [4,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;
then [4,I] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . (4 + 1)) = I by A10, FUNCT_1:1; :: thesis: ( the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
thus the connectives of B . 4 <> the connectives of B . (4 + 1) by A9, Th25; :: thesis: ( the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
A11: ( the connectives of B . 6 = 5 & 5 nin dom ({0} --> {}) ) by Th25;
hence the Arity of B . ( the connectives of B . (4 + 2)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 5 by FUNCT_4:11
.= <*I*> by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 2)) = I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
( 5 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;
then [5,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;
then [5,I] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . (4 + 2)) = I by A11, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
A12: ( the connectives of B . 7 = 6 & 6 nin dom ({0} --> {}) ) by Th25;
hence the Arity of B . ( the connectives of B . (4 + 3)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 6 by FUNCT_4:11
.= <*I,I*> by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 3)) = I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
( 6 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;
then [6,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;
then [6,I] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . (4 + 3)) = I by A12, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
A13: ( the connectives of B . 8 = 7 & 7 nin dom ({0} --> {}) ) by Th25;
hence the Arity of B . ( the connectives of B . (4 + 4)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 7 by FUNCT_4:11
.= <*I,I*> by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 4)) = I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
( 7 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;
then [7,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;
then [7,I] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . (4 + 4)) = I by A13, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
A14: ( the connectives of B . 9 = 8 & 8 nin dom ({0} --> {}) ) by Th25;
hence the Arity of B . ( the connectives of B . (4 + 5)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 8 by FUNCT_4:11
.= <*I,I*> by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 5)) = I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
( 8 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;
then [8,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;
then [8,I] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . (4 + 5)) = I by A14, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
thus the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) by A13, Th25; :: thesis: ( the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
thus the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) by A14, Th25; :: thesis: ( the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )
thus the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) by A14, Th25; :: thesis: the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B
A15: ( the connectives of B . 10 = 9 & 9 nin dom ({0} --> {}) ) by Th25;
hence the Arity of B . ( the connectives of B . (4 + 6)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 9 by FUNCT_4:11
.= <*I,I*> by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: the ResultSort of B . ( the connectives of B . (4 + 6)) = the bool-sort of B
( 9 in {0,1,2,9} & the bool-sort of B in { the bool-sort of B} ) by TARSKI:def 1, ENUMSET1:def 2;
then [9,00] in {0,1,2,9} --> 00 by ZFMISC_1:87;
then [9,00] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . (4 + 6)) = the bool-sort of B by A15, FUNCT_1:1; :: thesis: verum
end;
thus len the connectives of B >= 3 by A5; :: according to AOFA_A00:def 30 :: thesis: ( the connectives of B . 1 is_of_type {} , the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
A16: ( the connectives of B . 1 = 0 & 0 in {0} ) by Th25, TARSKI:def 1;
hence the Arity of B . ( the connectives of B . 1) = ({0} --> {}) . 0 by A1, FUNCT_4:13
.= {} ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 1) = the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
( 0 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;
then [0, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;
then [0, the bool-sort of B] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . 1) = the bool-sort of B by A16, FUNCT_1:1; :: thesis: ( the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
A17: ( the connectives of B . 2 = 1 & 1 nin {0} ) by Th25, TARSKI:def 1;
hence the Arity of B . ( the connectives of B . 2) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 1 by A1, FUNCT_4:11
.= <* the bool-sort of B*> by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 2) = the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
( 1 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;
then [1, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;
then [1, the bool-sort of B] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . 2) = the bool-sort of B by A17, FUNCT_1:1; :: thesis: ( the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
A18: ( the connectives of B . 3 = 2 & 2 nin {0} ) by Th25, TARSKI:def 1;
hence the Arity of B . ( the connectives of B . 3) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 2 by A1, FUNCT_4:11
.= <* the bool-sort of B, the bool-sort of B*> by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 3) = the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
( 2 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;
then [2, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;
then [2, the bool-sort of B] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . 3) = the bool-sort of B by A18, FUNCT_1:1; :: thesis: ( the carrier of B = {0,1} & ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )
thus the carrier of B = {0,1} ; :: thesis: ex I being SortSymbol of B st
( I = 1 & the connectives of B . 4 is_of_type {} ,I )
reconsider I = 1 as SortSymbol of B ;
take I ; :: thesis: ( I = 1 & the connectives of B . 4 is_of_type {} ,I )
thus I = 1 ; :: thesis: the connectives of B . 4 is_of_type {} ,I
A19: ( the connectives of B . 4 = 3 & 3 nin dom ({0} --> {}) ) by Th25;
hence the Arity of B . ( the connectives of B . 4) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 3 by FUNCT_4:11
.= {} by Th24 ;
:: according to AOFA_A00:def 8 :: thesis: the ResultSort of B . ( the connectives of B . 4) = I
( 3 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;
then [3,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;
then [3,I] in r by XBOOLE_0:def 3;
hence the ResultSort of B . ( the connectives of B . 4) = I by A19, FUNCT_1:1; :: thesis: verum