let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k)
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 ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k)
let I be parahalting Program of SCMPDS; :: thesis: for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k)
let J be Program of SCMPDS; :: thesis: for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k)
let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) )
A1: stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27;
A2: s = Initialize s by MEMSTR_0:44;
hence ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) ) by A1, Th33; :: thesis: verum