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 ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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 ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . a
let a be Int_position ; :: thesis: ( I is_halting_on s implies (IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . a )
set s1 = (Initialize s) +* (stop I);
assume I is_halting_on s ; :: thesis: (IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . a
then A1: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by SCMPDS_6:def 3;
A2: dom (ProgramPart s) = NAT by COMPOS_1:34;
not a in dom (s | NAT ) by A2, SCMPDS_2:53;
hence (IExec I,s) . a = (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) . a by FUNCT_4:12
.= (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . a by A1, AMI_1:122 ;
:: thesis: verum