let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st not I destroysdestroy a holds
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a
let I be Program of SCM+FSA ; :: thesis: for a being Int-Location st not I destroysdestroy a holds
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a
let a be Int-Location ; :: thesis: ( not I destroysdestroy a implies for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a )
assume A1: not I destroysdestroy a ; :: thesis: for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a
set s1 = s +* (I +* (Start-At 0 ,SCM+FSA ));
let m be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I ) implies for n being Element of NAT st n <= m holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a )
defpred S₁[ Nat] means ( $1 <= m implies (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),$1) . a = s . a );
assume A2: for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I ; :: thesis: for n being Element of NAT st n <= m holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: k + 0 < k + 1 by XREAL_1:8;
assume A6: k + 1 <= m ; :: thesis: (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) . a = s . a
then k < m by A5, XXREAL_0:2;
then IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I by A2;
hence (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) . a = s . a by A1, A4, A6, A5, Th93, XXREAL_0:2; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( n <= m implies (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a )
assume A7: n <= m ; :: thesis: (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) . a = (s +* (I +* (Start-At 0 ,SCM+FSA ))) . a by AMI_1:13
.= s . a by Th28 ;
then A8: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A3);
hence (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a by A7; :: thesis: verum