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 (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k, Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize 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 ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k, Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize 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 ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k, Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k equal_outside NAT
let k be Element of NAT ; :: thesis: ( k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) implies Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k, Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k equal_outside NAT )
A1: Initialize (stop (I ';' J)) = (I ';' (J ';' (Stop SCMPDS ))) +* (Start-At 0 ,SCMPDS ) by SCMPDS_4:46;
I2: (Initialize s) +* (stop (I ';' J)) = s +* (Initialize (stop (I ';' J))) by SCMPDS_4:5;
assume k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) ; :: thesis: Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k, Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k equal_outside NAT
hence Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k, Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k equal_outside NAT by A1, Th33, I2; :: thesis: verum