begin
set A = NAT ;
set D = SCM-Data-Loc ;
theorem Th25:
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
s1,
s2 being
State of
SCMPDS for
I being
Program of
SCMPDS st
I is_closed_on s1,
P1 &
DataPart s1 = DataPart s2 holds
for
k being
Element of
NAT holds
(
Comput (
(P1 +* (stop I)),
(Initialize s1),
k)
= Comput (
(P2 +* (stop I)),
(Initialize s2),
k) &
CurInstr (
(P1 +* (stop I)),
(Comput ((P1 +* (stop I)),(Initialize s1),k)))
= CurInstr (
(P2 +* (stop I)),
(Comput ((P2 +* (stop I)),(Initialize s2),k))) )
theorem Th26:
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
Program of
SCMPDS st
I is_closed_on s,
P1 &
stop I c= P1 &
stop 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))) )
theorem Th34:
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 &
I is_halting_on s1,
P1 holds
for
n being
Element of
NAT st
Shift (
I,
n)
c= P2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT st
i < LifeSpan (
P1,
s1) 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)) )
theorem Th36:
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
SCMPDS st
stop I c= P1 &
I is_closed_on s1,
P1 &
I is_halting_on s1,
P1 holds
for
n being
Element of
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)))) )
theorem Th41:
for
s being
State of
SCMPDS for
P being
Instruction-Sequence of
SCMPDS for
I,
J being
Program of
SCMPDS st
I c= J &
I is_closed_on s,
P &
I is_halting_on s,
P & not
CurInstr (
(P +* J),
(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))
= halt SCMPDS holds
IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
theorem Th42:
for
s being
State of
SCMPDS for
P being
Instruction-Sequence of
SCMPDS for
I,
J being
Program of
SCMPDS st
I is_halting_on s,
P &
J is_closed_on IExec (
I,
P,
(Initialize s)),
P &
J is_halting_on IExec (
I,
P,
(Initialize s)),
P holds
(
J is_closed_on Comput (
(P +* (stop I)),
(Initialize s),
(LifeSpan ((P +* (stop I)),(Initialize s)))),
P +* (stop I) &
J is_halting_on Comput (
(P +* (stop I)),
(Initialize s),
(LifeSpan ((P +* (stop I)),(Initialize s)))),
P +* (stop I) )
theorem Th43:
for
s being
State of
SCMPDS for
P being
Instruction-Sequence of
SCMPDS for
I being
Program of
SCMPDS for
J being
shiftable Program of
SCMPDS st
I is_closed_on s,
P &
I is_halting_on s,
P &
J is_closed_on IExec (
I,
P,
(Initialize s)),
P &
J is_halting_on IExec (
I,
P,
(Initialize s)),
P holds
(
I ';' J is_closed_on s,
P &
I ';' J is_halting_on s,
P )
Lm1:
for P, P2, P1 being Instruction-Sequence of SCMPDS
for I being halt-free Program of SCMPDS
for J being shiftable Program of SCMPDS
for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds
( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
theorem
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
halt-free Program of
SCMPDS for
J being
shiftable Program of
SCMPDS st
I is_closed_on s,
P &
I is_halting_on s,
P &
J is_closed_on IExec (
I,
P,
s),
P &
J is_halting_on IExec (
I,
P,
s),
P holds
LifeSpan (
(P +* (stop (I ';' J))),
s)
= (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) by Lm1;
theorem Th48:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
halt-free Program of
SCMPDS for
J being
shiftable Program of
SCMPDS st
I is_closed_on s,
P &
I is_halting_on s,
P &
J is_closed_on IExec (
I,
P,
s),
P &
J is_halting_on IExec (
I,
P,
s),
P holds
IExec (
(I ';' J),
P,
s)
= IncIC (
(IExec (J,P,(Initialize (IExec (I,P,s))))),
(card I))
theorem Th49:
for
a being
Int_position for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
halt-free Program of
SCMPDS for
J being
shiftable Program of
SCMPDS st
I is_closed_on s,
P &
I is_halting_on s,
P &
J is_closed_on IExec (
I,
P,
s),
P &
J is_halting_on IExec (
I,
P,
s),
P holds
(IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a
begin
begin
Lm2:
for a being Int_position
for i being Integer
for n being Element of NAT
for I being Program of SCMPDS holds card (stop (for-up (a,i,n,I))) = (card I) + 4
theorem Th53:
for
a being
Int_position for
i being
Integer for
n being
Element of
NAT for
I being
Program of
SCMPDS holds
(
(for-up (a,i,n,I)) . 0 = (
a,
i)
>=0_goto ((card I) + 3) &
(for-up (a,i,n,I)) . ((card I) + 1) = AddTo (
a,
i,
n) &
(for-up (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
Lm3:
for I being Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of NAT holds Shift (I,1) c= for-up (a,i,n,I)
theorem Th58:
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
i being
Integer for
n being
Element of
NAT for
X being
set st
s . (DataLoc ((s . a),i)) < 0 & not
DataLoc (
(s . a),
i)
in X &
n > 0 &
a <> DataLoc (
(s . a),
i) & ( for
t being
State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a holds
(
(IExec (I,Q,(Initialize t))) . a = t . a &
(IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) &
I is_closed_on t,
Q &
I is_halting_on t,
Q & ( for
y being
Int_position st
y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
(
for-up (
a,
i,
n,
I)
is_closed_on s,
P &
for-up (
a,
i,
n,
I)
is_halting_on s,
P )
theorem
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
a being
Int_position for
i being
Integer for
n being
Element of
NAT for
X being
set st
s . (DataLoc ((s . a),i)) < 0 & not
DataLoc (
(s . a),
i)
in X &
n > 0 &
a <> DataLoc (
(s . a),
i) & ( for
t being
State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a holds
(
(IExec (I,Q,(Initialize t))) . a = t . a &
(IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) &
I is_closed_on t,
Q &
I is_halting_on t,
Q & ( for
y being
Int_position st
y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
IExec (
(for-up (a,i,n,I)),
P,
s)
= IExec (
(for-up (a,i,n,I)),
P,
(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
begin
begin
Lm4:
for a being Int_position
for i being Integer
for n being Element of NAT
for I being Program of SCMPDS holds card (stop (for-down (a,i,n,I))) = (card I) + 4
theorem Th62:
for
a being
Int_position for
i being
Integer for
n being
Element of
NAT for
I being
Program of
SCMPDS holds
(
(for-down (a,i,n,I)) . 0 = (
a,
i)
<=0_goto ((card I) + 3) &
(for-down (a,i,n,I)) . ((card I) + 1) = AddTo (
a,
i,
(- n)) &
(for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
Lm5:
for I being Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of NAT holds Shift (I,1) c= for-down (a,i,n,I)
theorem Th67:
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
i being
Integer for
n being
Element of
NAT for
X being
set st
s . (DataLoc ((s . a),i)) > 0 & not
DataLoc (
(s . a),
i)
in X &
n > 0 &
a <> DataLoc (
(s . a),
i) & ( for
t being
0 -started State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a holds
(
(IExec (I,Q,t)) . a = t . a &
(IExec (I,Q,t)) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) &
I is_closed_on t,
Q &
I is_halting_on t,
Q & ( for
y being
Int_position st
y in X holds
(IExec (I,Q,t)) . y = t . y ) ) ) holds
(
for-down (
a,
i,
n,
I)
is_closed_on s,
P &
for-down (
a,
i,
n,
I)
is_halting_on s,
P )
theorem Th68:
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
a being
Int_position for
i being
Integer for
n being
Element of
NAT for
X being
set st
s . (DataLoc ((s . a),i)) > 0 & not
DataLoc (
(s . a),
i)
in X &
n > 0 &
a <> DataLoc (
(s . a),
i) & ( for
t being
0 -started State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a holds
(
(IExec (I,Q,t)) . a = t . a &
(IExec (I,Q,t)) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) &
I is_closed_on t,
Q &
I is_halting_on t,
Q & ( for
y being
Int_position st
y in X holds
(IExec (I,Q,t)) . y = t . y ) ) ) holds
IExec (
(for-down (a,i,n,I)),
P,
s)
= IExec (
(for-down (a,i,n,I)),
P,
(Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s))))
begin
theorem Th69:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS st
s . GBP = 0 holds
(
for-down (
GBP,2,1,
(Load (AddTo (GBP,3,1))))
is_closed_on s,
P &
for-down (
GBP,2,1,
(Load (AddTo (GBP,3,1))))
is_halting_on s,
P )
definition
let sp,
control,
result,
pp,
pData be
Element of
NAT ;
func sum (
sp,
control,
result,
pp,
pData)
-> Program of
SCMPDS equals
((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1)))));
coherence
((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1))))) is Program of SCMPDS
;
end;
::
deftheorem defines
sum SCMPDS_7:def 4 :
for sp, control, result, pp, pData being Element of NAT holds sum (sp,control,result,pp,pData) = ((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1)))));
theorem Th72:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
sp,
cv,
result,
pp,
pD being
Element of
NAT st
s . (intpos sp) > sp &
cv < result &
s . (intpos pp) = pD &
(s . (intpos sp)) + result < pp &
pp < pD &
pD < s . (intpos pD) holds
(
for-down (
(intpos sp),
cv,1,
((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))
is_closed_on s,
P &
for-down (
(intpos sp),
cv,1,
((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))
is_halting_on s,
P )
theorem Th73:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
sp,
cv,
result,
pp,
pD being
Element of
NAT for
f being
FinSequence of
NAT st
s . (intpos sp) > sp &
cv < result &
s . (intpos pp) = pD &
(s . (intpos sp)) + result < pp &
pp < pD &
pD < s . (intpos pD) &
s . (DataLoc ((s . (intpos sp)),result)) = 0 &
len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for
k being
Element of
NAT st
k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f
theorem
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
sp,
cv,
result,
pp,
pD being
Element of
NAT for
f being
FinSequence of
NAT st
s . (intpos sp) > sp &
cv < result &
(s . (intpos sp)) + result < pp &
pp < pD &
pD < s . (intpos pD) &
len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for
k being
Element of
NAT st
k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((sum (sp,cv,result,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f