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