let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for A being non-empty bool-correct 4,1 integer MSAlgebra over S

for I being integer SortSymbol of S holds

( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

let A be non-empty bool-correct 4,1 integer MSAlgebra over S; :: thesis: for I being integer SortSymbol of S holds

( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

let I be integer SortSymbol of S; :: thesis: ( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

set n = 4;

consider J being SortSymbol of S such that

A1: ( J = 1 & the connectives of S . 4 is_of_type {} ,J & the Sorts of A . J = 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 Def49;

thus the Sorts of A . I = INT by A1, Def39; :: thesis: ( \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

thus \0 (A,I) = 0 by A1; :: thesis: ( \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

thus \1 (A,I) = 1 by A1; :: thesis: for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

let i, j be Integer; :: thesis: for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

let a, b be Element of the Sorts of A . I; :: thesis: ( a = i & b = j implies ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) )

assume A2: a = i ; :: thesis: ( not b = j or ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) )

assume A3: b = j ; :: thesis: ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus - a = - i by A1, A2; :: thesis: ( a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus a + b = i + j by A1, A2, A3; :: thesis: ( a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus a * b = i * j by A1, A2, A3; :: thesis: ( ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus ( j <> 0 implies a div b = i div j ) by A1, A2, A3; :: thesis: ( leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus A4: leq (a,b) = IFGT (i,j,FALSE,TRUE) by A1, A2, A3; :: thesis: ( ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus ( leq (a,b) = TRUE iff i <= j ) by A4, XXREAL_0:def 11; :: thesis: ( ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus ( leq (a,b) = FALSE implies i > j ) by A4, XXREAL_0:def 11; :: thesis: ( i > j implies leq (a,b) = FALSE )

assume i > j ; :: thesis: leq (a,b) = FALSE

hence leq (a,b) = FALSE by A4, XXREAL_0:def 11; :: thesis: verum

for I being integer SortSymbol of S holds

( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

let A be non-empty bool-correct 4,1 integer MSAlgebra over S; :: thesis: for I being integer SortSymbol of S holds

( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

let I be integer SortSymbol of S; :: thesis: ( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

set n = 4;

consider J being SortSymbol of S such that

A1: ( J = 1 & the connectives of S . 4 is_of_type {} ,J & the Sorts of A . J = 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 Def49;

thus the Sorts of A . I = INT by A1, Def39; :: thesis: ( \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

thus \0 (A,I) = 0 by A1; :: thesis: ( \1 (A,I) = 1 & ( for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )

thus \1 (A,I) = 1 by A1; :: thesis: for i, j being Integer

for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

let i, j be Integer; :: thesis: for a, b being Element of the Sorts of A . I st a = i & b = j holds

( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

let a, b be Element of the Sorts of A . I; :: thesis: ( a = i & b = j implies ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) )

assume A2: a = i ; :: thesis: ( not b = j or ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) )

assume A3: b = j ; :: thesis: ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus - a = - i by A1, A2; :: thesis: ( a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus a + b = i + j by A1, A2, A3; :: thesis: ( a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus a * b = i * j by A1, A2, A3; :: thesis: ( ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus ( j <> 0 implies a div b = i div j ) by A1, A2, A3; :: thesis: ( leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus A4: leq (a,b) = IFGT (i,j,FALSE,TRUE) by A1, A2, A3; :: thesis: ( ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus ( leq (a,b) = TRUE iff i <= j ) by A4, XXREAL_0:def 11; :: thesis: ( ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )

thus ( leq (a,b) = FALSE implies i > j ) by A4, XXREAL_0:def 11; :: thesis: ( i > j implies leq (a,b) = FALSE )

assume i > j ; :: thesis: leq (a,b) = FALSE

hence leq (a,b) = FALSE by A4, XXREAL_0:def 11; :: thesis: verum