let n be Nat; :: thesis: for I being set st n >= 4 holds
for B being non empty non void bool-correct BoolSignature st B is n,I integer holds
for A1 being non-empty bool-correct MSAlgebra over B st A1 is n,I integer holds
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,I integer
let s be set ; :: thesis: ( n >= 4 implies for B being non empty non void bool-correct BoolSignature st B is n,s integer holds
for A1 being non-empty bool-correct MSAlgebra over B st A1 is n,s integer holds
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer )
assume A1: n >= 4 ; :: thesis: for B being non empty non void bool-correct BoolSignature st B is n,s integer holds
for A1 being non-empty bool-correct MSAlgebra over B st A1 is n,s integer holds
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer
let B be non empty non void bool-correct BoolSignature ; :: thesis: ( B is n,s integer implies for A1 being non-empty bool-correct MSAlgebra over B st A1 is n,s integer holds
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer )
assume A2: B is n,s integer ; :: thesis: for A1 being non-empty bool-correct MSAlgebra over B st A1 is n,s integer holds
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer
let A1 be non-empty bool-correct MSAlgebra over B; :: thesis: ( A1 is n,s integer implies for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer )
given I being SortSymbol of B such that A3: ( I = s & the connectives of B . n is_of_type {} ,I & the Sorts of A1 . I = INT & (Den ((In (( the connectives of B . n), the carrier' of B)),A1)) . {} = 0 & (Den ((In (( the connectives of B . (n + 1)), the carrier' of B)),A1)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of B . (n + 2)), the carrier' of B)),A1)) . <*i*> = - i & (Den ((In (( the connectives of B . (n + 3)), the carrier' of B)),A1)) . <*i,j*> = i + j & (Den ((In (( the connectives of B . (n + 4)), the carrier' of B)),A1)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of B . (n + 5)), the carrier' of B)),A1)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of B . (n + 6)), the carrier' of B)),A1)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) ) ; :: according to AOFA_A00:def 49 :: thesis: for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer
let C be non empty non void ConnectivesSignature ; :: thesis: ( the carrier' of B misses the carrier' of C implies for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer )
assume A4: the carrier' of B misses the carrier' of C ; :: thesis: for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer
let A2 be non-empty MSAlgebra over C; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer )
assume A5: the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer
let S be non empty non void bool-correct BoolSignature ; :: thesis: ( BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C implies for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer )
assume A6: BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C ; :: thesis: for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,s integer
let A be non-empty bool-correct MSAlgebra over S; :: thesis: ( A = (B,A1) +* A2 implies A is n,s integer )
assume A7: A = (B,A1) +* A2 ; :: thesis: A is n,s integer
the carrier of S = the carrier of B \/ the carrier of C by A6, Th51;
then reconsider I = I as SortSymbol of S by XBOOLE_0:def 3;
take I ; :: according to AOFA_A00:def 49 :: thesis: ( I = s & the connectives of S . n is_of_type {} ,I & the Sorts of A . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
thus I = s by A3; :: thesis: ( the connectives of S . n is_of_type {} ,I & the Sorts of A . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
A8: dom the Sorts of A1 = the carrier of B by PARTFUN1:def 2;
A9: ( the Sorts of A = the Sorts of A1 +* the Sorts of A2 & the Charact of A = the Charact of A1 +* the Charact of A2 ) by A5, A7, CIRCCOMB:def 4;
A10: ( len the connectives of B >= n + 6 & n <= n + 6 ) by A2, NAT_1:12;
then ( 1 <= n & n <= len the connectives of B ) by A1, XXREAL_0:2;
then A11: ( n in dom the connectives of B & the connectives of S = the connectives of B ^ the connectives of C ) by A6, Def52, FINSEQ_3:25;
then A12: ( the connectives of S . n = the connectives of B . n & the connectives of B . n in the carrier' of B ) by FUNCT_1:102, FINSEQ_1:def 7;
A13: ( dom the ResultSort of B = the carrier' of B & dom the ResultSort of C = the carrier' of C & dom the Arity of B = the carrier' of B & dom the Arity of C = the carrier' of C ) by FUNCT_2:def 1;
( the ResultSort of S = the ResultSort of B +* the ResultSort of C & the Arity of S = the Arity of B +* the Arity of C ) by A6, Th51;
then ( the ResultSort of S . ( the connectives of S . n) = the ResultSort of B . ( the connectives of B . n) & the Arity of S . ( the connectives of S . n) = the Arity of B . ( the connectives of B . n) ) by A4, A12, A13, FUNCT_4:16;
hence ( the Arity of S . ( the connectives of S . n) = {} & the ResultSort of S . ( the connectives of S . n) = I ) by A3; :: according to AOFA_A00:def 8 :: thesis: ( the Sorts of A . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
thus the Sorts of A . I = INT by A8, A9, A3, A5, FUNCT_4:15; :: thesis: ( (Den ((In (( the connectives of S . n), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
A14: now :: thesis: for i being Nat st i >= 4 & i <= n + 6 holds
Den ((In (( the connectives of S . i), the carrier' of S)),A) = Den ((In (( the connectives of B . i), the carrier' of B)),A1)
let i be Nat; :: thesis: ( i >= 4 & i <= n + 6 implies Den ((In (( the connectives of S . i), the carrier' of S)),A) = Den ((In (( the connectives of B . i), the carrier' of B)),A1) )
assume ( i >= 4 & i <= n + 6 ) ; :: thesis: Den ((In (( the connectives of S . i), the carrier' of S)),A) = Den ((In (( the connectives of B . i), the carrier' of B)),A1)
then ( 1 <= i & i <= len the connectives of B ) by A10, XXREAL_0:2;
then A15: i in dom the connectives of B by FINSEQ_3:25;
then A16: ( the connectives of B . i in the carrier' of B & the connectives of B . i = the connectives of S . i ) by A11, FUNCT_1:102, FINSEQ_1:def 7;
the carrier' of S = the carrier' of B \/ the carrier' of C by A6, Th51;
then the connectives of S . i in the carrier' of S by A16, XBOOLE_0:def 3;
then A17: ( In (( the connectives of B . i), the carrier' of B) = the connectives of B . i & In (( the connectives of S . i), the carrier' of S) = the connectives of S . i ) by A15, FUNCT_1:102, SUBSET_1:def 8;
( dom the Charact of A1 = the carrier' of B & dom the Charact of A2 = the carrier' of C ) by PARTFUN1:def 2;
hence Den ((In (( the connectives of S . i), the carrier' of S)),A) = Den ((In (( the connectives of B . i), the carrier' of B)),A1) by A9, A16, A17, A4, FUNCT_4:16; :: thesis: verum
end;
n <= n + 6 by NAT_1:11;
hence (Den ((In (( the connectives of S . n), the carrier' of S)),A)) . {} = 0 by A1, A3, A14; :: thesis: ( (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
( n + 1 >= 4 & n + 1 <= n + 6 ) by A1, NAT_1:12, XREAL_1:6;
hence (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),A)) . {} = 1 by A3, A14; :: thesis: for i, j being Integer holds
( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
let i, j be Integer; :: thesis: ( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
( n + 2 >= 4 & n + 2 <= n + 6 ) by A1, NAT_1:12, XREAL_1:6;
hence (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = (Den ((In (( the connectives of B . (n + 2)), the carrier' of B)),A1)) . <*i*> by A14
.= - i by A3 ;
:: thesis: ( (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
( n + 3 >= 4 & n + 3 <= n + 6 ) by A1, NAT_1:12, XREAL_1:6;
hence (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = (Den ((In (( the connectives of B . (n + 3)), the carrier' of B)),A1)) . <*i,j*> by A14
.= i + j by A3 ;
:: thesis: ( (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
( n + 4 >= 4 & n + 4 <= n + 6 ) by NAT_1:12, XREAL_1:6;
hence (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = (Den ((In (( the connectives of B . (n + 4)), the carrier' of B)),A1)) . <*i,j*> by A14
.= i * j by A3 ;
:: thesis: ( ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
hereby :: thesis: (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE)
assume A18: j <> 0 ; :: thesis: (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j
( n + 5 >= 4 & n + 5 <= n + 6 ) by NAT_1:12, XREAL_1:6;
hence (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = (Den ((In (( the connectives of B . (n + 5)), the carrier' of B)),A1)) . <*i,j*> by A14
.= i div j by A18, A3 ;
:: thesis: verum
end;
n + 6 >= 4 by NAT_1:12;
hence (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = (Den ((In (( the connectives of B . (n + 6)), the carrier' of B)),A1)) . <*i,j*> by A14
.= IFGT (i,j,FALSE,TRUE) by A3 ;
:: thesis: verum