let A be preIfWhileAlgebra; :: 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:
let P be set ; :: thesis:
let C, I be Element of A; :: thesis:
assume that
A1: ( C is_terminating_wrt f,P & I is_terminating_wrt f,P ) and
A2: ( P is_invariant_wrt C,f & P is_invariant_wrt I,f ) ; :: thesis:
given r being non empty FinSequence of S such that A3: ( r . 1 = f . s,C & 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 \; C) ) ; :: according to AOFA_000:def 33 :: thesis:
assume A5: s in P ; :: thesis:
defpred S₁[ Nat] means ( $1 < len r implies r . ($1 + 1) in P );
A6: S₁[ 0 ] by A3, A2, A5, Def39;
A7: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume that
A8: S₁[i] and
A9: i + 1 < len r ; :: thesis:
i + 1 >= 1 by NAT_1:11;
then A10: ( r . (i + 1) in T & r . ((i + 1) + 1) = f . (r . (i + 1)),(I \; C) ) by A4, A9;
then reconsider s = r . (i + 1) as Element of S ;
f . s,I in P by A2, A8, Def39, A9, NAT_1:13;
then f . (f . s,I),C in P by A2, Def39;
hence r . ((i + 1) + 1) in P by A10, Def29; :: thesis:

end;

A11: for i being Nat holds S₁[i] from NAT_1:sch 2(A6, A7);

A12: now

let i be Nat; :: thesis:
assume A13: ( 1 <= i & i < len r ) ; :: thesis:
hence r . i in T by A4; :: thesis:
then reconsider s = r . i as Element of S ;
i -' 1 <= i by NAT_D:35;
then ( i = (i -' 1) + 1 & i -' 1 < len r ) by A13, XREAL_1:237, XXREAL_0:2;
then s in P by A11;
then A14: ( [s,I] in TerminatingPrograms A,S,T,f & f . s,I in P ) by A1, A2, Def38, Def39;
then [(f . s,I),C] in TerminatingPrograms A,S,T,f by A1, Def38;
hence ( [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) ) by A4, A13, A14, Def35; :: thesis:

end;

[s,C] in TerminatingPrograms A,S,T,f by A1, A5, Def38;
hence [s,(while C,I)] in TerminatingPrograms A,S,T,f by A3, A12, Def35; :: thesis: