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 S1[ 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:
S1[ 0 ]
by A3, A1, Def31;
A6:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
:: thesis: ( S1[i] implies S1[i + 1] )
assume that A7:
S1[
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;
(j + 1) + i = len r
;
then A9:
( 1
<= j + 1 &
j + 1
<= len r )
by NAT_1:11;
then A10:
( 1
<= j &
j < len r &
(len r) - i in dom r )
by A8, FINSEQ_3:27, NAT_1:13;
then A11:
r . (j + 1) = f . (r . j),
(I \; C)
by A4;
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 A12:
f . q,
C = r . ((len r) - (i + 1))
;
:: thesis: f . q,(while C,I) = r . (len r)
then A13:
f . q,
C in T
by A4, A10;
r . (j + 1) = f . (f . (f . q,C),I),
C
by A11, A12, Def29;
then
f . (f . (f . q,C),I),
(while C,I) = r . (len r)
by A7, A9, FINSEQ_3:27;
hence
f . q,
(while C,I) = r . (len r)
by A13, A1, Def31;
:: thesis: verum
end;
A14:
for i being Nat holds S1[i]
from NAT_1:sch 2(A5, A6);
A15:
len r >= 0 + 1
by NAT_1:13;
then consider i being Nat such that
A16:
len r = 1 + i
by NAT_1:10;
( S1[i] & (len r) - i = 1 & 1 in dom r )
by A16, A14, A15, FINSEQ_3:27;
hence
f . s,(while C,I) = r . (len r)
by A2; :: thesis: verum