begin
set SA0 = Start-At (0,SCM+FSA);
definition
let I be
Program of ;
canceled;canceled;
end;
Lm1:
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds not P +* ((IC s),(goto (IC s))) halts_on s
theorem Th6:
for
s2 being
State of
SCM+FSA for
s1 being
0 -started State of
SCM+FSA for
P,
Q being
Instruction-Sequence of
SCM+FSA for
J being
parahalting Program of st
J c= P holds
for
n being
Element of
NAT st
Reloc (
J,
n)
c= Q &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
(IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) &
IncAddr (
(CurInstr (P,(Comput (P,s1,i)))),
n)
= CurInstr (
Q,
(Comput (Q,s2,i))) &
DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
theorem Th7:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s being
0 -started State of
SCM+FSA for
I being
parahalting Program of st
I c= P1 &
I c= P2 holds
for
k being
Element of
NAT holds
(
Comput (
P1,
s,
k)
= Comput (
P2,
s,
k) &
CurInstr (
P1,
(Comput (P1,s,k)))
= CurInstr (
P2,
(Comput (P2,s,k))) )
begin
Lm2:
for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of
for s being State of SCM+FSA st I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )