begin
set A = NAT ;
set D = SCM-Data-Loc ;
theorem Th1:
:: deftheorem Def1 defines Dstate SCMPDS_8:def 1 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
begin
:: deftheorem defines while<0 SCMPDS_8:def 2 :
theorem Th6:
Lm1:
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds card (stop (while<0 a,i,I)) = (card I) + 3
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem
Lm2:
for I being Program of SCMPDS
for a being Int_position
for i being Integer holds Shift I,1 c= while<0 a,i,I
theorem
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i being
Integer for
X being
set for
f being
Function of
(product the Object-Kind of SCMPDS ),
NAT st
card I > 0 & ( for
t being
State of
SCMPDS st
f . (Dstate t) = 0 holds
t . (DataLoc (s . a),i) >= 0 ) & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) < 0 holds
(
(IExec I,t) . a = t . a &
f . (Dstate (IExec I,t)) < f . (Dstate t) &
I is_closed_on t &
I is_halting_on t & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x = t . x ) ) ) holds
(
while<0 a,
i,
I is_closed_on s &
while<0 a,
i,
I is_halting_on s )
theorem
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i being
Integer for
X being
set for
f being
Function of
(product the Object-Kind of SCMPDS ),
NAT st
card I > 0 &
s . (DataLoc (s . a),i) < 0 & ( for
t being
State of
SCMPDS st
f . (Dstate t) = 0 holds
t . (DataLoc (s . a),i) >= 0 ) & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) < 0 holds
(
(IExec I,t) . a = t . a &
I is_closed_on t &
I is_halting_on t &
f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while<0 a,i,I),
s = IExec (while<0 a,i,I),
(IExec I,s)
theorem Th15:
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i being
Integer for
X being
set st
card I > 0 & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) < 0 holds
(
(IExec I,t) . a = t . a &
(IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) &
I is_closed_on t &
I is_halting_on t & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x = t . x ) ) ) holds
(
while<0 a,
i,
I is_closed_on s &
while<0 a,
i,
I is_halting_on s )
theorem
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i being
Integer for
X being
set st
s . (DataLoc (s . a),i) < 0 &
card I > 0 & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) < 0 holds
(
(IExec I,t) . a = t . a &
(IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) &
I is_closed_on t &
I is_halting_on t & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while<0 a,i,I),
s = IExec (while<0 a,i,I),
(IExec I,s)
begin
:: deftheorem defines while>0 SCMPDS_8:def 3 :
theorem Th17:
Lm3:
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds card (stop (while>0 a,i,I)) = (card I) + 3
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
Lm4:
for I being Program of SCMPDS
for a being Int_position
for i being Integer holds Shift I,1 c= while>0 a,i,I
theorem Th24:
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i,
c being
Integer for
X,
Y being
set for
f being
Function of
(product the Object-Kind of SCMPDS ),
NAT st
card I > 0 & ( for
t being
State of
SCMPDS st
f . (Dstate t) = 0 holds
t . (DataLoc (s . a),i) <= 0 ) & ( for
x being
Int_position st
x in X holds
s . x >= c + (s . (DataLoc (s . a),i)) ) & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x >= c + (t . (DataLoc (s . a),i)) ) & ( for
x being
Int_position st
x in Y holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) > 0 holds
(
(IExec I,t) . a = t . a &
I is_closed_on t &
I is_halting_on t &
f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for
x being
Int_position st
x in Y holds
(IExec I,t) . x = t . x ) ) ) holds
(
while>0 a,
i,
I is_closed_on s &
while>0 a,
i,
I is_halting_on s )
theorem Th25:
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i,
c being
Integer for
X,
Y being
set for
f being
Function of
(product the Object-Kind of SCMPDS ),
NAT st
s . (DataLoc (s . a),i) > 0 &
card I > 0 & ( for
t being
State of
SCMPDS st
f . (Dstate t) = 0 holds
t . (DataLoc (s . a),i) <= 0 ) & ( for
x being
Int_position st
x in X holds
s . x >= c + (s . (DataLoc (s . a),i)) ) & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x >= c + (t . (DataLoc (s . a),i)) ) & ( for
x being
Int_position st
x in Y holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) > 0 holds
(
(IExec I,t) . a = t . a &
I is_closed_on t &
I is_halting_on t &
f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for
x being
Int_position st
x in Y holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while>0 a,i,I),
s = IExec (while>0 a,i,I),
(IExec I,s)
theorem
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i being
Integer for
X being
set for
f being
Function of
(product the Object-Kind of SCMPDS ),
NAT st
card I > 0 & ( for
t being
State of
SCMPDS st
f . (Dstate t) = 0 holds
t . (DataLoc (s . a),i) <= 0 ) & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) > 0 holds
(
(IExec I,t) . a = t . a &
I is_closed_on t &
I is_halting_on t &
f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x = t . x ) ) ) holds
(
while>0 a,
i,
I is_closed_on s &
while>0 a,
i,
I is_halting_on s & (
s . (DataLoc (s . a),i) > 0 implies
IExec (while>0 a,i,I),
s = IExec (while>0 a,i,I),
(IExec I,s) ) )
theorem Th27:
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i,
c being
Integer for
X,
Y being
set st
card I > 0 & ( for
x being
Int_position st
x in X holds
s . x >= c + (s . (DataLoc (s . a),i)) ) & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x >= c + (t . (DataLoc (s . a),i)) ) & ( for
x being
Int_position st
x in Y holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) > 0 holds
(
(IExec I,t) . a = t . a &
I is_closed_on t &
I is_halting_on t &
(IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for
x being
Int_position st
x in Y holds
(IExec I,t) . x = t . x ) ) ) holds
(
while>0 a,
i,
I is_closed_on s &
while>0 a,
i,
I is_halting_on s & (
s . (DataLoc (s . a),i) > 0 implies
IExec (while>0 a,i,I),
s = IExec (while>0 a,i,I),
(IExec I,s) ) )
theorem
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i being
Integer for
X being
set st
card I > 0 & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a &
t . (DataLoc (s . a),i) > 0 holds
(
(IExec I,t) . a = t . a &
I is_closed_on t &
I is_halting_on t &
(IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x = t . x ) ) ) holds
(
while>0 a,
i,
I is_closed_on s &
while>0 a,
i,
I is_halting_on s & (
s . (DataLoc (s . a),i) > 0 implies
IExec (while>0 a,i,I),
s = IExec (while>0 a,i,I),
(IExec I,s) ) )
theorem
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a being
Int_position for
i,
c being
Integer for
X being
set st
card I > 0 & ( for
x being
Int_position st
x in X holds
s . x >= c + (s . (DataLoc (s . a),i)) ) & ( for
t being
State of
SCMPDS st ( for
x being
Int_position st
x in X holds
t . x >= c + (t . (DataLoc (s . a),i)) ) &
t . a = s . a &
t . (DataLoc (s . a),i) > 0 holds
(
(IExec I,t) . a = t . a &
I is_closed_on t &
I is_halting_on t &
(IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & ( for
x being
Int_position st
x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) ) ) holds
(
while>0 a,
i,
I is_closed_on s &
while>0 a,
i,
I is_halting_on s & (
s . (DataLoc (s . a),i) > 0 implies
IExec (while>0 a,i,I),
s = IExec (while>0 a,i,I),
(IExec I,s) ) )