:: deftheorem Def19 defines := AOFA_A01:def 19 :
for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature
for X being non-empty ManySortedSet of the carrier of S
for T being non-empty b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for G being basic GeneratorSystem over S,X,T
for A being elementary IfWhileAlgebra of the generators of G
for a being SortSymbol of S
for t1, t2 being Element of T,a st t1 in the generators of G . a holds
t1 := (t2,A) = the assignments of A . [t1,t2];