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 st s nin T holds
( f iteration_terminates_for I,s & 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 st s nin T holds
( f iteration_terminates_for I,s & 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 st s nin T holds
( f iteration_terminates_for I,s & 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 st s nin T holds
( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T st s nin T holds
( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )
let f be ExecutionFunction of A,S,T; :: thesis: ( s nin T implies ( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 ) )
assume A1: s nin T ; :: thesis: ( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )
set r = <*s*>;
A2: <*s*> . 1 = s ;
A3: len <*s*> = 1 by FINSEQ_1:40;
A4: for i being Nat st 1 <= i & i < len <*s*> holds
( <*s*> . i in T & <*s*> . (i + 1) = f . ((<*s*> . i),I) ) by FINSEQ_1:40;
A5: 1 - 1 = 0. ;
thus f iteration_terminates_for I,s :: thesis: iteration-degree (I,s,f) = 0

proof

take <*s*> ; :: according to AOFA_000:def 33 :: thesis: ( <*s*> . 1 = s & <*s*> . (len <*s*>) nin T & ( for i being Nat st 1 <= i & i < len <*s*> holds
( <*s*> . i in T & <*s*> . (i + 1) = f . ((<*s*> . i),I) ) ) )
thus ( <*s*> . 1 = s & <*s*> . (len <*s*>) nin T & ( for i being Nat st 1 <= i & i < len <*s*> holds
( <*s*> . i in T & <*s*> . (i + 1) = f . ((<*s*> . i),I) ) ) ) by A1, A2, FINSEQ_1:40; :: thesis: verum

end;

hence iteration-degree (I,s,f) = 0 by A1, A2, A3, A4, A5, Def34; :: thesis: verum