let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position st I is_halting_on s,P holds
(IExec (I,P,s)) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a
let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS
for a being Int_position st I is_halting_on s,P holds
(IExec (I,P,s)) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a
let I be Program of SCMPDS; :: thesis: for a being Int_position st I is_halting_on s,P holds
(IExec (I,P,s)) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a
let a be Int_position ; :: thesis: ( I is_halting_on s,P implies (IExec (I,P,s)) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a )
set s1 = Initialize s;
set P1 = P +* (stop I);
assume I is_halting_on s,P ; :: thesis: (IExec (I,P,s)) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a
then A1: P +* (stop I) halts_on Initialize s 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,P,s)) . a = (Result ((P +* (stop I)),(Initialize s))) . a by FUNCT_4:12
.= (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by A1, EXTPRO_1:23 ;
:: thesis: verum