:: deftheorem defines is_odd AOFA_A01:def 11 :
for S being non empty non void bool-correct 4,1 integer BoolSignature
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for b being pure Element of the generators of G . the bool-sort of S
for I being integer SortSymbol of S
for t being Element of T,I holds t is_odd (b,A) = b gt ((t mod (\2 (T,I))),(\0 (T,I)),A);