let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis:
let A be non-empty bool-correct 4,1 integer MSAlgebra over S; :: thesis:
let I be integer SortSymbol of S; :: thesis:
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:
thus \0 (A,I) = 0 by A1; :: thesis:
thus \1 (A,I) = 1 by A1; :: thesis:
let i, j be Integer; :: thesis:
let a, b be Element of the Sorts of A . I; :: thesis:
assume A2: a = i ; :: thesis:
assume A3: b = j ; :: thesis:
thus - a = - i by A1, A2; :: thesis:
thus a + b = i + j by A1, A2, A3; :: thesis:
thus a * b = i * j by A1, A2, A3; :: thesis:
thus ( j <> 0 implies a div b = i div j ) by A1, A2, A3; :: thesis:
thus A4: leq (a,b) = IFGT (i,j,FALSE,TRUE) by A1, A2, A3; :: thesis:
thus ( leq (a,b) = TRUE iff i <= j ) by A4, XXREAL_0:def 11; :: thesis:
thus ( leq (a,b) = FALSE implies i > j ) by A4, XXREAL_0:def 11; :: thesis:
assume i > j ; :: thesis:
hence leq (a,b) = FALSE by A4, XXREAL_0:def 11; :: thesis: