let s be State of ; :: thesis: for I being Program of
for a being Int-Location st I does_not_destroy a holds
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = s . a
let I be Program of ; :: thesis: for a being Int-Location st I does_not_destroy a holds
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = s . a
let a be Int-Location ; :: thesis: ( I does_not_destroy a implies for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = s . a )
assume A1: I does_not_destroy a ; :: thesis: for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = s . a
set s1 = s +* (I +* (Start-At (insloc 0 )));
let m be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n < m holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ) implies for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = s . a )
defpred S₁[ Element of NAT ] means ( $1 <= m implies (Computation (s +* (I +* (Start-At (insloc 0 )))),$1) . a = s . a );
assume A2: for n being Element of NAT st n < m holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ; :: thesis: for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),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: (Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1)) . a = s . a
then k < m by A5, XXREAL_0:2;
then IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) in dom I by A2;
hence (Computation (s +* (I +* (Start-At (insloc 0 )))),(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 (Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = s . a )
assume A7: n <= m ; :: thesis: (Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = s . a
(Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) . a = (s +* (I +* (Start-At (insloc 0 )))) . 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 (Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = s . a by A7; :: thesis: verum