for S being non empty non void bool-correct 4,1 integer BoolSignature
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 ) ) ) )