let A be preIfWhileAlgebra; :: thesis: 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
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . s,C holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let S be non empty set ; :: thesis: for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . s,C holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . s,C holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . s,C holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let f be ExecutionFunction of A,S,T; :: thesis: for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . s,C holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let C, I be Element of A; :: thesis: ( C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . s,C implies [s,(while C,I)] in TerminatingPrograms A,S,T,f )
assume A1: ( C is_terminating_wrt f & I is_terminating_wrt f ) ; :: thesis: ( not f iteration_terminates_for I \; C,f . s,C or [s,(while C,I)] in TerminatingPrograms A,S,T,f )
given r being non empty FinSequence of S such that A2: ( r . 1 = f . s,C & r . (len r) nin T ) and
A3: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . (r . i),(I \; C) ) ; :: according to AOFA_000:def 33 :: thesis: [s,(while C,I)] in TerminatingPrograms A,S,T,f

A4: now

let i be Nat; :: thesis: ( 1 <= i & i < len r implies ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) ) )
assume A5: ( 1 <= i & i < len r ) ; :: thesis: ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) )
hence r . i in T by A3; :: thesis: ( [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) )
then reconsider s = r . i as Element of S ;
( [s,I] in TerminatingPrograms A,S,T,f & [(f . s,I),C] in TerminatingPrograms A,S,T,f ) by A1, Def37;
hence ( [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) ) by A3, A5, Def35; :: thesis: verum

end;

[s,C] in TerminatingPrograms A,S,T,f by A1, Def37;
hence [s,(while C,I)] in TerminatingPrograms A,S,T,f by A2, A4, Def35; :: thesis: verum