let s be State of ; :: thesis: for I being Program of
for a being Int-Location st I does_not_destroy a & I is_closed_on s holds
for k being Element of NAT holds (Computation (s +* (I +* (Start-At (insloc 0 )))),k) . a = s . a
let I be Program of ; :: thesis: for a being Int-Location st I does_not_destroy a & I is_closed_on s holds
for k being Element of NAT holds (Computation (s +* (I +* (Start-At (insloc 0 )))),k) . a = s . a
let a be Int-Location ; :: thesis: ( I does_not_destroy a & I is_closed_on s implies for k being Element of NAT holds (Computation (s +* (I +* (Start-At (insloc 0 )))),k) . a = s . a )
assume A1: I does_not_destroy a ; :: thesis: ( not I is_closed_on s or for k being Element of NAT holds (Computation (s +* (I +* (Start-At (insloc 0 )))),k) . a = s . a )
defpred S₁[ Element of NAT ] means (Computation (s +* (I +* (Start-At (insloc 0 )))),$1) . a = s . a;
dom I misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then ( I +* (Start-At (insloc 0 )) c= s +* (I +* (Start-At (insloc 0 ))) & I c= I +* (Start-At (insloc 0 )) ) by FUNCT_4:26, FUNCT_4:33;
then A2: I c= s +* (I +* (Start-At (insloc 0 ))) by XBOOLE_1:1;
assume A3: I is_closed_on s ; :: thesis: for k being Element of NAT holds (Computation (s +* (I +* (Start-At (insloc 0 )))),k) . a = s . a

A4: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
set l = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k);
A6: IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) in dom I by A3, Def7;
then (s +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k)) = I . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k)) by A2, GRFUNC_1:8;
then (s +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k)) in rng I by A6, FUNCT_1:def 5;
then A7: (s +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k)) does_not_destroy a by A1, Def4;
(Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1)) . a = (Following (Computation (s +* (I +* (Start-At (insloc 0 )))),k)) . a by AMI_1:14
.= (Exec (CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s +* (I +* (Start-At (insloc 0 )))),k)) . a by AMI_1:def 18
.= (Exec ((Computation (s +* (I +* (Start-At (insloc 0 )))),k) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k))),(Computation (s +* (I +* (Start-At (insloc 0 )))),k)) . a by AMI_1:def 16
.= (Exec ((s +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k))),(Computation (s +* (I +* (Start-At (insloc 0 )))),k)) . a by AMI_1:54
.= s . a by A5, A7, Th26 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A8: not a in dom (I +* (Start-At (insloc 0 ))) by SCMFSA6B:12;
(Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) . a = (s +* (I +* (Start-At (insloc 0 )))) . a by AMI_1:13
.= s . a by A8, FUNCT_4:12 ;
then A9: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A9, A4); :: thesis: verum