let A be preIfWhileAlgebra; :: thesis:
let I be Element of A; :: thesis:
let S be non empty set ; :: thesis:
let T be Subset of S; :: thesis:
let s be Element of S; :: thesis:
let f be ExecutionFunction of A,S,T; :: thesis:
assume A1: s in T ; :: thesis:
thus A2: ( f iteration_terminates_for I,s iff f iteration_terminates_for I,f . s,I ) :: thesis:

proof

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

proof

given r being non empty FinSequence of S such that A3: ( r . 1 = s & r . (len r) nin T ) and
A4: 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:
consider r1 being Element of S, q being FinSequence of S such that
A5: ( r1 = r . 1 & r = <*r1*> ^ q ) by FINSEQ_3:111;
A6: len r = 1 + (len q) by A5, FINSEQ_5:8;
reconsider q = q as non empty FinSequence of S by A6, A1, A3, CARD_1:47;
( len r <> 1 & len r >= 1 & len q > 0 ) by A6, A1, A3, NAT_1:11;
then A8: ( 1 < len r & len q >= 0 + 1 ) by NAT_1:13, XXREAL_0:1;
take q ; :: according to AOFA_000:def 33 :: thesis:
A9: ( len <*r1*> = 1 & 1 in dom q ) by A8, FINSEQ_1:57, FINSEQ_3:27;
hence q . 1 = r . (1 + 1) by A5, FINSEQ_1:def 7
.= f . s,I by A3, A4, A8 ;
:: thesis:
len q in dom q by A8, FINSEQ_3:27;
hence q . (len q) nin T by A3, A5, A6, A9, FINSEQ_1:def 7; :: thesis:
let i be Nat; :: thesis:
assume A10: ( 1 <= i & i < len q ) ; :: thesis:
i in NAT by ORDINAL1:def 13;
then ( i in dom q & 1 <= i + 1 & i + 1 < len r & i + 1 in dom q ) by A6, A10, MSUALG_8:1, NAT_1:11, XREAL_1:8;
then ( r . (i + 1) = q . i & r . ((i + 1) + 1) = q . (i + 1) & r . (i + 1) in T & r . ((i + 1) + 1) = f . (r . (i + 1)),I ) by A5, A9, A4, FINSEQ_1:def 7;
hence ( q . i in T & q . (i + 1) = f . (q . i),I ) ; :: thesis:

end;

given q being non empty FinSequence of S such that A11: ( q . 1 = f . s,I & q . (len q) nin T ) and
A12: 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:
take r = <*s*> ^ q; :: according to AOFA_000:def 33 :: thesis:
A13: len <*s*> = 1 by FINSEQ_1:57;
thus A14: r . 1 = s by FINSEQ_1:58; :: thesis:
A15: len r = 1 + (len q) by FINSEQ_5:8;
A16: 0 + 1 <= len q by NAT_1:13;
then len q in dom q by FINSEQ_3:27;
hence r . (len r) nin T by A11, A13, A15, FINSEQ_1:def 7; :: thesis:
let i be Nat; :: thesis:
assume A17: ( 1 <= i & i < len r ) ; :: thesis:
then consider j being Nat such that
A18: i = 1 + j by NAT_1:10;

per cases ;

suppose A19: j = 0 ; :: thesis:

1 in dom q by A16, FINSEQ_3:27;
hence ( r . i in T & r . (i + 1) = f . (r . i),I ) by A1, A11, A18, A14, A19, A13, FINSEQ_1:def 7; :: thesis:

end;

suppose j > 0 ; :: thesis:

then A20: ( j >= 0 + 1 & j < len q & j in NAT ) by A15, A17, A18, NAT_1:13, ORDINAL1:def 13, XREAL_1:8;
then ( j in dom q & 1 <= j + 1 & j + 1 < len r & j + 1 in dom q ) by A15, MSUALG_8:1, XREAL_1:8;
then ( r . (j + 1) = q . j & r . ((j + 1) + 1) = q . (j + 1) & q . j in T & q . (j + 1) = f . (q . j),I ) by A13, A12, A20, FINSEQ_1:def 7;
hence ( r . i in T & r . (i + 1) = f . (r . i),I ) by A18; :: thesis:

end;

per cases by A2;

suppose not f iteration_terminates_for I,s ; :: thesis:

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

end;

suppose A21: f iteration_terminates_for I,f . s,I ; :: thesis:

then consider q being non empty FinSequence of S such that
A22: iteration-degree I,(f . s,I),f = (len q) - 1 and
A23: ( q . 1 = f . s,I & q . (len q) nin T ) and
A24: 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;
A25: len <*s*> = 1 by FINSEQ_1:57;
A26: (<*s*> ^ q) . 1 = s by FINSEQ_1:58;
A27: len (<*s*> ^ q) = 1 + (len q) by FINSEQ_5:8;
then ( 1 + ((len q) - 1) = len q & (len (<*s*> ^ q)) - 1 = len q & (len q) - 1 in REAL & 1 in REAL & (len (<*s*> ^ q)) - 1 in ExtREAL ) by XREAL_0:def 1, XXREAL_0:def 1;
then A28: (len (<*s*> ^ q)) - 1 = 1. + (iteration-degree I,(f . s,I),f) by A22, XXREAL_3:def 2;
A29: 0 + 1 <= len q by NAT_1:13;
then len q in dom q by FINSEQ_3:27;
then A30: (<*s*> ^ q) . (len (<*s*> ^ q)) nin T by A23, A25, A27, FINSEQ_1:def 7;

now

let i be Nat; :: thesis:
assume A31: ( 1 <= i & i < len (<*s*> ^ q) ) ; :: thesis:
then consider j being Nat such that
A32: i = 1 + j by NAT_1:10;

per cases ;

suppose A33: j = 0 ; :: thesis:

1 in dom q by A29, FINSEQ_3:27;
hence ( (<*s*> ^ q) . i in T & (<*s*> ^ q) . (i + 1) = f . ((<*s*> ^ q) . i),I ) by A1, A23, A32, A26, A33, A25, FINSEQ_1:def 7; :: thesis:

end;

suppose j > 0 ; :: thesis:

then A34: ( j >= 0 + 1 & j < len q & j in NAT ) by A27, A31, A32, NAT_1:13, ORDINAL1:def 13, XREAL_1:8;
then ( j in dom q & 1 <= j + 1 & j + 1 < len (<*s*> ^ q) & j + 1 in dom q ) by A27, MSUALG_8:1, XREAL_1:8;
then ( (<*s*> ^ q) . (j + 1) = q . j & (<*s*> ^ q) . ((j + 1) + 1) = q . (j + 1) & q . j in T & q . (j + 1) = f . (q . j),I ) by A25, A24, A34, FINSEQ_1:def 7;
hence ( (<*s*> ^ q) . i in T & (<*s*> ^ q) . (i + 1) = f . ((<*s*> ^ q) . i),I ) by A32; :: thesis:

end;

hence iteration-degree I,s,f = 1. + (iteration-degree I,(f . s,I),f) by A26, A30, A2, A28, A21, Def34; :: thesis:

end;