let s be 0 -started 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 ((ProgramPart (s +* (stop I))),(s +* (stop I))) holds
Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k), Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (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 ((ProgramPart (s +* (stop I))),(s +* (stop I))) holds
Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k), Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),k) equal_outside NAT
let J be Program of SCMPDS; :: thesis: for k being Element of NAT st k <= LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) holds
Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k), Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),k) equal_outside NAT
let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) implies Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k), Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),k) equal_outside NAT )
A1: stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30;
AA: s = Initialize s by COMPOS_1:78;
I2: (Initialize s) +* (stop (I ';' J)) = s +* (Initialize (stop (I ';' J))) by COMPOS_1:125;
assume k <= LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) ; :: thesis: Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k), Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),k) equal_outside NAT
hence Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k), Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),k) equal_outside NAT by A1, Th33, I2, AA; :: thesis: verum