begin
set SA0 = Start-At (0,SCM+FSA);
set Q = (intloc 0) .--> 1;
theorem Th16:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1 being
0 -started State of
SCM+FSA for
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1,
P1 &
I c= P1 holds
for
n being
Element of
NAT st
Reloc (
I,
n)
c= P2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
(IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) &
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
n)
= CurInstr (
P2,
(Comput (P2,s2,i))) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
theorem Th17:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
0 -started State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1,
P1 &
I c= P1 &
I c= P2 &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) &
CurInstr (
P1,
(Comput (P1,s1,i)))
= CurInstr (
P2,
(Comput (P2,s2,i))) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
theorem Th22:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1 being
0 -started State of
SCM+FSA for
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I c= P1 &
I is_pseudo-closed_on s1,
P1 holds
for
n being
Element of
NAT st
Reloc (
I,
n)
c= P2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
( ( for
i being
Element of
NAT st
i < pseudo-LifeSpan (
s1,
P1,
I) holds
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
n)
= CurInstr (
P2,
(Comput (P2,s2,i))) ) & ( for
i being
Element of
NAT st
i <= pseudo-LifeSpan (
s1,
P1,
I) holds
(
(IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )
theorem Th29:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
Directed I is_pseudo-closed_on s,
P holds
(
I ";" (Stop SCM+FSA) is_closed_on s,
P &
I ";" (Stop SCM+FSA) is_halting_on s,
P &
LifeSpan (
(P +* (I ";" (Stop SCM+FSA))),
(Initialize s))
= pseudo-LifeSpan (
s,
P,
(Directed I)) & ( for
n being
Element of
NAT st
n < pseudo-LifeSpan (
s,
P,
(Directed I)) holds
IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) & ( for
n being
Element of
NAT st
n <= pseudo-LifeSpan (
s,
P,
(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )
theorem Th37:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a = 0 &
Directed I is_pseudo-closed_on s,
P holds
(
if=0 (
a,
I,
J)
is_halting_on s,
P &
if=0 (
a,
I,
J)
is_closed_on s,
P &
LifeSpan (
(P +* (if=0 (a,I,J))),
(Initialize s))
= (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )
theorem Th39:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a > 0 &
Directed I is_pseudo-closed_on s,
P holds
(
if>0 (
a,
I,
J)
is_halting_on s,
P &
if>0 (
a,
I,
J)
is_closed_on s,
P &
LifeSpan (
(P +* (if>0 (a,I,J))),
(Initialize s))
= (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )
theorem Th41:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a <> 0 &
Directed J is_pseudo-closed_on s,
P holds
(
if=0 (
a,
I,
J)
is_halting_on s,
P &
if=0 (
a,
I,
J)
is_closed_on s,
P &
LifeSpan (
(P +* (if=0 (a,I,J))),
(Initialize s))
= (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )
theorem Th43:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a <= 0 &
Directed J is_pseudo-closed_on s,
P holds
(
if>0 (
a,
I,
J)
is_halting_on s,
P &
if>0 (
a,
I,
J)
is_closed_on s,
P &
LifeSpan (
(P +* (if>0 (a,I,J))),
(s +* (Start-At (0,SCM+FSA))))
= (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )
theorem Th58:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_halting_on Initialized s,
P holds
( ( for
a being
read-write Int-Location holds
(IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a ) & ( for
f being
FinSeq-Location holds
(IExec (I,P,s)) . f = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . f ) )
theorem Th71:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1,
P1 &
I is_halting_on s1,
P1 &
DataPart s1 = DataPart s2 holds
for
k being
Element of
NAT holds
(
Comput (
(P1 +* I),
(Initialize s1),
k)
= Comput (
(P2 +* I),
(Initialize s2),
k) &
CurInstr (
(P1 +* I),
(Comput ((P1 +* I),(Initialize s1),k)))
= CurInstr (
(P2 +* I),
(Comput ((P2 +* I),(Initialize s2),k))) )
begin
Lm1:
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA ) )
begin
theorem Th89:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
good parahalting Program of
SCM+FSA for
a being
read-write Int-Location st not
I destroys a &
s . (intloc 0) = 1 &
s . a > 0 holds
ex
s2 being
State of
SCM+FSA ex
P2 being
Instruction-Sequence of
SCM+FSA ex
k being
Element of
NAT st
(
s2 = s +* (Start-At (0,SCM+FSA)) &
P2 = P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) &
k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 &
(Comput (P2,s2,k)) . a = (s . a) - 1 &
(Comput (P2,s2,k)) . (intloc 0) = 1 & ( for
b being
read-write Int-Location st
b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for
f being
FinSeq-Location holds
(Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) &
IC (Comput (P2,s2,k)) = 0 & ( for
n being
Element of
NAT st
n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) )
theorem Th91:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
good parahalting Program of
SCM+FSA for
a being
read-write Int-Location st not
I destroys a &
s . a > 0 holds
(
(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 &
DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) )
begin