:: deftheorem defines gt AOFA_A01:def 9 :
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 t1, t2 being Element of T,I holds b gt (t1,t2,A) = b := ((\not (leq (t1,t2))),A);