let s be State of ; :: thesis: for I being Program of
for a being Int_position st I is_halting_on s holds
(IExec I,s) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a
let I be Program of ; :: thesis: for a being Int_position st I is_halting_on s holds
(IExec I,s) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a
let a be Int_position ; :: thesis: ( I is_halting_on s implies (IExec I,s) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a )
set s1 = s +* (Initialized (stop I));
assume I is_halting_on s ; :: thesis: (IExec I,s) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a
then A1: ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by SCMPDS_6:def 3;
A2: dom (s | NAT ) = NAT by SCMPDS_6:1;

now

assume a in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = a as Instruction-Location of SCMPDS by A2, AMI_1:def 4;
l = a ;
hence contradiction by SCMPDS_2:53; :: thesis: verum

end;

hence (IExec I,s) . a = (Result (s +* (Initialized (stop I)))) . a by FUNCT_4:12
.= (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a by A1, AMI_1:122 ;
:: thesis: verum