let s be State of SCMPDS ; :: thesis: for I being parahalting Program of SCMPDS
for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k, Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),k equal_outside NAT
let I be parahalting Program of SCMPDS ; :: thesis: for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k, Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),k equal_outside NAT
let J be Program of SCMPDS ; :: thesis: for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k, Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),k equal_outside NAT
let k be Element of NAT ; :: thesis: ( k <= LifeSpan (s +* (Initialized (stop I))) implies Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k, Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),k equal_outside NAT )
A1: Initialized (stop (I ';' J)) = (I ';' (J ';' (Stop SCMPDS ))) +* (Start-At 0 ,SCMPDS ) by SCMPDS_4:46;
assume k <= LifeSpan (s +* (Initialized (stop I))) ; :: thesis: Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k, Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),k equal_outside NAT
hence Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k, Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),k equal_outside NAT by A1, Th33; :: thesis: verum