let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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
NPP (Comput ((P +* (stop I)),s,k)) = NPP (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
NPP (Comput ((P +* (stop I)),s,k)) = NPP (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
NPP (Comput ((P +* (stop I)),s,k)) = NPP (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
NPP (Comput ((P +* (stop I)),s,k)) = NPP (Comput ((P +* (stop (I ';' J))),s,k))
let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((P +* (stop I)),s) implies NPP (Comput ((P +* (stop I)),s,k)) = NPP (Comput ((P +* (stop (I ';' J))),s,k)) )
A1: stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30;
A2: s = Initialize s by COMPOS_1:78;
assume k <= LifeSpan ((P +* (stop I)),s) ; :: thesis: NPP (Comput ((P +* (stop I)),s,k)) = NPP (Comput ((P +* (stop (I ';' J))),s,k))
hence NPP (Comput ((P +* (stop I)),s,k)) = NPP (Comput ((P +* (stop (I ';' J))),s,k)) by A1, Th33, A2; :: thesis: verum