:: deftheorem Def38 defines integer AOFA_A00:def 38 :
for i being Nat
for s being set
for S being BoolSignature holds
( S is i,s integer iff ( len the connectives of S >= i + 6 & ex I being Element of S st
( I = s & I <> the bool-sort of S & the connectives of S . i is_of_type {} ,I & the connectives of S . (i + 1) is_of_type {} ,I & the connectives of S . i <> the connectives of S . (i + 1) & the connectives of S . (i + 2) is_of_type <*I*>,I & the connectives of S . (i + 3) is_of_type <*I,I*>,I & the connectives of S . (i + 4) is_of_type <*I,I*>,I & the connectives of S . (i + 5) is_of_type <*I,I*>,I & the connectives of S . (i + 3) <> the connectives of S . (i + 4) & the connectives of S . (i + 3) <> the connectives of S . (i + 5) & the connectives of S . (i + 4) <> the connectives of S . (i + 5) & the connectives of S . (i + 6) is_of_type <*I,I*>, the bool-sort of S ) ) );