let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS
for a being Int_position st I is_halting_on s holds
(IExec I,s) . a = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a
let I be Program of SCMPDS ; :: thesis: for a being Int_position st I is_halting_on s holds
(IExec I,s) . a = (Comput (ProgramPart (s +* (Initialized (stop I)))),(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 = (Comput (ProgramPart (s +* (Initialized (stop I)))),(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 = (Comput (ProgramPart (s +* (Initialized (stop I)))),(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;
not a in dom (s | NAT ) by A2, SCMPDS_2:53;
hence (IExec I,s) . a = (Result (s +* (Initialized (stop I)))) . a by FUNCT_4:12
.= (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a by A1, AMI_1:122 ;
:: thesis: verum