let A be preIfWhileAlgebra; for S being non empty set
for T being Subset 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 & ( for s being Element of S holds f iteration_terminates_for I \; C,s ) holds
while (C,I) is_terminating_wrt f
let S be non empty set ; for T being Subset 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 & ( for s being Element of S holds f iteration_terminates_for I \; C,s ) holds
while (C,I) is_terminating_wrt f
let T be Subset 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 & ( for s being Element of S holds f iteration_terminates_for I \; C,s ) holds
while (C,I) is_terminating_wrt f
let f be ExecutionFunction of A,S,T; for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & ( for s being Element of S holds f iteration_terminates_for I \; C,s ) holds
while (C,I) is_terminating_wrt f
let C, I be Element of A; ( C is_terminating_wrt f & I is_terminating_wrt f & ( for s being Element of S holds f iteration_terminates_for I \; C,s ) implies while (C,I) is_terminating_wrt f )
assume that
A1:
C is_terminating_wrt f
and
A2:
I is_terminating_wrt f
and
A3:
for s being Element of S holds f iteration_terminates_for I \; C,s
; while (C,I) is_terminating_wrt f
let s be Element of S; AOFA_000:def 37 [s,(while (C,I))] in TerminatingPrograms (A,S,T,f)
f iteration_terminates_for I \; C,f . (s,C)
by A3;
hence
[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)
by A1, A2, Th114; verum