let s, I be set ; for S being non empty non void bool-correct BoolSignature st S is 4,I integer holds
for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S holds
ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X )
let S be non empty non void bool-correct BoolSignature ; ( S is 4,I integer implies for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S holds
ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X ) )
assume A1:
S is 4,I integer
; for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S holds
ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X )
then consider J being Element of S such that
A2:
( J = I & J <> the bool-sort of S & the connectives of S . 4 is_of_type {} ,J & the connectives of S . (4 + 1) is_of_type {} ,J & the connectives of S . 4 <> the connectives of S . (4 + 1) & the connectives of S . (4 + 2) is_of_type <*J*>,J & the connectives of S . (4 + 3) is_of_type <*J,J*>,J & the connectives of S . (4 + 4) is_of_type <*J,J*>,J & the connectives of S . (4 + 5) is_of_type <*J,J*>,J & the connectives of S . (4 + 3) <> the connectives of S . (4 + 4) & the connectives of S . (4 + 3) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 4) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 6) is_of_type <*J,J*>, the bool-sort of S )
;
A3:
( len the connectives of S >= 3 & the connectives of S . 1 is_of_type {} , the bool-sort of S & the connectives of S . 2 is_of_type <* the bool-sort of S*>, the bool-sort of S & the connectives of S . 3 is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S )
by Def30;
let X be non empty set ; ( s in the carrier of S & s <> I & s <> the bool-sort of S implies ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X ) )
assume A4:
s in the carrier of S
; ( not s <> I or not s <> the bool-sort of S or ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X ) )
assume A5:
s <> I
; ( not s <> the bool-sort of S or ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X ) )
assume A6:
s <> the bool-sort of S
; ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X )
consider A being strict non-empty bool-correct MSAlgebra over S such that
A7:
A is 4,I integer
by A1, Th49;
A8:
( the Sorts of A . the bool-sort of S = BOOLEAN & (Den ((In (( the connectives of S . 1), the carrier' of S)),A)) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),A)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),A)) . <*x,y*> = x '&' y ) ) )
by Def31;
consider K being SortSymbol of S such that
A9:
( K = I & the connectives of S . 4 is_of_type {} ,K & the Sorts of A . K = INT & (Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
by A7;
set Q = the Sorts of A +* (s,X);
set F = the ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S;
set Ch = the ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S +* ( the Charact of A | ( the connectives of S .: (Seg 10)));
dom the Charact of A = the carrier' of S
by PARTFUN1:def 2;
then A10:
dom ( the Charact of A | ( the connectives of S .: (Seg 10))) = the connectives of S .: (Seg 10)
by Th1, RELAT_1:62;
reconsider Ch = the ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S +* ( the Charact of A | ( the connectives of S .: (Seg 10))) as ManySortedFunction of the carrier' of S ;
Ch is ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S
proof
let x be
object ;
PBOOLE:def 15 ( not x in the carrier' of S or Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):] )
assume
x in the
carrier' of
S
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]
then reconsider o =
x as
OperSymbol of
S ;
per cases
( x in the connectives of S .: (Seg 10) or x nin the connectives of S .: (Seg 10) )
;
suppose A11:
x in the
connectives of
S .: (Seg 10)
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]then A12:
Ch . x =
( the Charact of A | ( the connectives of S .: (Seg 10))) . x
by A10, FUNCT_4:13
.=
the
Charact of
A . x
by A11, FUNCT_1:49
;
A13:
(
(( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . ( the Arity of S . o) &
( the Sorts of A * the ResultSort of S) . o = the
Sorts of
A . ( the ResultSort of S . o) &
((( the Sorts of A +* (s,X)) #) * the Arity of S) . o = (( the Sorts of A +* (s,X)) #) . ( the Arity of S . x) &
(( the Sorts of A +* (s,X)) * the ResultSort of S) . o = ( the Sorts of A +* (s,X)) . ( the ResultSort of S . x) )
by FUNCT_2:15;
consider y being
object such that A14:
(
y in dom the
connectives of
S &
y in Seg 10 &
o = the
connectives of
S . y )
by A11, FUNCT_1:def 6;
per cases
( 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 A14, Th23, ENUMSET1:def 8;
suppose
y = 1
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]then
( the
Arity of
S . o = {} & the
ResultSort of
S . o = the
bool-sort of
S &
<*> the
carrier of
S in the
carrier of
S * )
by A3, A14, FINSEQ_1:def 11;
then
(
( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * (<*> the carrier of S)) &
(( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * (<*> the carrier of S)) & the
Sorts of
A . ( the ResultSort of S . o) = BOOLEAN &
( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = BOOLEAN )
by A6, A8, FINSEQ_2:def 5, FUNCT_7:32;
hence
Ch . x is
Function of
(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),
((( the Sorts of A +* (s,X)) * the ResultSort of S) . x)
by A12, A13;
verum end; suppose
y = 2
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]then
( the
Arity of
S . o = <* the bool-sort of S*> & the
ResultSort of
S . o = the
bool-sort of
S &
<* the bool-sort of S*> in the
carrier of
S * )
by A3, A14, FINSEQ_1:def 11;
then A15:
(
( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <* the bool-sort of S*>) &
(( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <* the bool-sort of S*>) & the
Sorts of
A . ( the ResultSort of S . o) = BOOLEAN &
( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = BOOLEAN )
by A6, A8, FINSEQ_2:def 5, FUNCT_7:32;
(
dom the
Sorts of
A = the
carrier of
S &
dom ( the Sorts of A +* (s,X)) = the
carrier of
S )
by PARTFUN1:def 2;
then
( the
Sorts of
A * <* the bool-sort of S*> = <*( the Sorts of A . the bool-sort of S)*> &
( the Sorts of A +* (s,X)) * <* the bool-sort of S*> = <*(( the Sorts of A +* (s,X)) . the bool-sort of S)*> & the
Sorts of
A . the
bool-sort of
S = ( the Sorts of A +* (s,X)) . the
bool-sort of
S )
by A6, FUNCT_7:32, FINSEQ_2:34;
hence
Ch . x is
Function of
(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),
((( the Sorts of A +* (s,X)) * the ResultSort of S) . x)
by A12, A13, A15;
verum end; suppose
y = 3
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]then
( the
Arity of
S . o = <* the bool-sort of S, the bool-sort of S*> & the
ResultSort of
S . o = the
bool-sort of
S &
<* the bool-sort of S, the bool-sort of S*> in the
carrier of
S * )
by A3, A14, FINSEQ_1:def 11;
then A16:
(
( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <* the bool-sort of S, the bool-sort of S*>) &
(( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <* the bool-sort of S, the bool-sort of S*>) & the
Sorts of
A . ( the ResultSort of S . o) = BOOLEAN &
( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = BOOLEAN )
by A6, A8, FINSEQ_2:def 5, FUNCT_7:32;
(
dom the
Sorts of
A = the
carrier of
S &
dom ( the Sorts of A +* (s,X)) = the
carrier of
S )
by PARTFUN1:def 2;
then
( the
Sorts of
A * <* the bool-sort of S, the bool-sort of S*> = <*( the Sorts of A . the bool-sort of S),( the Sorts of A . the bool-sort of S)*> &
( the Sorts of A +* (s,X)) * <* the bool-sort of S, the bool-sort of S*> = <*(( the Sorts of A +* (s,X)) . the bool-sort of S),(( the Sorts of A +* (s,X)) . the bool-sort of S)*> & the
Sorts of
A . the
bool-sort of
S = ( the Sorts of A +* (s,X)) . the
bool-sort of
S )
by A6, FUNCT_7:32, FINSEQ_2:125;
hence
Ch . x is
Function of
(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),
((( the Sorts of A +* (s,X)) * the ResultSort of S) . x)
by A12, A13, A16;
verum end; suppose
(
y = 4 or
y = 5 )
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]then
( the
Arity of
S . o = {} & the
ResultSort of
S . o = J &
<*> the
carrier of
S in the
carrier of
S * )
by A2, A14, FINSEQ_1:def 11;
then
(
( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * (<*> the carrier of S)) &
(( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * (<*> the carrier of S)) & the
Sorts of
A . ( the ResultSort of S . o) = INT &
( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = INT )
by A5, A2, A9, FINSEQ_2:def 5, FUNCT_7:32;
hence
Ch . x is
Function of
(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),
((( the Sorts of A +* (s,X)) * the ResultSort of S) . x)
by A12, A13;
verum end; suppose
y = 6
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]then
( the
Arity of
S . o = <*J*> & the
ResultSort of
S . o = J &
<*J*> in the
carrier of
S * )
by A2, A14, FINSEQ_1:def 11;
then A17:
(
( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <*J*>) &
(( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <*J*>) & the
Sorts of
A . ( the ResultSort of S . o) = INT &
( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = INT )
by A5, A2, A9, FINSEQ_2:def 5, FUNCT_7:32;
(
dom the
Sorts of
A = the
carrier of
S &
dom ( the Sorts of A +* (s,X)) = the
carrier of
S )
by PARTFUN1:def 2;
then
( the
Sorts of
A * <*J*> = <*( the Sorts of A . J)*> &
( the Sorts of A +* (s,X)) * <*J*> = <*(( the Sorts of A +* (s,X)) . J)*> & the
Sorts of
A . J = ( the Sorts of A +* (s,X)) . J )
by A2, A5, FUNCT_7:32, FINSEQ_2:34;
hence
Ch . x is
Function of
(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),
((( the Sorts of A +* (s,X)) * the ResultSort of S) . x)
by A12, A13, A17;
verum end; suppose
(
y = 7 or
y = 8 or
y = 9 )
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]then
( the
Arity of
S . o = <*J,J*> & the
ResultSort of
S . o = J &
<*J,J*> in the
carrier of
S * )
by A2, A14, FINSEQ_1:def 11;
then A18:
(
( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <*J,J*>) &
(( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <*J,J*>) & the
Sorts of
A . ( the ResultSort of S . o) = INT &
( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = INT )
by A5, A2, A9, FINSEQ_2:def 5, FUNCT_7:32;
(
dom the
Sorts of
A = the
carrier of
S &
dom ( the Sorts of A +* (s,X)) = the
carrier of
S )
by PARTFUN1:def 2;
then
( the
Sorts of
A * <*J,J*> = <*( the Sorts of A . J),( the Sorts of A . J)*> &
( the Sorts of A +* (s,X)) * <*J,J*> = <*(( the Sorts of A +* (s,X)) . J),(( the Sorts of A +* (s,X)) . J)*> & the
Sorts of
A . J = ( the Sorts of A +* (s,X)) . J )
by A5, A2, FUNCT_7:32, FINSEQ_2:125;
hence
Ch . x is
Function of
(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),
((( the Sorts of A +* (s,X)) * the ResultSort of S) . x)
by A12, A13, A18;
verum end; suppose
y = 10
;
Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]then
( the
Arity of
S . o = <*J,J*> & the
ResultSort of
S . o = the
bool-sort of
S &
<*J,J*> in the
carrier of
S * )
by A2, A14, FINSEQ_1:def 11;
then A19:
(
( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <*J,J*>) &
(( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <*J,J*>) & the
Sorts of
A . ( the ResultSort of S . o) = BOOLEAN &
( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = BOOLEAN )
by A6, A8, FINSEQ_2:def 5, FUNCT_7:32;
(
dom the
Sorts of
A = the
carrier of
S &
dom ( the Sorts of A +* (s,X)) = the
carrier of
S )
by PARTFUN1:def 2;
then
( the
Sorts of
A * <*J,J*> = <*( the Sorts of A . J),( the Sorts of A . J)*> &
( the Sorts of A +* (s,X)) * <*J,J*> = <*(( the Sorts of A +* (s,X)) . J),(( the Sorts of A +* (s,X)) . J)*> & the
Sorts of
A . J = ( the Sorts of A +* (s,X)) . J )
by A5, A2, FUNCT_7:32, FINSEQ_2:125;
hence
Ch . x is
Function of
(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),
((( the Sorts of A +* (s,X)) * the ResultSort of S) . x)
by A12, A13, A19;
verum end; end;
end;
then reconsider Ch = Ch as ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S ;
set A0 = MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #);
A20:
MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) is bool-correct
proof
thus the
Sorts of
MSAlgebra(#
( the Sorts of A +* (s,X)),
Ch #)
. the
bool-sort of
S =
the
Sorts of
A . the
bool-sort of
S
by A6, FUNCT_7:32
.=
BOOLEAN
by Def31
;
AOFA_A00:def 31 ( (Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y ) ) )
4
+ 6
<= len the
connectives of
S
by A1;
then
1
<= len the
connectives of
S
by XXREAL_0:2;
then A21:
1
in dom the
connectives of
S
by FINSEQ_3:25;
then A22:
In (
( the connectives of S . 1), the
carrier' of
S)
= the
connectives of
S . 1
by SUBSET_1:def 8, FUNCT_1:102;
1
in Seg 10
;
then A23:
the
connectives of
S . 1
in the
connectives of
S .: (Seg 10)
by A21, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 1), the carrier' of S)),
MSAlgebra(#
( the Sorts of A +* (s,X)),
Ch #)) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 1)
by A22, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 1), the carrier' of S)),
A)
by A22, A23, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . {} = TRUE
by Def31;
for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y )
let x,
y be
boolean object ;
( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y )
4
+ 6
<= len the
connectives of
S
by A1;
then
2
<= len the
connectives of
S
by XXREAL_0:2;
then A24:
2
in dom the
connectives of
S
by FINSEQ_3:25;
then A25:
In (
( the connectives of S . 2), the
carrier' of
S)
= the
connectives of
S . 2
by SUBSET_1:def 8, FUNCT_1:102;
2
in Seg 10
;
then A26:
In (
( the connectives of S . 2), the
carrier' of
S)
in the
connectives of
S .: (Seg 10)
by A24, A25, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 2), the carrier' of S)),
MSAlgebra(#
( the Sorts of A +* (s,X)),
Ch #)) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 2)
by A25, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 2), the carrier' of S)),
A)
by A25, A26, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x*> = 'not' x
by Def31;
(Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y
4
+ 6
<= len the
connectives of
S
by A1;
then
3
<= len the
connectives of
S
by XXREAL_0:2;
then A27:
3
in dom the
connectives of
S
by FINSEQ_3:25;
then A28:
In (
( the connectives of S . 3), the
carrier' of
S)
= the
connectives of
S . 3
by SUBSET_1:def 8, FUNCT_1:102;
3
in Seg 10
;
then A29:
the
connectives of
S . 3
in the
connectives of
S .: (Seg 10)
by A27, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 3), the carrier' of S)),
MSAlgebra(#
( the Sorts of A +* (s,X)),
Ch #)) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 3)
by A28, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 3), the carrier' of S)),
A)
by A28, A29, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y
by Def31;
verum
end;
MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) is non-empty
;
then reconsider A0 = MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) as non-empty bool-correct MSAlgebra over S by A20;
take
A0
; ( A0 is 4,I integer & the Sorts of A0 . s = X )
thus
A0 is 4,I integer
the Sorts of A0 . s = Xproof
take
K
;
AOFA_A00:def 49 ( K = I & the connectives of S . 4 is_of_type {} ,K & the Sorts of A0 . K = INT & (Den ((In (( the connectives of S . 4), the carrier' of S)),A0)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
thus
(
K = I & the
connectives of
S . 4
is_of_type {} ,
K )
by A9;
( the Sorts of A0 . K = INT & (Den ((In (( the connectives of S . 4), the carrier' of S)),A0)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
thus
the
Sorts of
A0 . K = INT
by A9, A5, FUNCT_7:32;
( (Den ((In (( the connectives of S . 4), the carrier' of S)),A0)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
4
+ 6
<= len the
connectives of
S
by A1;
then
4
<= len the
connectives of
S
by XXREAL_0:2;
then A30:
4
in dom the
connectives of
S
by FINSEQ_3:25;
then A31:
In (
( the connectives of S . 4), the
carrier' of
S)
= the
connectives of
S . 4
by FUNCT_1:102, SUBSET_1:def 8;
4
in Seg 10
;
then A32:
the
connectives of
S . 4
in the
connectives of
S .: (Seg 10)
by A30, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 4), the carrier' of S)),
A0) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 4)
by A31, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 4), the carrier' of S)),
A)
by A31, A32, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . 4), the carrier' of S)),A0)) . {} = 0
by A9;
( (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
4
+ 6
<= len the
connectives of
S
by A1;
then
5
<= len the
connectives of
S
by XXREAL_0:2;
then A33:
5
in dom the
connectives of
S
by FINSEQ_3:25;
then A34:
In (
( the connectives of S . 5), the
carrier' of
S)
= the
connectives of
S . 5
by FUNCT_1:102, SUBSET_1:def 8;
5
in Seg 10
;
then A35:
the
connectives of
S . 5
in the
connectives of
S .: (Seg 10)
by A33, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 5), the carrier' of S)),
A0) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 5)
by A34, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 5), the carrier' of S)),
A)
by A34, A35, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1
by A9;
for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
let i,
j be
Integer;
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
4
+ 6
<= len the
connectives of
S
by A1;
then
6
<= len the
connectives of
S
by XXREAL_0:2;
then A36:
6
in dom the
connectives of
S
by FINSEQ_3:25;
then A37:
In (
( the connectives of S . 6), the
carrier' of
S)
= the
connectives of
S . 6
by FUNCT_1:102, SUBSET_1:def 8;
6
in Seg 10
;
then A38:
the
connectives of
S . 6
in the
connectives of
S .: (Seg 10)
by A36, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 6), the carrier' of S)),
A0) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 6)
by A37, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 6), the carrier' of S)),
A)
by A37, A38, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i
by A9;
( (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
4
+ 6
<= len the
connectives of
S
by A1;
then
7
<= len the
connectives of
S
by XXREAL_0:2;
then A39:
7
in dom the
connectives of
S
by FINSEQ_3:25;
then A40:
In (
( the connectives of S . 7), the
carrier' of
S)
= the
connectives of
S . 7
by FUNCT_1:102, SUBSET_1:def 8;
7
in Seg 10
;
then A41:
the
connectives of
S . 7
in the
connectives of
S .: (Seg 10)
by A39, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 7), the carrier' of S)),
A0) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 7)
by A40, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 7), the carrier' of S)),
A)
by A40, A41, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j
by A9;
( (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
4
+ 6
<= len the
connectives of
S
by A1;
then
8
<= len the
connectives of
S
by XXREAL_0:2;
then A42:
8
in dom the
connectives of
S
by FINSEQ_3:25;
then A43:
In (
( the connectives of S . 8), the
carrier' of
S)
= the
connectives of
S . 8
by FUNCT_1:102, SUBSET_1:def 8;
8
in Seg 10
;
then A44:
the
connectives of
S . 8
in the
connectives of
S .: (Seg 10)
by A42, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 8), the carrier' of S)),
A0) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 8)
by A43, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 8), the carrier' of S)),
A)
by A43, A44, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j
by A9;
( ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
hereby (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE)
assume A45:
j <> 0
;
(Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j
4
+ 6
<= len the
connectives of
S
by A1;
then
9
<= len the
connectives of
S
by XXREAL_0:2;
then A46:
9
in dom the
connectives of
S
by FINSEQ_3:25;
then A47:
In (
( the connectives of S . 9), the
carrier' of
S)
= the
connectives of
S . 9
by FUNCT_1:102, SUBSET_1:def 8;
9
in Seg 10
;
then A48:
the
connectives of
S . 9
in the
connectives of
S .: (Seg 10)
by A46, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 9), the carrier' of S)),
A0) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 9)
by A47, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 9), the carrier' of S)),
A)
by A47, A48, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j
by A45, A9;
verum
end;
4
+ 6
<= len the
connectives of
S
by A1;
then A49:
10
in dom the
connectives of
S
by FINSEQ_3:25;
then A50:
In (
( the connectives of S . 10), the
carrier' of
S)
= the
connectives of
S . 10
by FUNCT_1:102, SUBSET_1:def 8;
10
in Seg 10
;
then A51:
the
connectives of
S . 10
in the
connectives of
S .: (Seg 10)
by A49, FUNCT_1:def 6;
then Den (
(In (( the connectives of S . 10), the carrier' of S)),
A0) =
( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 10)
by A50, A10, FUNCT_4:13
.=
Den (
(In (( the connectives of S . 10), the carrier' of S)),
A)
by A50, A51, FUNCT_1:49
;
hence
(Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (
i,
j,
FALSE,
TRUE)
by A9;
verum
end;
dom the Sorts of A = the carrier of S
by PARTFUN1:def 2;
hence
the Sorts of A0 . s = X
by A4, FUNCT_7:31; verum