begin
set A = NAT ;
set D = SCM-Data-Loc ;
Lm1:
(Stop SCMPDS) . 0 = halt SCMPDS
by AFINSQ_1:34;
Lm2:
0 in dom (Stop SCMPDS)
by COMPOS_1:3;
begin
theorem Th25:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I,
J being
Program of
SCMPDS st
I is_closed_on s,
P &
I is_halting_on s,
P holds
( ( for
k being
Element of
NAT st
k <= LifeSpan (
(P +* (stop I)),
s) holds
IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) ) &
DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) )
theorem Th27:
for
P being
Instruction-Sequence of
SCMPDS for
I,
J being
Program of
SCMPDS for
s being
0 -started State of
SCMPDS for
k being
Element of
NAT st
I is_closed_on s,
P &
I is_halting_on s,
P &
k < LifeSpan (
(P +* (stop I)),
s) holds
CurInstr (
(P +* (stop I)),
(Comput ((P +* (stop I)),s,k)))
= CurInstr (
(P +* (stop (I ';' J))),
(Comput ((P +* (stop (I ';' J))),s,k)))
Lm3:
for P being Instruction-Sequence of SCMPDS
for I being halt-free Program of SCMPDS
for J being Program of SCMPDS
for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) & ( for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds
CurInstr ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,k))) <> halt SCMPDS ) & IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I & P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on s & LifeSpan ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + 1 )
theorem Th31:
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
shiftable Program of
SCMPDS st
stop I c= P1 &
I is_closed_on s1,
P1 holds
for
n being
Element of
NAT st
Shift (
(stop 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)) &
CurInstr (
P1,
(Comput (P1,s1,i)))
= CurInstr (
P2,
(Comput (P2,s2,i))) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
begin
Lm4:
for n being Element of NAT
for i being Instruction of SCMPDS
for I, J being Program of SCMPDS holds card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2
begin
Lm5:
for i being Instruction of SCMPDS
for I, J, K being Program of SCMPDS holds (((i ';' I) ';' J) ';' K) . 0 = i
Lm6:
for i being Instruction of SCMPDS
for I being Program of SCMPDS
for P being Instruction-Sequence of SCMPDS holds Shift ((stop I),1) c= P +* (stop (i ';' I))
Lm7:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS
for P being Instruction-Sequence of SCMPDS holds Shift ((stop I),2) c= P +* (stop ((i ';' j) ';' I))
theorem Th38:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I,
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) = 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
(
if=0 (
a,
k1,
I,
J)
is_closed_on s,
P &
if=0 (
a,
k1,
I,
J)
is_halting_on s,
P )
theorem Th39:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
Program of
SCMPDS for
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) <> 0 &
J is_closed_on s,
P &
J is_halting_on s,
P holds
(
if=0 (
a,
k1,
I,
J)
is_closed_on s,
P &
if=0 (
a,
k1,
I,
J)
is_halting_on s,
P )
theorem Th40:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) = 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if=0 (a,k1,I,J)),
P,
s)
= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
theorem Th41:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
Program of
SCMPDS for
J being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) <> 0 &
J is_closed_on s,
P &
J is_halting_on s,
P holds
IExec (
(if=0 (a,k1,I,J)),
P,
(Initialize s))
= (IExec (J,P,(Initialize s))) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
begin
theorem Th50:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) = 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if=0 (a,k1,I)),
P,
(Initialize s))
= (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
Lm8:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds card ((i ';' j) ';' I) = (card I) + 2
begin
Lm9:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds
( 0 in dom ((i ';' j) ';' I) & 1 in dom ((i ';' j) ';' I) )
Lm10:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds
( ((i ';' j) ';' I) . 0 = i & ((i ';' j) ';' I) . 1 = j )
theorem Th60:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) <> 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if<>0 (a,k1,I)),
P,
(Initialize s))
= (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))
begin
theorem Th68:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I,
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) > 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
(
if>0 (
a,
k1,
I,
J)
is_closed_on s,
P &
if>0 (
a,
k1,
I,
J)
is_halting_on s,
P )
theorem Th69:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
Program of
SCMPDS for
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) <= 0 &
J is_closed_on s,
P &
J is_halting_on s,
P holds
(
if>0 (
a,
k1,
I,
J)
is_closed_on s,
P &
if>0 (
a,
k1,
I,
J)
is_halting_on s,
P )
theorem Th70:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) > 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if>0 (a,k1,I,J)),
P,
s)
= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
theorem Th71:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
Program of
SCMPDS for
J being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) <= 0 &
J is_closed_on s,
P &
J is_halting_on s,
P holds
IExec (
(if>0 (a,k1,I,J)),
P,
s)
= (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
begin
theorem Th80:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) > 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if>0 (a,k1,I)),
P,
(Initialize s))
= (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
begin
theorem Th90:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) <= 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if<=0 (a,k1,I)),
P,
(Initialize s))
= (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))
begin
theorem Th98:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I,
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) < 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
(
if<0 (
a,
k1,
I,
J)
is_closed_on s,
P &
if<0 (
a,
k1,
I,
J)
is_halting_on s,
P )
theorem Th99:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
Program of
SCMPDS for
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) >= 0 &
J is_closed_on s,
P &
J is_halting_on s,
P holds
(
if<0 (
a,
k1,
I,
J)
is_closed_on s,
P &
if<0 (
a,
k1,
I,
J)
is_halting_on s,
P )
theorem Th100:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
J being
shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) < 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if<0 (a,k1,I,J)),
P,
s)
= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
theorem Th101:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
Program of
SCMPDS for
J being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) >= 0 &
J is_closed_on s,
P &
J is_halting_on s,
P holds
IExec (
(if<0 (a,k1,I,J)),
P,
(Initialize s))
= (IExec (J,P,(Initialize s))) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
begin
theorem Th110:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) < 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if<0 (a,k1,I)),
P,
(Initialize s))
= (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
begin
theorem Th120:
for
P being
Instruction-Sequence of
SCMPDS for
s being
State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS for
a being
Int_position for
k1 being
Integer st
s . (DataLoc ((s . a),k1)) >= 0 &
I is_closed_on s,
P &
I is_halting_on s,
P holds
IExec (
(if>=0 (a,k1,I)),
P,
(Initialize s))
= (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))