:: Quick Sort on SCMPDS
:: by JingChao Chen
::
:: Received June 14, 2000
:: Copyright (c) 2000 Association of Mizar Users
Lm1:
for s being State of SCMPDS
for I, J being shiftable Program of SCMPDS
for n being Element of NAT holds (I ';' (Goto n)) ';' J is shiftable
theorem Th1: :: SCPQSORT:1
set A = NAT ;
set D = SCM-Data-Loc ;
Lm2:
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
Lm3:
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 Th2: :: SCPQSORT:2
theorem Th3: :: SCPQSORT:3
theorem Th4: :: SCPQSORT:4
theorem Th5: :: SCPQSORT:5
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a,
x,
y being
Int_position for
i,
c being
Integer st
card I > 0 &
s . x >= c + (s . (DataLoc (s . a),i)) & ( for
t being
State of
SCMPDS st
t . x >= c + (t . (DataLoc (s . a),i)) &
t . y = s . y &
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) &
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) &
(IExec I,t) . y = t . y ) ) 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 Th6: :: SCPQSORT:6
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a,
x,
y being
Int_position for
i,
c being
Integer st
card I > 0 &
s . x >= c & ( for
t being
State of
SCMPDS st
t . x >= c &
t . y = s . y &
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) &
(IExec I,t) . x >= c &
(IExec I,t) . y = t . y ) ) 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 Th7: :: SCPQSORT:7
for
s being
State of
SCMPDS for
I being
shiftable No-StopCode Program of
SCMPDS for
a,
x1,
x2,
x3,
x4 being
Int_position for
i,
c,
md being
Integer st
card I > 0 &
s . x4 = ((s . x3) - c) + (s . x1) &
md <= (s . x3) - c & ( for
t being
State of
SCMPDS st
t . x4 = ((t . x3) - c) + (t . x1) &
md <= (t . x3) - c &
t . x2 = s . x2 &
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) &
(IExec I,t) . x4 = (((IExec I,t) . x3) - c) + ((IExec I,t) . x1) &
md <= ((IExec I,t) . x3) - c &
(IExec I,t) . x2 = t . x2 ) ) 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 Th8: :: SCPQSORT:8
Lm4:
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 f, g being FinSequence of INT
for m, n, m1 being Element of NAT st card I > 0 & s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec (while>0 a,i,I),s,m & 1 = s . (DataLoc c,i) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc c,i) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec I,t) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec I,t) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec I,t) . (DataLoc c,i) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec I,t) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec I,t) . (DataLoc c,i) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec I,t) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec I,t) . (intpos k2) & (m + ym) - 1 = (IExec I,t) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec I,t) . (intpos (k2 + 2)) & m + yn = (IExec I,t) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec I,t) . (intpos (m + j)) <= (IExec I,t) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec I,t) . (intpos (m + j)) >= (IExec I,t) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec I,t,m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 a,i,I is_halting_on s & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
Lm5:
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 m, n, m1 being Element of NAT st card I > 0 & s . a = c & 1 = s . (DataLoc c,i) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc c,i) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec I,t) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec I,t) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec I,t) . (DataLoc c,i) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec I,t) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec I,t) . (DataLoc c,i) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec I,t) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec I,t) . (intpos k2) & (m + ym) - 1 = (IExec I,t) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec I,t) . (intpos (k2 + 2)) & m + yn = (IExec I,t) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec I,t) . (intpos (m + j)) <= (IExec I,t) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec I,t) . (intpos (m + j)) >= (IExec I,t) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec I,t,m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
while>0 a,i,I is_halting_on s
Lm6:
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 m, n, m1 being Element of NAT st card I > 0 & s . a = c & 1 = s . (DataLoc c,i) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc c,i) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec I,t) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec I,t) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec I,t) . (DataLoc c,i) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec I,t) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec I,t) . (DataLoc c,i) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec I,t) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec I,t) . (intpos k2) & (m + ym) - 1 = (IExec I,t) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec I,t) . (intpos (k2 + 2)) & m + yn = (IExec I,t) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec I,t) . (intpos (m + j)) <= (IExec I,t) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec I,t) . (intpos (m + j)) >= (IExec I,t) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec I,t,m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 a,i,I is_halting_on s & while>0 a,i,I is_closed_on s )
definition
func Partition -> Program of
SCMPDS equals :: SCPQSORT:def 1
(((((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)) ';' (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))))) ';' (GBP ,6 := (intpos 4),0 )) ';' ((intpos 4),0 := (intpos 2),0 )) ';' ((intpos 2),0 := GBP ,6);
coherence
(((((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)) ';' (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))))) ';' (GBP ,6 := (intpos 4),0 )) ';' ((intpos 4),0 := (intpos 2),0 )) ';' ((intpos 2),0 := GBP ,6) is Program of SCMPDS
;
end;
:: deftheorem defines Partition SCPQSORT:def 1 :
Partition = (((((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)) ';' (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))))) ';' (GBP ,6 := (intpos 4),0 )) ';' ((intpos 4),0 := (intpos 2),0 )) ';' ((intpos 2),0 := GBP ,6);
definition
let n,
p0 be
Element of
NAT ;
func QuickSort n,
p0 -> Program of
SCMPDS equals :: SCPQSORT:def 2
((((GBP := 0 ) ';' (SBP := 1)) ';' (SBP ,(p0 + n) := (p0 + 1))) ';' (SBP ,((p0 + n) + 1) := (p0 + n))) ';' (while>0 GBP ,1,(((GBP ,2 := SBP ,((p0 + n) + 1)) ';' (SubFrom GBP ,2,SBP ,(p0 + n))) ';' (if>0 GBP ,2,((((GBP ,2 := SBP ,(p0 + n)) ';' (GBP ,4 := SBP ,((p0 + n) + 1))) ';' Partition ) ';' ((((((SBP ,((p0 + n) + 3) := SBP ,((p0 + n) + 1)) ';' (SBP ,((p0 + n) + 1) := GBP ,4)) ';' (SBP ,((p0 + n) + 2) := GBP ,4)) ';' (AddTo SBP ,((p0 + n) + 1),(- 1))) ';' (AddTo SBP ,((p0 + n) + 2),1)) ';' (AddTo GBP ,1,2))),(Load (AddTo GBP ,1,(- 2))))));
coherence
((((GBP := 0 ) ';' (SBP := 1)) ';' (SBP ,(p0 + n) := (p0 + 1))) ';' (SBP ,((p0 + n) + 1) := (p0 + n))) ';' (while>0 GBP ,1,(((GBP ,2 := SBP ,((p0 + n) + 1)) ';' (SubFrom GBP ,2,SBP ,(p0 + n))) ';' (if>0 GBP ,2,((((GBP ,2 := SBP ,(p0 + n)) ';' (GBP ,4 := SBP ,((p0 + n) + 1))) ';' Partition ) ';' ((((((SBP ,((p0 + n) + 3) := SBP ,((p0 + n) + 1)) ';' (SBP ,((p0 + n) + 1) := GBP ,4)) ';' (SBP ,((p0 + n) + 2) := GBP ,4)) ';' (AddTo SBP ,((p0 + n) + 1),(- 1))) ';' (AddTo SBP ,((p0 + n) + 2),1)) ';' (AddTo GBP ,1,2))),(Load (AddTo GBP ,1,(- 2)))))) is Program of SCMPDS
;
end;
:: deftheorem defines QuickSort SCPQSORT:def 2 :
for
n,
p0 being
Element of
NAT holds
QuickSort n,
p0 = ((((GBP := 0 ) ';' (SBP := 1)) ';' (SBP ,(p0 + n) := (p0 + 1))) ';' (SBP ,((p0 + n) + 1) := (p0 + n))) ';' (while>0 GBP ,1,(((GBP ,2 := SBP ,((p0 + n) + 1)) ';' (SubFrom GBP ,2,SBP ,(p0 + n))) ';' (if>0 GBP ,2,((((GBP ,2 := SBP ,(p0 + n)) ';' (GBP ,4 := SBP ,((p0 + n) + 1))) ';' Partition ) ';' ((((((SBP ,((p0 + n) + 3) := SBP ,((p0 + n) + 1)) ';' (SBP ,((p0 + n) + 1) := GBP ,4)) ';' (SBP ,((p0 + n) + 2) := GBP ,4)) ';' (AddTo SBP ,((p0 + n) + 1),(- 1))) ';' (AddTo SBP ,((p0 + n) + 2),1)) ';' (AddTo GBP ,1,2))),(Load (AddTo GBP ,1,(- 2))))));
set i1 = GBP ,7 := GBP ,5;
set i2 = AddTo GBP ,5,(- 1);
set i3 = GBP ,6 := (intpos 4),0 ;
set i4 = SubFrom GBP ,6,(intpos 2),0 ;
set i5 = AddTo GBP ,4,(- 1);
set i6 = AddTo GBP ,7,(- 1);
set i7 = Load (GBP ,5 := 0 );
set IF1 = if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ));
set WB1 = ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )));
set WH1 = while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))));
set j1 = GBP ,5 := GBP ,7;
set j2 = AddTo GBP ,7,(- 1);
set j3 = GBP ,6 := (intpos 2),0 ;
set j4 = SubFrom GBP ,6,(intpos 3),0 ;
set j5 = AddTo GBP ,3,1;
set j6 = AddTo GBP ,5,(- 1);
set j7 = Load (GBP ,7 := 0 );
set IF2 = if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ));
set WB2 = ((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )));
set WH2 = while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))));
set k1 = GBP ,5 := GBP ,4;
set k2 = SubFrom GBP ,5,GBP ,2;
set k3 = GBP ,3 := GBP ,2;
set k4 = AddTo GBP ,3,1;
set K4 = (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1);
set k5 = GBP ,6 := (intpos 4),0 ;
set k6 = (intpos 4),0 := (intpos 3),0 ;
set k7 = (intpos 3),0 := GBP ,6;
set k8 = AddTo GBP ,5,(- 2);
set k9 = AddTo GBP ,3,1;
set k0 = AddTo GBP ,4,(- 1);
set IF3 = if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)));
set WB3 = ((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))));
set WH3 = while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))));
set j8 = GBP ,6 := (intpos 4),0 ;
set j9 = (intpos 4),0 := (intpos 2),0 ;
set j0 = (intpos 2),0 := GBP ,6;
set a1 = intpos 1;
set a2 = intpos 2;
set a3 = intpos 3;
set a4 = intpos 4;
set a5 = intpos 5;
set a6 = intpos 6;
set a7 = intpos 7;
Lm7:
card (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))) = 9
Lm8:
for s being State of SCMPDS
for md, me being Element of NAT st s . (intpos 2) = md & s . (intpos 4) = me & md >= 8 & me >= 8 & s . GBP = 0 & s . (intpos 5) > 0 holds
( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . GBP = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 1) = s . (intpos 1) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) & ( s . (intpos md) < s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = (s . (intpos 5)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1 ) ) & ( s . (intpos md) >= s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) ) ) )
Lm9:
for s being State of SCMPDS
for m4, md being Element of NAT st s . GBP = 0 & s . (intpos 5) > 0 & s . (intpos 4) = m4 + (s . (intpos 5)) & m4 >= 8 & s . (intpos 2) = md & md >= 8 holds
( (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . GBP = 0 & (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos 1) = s . (intpos 1) & (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos 5) = 0 & (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos 2) = s . (intpos 2) & (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos i) = s . (intpos i) ) & ex mE being Element of NAT st
( mE = (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos 7) & (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos 4) = m4 + mE & mE <= s . (intpos 5) & ( for i being Element of NAT st m4 + mE < i & i <= s . (intpos 4) holds
(IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos md) < (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos i) ) & ( mE = 0 or (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos md) >= (IExec (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))),s) . (intpos (m4 + mE)) ) ) )
Lm10:
for s being State of SCMPDS
for m4, md being Element of NAT st s . GBP = 0 & s . (intpos 5) > 0 & s . (intpos 4) = m4 + (s . (intpos 5)) & m4 >= 8 & s . (intpos 2) = md & md >= 8 holds
( while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))) is_closed_on s & while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))) is_halting_on s )
Lm11:
card (while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) = 11
Lm12:
card (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))) = 9
Lm13:
card (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))) = 11
Lm14:
for s being State of SCMPDS
for md, me being Element of NAT st s . (intpos 2) = md & s . (intpos 3) = me & md >= 8 & me >= 8 & s . GBP = 0 & s . (intpos 7) > 0 holds
( (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . GBP = 0 & (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 1) = s . (intpos 1) & (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 4) = s . (intpos 4) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos i) = s . (intpos i) ) & ( s . (intpos md) > s . (intpos me) implies ( (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 7) = (s . (intpos 7)) - 1 & (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 5) = (s . (intpos 7)) - 1 ) ) & ( s . (intpos md) <= s . (intpos me) implies ( (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 7) = 0 & (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 3) = s . (intpos 3) & (IExec (((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))),s) . (intpos 5) = s . (intpos 7) ) ) )
Lm15:
for s being State of SCMPDS
for m3, md being Element of NAT st s . GBP = 0 & s . (intpos 7) > 0 & (s . (intpos 3)) + (s . (intpos 7)) = m3 & s . (intpos 3) >= 8 & s . (intpos 2) = md & md >= 8 holds
( (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . GBP = 0 & (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos 1) = s . (intpos 1) & (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos 7) = 0 & (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos 2) = s . (intpos 2) & (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos 4) = s . (intpos 4) & ( for i being Element of NAT st i >= 8 holds
(IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos i) = s . (intpos i) ) & ex m5, mE3 being Element of NAT st
( m5 = (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos 5) & (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos 3) = mE3 & mE3 + m5 = m3 & m5 <= s . (intpos 7) & ( for i being Element of NAT st s . (intpos 3) <= i & i < mE3 holds
(IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos md) > (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos i) ) & ( m5 = 0 or (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos md) <= (IExec (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 ))))),s) . (intpos mE3) ) ) )
Lm16:
for s being State of SCMPDS
for md being Element of NAT st s . GBP = 0 & s . (intpos 7) > 0 & s . (intpos 3) >= 8 & s . (intpos 2) = md & md >= 8 holds
( while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))) is_closed_on s & while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))) is_halting_on s )
Lm17:
card (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))) = 29
Lm18:
card (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))) = 31
theorem :: SCPQSORT:9
canceled;
theorem :: SCPQSORT:10
canceled;
theorem :: SCPQSORT:11
canceled;
theorem Th12: :: SCPQSORT:12
Lm19:
for s being State of SCMPDS
for m3, m4 being Element of NAT st s . GBP = 0 & s . (intpos 5) > 0 & s . (intpos 3) = m3 & s . (intpos 4) = m4 & m3 > 6 & m4 > 6 holds
( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . GBP = 0 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m3) = s . (intpos m4) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
Lm20:
for s being State of SCMPDS
for md, m3 being Element of NAT st s . GBP = 0 & s . (intpos 5) > 0 & s . (intpos 4) = m3 + (s . (intpos 5)) & m3 = (s . (intpos 3)) - 1 & s . (intpos 2) = md & md >= 8 & md <= m3 holds
( ((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))) is_closed_on s & ((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))) is_halting_on s & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . GBP = 0 & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 1) = s . (intpos 1) & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 2) = md & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 3) >= s . (intpos 3) & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 4) <= s . (intpos 4) & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 4) >= m3 & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 5) < s . (intpos 5) & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 5) >= - 1 & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 4) = (((IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 3)) - 1) + ((IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 5)) & ex n1, n2 being Element of NAT st
( n1 = ((IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 3)) - 1 & n2 = ((IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos 4)) + 1 & ( for i being Element of NAT st i >= 8 & i <> n1 & i <> n2 holds
(IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos i) = s . (intpos i) ) & ( ( (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos n1) = s . (intpos n1) & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos n2) = s . (intpos n2) ) or ( n1 >= s . (intpos 3) & n2 <= s . (intpos 4) & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos n1) = s . (intpos n2) & (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos n2) = s . (intpos n1) ) ) & ( for i being Element of NAT st s . (intpos 3) <= i & i <= n1 holds
(IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos md) >= (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos i) ) & ( for i being Element of NAT st n2 <= i & i <= s . (intpos 4) holds
(IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos md) <= (IExec (((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))),s) . (intpos i) ) ) )
Lm21:
for i being Integer st i >= - 1 & i <= 0 & not i = - 1 holds
i = 0
Lm22:
for i1, i2 being Integer
for n1, n2, i being Element of NAT st i1 >= - 1 & i1 <= 0 & n2 = i2 + 1 & i2 = n1 + i1 & i < n2 holds
i <= n1
Lm23:
for i1, i2 being Integer
for n1, n2 being Element of NAT st i1 >= - 1 & n2 = i2 + 1 & i2 = n1 + i1 holds
n1 <= n2
Lm24:
for s, s1 being State of SCMPDS
for n0, n1, n2, n being Element of NAT
for f, f1 being FinSequence of INT st f is_FinSequence_on s,n0 & f1 is_FinSequence_on s1,n0 & len f = n & len f1 = n & ( for i being Element of NAT st i >= n0 + 1 & i <> n1 & i <> n2 holds
s1 . (intpos i) = s . (intpos i) ) & ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) holds
f,f1 are_fiberwise_equipotent
Lm25:
for s, s1 being State of SCMPDS
for n0, n1, n2 being Element of NAT
for c1, c2 being Integer st ( for i being Element of NAT st i >= n0 & i <> n1 & i <> n2 holds
s1 . (intpos i) = s . (intpos i) ) & n1 <= n2 & ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( c1 <= n1 & n2 <= c2 & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) holds
for i being Element of NAT st i >= n0 & ( i < c1 or i > c2 ) holds
s1 . (intpos i) = s . (intpos i)
Lm26:
for n being Element of NAT
for s being State of SCMPDS
for md, m3, n0 being Element of NAT
for f, f1 being FinSequence of INT st s . GBP = 0 & s . (intpos 5) > 0 & s . (intpos 4) = m3 + (s . (intpos 5)) & m3 = (s . (intpos 3)) - 1 & s . (intpos 2) = md & md >= n0 + 1 & md <= m3 & n0 + 1 <= s . (intpos 3) & s . (intpos 4) <= n0 + n & f is_FinSequence_on s,n0 & f1 is_FinSequence_on IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s,n0 & n0 >= 7 & len f = n & len f1 = n holds
( (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . GBP = 0 & (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos 1) = s . (intpos 1) & (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos 2) = md & (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos 4) >= md & (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos 4) <= s . (intpos 4) & f,f1 are_fiberwise_equipotent & ( for i being Element of NAT st s . (intpos 3) <= i & i <= (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos 4) holds
(IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos md) >= (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos i) ) & ( for i being Element of NAT st (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos 4) < i & i <= s . (intpos 4) holds
(IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos md) <= (IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos i) ) & ( for i being Element of NAT st i >= n0 + 1 & ( i < s . (intpos 3) or i > s . (intpos 4) ) holds
(IExec (while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))))),s) . (intpos i) = s . (intpos i) ) )
Lm27:
for s being State of SCMPDS
for md, m3, n0 being Element of NAT st s . GBP = 0 & s . (intpos 5) > 0 & s . (intpos 4) = m3 + (s . (intpos 5)) & m3 = (s . (intpos 3)) - 1 & s . (intpos 2) = md & md >= n0 + 1 & md <= m3 & n0 >= 7 holds
( while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))) is_closed_on s & while>0 GBP ,5,(((while>0 GBP ,5,(((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))))) ';' (while>0 GBP ,7,(((((GBP ,5 := GBP ,7) ';' (AddTo GBP ,7,(- 1))) ';' (GBP ,6 := (intpos 2),0 )) ';' (SubFrom GBP ,6,(intpos 3),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,3,1) ';' (AddTo GBP ,5,(- 1))),(Load (GBP ,7 := 0 )))))) ';' (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))))) is_halting_on s )
Lm28:
for s being State of SCMPDS st s . GBP = 0 holds
( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . GBP = 0 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = s . (intpos 1) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 4) = s . (intpos 4) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
theorem Th13: :: SCPQSORT:13
theorem Th14: :: SCPQSORT:14
for
s being
State of
SCMPDS for
md,
p0,
n being
Element of
NAT for
f,
f1 being
FinSequence of
INT st
s . GBP = 0 &
(s . (intpos 4)) - (s . (intpos 2)) > 0 &
s . (intpos 2) = md &
md >= p0 + 1 &
s . (intpos 4) <= p0 + n &
p0 >= 7 &
f is_FinSequence_on s,
p0 &
len f = n &
f1 is_FinSequence_on IExec Partition ,
s,
p0 &
len f1 = n holds
(
(IExec Partition ,s) . GBP = 0 &
(IExec Partition ,s) . (intpos 1) = s . (intpos 1) &
f,
f1 are_fiberwise_equipotent & ex
m4 being
Element of
NAT st
(
m4 = (IExec Partition ,s) . (intpos 4) &
md <= m4 &
m4 <= s . (intpos 4) & ( for
i being
Element of
NAT st
md <= i &
i < m4 holds
(IExec Partition ,s) . (intpos m4) >= (IExec Partition ,s) . (intpos i) ) & ( for
i being
Element of
NAT st
m4 < i &
i <= s . (intpos 4) holds
(IExec Partition ,s) . (intpos m4) <= (IExec Partition ,s) . (intpos i) ) & ( for
i being
Element of
NAT st
i >= p0 + 1 & (
i < s . (intpos 2) or
i > s . (intpos 4) ) holds
(IExec Partition ,s) . (intpos i) = s . (intpos i) ) ) )
theorem :: SCPQSORT:15
Lm29:
for s being State of SCMPDS
for p0, n being Element of NAT holds
( card (QuickSort n,p0) = 57 & ( p0 >= 7 implies ( QuickSort n,p0 is_halting_on s & ex f, g being FinSequence of INT st
( len f = n & f is_FinSequence_on s,p0 & len g = n & g is_FinSequence_on IExec (QuickSort n,p0),s,p0 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) ) ) )
theorem :: SCPQSORT:16
theorem :: SCPQSORT:17
theorem :: SCPQSORT:18