begin
:: deftheorem Def1 defines is_FinSequence_on SCPISORT:def 1 :
Lm1:
for f being FinSequence of INT
for k being Element of NAT holds f is_non_decreasing_on k,k
theorem Th1:
theorem Th2:
theorem
theorem Th4:
set A = NAT ;
set D = SCM-Data-Loc ;
theorem Th5:
theorem Th6:
theorem
theorem
theorem
theorem
theorem
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-down a,i,n,I)) = (card I) + 4
Lm3:
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 = (a,i <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo a,i,(- n))) ';' (goto (- ((card I) + 2))))
Lm4:
for I being Program of
for a being Int_position
for i being Integer
for n being Element of NAT holds Shift (I ';' (AddTo a,i,(- n))),1 c= for-down a,i,n,I
begin
scheme
ForDownHalt{
P1[
set ],
F1()
-> State of ,
F2()
-> shiftable No-StopCode Program of ,
F3()
-> Int_position ,
F4()
-> Integer,
F5()
-> Element of
NAT } :
provided
A1:
F5()
> 0
and A2:
P1[
Dstate F1()]
and A3:
for
t being
State of st
P1[
Dstate t] &
t . F3()
= F1()
. F3() &
t . (DataLoc (F1() . F3()),F4()) > 0 holds
(
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3()
= t . F3() &
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc (F1() . F3()),F4()) = (t . (DataLoc (F1() . F3()),F4())) - F5() &
F2()
is_closed_on t &
F2()
is_halting_on t &
P1[
Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] )
scheme
ForDownExec{
P1[
set ],
F1()
-> State of ,
F2()
-> shiftable No-StopCode Program of ,
F3()
-> Int_position ,
F4()
-> Integer,
F5()
-> Element of
NAT } :
( (
P1[
F1()] or not
P1[
F1()] ) &
IExec (for-down F3(),F4(),F5(),F2()),
F1()
= IExec (for-down F3(),F4(),F5(),F2()),
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) )
provided
A1:
F5()
> 0
and A2:
F1()
. (DataLoc (F1() . F3()),F4()) > 0
and A3:
P1[
Dstate F1()]
and A4:
for
t being
State of st
P1[
Dstate t] &
t . F3()
= F1()
. F3() &
t . (DataLoc (F1() . F3()),F4()) > 0 holds
(
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3()
= t . F3() &
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc (F1() . F3()),F4()) = (t . (DataLoc (F1() . F3()),F4())) - F5() &
F2()
is_closed_on t &
F2()
is_halting_on t &
P1[
Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] )
scheme
ForDownEnd{
P1[
set ],
F1()
-> State of ,
F2()
-> shiftable No-StopCode Program of ,
F3()
-> Int_position ,
F4()
-> Integer,
F5()
-> Element of
NAT } :
provided
A1:
F5()
> 0
and A2:
P1[
Dstate F1()]
and A3:
for
t being
State of st
P1[
Dstate t] &
t . F3()
= F1()
. F3() &
t . (DataLoc (F1() . F3()),F4()) > 0 holds
(
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3()
= t . F3() &
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc (F1() . F3()),F4()) = (t . (DataLoc (F1() . F3()),F4())) - F5() &
F2()
is_closed_on t &
F2()
is_halting_on t &
P1[
Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] )
theorem Th12:
for
s being
State of
for
I being
shiftable No-StopCode Program of
for
a,
x,
y being
Int_position for
i,
c being
Integer for
n being
Element of
NAT st
n > 0 &
s . x >= (s . y) + c & ( for
t being
State of st
t . x >= (t . y) + c &
t . a = s . a &
t . (DataLoc (s . a),i) > 0 holds
(
(IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a &
(IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n &
I is_closed_on t &
I is_halting_on t &
(IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
(
for-down a,
i,
n,
I is_closed_on s &
for-down a,
i,
n,
I is_halting_on s )
theorem Th13:
for
s being
State of
for
I being
shiftable No-StopCode Program of
for
a,
x,
y being
Int_position for
i,
c being
Integer for
n being
Element of
NAT st
n > 0 &
s . x >= (s . y) + c &
s . (DataLoc (s . a),i) > 0 & ( for
t being
State of st
t . x >= (t . y) + c &
t . a = s . a &
t . (DataLoc (s . a),i) > 0 holds
(
(IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a &
(IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n &
I is_closed_on t &
I is_halting_on t &
(IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
IExec (for-down a,i,n,I),
s = IExec (for-down a,i,n,I),
(IExec (I ';' (AddTo a,i,(- n))),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 st
s . (DataLoc (s . a),i) > 0 &
n > 0 &
card I > 0 &
a <> DataLoc (s . a),
i & ( for
t being
State of st
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 ) ) holds
(
for-down a,
i,
n,
I is_closed_on s &
for-down a,
i,
n,
I is_halting_on s )
begin
definition
let n,
p0 be
Element of
NAT ;
func insert-sort n,
p0 -> Program of
equals
((((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := p0)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))));
coherence
((((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := p0)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))))) is Program of
;
end;
:: deftheorem defines insert-sort SCPISORT:def 2 :
for
n,
p0 being
Element of
NAT holds
insert-sort n,
p0 = ((((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := p0)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))));
set j1 = AddTo GBP ,3,1;
set j2 = GBP ,4 := GBP ,3;
set j3 = AddTo GBP ,1,1;
set j4 = GBP ,6 := GBP ,1;
set k1 = GBP ,5 := (intpos 4),(- 1);
set k2 = SubFrom GBP ,5,(intpos 4),0 ;
set k3 = GBP ,5 := (intpos 4),(- 1);
set k4 = (intpos 4),(- 1) := (intpos 4),0 ;
set k5 = (intpos 4),0 := GBP ,5;
set k6 = AddTo GBP ,4,(- 1);
set k7 = AddTo GBP ,6,(- 1);
set FA = Load (GBP ,6 := 0 );
set TR = ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1));
set IF = if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ));
set B1 = ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )));
set WH = while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))));
set J4 = (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1);
set B2 = ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))));
set FR = for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))));
Lm5:
card (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))) = 10
Lm6:
card (((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) = 16
set a1 = intpos 1;
set a2 = intpos 2;
set a3 = intpos 3;
set a4 = intpos 4;
set a5 = intpos 5;
set a6 = intpos 6;
Lm7:
for s being State of st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 holds
( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . GBP = 0 & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 1) = s . (intpos 1) )
Lm8:
for s being State of st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 holds
( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 2) = s . (intpos 2) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 3) = s . (intpos 3) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 6) < s . (intpos 6) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 4) >= 7 + ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc (s . (intpos 4)),(- 1)) > s . (DataLoc (s . (intpos 4)),0 ) implies ( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),0 ) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (DataLoc (s . (intpos 4)),0 ) = s . (DataLoc (s . (intpos 4)),(- 1)) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc (s . (intpos 4)),(- 1)) <= s . (DataLoc (s . (intpos 4)),0 ) implies ( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),(- 1)) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (DataLoc (s . (intpos 4)),0 ) = s . (DataLoc (s . (intpos 4)),0 ) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s) . (intpos 6) = 0 ) ) )
Lm9:
for s being State of st s . (intpos 4) >= 7 + (s . (DataLoc (s . GBP ),6)) & s . GBP = 0 holds
( while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))) is_closed_on s & while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))) is_halting_on s )
Lm10:
for s being State of st s . (intpos 4) >= 7 + (s . (DataLoc (s . GBP ),6)) & s . GBP = 0 holds
( (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s) . GBP = 0 & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s) . (intpos 1) = s . (intpos 1) & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s) . (intpos 2) = s . (intpos 2) & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s) . (intpos 3) = s . (intpos 3) )
Lm11:
for s being State of st s . GBP = 0 holds
( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . GBP = 0 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) )
set jf = AddTo GBP ,2,(- 1);
set B3 = (((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) ';' (AddTo GBP ,2,(- 1));
Lm12:
for s being State of st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . GBP = 0 holds
( (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) ';' (AddTo GBP ,2,(- 1))),s) . GBP = 0 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 2) = (s . (intpos 2)) - 1 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 1) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i <> 2 holds
(IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) ';' (AddTo GBP ,2,(- 1))),s) . (intpos i) = (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s)) . (intpos i) ) )
Lm13:
for s being State of st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . GBP = 0 holds
( for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) is_closed_on s & for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) is_halting_on s )
Lm14:
for s being State of st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . GBP = 0 & s . (intpos 2) > 0 holds
IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))))),s = IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))))),(IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))))) ';' (AddTo GBP ,2,(- 1))),s)
begin
theorem
theorem
Lm15:
for s being State of st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 holds
IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s = IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),s)
theorem Th17:
for
s being
State of
for
f,
g being
FinSequence of
INT for
k0,
k being
Element of
NAT st
s . (intpos 4) >= 7
+ (s . (intpos 6)) &
s . GBP = 0 &
k = s . (intpos 6) &
k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 &
f is_FinSequence_on s,
k0 &
g is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),
s,
k0 &
len f = len g &
len f > k &
f is_non_decreasing_on 1,
k holds
(
f,
g are_fiberwise_equipotent &
g is_non_decreasing_on 1,
k + 1 & ( for
i being
Element of
NAT st
i > k + 1 &
i <= len f holds
f . i = g . i ) & ( for
i being
Element of
NAT st 1
<= i &
i <= k + 1 holds
ex
j being
Element of
NAT st
( 1
<= j &
j <= k + 1 &
g . i = f . j ) ) )
Lm16:
for s being State of
for f, g being FinSequence of INT
for p0, n being Element of NAT st s . GBP = 0 & s . (intpos 2) = n - 1 & s . (intpos 3) = p0 + 1 & s . (intpos 1) = 0 & p0 >= 6 & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))))),s,p0 & len f = n & len g = n holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
theorem