for A being ECIW-strict preIfWhileAlgebra
for x being set
for n being Nat holds
( not x in (ElementaryInstructions A) |^ (n + 1) or x in (ElementaryInstructions A) |^ n or x = EmptyIns A or ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )