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}
;
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
;
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
; ( 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
AOFA_A00:def 28 ( 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
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
thus
len the
connectives of
B >= 4
+ 6
by A5;
AOFA_A00:def 38 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
;
( 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
;
( 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
;
( 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
;
AOFA_A00:def 8 ( 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;
( 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
;
AOFA_A00:def 8 ( 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;
( 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;
( 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
;
AOFA_A00:def 8 ( 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;
( 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
;
AOFA_A00:def 8 ( 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;
( 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
;
AOFA_A00:def 8 ( 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;
( 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
;
AOFA_A00:def 8 ( 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;
( 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;
( 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;
( 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;
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
;
AOFA_A00:def 8 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;
verum
end;
thus
len the connectives of B >= 3
by A5; AOFA_A00:def 30 ( 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
.=
{}
;
AOFA_A00:def 8 ( 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; ( 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
;
AOFA_A00:def 8 ( 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; ( 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
;
AOFA_A00:def 8 ( 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; ( 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}
; 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
; ( I = 1 & the connectives of B . 4 is_of_type {} ,I )
thus
I = 1
; 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
;
AOFA_A00:def 8 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; verum