let A be preIfWhileAlgebra; :: thesis: for S being non empty set
for T being Subset of S
for f being ExecutionFunction of A,S,T
for P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & ( for s being Element of S st f . s,C in P holds
f iteration_terminates_for I \; C,f . s,C ) holds
while C,I is_terminating_wrt f,P
let S be non empty set ; :: thesis: for T being Subset of S
for f being ExecutionFunction of A,S,T
for P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & ( for s being Element of S st f . s,C in P holds
f iteration_terminates_for I \; C,f . s,C ) holds
while C,I is_terminating_wrt f,P
let T be Subset of S; :: thesis: for f being ExecutionFunction of A,S,T
for P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & ( for s being Element of S st f . s,C in P holds
f iteration_terminates_for I \; C,f . s,C ) holds
while C,I is_terminating_wrt f,P
let f be ExecutionFunction of A,S,T; :: thesis: for P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & ( for s being Element of S st f . s,C in P holds
f iteration_terminates_for I \; C,f . s,C ) holds
while C,I is_terminating_wrt f,P
let P be set ; :: thesis: for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & ( for s being Element of S st f . s,C in P holds
f iteration_terminates_for I \; C,f . s,C ) holds
while C,I is_terminating_wrt f,P
let C, I be Element of A; :: thesis: ( C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & ( for s being Element of S st f . s,C in P holds
f iteration_terminates_for I \; C,f . s,C ) implies while C,I is_terminating_wrt f,P )
assume that
A1: C is_terminating_wrt f and
A2: I is_terminating_wrt f,P and
A3: P is_invariant_wrt C,f and
A4: for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P and
A5: for s being Element of S st f . s,C in P holds
f iteration_terminates_for I \; C,f . s,C ; :: thesis: while C,I is_terminating_wrt f,P
let s be Element of S; :: according to AOFA_000:def 38 :: thesis: ( s in P implies [s,(while C,I)] in TerminatingPrograms A,S,T,f )
assume A6: s in P ; :: thesis: [s,(while C,I)] in TerminatingPrograms A,S,T,f
then f . s,C in P by A3, Def39;
hence [s,(while C,I)] in TerminatingPrograms A,S,T,f by A1, A2, A3, A4, A5, A6, Th116; :: thesis: verum