let P be Instruction-Sequence of SCM+FSA; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( ( 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 S₁[ 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 ; :: thesis: for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . a = s . a
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: k + 0 < k + 1 by XREAL_1:6;
assume A6: k + 1 <= m ; :: thesis: (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; :: thesis: verum

end;

let n be Nat; :: thesis: ( n <= m implies (Comput ((P +* I),(Initialize s),n)) . a = s . a )
assume A7: n <= m ; :: thesis: (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: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A3);
hence (Comput ((P +* I),(Initialize s),n)) . a = s . a by A7; :: thesis: verum