begin
set A = NAT ;
set D = SCM-Data-Loc ;
theorem Th1:
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem
theorem Th12:
theorem
canceled;
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem
theorem
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem Th46:
Lm1:
for I being No-StopCode Program of
for J being shiftable Program of
for s, s1, s2 being State of st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s & s2 = s +* (Initialized (stop (I ';' J))) & s1 = s +* (Initialized (stop I)) holds
( IC (Computation s2,(LifeSpan s1)) = inspos (card I) & DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) & LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
theorem
theorem Th48:
theorem Th49:
theorem Th50:
begin
:: deftheorem defines for-up SCMPDS_7:def 1 :
begin
theorem Th51:
Lm2:
for a being Int_position
for i being Integer
for n being Element of NAT
for I being Program of holds card (stop (for-up a,i,n,I)) = (card I) + 4
theorem Th52:
theorem Th53:
for
a being
Int_position for
i being
Integer for
n being
Element of
NAT for
I being
Program of holds
(
(for-up a,i,n,I) . (inspos 0 ) = a,
i >=0_goto ((card I) + 3) &
(for-up a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,
i,
n &
(for-up a,i,n,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2)) )
theorem Th54:
theorem Th55:
theorem
theorem
Lm3:
for I being Program of
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
s being
State of
for
I being
shiftable No-StopCode Program of
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 &
card I > 0 &
a <> DataLoc (s . a),
i & ( for
t being
State of st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a 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
y being
Int_position st
y in X holds
(IExec I,t) . y = t . y ) ) ) holds
(
for-up a,
i,
n,
I is_closed_on s &
for-up a,
i,
n,
I is_halting_on s )
theorem
for
s being
State of
for
I being
shiftable No-StopCode Program of
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 &
card I > 0 &
a <> DataLoc (s . a),
i & ( for
t being
State of st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a 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
y being
Int_position st
y in X holds
(IExec I,t) . y = t . y ) ) ) holds
IExec (for-up a,i,n,I),
s = IExec (for-up a,i,n,I),
(IExec (I ';' (AddTo a,i,n)),s)
begin
:: deftheorem defines for-down SCMPDS_7:def 2 :
begin
theorem Th60:
Lm4:
for a being Int_position
for i being Integer
for n being Element of NAT
for I being Program of holds card (stop (for-down a,i,n,I)) = (card I) + 4
theorem Th61:
theorem Th62:
for
a being
Int_position for
i being
Integer for
n being
Element of
NAT for
I being
Program of holds
(
(for-down a,i,n,I) . (inspos 0 ) = a,
i <=0_goto ((card I) + 3) &
(for-down a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,
i,
(- n) &
(for-down a,i,n,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2)) )
theorem Th63:
theorem Th64:
theorem
theorem Th66:
Lm5:
for I being Program of
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
s being
State of
for
I being
shiftable No-StopCode Program of
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 &
card I > 0 &
a <> DataLoc (s . a),
i & ( for
t being
State of st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a 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
y being
Int_position st
y in X holds
(IExec I,t) . y = t . y ) ) ) holds
(
for-down a,
i,
n,
I is_closed_on s &
for-down a,
i,
n,
I is_halting_on s )
theorem Th68:
for
s being
State of
for
I being
shiftable No-StopCode Program of
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 &
card I > 0 &
a <> DataLoc (s . a),
i & ( for
t being
State of st ( for
x being
Int_position st
x in X holds
t . x = s . x ) &
t . a = s . a 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
y being
Int_position st
y in X holds
(IExec I,t) . y = t . y ) ) ) holds
IExec (for-down a,i,n,I),
s = IExec (for-down a,i,n,I),
(IExec (I ';' (AddTo a,i,(- n))),s)
begin
definition
let n be
Element of
NAT ;
func sum n -> Program of
equals
(((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )) ';' (for-down GBP ,2,1,(Load (AddTo GBP ,3,1)));
coherence
(((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )) ';' (for-down GBP ,2,1,(Load (AddTo GBP ,3,1))) is Program of
;
end;
:: deftheorem defines sum SCMPDS_7:def 3 :
theorem Th69:
for
s being
State of st
s . GBP = 0 holds
(
for-down GBP ,2,1,
(Load (AddTo GBP ,3,1)) is_closed_on s &
for-down GBP ,2,1,
(Load (AddTo GBP ,3,1)) is_halting_on s )
theorem Th70:
theorem
definition
let sp,
control,
result,
pp,
pData be
Element of
NAT ;
func sum sp,
control,
result,
pp,
pData -> Program of
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
;
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
s being
State of
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 &
for-down (intpos sp),
cv,1,
((AddTo (intpos sp),result,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) is_halting_on s )
theorem Th73:
for
s being
State of
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))),s) . (DataLoc (s . (intpos sp)),result) = Sum f
theorem
for
s being
State of
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),s) . (DataLoc (s . (intpos sp)),result) = Sum f