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 and
A2: I is_terminating_wrt f,P and
A3: P is_invariant_wrt C,f and
A4: for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ; :: thesis:
given r being non empty FinSequence of S such that A5: r . 1 = f . s,C and
A6: r . (len r) nin T and
A7: 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 A8: s in P ; :: thesis:
defpred S₁[ Nat] means ( $1 + 1 < len r implies r . ($1 + 1) in P );
A9: S₁[ 0 ] by A3, A5, A8, Def39;
A10: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis:
assume that
A11: S₁[i] and
A12: (i + 1) + 1 < len r ; :: thesis:
A13: i + 1 >= 1 by NAT_1:11;
A14: (i + 1) + 1 >= 1 by NAT_1:11;
A15: i + 1 < len r by A12, NAT_1:13;
then A16: r . (i + 1) in T by A7, A13;
A17: r . ((i + 1) + 1) in T by A7, A12, A14;
A18: r . ((i + 1) + 1) = f . (r . (i + 1)),(I \; C) by A7, A13, A15;
reconsider s = r . (i + 1) as Element of S by A16;
f . (f . s,I),C in T by A17, A18, Def29;
then f . s,I in P by A4, A11, A12, NAT_1:13;
then f . (f . s,I),C in P by A3, Def39;
hence r . ((i + 1) + 1) in P by A18, Def29; :: thesis:

end;

A20: now

let i be Nat; :: thesis:
assume that
A21: 1 <= i and
A22: i < len r ; :: thesis:
thus r . i in T by A7, A21, A22; :: thesis:
then reconsider s = r . i as Element of S ;
i = (i -' 1) + 1 by A21, XREAL_1:237;
then s in P by A19, A22;
then A23: [s,I] in TerminatingPrograms A,S,T,f by A2, Def38;
[(f . s,I),C] in TerminatingPrograms A,S,T,f by A1, Def37;
hence ( [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) ) by A7, A21, A22, A23, Def35; :: thesis:

end;