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 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 ; :: thesis: 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; :: 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 & ( 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; :: thesis: 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; :: thesis: ( 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 & I is_terminating_wrt f ) and
A2: for s being Element of S holds f iteration_terminates_for I \; C,s ; :: thesis: while C,I is_terminating_wrt f
let s be Element of S; :: according to AOFA_000:def 37 :: thesis: [s,(while C,I)] in TerminatingPrograms A,S,T,f
f iteration_terminates_for I \; C,f . s,C by A2;
hence [s,(while C,I)] in TerminatingPrograms A,S,T,f by A1, Th114; :: thesis: verum