scheme :: AOFA_000:sch 5
InvariantSch{ F₁() -> preIfWhileAlgebra, F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> non empty set , F₅() -> Element of F₄(), F₆() -> Subset of F₄(), F₇() -> ExecutionFunction of F₁(),F₄(),F₆(), P₁[ set ], P₂[ set ] } :

( P₁[F₇() . (F₅(),(while (F₂(),F₃())))] & P₂[F₇() . (F₅(),(while (F₂(),F₃())))] )

provided

A1: P₁[F₅()] and
A2: F₇() iteration_terminates_for F₃() \; F₂(),F₇() . (F₅(),F₂()) and
A3: for s being Element of F₄() st P₁[s] & s in F₆() & P₂[s] holds
P₁[F₇() . (s,F₃())] and
A4: for s being Element of F₄() st P₁[s] holds
( P₁[F₇() . (s,F₂())] & ( F₇() . (s,F₂()) in F₆() implies P₂[F₇() . (s,F₂())] ) & ( P₂[F₇() . (s,F₂())] implies F₇() . (s,F₂()) in F₆() ) )