let A be preIfWhileAlgebra; :: thesis: 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 iteration-degree (I,s,f) >= 0
let I be Element of A; :: thesis: 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 iteration-degree (I,s,f) >= 0
let S be non empty set ; :: thesis: for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T holds iteration-degree (I,s,f) >= 0
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T holds iteration-degree (I,s,f) >= 0
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T holds iteration-degree (I,s,f) >= 0
let f be ExecutionFunction of A,S,T; :: thesis: iteration-degree (I,s,f) >= 0
per cases ( not f iteration_terminates_for I,s or f iteration_terminates_for I,s ) ;
suppose not f iteration_terminates_for I,s ; :: thesis: iteration-degree (I,s,f) >= 0
hence iteration-degree (I,s,f) >= 0 by Def34; :: thesis: verum
end;
suppose f iteration_terminates_for I,s ; :: thesis: iteration-degree (I,s,f) >= 0
then consider r being non empty FinSequence of S such that
A1: iteration-degree (I,s,f) = (len r) - 1 and
r . 1 = s and
r . (len r) nin T and
for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),I) ) by Def34;
ex i being Nat st len r = i + 1 by NAT_1:6;
hence iteration-degree (I,s,f) >= 0 by A1; :: thesis: verum
end;
end;