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 st s nin T holds
( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )
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 st s nin T holds
( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )
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 st s nin T holds
( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )
let T be 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 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 f be ExecutionFunction of A,S,T; ( s nin T implies ( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 ) )
assume A1:
s nin T
; ( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )
set r = <*s*>;
A2:
<*s*> . 1 = s
by FINSEQ_1:40;
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
iteration-degree (I,s,f) = 0
hence
iteration-degree (I,s,f) = 0
by A1, A2, A3, A4, A5, Def34; verum