begin
set A = NAT ;
set D = SCM-Data-Loc ;
begin
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
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)
scheme
WhileLHalt{
F1(
State of
SCMPDS)
-> Element of
NAT ,
F2()
-> 0 -started State of
SCMPDS,
F3()
-> Instruction-Sequence of
SCMPDS,
F4()
-> halt-free shiftable Program of
SCMPDS,
F5()
-> Int_position,
F6()
-> Integer,
P1[
State of
SCMPDS] } :
provided
A2:
for
t being
0 -started State of
SCMPDS st
P1[
t] &
F1(
t)
= 0 holds
t . (DataLoc ((F2() . F5()),F6())) >= 0
and A3:
P1[
F2()]
and A4:
for
t being
0 -started State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st
P1[
t] &
t . F5()
= F2()
. F5() &
t . (DataLoc ((F2() . F5()),F6())) < 0 holds
(
(IExec (F4(),Q,t)) . F5()
= t . F5() &
F4()
is_closed_on t,
Q &
F4()
is_halting_on t,
Q &
F1(
(Initialize (IExec (F4(),Q,t))))
< F1(
t) &
P1[
Initialize (IExec (F4(),Q,t))] )
scheme
WhileLExec{
F1(
State of
SCMPDS)
-> Element of
NAT ,
F2()
-> 0 -started State of
SCMPDS,
F3()
-> Instruction-Sequence of
SCMPDS,
F4()
-> halt-free shiftable Program of
SCMPDS,
F5()
-> Int_position,
F6()
-> Integer,
P1[
State of
SCMPDS] } :
IExec (
(while<0 (F5(),F6(),F4())),
F3(),
F2())
= IExec (
(while<0 (F5(),F6(),F4())),
F3(),
(Initialize (IExec (F4(),F3(),F2()))))
provided
A2:
F2()
. (DataLoc ((F2() . F5()),F6())) < 0
and A3:
for
t being
0 -started State of
SCMPDS st
P1[
t] &
F1(
t)
= 0 holds
t . (DataLoc ((F2() . F5()),F6())) >= 0
and A4:
P1[
F2()]
and A5:
for
t being
0 -started State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st
P1[
t] &
t . F5()
= F2()
. F5() &
t . (DataLoc ((F2() . F5()),F6())) < 0 holds
(
(IExec (F4(),Q,t)) . F5()
= t . F5() &
F4()
is_closed_on t,
Q &
F4()
is_halting_on t,
Q &
F1(
(Initialize (IExec (F4(),Q,t))))
< F1(
t) &
P1[
Initialize (IExec (F4(),Q,t))] )
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
X being
set for
f being
Function of
(product (the_Values_of SCMPDS)),
NAT st ( for
t being
0 -started State of
SCMPDS st
f . t = 0 holds
t . (DataLoc ((s . a),i)) >= 0 ) & ( 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 &
t . (DataLoc ((s . a),i)) < 0 holds
(
(IExec (I,Q,t)) . a = t . a &
f . (Initialize (IExec (I,Q,t))) < f . t &
I is_closed_on t,
Q &
I is_halting_on t,
Q & ( for
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
(
while<0 (
a,
i,
I)
is_closed_on s,
P &
while<0 (
a,
i,
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
X being
set for
f being
Function of
(product (the_Values_of SCMPDS)),
NAT st
s . (DataLoc ((s . a),i)) < 0 & ( for
t being
0 -started State of
SCMPDS st
f . t = 0 holds
t . (DataLoc ((s . a),i)) >= 0 ) & ( 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 &
t . (DataLoc ((s . a),i)) < 0 holds
(
(IExec (I,Q,t)) . a = t . a &
I is_closed_on t,
Q &
I is_halting_on t,
Q &
f . (Initialize (IExec (I,Q,t))) < f . t & ( for
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
IExec (
(while<0 (a,i,I)),
P,
s)
= IExec (
(while<0 (a,i,I)),
P,
(Initialize (IExec (I,P,s))))
theorem Th15:
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
X being
set st ( 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 &
t . (DataLoc ((s . a),i)) < 0 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
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
(
while<0 (
a,
i,
I)
is_closed_on s,
P &
while<0 (
a,
i,
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
X being
set st
s . (DataLoc ((s . a),i)) < 0 & ( 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 &
t . (DataLoc ((s . a),i)) < 0 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
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
IExec (
(while<0 (a,i,I)),
P,
s)
= IExec (
(while<0 (a,i,I)),
P,
(Initialize (IExec (I,P,s))))
begin
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
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)
scheme
WhileGHalt{
F1(
State of
SCMPDS)
-> Element of
NAT ,
F2()
-> 0 -started State of
SCMPDS,
F3()
-> Instruction-Sequence of
SCMPDS,
F4()
-> halt-free shiftable Program of
SCMPDS,
F5()
-> Int_position,
F6()
-> Integer,
P1[
State of
SCMPDS] } :
provided
A2:
for
t being
0 -started State of
SCMPDS st
P1[
t] &
F1(
t)
= 0 holds
t . (DataLoc ((F2() . F5()),F6())) <= 0
and A3:
P1[
F2()]
and A4:
for
t being
0 -started State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st
P1[
t] &
t . F5()
= F2()
. F5() &
t . (DataLoc ((F2() . F5()),F6())) > 0 holds
(
(IExec (F4(),Q,t)) . F5()
= t . F5() &
F4()
is_closed_on t,
Q &
F4()
is_halting_on t,
Q &
F1(
(Initialize (IExec (F4(),Q,t))))
< F1(
t) &
P1[
Initialize (IExec (F4(),Q,t))] )
scheme
WhileGExec{
F1(
State of
SCMPDS)
-> Element of
NAT ,
F2()
-> 0 -started State of
SCMPDS,
F3()
-> Instruction-Sequence of
SCMPDS,
F4()
-> halt-free shiftable Program of
SCMPDS,
F5()
-> Int_position,
F6()
-> Integer,
P1[
State of
SCMPDS] } :
IExec (
(while>0 (F5(),F6(),F4())),
F3(),
F2())
= IExec (
(while>0 (F5(),F6(),F4())),
F3(),
(Initialize (IExec (F4(),F3(),F2()))))
provided
A2:
F2()
. (DataLoc ((F2() . F5()),F6())) > 0
and A3:
for
t being
0 -started State of
SCMPDS st
P1[
t] &
F1(
t)
= 0 holds
t . (DataLoc ((F2() . F5()),F6())) <= 0
and A4:
P1[
F2()]
and A5:
for
t being
0 -started State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st
P1[
t] &
t . F5()
= F2()
. F5() &
t . (DataLoc ((F2() . F5()),F6())) > 0 holds
(
(IExec (F4(),Q,t)) . F5()
= t . F5() &
F4()
is_closed_on t,
Q &
F4()
is_halting_on t,
Q &
F1(
(Initialize (IExec (F4(),Q,t))))
< F1(
t) &
P1[
Initialize (IExec (F4(),Q,t))] )
theorem Th24:
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,
c being
Integer for
X,
Y being
set for
f being
Function of
(product (the_Values_of SCMPDS)),
NAT st ( for
t being
0 -started State of
SCMPDS st
f . 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
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 >= 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,Q,t)) . a = t . a &
I is_closed_on t,
Q &
I is_halting_on t,
Q &
f . (Initialize (IExec (I,Q,t))) < f . t & ( for
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for
x being
Int_position st
x in Y holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
(
while>0 (
a,
i,
I)
is_closed_on s,
P &
while>0 (
a,
i,
I)
is_halting_on s,
P )
theorem Th25:
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,
c being
Integer for
X,
Y being
set for
f being
Function of
(product (the_Values_of SCMPDS)),
NAT st
s . (DataLoc ((s . a),i)) > 0 & ( for
t being
0 -started State of
SCMPDS st
f . 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
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 >= 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,Q,t)) . a = t . a &
I is_closed_on t,
Q &
I is_halting_on t,
Q &
f . (Initialize (IExec (I,Q,t))) < f . t & ( for
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for
x being
Int_position st
x in Y holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
IExec (
(while>0 (a,i,I)),
P,
s)
= IExec (
(while>0 (a,i,I)),
P,
(Initialize (IExec (I,P,s))))
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
X being
set for
f being
Function of
(product (the_Values_of SCMPDS)),
NAT st ( for
t being
0 -started State of
SCMPDS st
f . t = 0 holds
t . (DataLoc ((s . a),i)) <= 0 ) & ( 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 &
t . (DataLoc ((s . a),i)) > 0 holds
(
(IExec (I,Q,t)) . a = t . a &
I is_closed_on t,
Q &
I is_halting_on t,
Q &
f . (Initialize (IExec (I,Q,t))) < f . t & ( for
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
(
while>0 (
a,
i,
I)
is_closed_on s,
P &
while>0 (
a,
i,
I)
is_halting_on s,
P & (
s . (DataLoc ((s . a),i)) > 0 implies
IExec (
(while>0 (a,i,I)),
P,
s)
= IExec (
(while>0 (a,i,I)),
P,
(Initialize (IExec (I,P,s)))) ) )
theorem Th27:
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,
c being
Integer for
X,
Y being
set st ( for
x being
Int_position st
x in X holds
s . x >= c + (s . (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 >= 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,Q,t)) . a = t . a &
I is_closed_on t,
Q &
I is_halting_on t,
Q &
(IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for
x being
Int_position st
x in Y holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
(
while>0 (
a,
i,
I)
is_closed_on s,
P &
while>0 (
a,
i,
I)
is_halting_on s,
P & (
s . (DataLoc ((s . a),i)) > 0 implies
IExec (
(while>0 (a,i,I)),
P,
s)
= IExec (
(while>0 (a,i,I)),
P,
(Initialize (IExec (I,P,s)))) ) )
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
X being
set st ( 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 &
t . (DataLoc ((s . a),i)) > 0 holds
(
(IExec (I,Q,t)) . a = t . a &
I is_closed_on t,
Q &
I is_halting_on t,
Q &
(IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
(
while>0 (
a,
i,
I)
is_closed_on s,
P &
while>0 (
a,
i,
I)
is_halting_on s,
P & (
s . (DataLoc ((s . a),i)) > 0 implies
IExec (
(while>0 (a,i,I)),
P,
s)
= IExec (
(while>0 (a,i,I)),
P,
(Initialize (IExec (I,P,s)))) ) )
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,
c being
Integer for
X being
set st ( for
x being
Int_position st
x in X holds
s . x >= c + (s . (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 >= c + (t . (DataLoc ((s . a),i))) ) &
t . a = s . a &
t . (DataLoc ((s . a),i)) > 0 holds
(
(IExec (I,Q,t)) . a = t . a &
I is_closed_on t,
Q &
I is_halting_on t,
Q &
(IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for
x being
Int_position st
x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds
(
while>0 (
a,
i,
I)
is_closed_on s,
P &
while>0 (
a,
i,
I)
is_halting_on s,
P & (
s . (DataLoc ((s . a),i)) > 0 implies
IExec (
(while>0 (a,i,I)),
P,
s)
= IExec (
(while>0 (a,i,I)),
P,
(Initialize (IExec (I,P,s)))) ) )