theorem Th99: :: AOFA_000:99

for A being preIfWhileAlgebra
for C, I being Element of A
for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )