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

F₆() iteration_terminates_for F₂(),F₄()

provided

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