:: deftheorem Def49 defines integer AOFA_A00:def 49 :
for n being Nat
for s being set
for S being non empty non void bool-correct BoolSignature
for A being bool-correct MSAlgebra over S holds
( A is n,s integer iff ex I being SortSymbol of S st
( 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) ) ) ) );