for S being non empty non void bool-correct 4,1 integer BoolSignature
for X being V3() 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 st A is elementary holds
for a being SortSymbol of S
for x being Element of the generators of G . a
for t being Element of T,a holds x := (t,A) in ElementaryInstructions A