scheme :: AOFA_000:sch 7
IndDef{ F₁() -> free ECIW-strict preIfWhileAlgebra, F₂() -> non empty set , F₃() -> Element of F₂(), F₄( set ) -> set , F₅( set , set ) -> Element of F₂(), F₆( set , set ) -> Element of F₂(), F₇( set , set , set ) -> Element of F₂() } :

ex f being Function of the carrier of F₁(),F₂() st
( ( for I being Element of F₁() st I in ElementaryInstructions F₁() holds
f . I = F₄(I) ) & f . (EmptyIns F₁()) = F₃() & ( for I1, I2 being Element of F₁() holds f . (I1 \; I2) = F₅((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F₁() holds f . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F₁() holds f . (while (C,I)) = F₆((f . C),(f . I)) ) )

provided