let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of
for J being Program of
for k being 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
for J being Program of
for k being 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 ; :: thesis: for J being Program of
for k being 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 ; :: thesis: for k being 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 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;
thus ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) ) by A1, Th17; :: thesis: verum