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 in T holds
( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )
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 in T holds
( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )
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 in T holds
( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T st s in T holds
( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T st s in T holds
( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )
let f be ExecutionFunction of A,S,T; :: thesis: ( s in T implies ( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) ) )
assume A1: s in T ; :: thesis: ( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )
thus A2: ( f iteration_terminates_for I,s iff f iteration_terminates_for I,f . (s,I) ) :: thesis: iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f))

proof

thus ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) :: thesis: ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s )

proof

given r being non empty FinSequence of S such that A3: r . 1 = s and
A4: r . (len r) nin T and
A5: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),I) ) ; :: according to AOFA_000:def 33 :: thesis: f iteration_terminates_for I,f . (s,I)
consider r1 being Element of S, q being FinSequence of S such that
r1 = r . 1 and
A6: r = <*r1*> ^ q by FINSEQ_3:102;
A7: len r = 1 + (len q) by A6, FINSEQ_5:8;
then reconsider q = q as non empty FinSequence of S by A1, A3, A4;
len r >= 1 by A7, NAT_1:11;
then A8: 1 < len r by A1, A3, A4, XXREAL_0:1;
A9: len q >= 0 + 1 by NAT_1:13;
take q ; :: according to AOFA_000:def 33 :: thesis: ( q . 1 = f . (s,I) & q . (len q) nin T & ( for i being Nat st 1 <= i & i < len q holds
( q . i in T & q . (i + 1) = f . ((q . i),I) ) ) )
A10: len <*r1*> = 1 by FINSEQ_1:40;
1 in dom q by A9, FINSEQ_3:25;
hence q . 1 = r . (1 + 1) by A6, A10, FINSEQ_1:def 7
.= f . (s,I) by A3, A5, A8 ;
:: thesis: ( q . (len q) nin T & ( for i being Nat st 1 <= i & i < len q holds
( q . i in T & q . (i + 1) = f . ((q . i),I) ) ) )
len q in dom q by A9, FINSEQ_3:25;
hence q . (len q) nin T by A4, A6, A7, A10, FINSEQ_1:def 7; :: thesis: for i being Nat st 1 <= i & i < len q holds
( q . i in T & q . (i + 1) = f . ((q . i),I) )
let i be Nat; :: thesis: ( 1 <= i & i < len q implies ( q . i in T & q . (i + 1) = f . ((q . i),I) ) )
assume that
A11: 1 <= i and
A12: i < len q ; :: thesis: ( q . i in T & q . (i + 1) = f . ((q . i),I) )
A13: i in dom q by A11, A12, MSUALG_8:1;
A14: 1 <= i + 1 by NAT_1:11;
A15: i + 1 < len r by A7, A12, XREAL_1:6;
A16: i + 1 in dom q by A11, A12, MSUALG_8:1;
A17: r . (i + 1) = q . i by A6, A10, A13, FINSEQ_1:def 7;
r . ((i + 1) + 1) = q . (i + 1) by A6, A10, A16, FINSEQ_1:def 7;
hence ( q . i in T & q . (i + 1) = f . ((q . i),I) ) by A5, A14, A15, A17; :: thesis: verum

end;

given q being non empty FinSequence of S such that A18: q . 1 = f . (s,I) and
A19: q . (len q) nin T and
A20: for i being Nat st 1 <= i & i < len q holds
( q . i in T & q . (i + 1) = f . ((q . i),I) ) ; :: according to AOFA_000:def 33 :: thesis: f iteration_terminates_for I,s
take r = <*s*> ^ q; :: according to AOFA_000:def 33 :: thesis: ( 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) ) ) )
A21: len <*s*> = 1 by FINSEQ_1:40;
thus A22: r . 1 = s by FINSEQ_1:41; :: thesis: ( 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) ) ) )
A23: len r = 1 + (len q) by FINSEQ_5:8;
A24: 0 + 1 <= len q by NAT_1:13;
then len q in dom q by FINSEQ_3:25;
hence r . (len r) nin T by A19, A21, A23, FINSEQ_1:def 7; :: thesis: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),I) )
let i be Nat; :: thesis: ( 1 <= i & i < len r implies ( r . i in T & r . (i + 1) = f . ((r . i),I) ) )
assume that
A25: 1 <= i and
A26: i < len r ; :: thesis: ( r . i in T & r . (i + 1) = f . ((r . i),I) )
consider j being Nat such that
A27: i = 1 + j by A25, NAT_1:10;

per cases ( j = 0 or j > 0 ) ;

suppose A28: j = 0 ; :: thesis: ( r . i in T & r . (i + 1) = f . ((r . i),I) )

1 in dom q by A24, FINSEQ_3:25;
hence ( r . i in T & r . (i + 1) = f . ((r . i),I) ) by A1, A18, A21, A22, A27, A28, FINSEQ_1:def 7; :: thesis: verum

end;

