let P be Instruction-Sequence of SCMPDS; :: 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,(Initialize 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,(Initialize 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,(Initialize 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,(Initialize 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,(Initialize 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;
thus (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by A1, EXTPRO_1:23; :: thesis: verum