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 I being Element of A st I is_terminating_wrt f holds
for P being set holds 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 I being Element of A st I is_terminating_wrt f holds
for P being set holds I is_terminating_wrt f,P
let T be Subset of S; :: thesis: for f being ExecutionFunction of A,S,T
for I being Element of A st I is_terminating_wrt f holds
for P being set holds I is_terminating_wrt f,P
let f be ExecutionFunction of A,S,T; :: thesis: for I being Element of A st I is_terminating_wrt f holds
for P being set holds I is_terminating_wrt f,P
let I be Element of A; :: thesis: ( I is_terminating_wrt f implies for P being set holds I is_terminating_wrt f,P )
assume A1: for s being Element of S holds [s,I] in TerminatingPrograms (A,S,T,f) ; :: according to AOFA_000:def 37 :: thesis: for P being set holds I is_terminating_wrt f,P
let P be set ; :: thesis: I is_terminating_wrt f,P
let s be Element of S; :: according to AOFA_000:def 38 :: thesis: ( s in P implies [s,I] in TerminatingPrograms (A,S,T,f) )
thus ( s in P implies [s,I] in TerminatingPrograms (A,S,T,f) ) by A1; :: thesis: verum