:: deftheorem Def34 defines iteration-degree AOFA_000:def 34 :
for A being preIfWhileAlgebra
for I being Element of A
for S being non empty set
for s being Element of S
for T being Subset of S
for f being ExecutionFunction of A,S,T
for b₇ being R_eal holds
( ( f iteration_terminates_for I,s implies ( b₇ = iteration-degree (I,s,f) iff ex r being non empty FinSequence of S st
( b₇ = (len r) - 1 & r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) ) ) & ( not f iteration_terminates_for I,s implies ( b₇ = iteration-degree (I,s,f) iff b₇ = +infty ) ) );