scheme :: AOFA_I00:sch 1
ForToIteration{ F₁() -> Euclidean preIfWhileAlgebra, F₂() -> non empty countable set , F₃() -> Element of F₂(), F₄() -> Element of F₁(), F₅() -> Element of F₁(), F₆() -> Euclidean ExecutionFunction of F₁(), Funcs (F₂(),INT),(Funcs (F₂(),INT)) \ (F₃(),0), F₇() -> Variable of F₆(), F₈() -> Variable of F₆(), F₉() -> Element of Funcs (F₂(),INT), F₁₀() -> INT-Expression of F₁(),F₆(), P₁[ set ] } :

( P₁[F₆() . (F₉(),F₅())] & ( F₁₀() . F₉() <= F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = (F₉() . F₈()) + 1 ) & ( F₁₀() . F₉() > F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = F₁₀() . F₉() ) & (F₆() . (F₉(),F₅())) . F₈() = F₉() . F₈() )

provided

A1: F₅() = for-do ((F₇() := F₁₀()),(F₇() leq F₈()),(F₇() += 1),F₄()) and
A2: P₁[F₆() . (F₉(),(F₇() := F₁₀()))] and
A3: for s being Element of Funcs (F₂(),INT) st P₁[s] holds
( P₁[F₆() . (s,(F₄() \; (F₇() += 1)))] & P₁[F₆() . (s,(F₇() leq F₈()))] ) and
A4: for s being Element of Funcs (F₂(),INT) st P₁[s] holds
( (F₆() . (s,F₄())) . F₇() = s . F₇() & (F₆() . (s,F₄())) . F₈() = s . F₈() ) and
A5: ( F₈() <> F₇() & F₈() <> F₃() & F₇() <> F₃() )