let A be preIfWhileAlgebra; :: thesis: for C, 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
for r being non empty FinSequence of S st r . 1 = f . (s,C) & 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 \; C)) ) ) holds
f . (s,(while (C,I))) = r . (len r)
let C, 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
for r being non empty FinSequence of S st r . 1 = f . (s,C) & 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 \; C)) ) ) holds
f . (s,(while (C,I))) = r . (len r)
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
for r being non empty FinSequence of S st r . 1 = f . (s,C) & 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 \; C)) ) ) holds
f . (s,(while (C,I))) = r . (len r)
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T
for r being non empty FinSequence of S st r . 1 = f . (s,C) & 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 \; C)) ) ) holds
f . (s,(while (C,I))) = r . (len r)
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T
for r being non empty FinSequence of S st r . 1 = f . (s,C) & 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 \; C)) ) ) holds
f . (s,(while (C,I))) = r . (len r)
let f be ExecutionFunction of A,S,T; :: thesis: for r being non empty FinSequence of S st r . 1 = f . (s,C) & 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 \; C)) ) ) holds
f . (s,(while (C,I))) = r . (len r)
A1: f complies_with_while_wrt T by Def32;
let r be non empty FinSequence of S; :: thesis: ( r . 1 = f . (s,C) & 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 \; C)) ) ) implies f . (s,(while (C,I))) = r . (len r) )
assume A2: r . 1 = f . (s,C) ; :: thesis: ( not r . (len r) nin T or ex i being Nat st
( 1 <= i & i < len r & not ( r . i in T & r . (i + 1) = f . ((r . i),(I \; C)) ) ) or f . (s,(while (C,I))) = r . (len r) )
assume A3: r . (len r) nin T ; :: thesis: ( ex i being Nat st
( 1 <= i & i < len r & not ( r . i in T & r . (i + 1) = f . ((r . i),(I \; C)) ) ) or f . (s,(while (C,I))) = r . (len r) )
assume A4: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),(I \; C)) ) ; :: thesis: f . (s,(while (C,I))) = r . (len r)
defpred S₁[ Nat] means ( (len r) - $1 in dom r implies for q being Element of S st f . (q,C) = r . ((len r) - $1) holds
f . (q,(while (C,I))) = r . (len r) );
A5: S₁[ 0 ] by A1, A3;
A6: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A7: S₁[i] and
A8: (len r) - (i + 1) in dom r ; :: thesis: for q being Element of S st f . (q,C) = r . ((len r) - (i + 1)) holds
f . (q,(while (C,I))) = r . (len r)
reconsider j = (len r) - (i + 1) as Element of NAT by A8;
A9: (j + 1) + i = len r ;
A10: 1 <= j + 1 by NAT_1:11;
A11: j + 1 <= len r by A9, NAT_1:11;
A12: 1 <= j by A8, FINSEQ_3:25;
A13: j < len r by A11, NAT_1:13;
then A14: r . (j + 1) = f . ((r . j),(I \; C)) by A4, A12;
let q be Element of S; :: thesis: ( f . (q,C) = r . ((len r) - (i + 1)) implies f . (q,(while (C,I))) = r . (len r) )
assume A15: f . (q,C) = r . ((len r) - (i + 1)) ; :: thesis: f . (q,(while (C,I))) = r . (len r)
then A16: f . (q,C) in T by A4, A12, A13;
r . (j + 1) = f . ((f . ((f . (q,C)),I)),C) by A14, A15, Def29;
then f . ((f . ((f . (q,C)),I)),(while (C,I))) = r . (len r) by A7, A10, A11, FINSEQ_3:25;
hence f . (q,(while (C,I))) = r . (len r) by A1, A16; :: thesis: verum

end;

A17: for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A6);
A18: len r >= 0 + 1 by NAT_1:13;
then consider i being Nat such that
A19: len r = 1 + i by NAT_1:10;
S₁[i] by A17;
hence f . (s,(while (C,I))) = r . (len r) by A2, A18, A19, FINSEQ_3:25; :: thesis: verum