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:

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

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:
consider r1 being Element of S, q being FinSequence of S such that
r1 = r . 1 and
A6: r = <*r1*> ^ q by FINSEQ_3:111;
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, CARD_1:47;
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:
A10: len <*r1*> = 1 by FINSEQ_1:57;
1 in dom q by A9, FINSEQ_3:27;
hence q . 1 = r . (1 + 1) by A6, A10, FINSEQ_1:def 7
.= f . s,I by A3, A5, A8 ;
:: thesis:
len q in dom q by A9, FINSEQ_3:27;
hence q . (len q) nin T by A4, A6, A7, A10, FINSEQ_1:def 7; :: thesis:
let i be Nat; :: thesis:
assume that
A11: 1 <= i and
A12: i < len q ; :: thesis:
A13: i in NAT by ORDINAL1:def 13;
then A14: i in dom q by A11, A12, MSUALG_8:1;
A15: 1 <= i + 1 by NAT_1:11;
A16: i + 1 < len r by A7, A12, XREAL_1:8;
A17: i + 1 in dom q by A11, A12, A13, MSUALG_8:1;
A18: r . (i + 1) = q . i by A6, A10, A14, FINSEQ_1:def 7;
r . ((i + 1) + 1) = q . (i + 1) by A6, A10, A17, FINSEQ_1:def 7;
hence ( q . i in T & q . (i + 1) = f . (q . i),I ) by A5, A15, A16, A18; :: thesis:

end;

given q being non empty FinSequence of S such that A19: q . 1 = f . s,I and
A20: q . (len q) nin T and
A21: 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:
A22: len <*s*> = 1 by FINSEQ_1:57;
thus A23: r . 1 = s by FINSEQ_1:58; :: thesis:
A24: len r = 1 + (len q) by FINSEQ_5:8;
A25: 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 A20, A22, A24, FINSEQ_1:def 7; :: thesis:
let i be Nat; :: thesis:
assume that
A26: 1 <= i and
A27: i < len r ; :: thesis:
consider j being Nat such that
A28: i = 1 + j by A26, NAT_1:10;

suppose A29: j = 0 ; :: thesis:

1 in dom q by A25, FINSEQ_3:27;
hence ( r . i in T & r . (i + 1) = f . (r . i),I ) by A1, A19, A22, A23, A28, A29, FINSEQ_1:def 7; :: thesis:

end;

suppose j > 0 ; :: thesis:

then A30: j >= 0 + 1 by NAT_1:13;
A31: j < len q by A24, A27, A28, XREAL_1:8;
A32: j in NAT by ORDINAL1:def 13;
then A33: j in dom q by A30, A31, MSUALG_8:1;
A34: j + 1 in dom q by A30, A31, A32, MSUALG_8:1;
A35: r . (j + 1) = q . j by A22, A33, FINSEQ_1:def 7;
r . ((j + 1) + 1) = q . (j + 1) by A22, A34, FINSEQ_1:def 7;
hence ( r . i in T & r . (i + 1) = f . (r . i),I ) by A21, A28, A30, A31, A35; :: thesis:

end;

end;

end;

per cases by A2;

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

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

end;

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

then consider q being non empty FinSequence of S such that
A39: iteration-degree I,(f . s,I),f = (len q) - 1 and
A40: q . 1 = f . s,I and
A41: q . (len q) nin T and
A42: 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;
A43: len <*s*> = 1 by FINSEQ_1:57;
A44: (<*s*> ^ q) . 1 = s by FINSEQ_1:58;
A45: len (<*s*> ^ q) = 1 + (len q) by FINSEQ_5:8;
1 + ((len q) - 1) = len q ;
then A46: (len (<*s*> ^ q)) - 1 = 1. + (iteration-degree I,(f . s,I),f) by A39, A45, XXREAL_3:def 2;
A47: 0 + 1 <= len q by NAT_1:13;
then len q in dom q by FINSEQ_3:27;
then A48: (<*s*> ^ q) . (len (<*s*> ^ q)) nin T by A41, A43, A45, FINSEQ_1:def 7;

let i be Nat; :: thesis:
assume that
A49: 1 <= i and
A50: i < len (<*s*> ^ q) ; :: thesis:
consider j being Nat such that
A51: i = 1 + j by A49, NAT_1:10;

suppose A52: j = 0 ; :: thesis:

1 in dom q by A47, FINSEQ_3:27;
hence ( (<*s*> ^ q) . i in T & (<*s*> ^ q) . (i + 1) = f . ((<*s*> ^ q) . i),I ) by A1, A40, A43, A44, A51, A52, FINSEQ_1:def 7; :: thesis:

end;

suppose j > 0 ; :: thesis:

then A53: j >= 0 + 1 by NAT_1:13;
A54: j < len q by A45, A50, A51, XREAL_1:8;
A55: j in NAT by ORDINAL1:def 13;
then A56: j in dom q by A53, A54, MSUALG_8:1;
A57: j + 1 in dom q by A53, A54, A55, MSUALG_8:1;
A58: (<*s*> ^ q) . (j + 1) = q . j by A43, A56, FINSEQ_1:def 7;
(<*s*> ^ q) . ((j + 1) + 1) = q . (j + 1) by A43, A57, FINSEQ_1:def 7;
hence ( (<*s*> ^ q) . i in T & (<*s*> ^ q) . (i + 1) = f . ((<*s*> ^ q) . i),I ) by A42, A51, A53, A54, A58; :: thesis:

end;

end;

end;

hence iteration-degree I,s,f = 1. + (iteration-degree I,(f . s,I),f) by A2, A38, A44, A46, A48, Def34; :: thesis:

end;

end;