let A be preIfWhileAlgebra; for I being Element of A
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 holds
( f iteration_terminates_for I,s iff iteration-degree (I,s,f) < +infty )
let I be Element of A; 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 holds
( f iteration_terminates_for I,s iff iteration-degree (I,s,f) < +infty )
let S be non empty set ; for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff iteration-degree (I,s,f) < +infty )
let T be Subset of S; for s being Element of S
for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff iteration-degree (I,s,f) < +infty )
let s be Element of S; for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff iteration-degree (I,s,f) < +infty )
let f be ExecutionFunction of A,S,T; ( f iteration_terminates_for I,s iff iteration-degree (I,s,f) < +infty )
thus
( iteration-degree (I,s,f) < +infty implies f iteration_terminates_for I,s )
by Def34; verum