let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
for m being Nat st ( for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a
let s be State of SCM+FSA; for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
for m being Nat st ( for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a
let I be Program of SCM+FSA; for a being Int-Location st not I destroys a holds
for m being Nat st ( for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a
let a be Int-Location; ( not I destroys a implies for m being Nat st ( for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a )
assume A1:
not I destroys a
; for m being Nat st ( for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a
set s1 = Initialize s;
set P1 = P +* I;
let m be Nat; ( ( for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) implies for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a )
defpred S1[ Nat] means ( $1 <= m implies (Comput ((P +* I),(Initialize s),$1)) . a = s . a );
assume A2:
for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I
; for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
A5:
k + 0 < k + 1
by XREAL_1:6;
assume A6:
k + 1
<= m
;
(Comput ((P +* I),(Initialize s),(k + 1))) . a = s . a
then
k < m
by A5, XXREAL_0:2;
then
IC (Comput ((P +* I),(Initialize s),k)) in dom I
by A2;
hence
(Comput ((P +* I),(Initialize s),(k + 1))) . a = s . a
by A1, A4, A6, A5, Th55, XXREAL_0:2;
verum
end;
let n be Nat; ( n <= m implies (Comput ((P +* I),(Initialize s),n)) . a = s . a )
assume A7:
n <= m
; (Comput ((P +* I),(Initialize s),n)) . a = s . a
(Comput ((P +* I),(Initialize s),0)) . a =
(Initialize s) . a
.=
s . a
by SCMFSA_M:21
;
then A8:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A8, A3);
hence
(Comput ((P +* I),(Initialize s),n)) . a = s . a
by A7; verum