begin
set A = NAT ;
set D = SCM-Data-Loc ;
theorem Th1:
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem
canceled;
theorem
theorem Th10:
theorem
theorem Th12:
theorem
canceled;
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem
theorem
canceled;
theorem Th23:
theorem Th24:
for
s1,
s2 being
State of
SCMPDS for
I being
Program of
SCMPDS st
I is_closed_on s1 &
Initialize (stop I) c= s1 &
Initialize (stop I) c= s2 &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
IC (Comput (ProgramPart s1),s1,i) = IC (Comput (ProgramPart s2),s2,i) &
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem Th25:
for
s1,
s2 being
State of
SCMPDS for
I being
Program of
SCMPDS st
I is_closed_on s1 &
DataPart s1 = DataPart s2 holds
for
k being
Element of
NAT holds
(
Comput (ProgramPart ((Initialize s1) +* (stop I))),
((Initialize s1) +* (stop I)),
k,
Comput (ProgramPart ((Initialize s2) +* (stop I))),
((Initialize s2) +* (stop I)),
k equal_outside NAT &
CurInstr (ProgramPart ((Initialize s1) +* (stop I))),
(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k) = CurInstr (ProgramPart ((Initialize s2) +* (stop I))),
(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) )
theorem Th26:
for
s1,
s2 being
State of
SCMPDS for
I being
Program of
SCMPDS st
I is_closed_on s1 &
Initialize (stop I) c= s1 &
Initialize (stop I) c= s2 &
s1,
s2 equal_outside NAT holds
for
k being
Element of
NAT holds
(
Comput (ProgramPart s1),
s1,
k,
Comput (ProgramPart s2),
s2,
k equal_outside NAT &
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,k) )
theorem
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem
theorem Th33:
theorem Th34:
for
s1,
s2 being
State of
SCMPDS for
I being
shiftable Program of
SCMPDS st
Initialize (stop I) c= s1 &
I is_closed_on s1 &
I is_halting_on s1 holds
for
n being
Element of
NAT st
Shift I,
n c= s2 &
card I > 0 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT st
i < LifeSpan (ProgramPart s1),
s1 holds
(
(IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem Th35:
theorem Th36:
for
s1,
s2 being
State of
SCMPDS for
I being
halt-free shiftable Program of
SCMPDS st
Initialize (stop I) c= s1 &
I is_closed_on s1 &
I is_halting_on s1 holds
for
n being
Element of
NAT st
Shift I,
n c= s2 &
card I > 0 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
(
IC (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = (card I) + n &
DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1)) = DataPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) )
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
for
s being
State of
SCMPDS for
I,
J being
Program of
SCMPDS st
I c= J &
I is_closed_on s &
I is_halting_on s & not
CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))),
(Comput (ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = halt SCMPDS holds
IC (Comput (ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem Th46:
Lm1:
for I being halt-free Program of SCMPDS
for J being shiftable Program of SCMPDS
for s, s1, s2 being State of SCMPDS 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 = (Initialize s) +* (stop (I ';' J)) & s1 = (Initialize s) +* (stop I) holds
( IC (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = card I & DataPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) & Shift (stop J),(card I) c= Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) & LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) )
theorem
theorem Th48:
theorem Th49:
theorem Th50:
begin
:: deftheorem defines for-up SCMPDS_7:def 1 :
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 = (((a,i >=0_goto ((card I) + 3)) ';' I) ';' (AddTo a,i,n)) ';' (goto (- ((card I) + 2)));
begin
theorem Th51:
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 Th52:
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)) )
theorem Th54:
theorem Th55:
theorem
theorem
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
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 &
card I > 0 &
a <> DataLoc (s . a),
i & ( 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 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
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 &
card I > 0 &
a <> DataLoc (s . a),
i & ( 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 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 :
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 = (((a,i <=0_goto ((card I) + 3)) ';' I) ';' (AddTo a,i,(- n))) ';' (goto (- ((card I) + 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 SCMPDS 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
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)) )
theorem Th63:
theorem Th64:
theorem
theorem Th66:
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
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 &
card I > 0 &
a <> DataLoc (s . a),
i & ( 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 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
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 &
card I > 0 &
a <> DataLoc (s . a),
i & ( 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 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
SCMPDS 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 SCMPDS
;
end;
:: deftheorem defines sum SCMPDS_7:def 3 :
for n being Element of NAT holds sum n = (((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )) ';' (for-down GBP ,2,1,(Load (AddTo GBP ,3,1)));
theorem Th69:
for
s being
State of
SCMPDS 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
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
s being
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 &
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
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))),s) . (DataLoc (s . (intpos sp)),result) = Sum f
theorem
for
s being
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),s) . (DataLoc (s . (intpos sp)),result) = Sum f