theorem Th16:
for
s2 being
State of
SCMPDS for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
s1 being
0 -started State of
SCMPDS for
I being
halt-free shiftable Program of st
stop I c= P1 &
I is_closed_on s1,
P1 &
I is_halting_on s1,
P1 holds
for
n being
Nat st
Shift (
I,
n)
c= P2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
(
IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n &
DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )