let A be preIfWhileAlgebra; :: 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 P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & f iteration_terminates_for I \; C,f . s,C & s in P holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
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 P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & f iteration_terminates_for I \; C,f . s,C & s in P holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T
for P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & f iteration_terminates_for I \; C,f . s,C & s in P holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T
for P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & f iteration_terminates_for I \; C,f . s,C & s in P holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let f be ExecutionFunction of A,S,T; :: thesis: for P being set
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & f iteration_terminates_for I \; C,f . s,C & s in P holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let P be set ; :: thesis: for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & f iteration_terminates_for I \; C,f . s,C & s in P holds
[s,(while C,I)] in TerminatingPrograms A,S,T,f
let C, I be Element of A; :: thesis: ( C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P ) & f iteration_terminates_for I \; C,f . s,C & s in P implies [s,(while C,I)] in TerminatingPrograms A,S,T,f )
assume that
A1:
( C is_terminating_wrt f & I is_terminating_wrt f,P )
and
A2:
P is_invariant_wrt C,f
and
A3:
for s being Element of S st s in P & f . (f . s,I),C in T holds
f . s,I in P
; :: thesis: ( not f iteration_terminates_for I \; C,f . s,C or not s in P or [s,(while C,I)] in TerminatingPrograms A,S,T,f )
given r being non empty FinSequence of S such that A4:
( r . 1 = f . s,C & 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 \; C) )
; :: according to AOFA_000:def 33 :: thesis: ( not s in P or [s,(while C,I)] in TerminatingPrograms A,S,T,f )
assume A6:
s in P
; :: thesis: [s,(while C,I)] in TerminatingPrograms A,S,T,f
defpred S1[ Nat] means ( $1 + 1 < len r implies r . ($1 + 1) in P );
A7:
S1[ 0 ]
by A4, A2, A6, Def39;
A8:
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 A9:
S1[
i]
and A10:
(i + 1) + 1
< len r
;
:: thesis: r . ((i + 1) + 1) in P
(
i + 1
>= 1 &
(i + 1) + 1
>= 1 &
i + 1
< len r )
by A10, NAT_1:11, NAT_1:13;
then A11:
(
r . (i + 1) in T &
r . ((i + 1) + 1) in T &
r . ((i + 1) + 1) = f . (r . (i + 1)),
(I \; C) )
by A5, A10;
then reconsider s =
r . (i + 1) as
Element of
S ;
(
s in T &
s in P &
f . (f . s,I),
C in T )
by A9, A10, A11, Def29, NAT_1:13;
then
f . s,
I in P
by A3;
then
f . (f . s,I),
C in P
by A2, Def39;
hence
r . ((i + 1) + 1) in P
by A11, Def29;
:: thesis: verum
end;
A12:
for i being Nat holds S1[i]
from NAT_1:sch 2(A7, A8);
A13:
now let i be
Nat;
:: thesis: ( 1 <= i & i < len r implies ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) ) )assume A14:
( 1
<= i &
i < len r )
;
:: thesis: ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) )hence
r . i in T
by A5;
:: thesis: ( [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) )then reconsider s =
r . i as
Element of
S ;
i = (i -' 1) + 1
by A14, XREAL_1:237;
then
s in P
by A14, A12;
then A15:
[s,I] in TerminatingPrograms A,
S,
T,
f
by A1, 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 A5, A14, A15, Def35;
:: thesis: verum end;
[s,C] in TerminatingPrograms A,S,T,f
by A1, Def37;
hence
[s,(while C,I)] in TerminatingPrograms A,S,T,f
by A4, A13, Def35; :: thesis: verum