theorem Th14:
for
s being
State of
SCM+FSA for
p being
Instruction-Sequence of
SCM+FSA for
I being
really-closed keepInt0_1 Program of
SCM+FSA st
p +* I halts_on s holds
for
J being
really-closed Program of
SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s &
I ";" J c= p holds
for
k being
Element of
NAT holds
(Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput (
(p +* (I ";" J)),
s,
(((LifeSpan ((p +* I),s)) + 1) + k))