suppose j > 0 ; :: thesis: ( r . i in T & r . (i + 1) = f . ((r . i),I) )

then A29: j >= 0 + 1 by NAT_1:13;
A30: j < len q by A23, A26, A27, XREAL_1:6;
A31: j in dom q by A29, A30, MSUALG_8:1;
A32: j + 1 in dom q by A29, A30, MSUALG_8:1;
A33: r . (j + 1) = q . j by A21, A31, FINSEQ_1:def 7;
r . ((j + 1) + 1) = q . (j + 1) by A21, A32, FINSEQ_1:def 7;
hence ( r . i in T & r . (i + 1) = f . ((r . i),I) ) by A20, A27, A29, A30, A33; :: thesis: verum

end;

end;

end;

per cases ( not f iteration_terminates_for I,s or f iteration_terminates_for I,f . (s,I) ) by A2;

suppose A34: not f iteration_terminates_for I,s ; :: thesis: iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f))

then A35: iteration-degree (I,s,f) = +infty by Def34;
iteration-degree (I,(f . (s,I)),f) = +infty by A2, A34, Def34;
hence iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) by A35, XXREAL_3:def 2; :: thesis: verum

end;

suppose f iteration_terminates_for I,f . (s,I) ; :: thesis: iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f))

then consider q being non empty FinSequence of S such that
A36: iteration-degree (I,(f . (s,I)),f) = (len q) - 1 and
A37: q . 1 = f . (s,I) and
A38: q . (len q) nin T and
A39: for i being Nat st 1 <= i & i < len q holds
( q . i in T & q . (i + 1) = f . ((q . i),I) ) by Def34;
set r = <*s*> ^ q;
A40: len <*s*> = 1 by FINSEQ_1:40;
A41: (<*s*> ^ q) . 1 = s by FINSEQ_1:41;
A42: len (<*s*> ^ q) = 1 + (len q) by FINSEQ_5:8;
1 + ((len q) - 1) = len q ;
then A43: (len (<*s*> ^ q)) - 1 = 1. + (iteration-degree (I,(f . (s,I)),f)) by A36, A42, XXREAL_3:def 2;
A44: 0 + 1 <= len q by NAT_1:13;
then len q in dom q by FINSEQ_3:25;
then A45: (<*s*> ^ q) . (len (<*s*> ^ q)) nin T by A38, A40, A42, FINSEQ_1:def 7;

now :: thesis: for i being Nat st 1 <= i & i < len (<*s*> ^ q) holds
( (<*s*> ^ q) . i in T & (<*s*> ^ q) . (i + 1) = f . (((<*s*> ^ q) . i),I) )

let i be Nat; :: thesis: ( 1 <= i & i < len (<*s*> ^ q) implies ( (<*s*> ^ q) . b₁ in T & (<*s*> ^ q) . (b₁ + 1) = f . (((<*s*> ^ q) . b₁),I) ) )
assume that
A46: 1 <= i and
A47: i < len (<*s*> ^ q) ; :: thesis: ( (<*s*> ^ q) . b₁ in T & (<*s*> ^ q) . (b₁ + 1) = f . (((<*s*> ^ q) . b₁),I) )
consider j being Nat such that
A48: i = 1 + j by A46, NAT_1:10;

per cases ( j = 0 or j > 0 ) ;

suppose A49: j = 0 ; :: thesis: ( (<*s*> ^ q) . b₁ in T & (<*s*> ^ q) . (b₁ + 1) = f . (((<*s*> ^ q) . b₁),I) )

1 in dom q by A44, FINSEQ_3:25;
hence ( (<*s*> ^ q) . i in T & (<*s*> ^ q) . (i + 1) = f . (((<*s*> ^ q) . i),I) ) by A1, A37, A40, A41, A48, A49, FINSEQ_1:def 7; :: thesis: verum

end;

suppose j > 0 ; :: thesis: ( (<*s*> ^ q) . b₁ in T & (<*s*> ^ q) . (b₁ + 1) = f . (((<*s*> ^ q) . b₁),I) )

then A50: j >= 0 + 1 by NAT_1:13;
A51: j < len q by A42, A47, A48, XREAL_1:6;
A52: j in dom q by A50, A51, MSUALG_8:1;
A53: j + 1 in dom q by A50, A51, MSUALG_8:1;
A54: (<*s*> ^ q) . (j + 1) = q . j by A40, A52, FINSEQ_1:def 7;
(<*s*> ^ q) . ((j + 1) + 1) = q . (j + 1) by A40, A53, FINSEQ_1:def 7;
hence ( (<*s*> ^ q) . i in T & (<*s*> ^ q) . (i + 1) = f . (((<*s*> ^ q) . i),I) ) by A39, A48, A50, A51, A54; :: thesis: verum

end;

end;

end;

hence iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) by A2, A41, A43, A45, Def34; :: thesis: verum

end;

end;