:: Insert Sort on SCMPDS
:: by JingChao Chen
::
:: Received June 14, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SCMPDS_2, SUBSET_1, FINSEQ_1, FSM_1, XXREAL_0, FUNCT_1,
SCMP_GCD, ARYTM_3, GRAPH_2, NAT_1, RELAT_1, CLASSES1, AMI_2, AMI_1,
SCMFSA6B, SCMPDS_4, UNIALG_2, SCMFSA7B, TURING_1, SCMFSA_7, INT_1,
CARD_1, SCMPDS_7, AMI_3, ARYTM_1, VALUED_1, TARSKI, FUNCT_4, CIRCUIT2,
GRAPHSP, MSUALG_1, XBOOLE_0, SCMISORT, SCMFSA_9, SCMFSA8B, COMPLEX1,
SCPISORT, EXTPRO_1, SCMFSA6C, COMPOS_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, VALUED_1, XCMPLX_0, FUNCT_4, INT_1, NAT_1, COMPLEX1, MEMSTR_0,
EXTPRO_1, COMPOS_0, COMPOS_1, AMI_2, SCMPDS_2, SCMPDS_4, SCMPDS_5,
SCMPDS_6, SCMP_GCD, DOMAIN_1, FINSEQ_1, SCMPDS_7, SCMPDS_8, GRAPH_2,
CLASSES1, XXREAL_0, FINSEQ_6;
constructors DOMAIN_1, REAL_1, INT_2, SCM_1, SCMPDS_4, SCMPDS_5, SCMPDS_6,
SCMP_GCD, SCMPDS_7, SCMPDS_8, CLASSES1, PRE_POLY, GRAPH_2, FINSEQ_6,
RELSET_1;
registrations XXREAL_0, XREAL_0, NAT_1, INT_1, SCMPDS_2, SCMPDS_4, SCMPDS_5,
SCMPDS_6, SCMPDS_7, SCMPDS_8, XBOOLE_0, VALUED_0, ORDINAL1, CARD_1,
COMPOS_1, AFINSQ_1, FUNCT_4, MEMSTR_0, RELSET_1, COMPOS_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities SCMPDS_2, SCMP_GCD, AMI_3, COMPOS_1, EXTPRO_1, MEMSTR_0;
theorems AMI_3, NAT_1, TARSKI, FUNCT_4, INT_1, SCMPDS_2, GRFUNC_1, SCMPDS_4,
SCMPDS_5, SCMPDS_6, ENUMSET1, SCMP_GCD, SCMPDS_7, SCMPDS_8, ABSVALUE,
FINSEQ_1, FINSEQ_2, RFINSEQ, XBOOLE_1, XREAL_1, XXREAL_0, GRAPH_2,
FINSEQ_3, CLASSES1, AFINSQ_1, COMPOS_1, EXTPRO_1, PBOOLE, MEMSTR_0,
XTUPLE_0, FINSEQ_6;
schemes NAT_1, FINSEQ_1;
begin :: Preliminaries
reserve x for Int_position,
n,p0 for Nat;
definition
let f be FinSequence of INT,s be State of SCMPDS,m be Nat;
pred f is_FinSequence_on s,m means
for i be Nat st 1 <= i
& i <= len f holds f.i=s.intpos(m+i);
end;
theorem Th1:
for s being State of SCMPDS,n,m be Nat holds ex f be
FinSequence of INT st len f=n & for i be Nat st 1<=i & i <= len f
holds f.i=s.intpos(m+i)
proof
let s be State of SCMPDS,n,m be Nat;
deffunc U(Nat) = s.intpos (m+$1);
consider f being FinSequence such that
A1: len f = n & for i be Nat st i in dom f holds f.i=U(i) from FINSEQ_1:
sch 2;
now
let i be Nat;
reconsider a = i as Nat;
assume
i in dom f;
then f.i = s.intpos (m+a) by A1;
hence f.i in INT by INT_1:def 2;
end;
then reconsider f as FinSequence of INT by FINSEQ_2:12;
take f;
thus len f=n by A1;
thus for i being Nat st 1<=i <= len f holds f.i = s.intpos (m+i)
by A1,FINSEQ_3:25;
end;
theorem
for s being State of SCMPDS,n,m be Nat holds ex f be
FinSequence of INT st len f=n & f is_FinSequence_on s,m
proof
let s be State of SCMPDS,n,m be Nat;
consider f be FinSequence of INT such that
A1: len f=n and
A2: for i be Nat st 1<=i & i <= len f holds f.i=s.intpos(m+i)
by Th1;
take f;
thus len f=n by A1;
thus thesis by A2;
end;
theorem Th3:
for f,g be FinSequence of INT,m,n be Nat st 1<=n & n
<= len f & 1<=m & m <= len f & len f=len g & f.m=g.n & f.n=g.m & (for k be
Nat st k<>m & k<>n & 1<=k & k <= len f holds f.k=g.k) holds f,g
are_fiberwise_equipotent
proof
let f,g be FinSequence of INT,m,n be Nat;
assume that
A1: 1<=n & n <= len f and
A2: 1<=m & m <= len f and
A3: len f=len g and
A4: f.m=g.n & f.n=g.m and
A5: for k be Nat st k<>m & k<>n & 1<=k & k <= len f holds f.k
=g.k;
A6: m in Seg (len f) by A2,FINSEQ_1:1;
A7: Seg (len f) = dom f by FINSEQ_1:def 3;
A8: now
let k be set;
assume that
A9: k<>m & k<>n and
A10: k in dom f;
reconsider i=k as Nat by A10;
1 <= i & i <= len f by A7,A10,FINSEQ_1:1;
hence f.k=g.k by A5,A9;
end;
n in dom f & dom f=dom g by A1,A3,A7,FINSEQ_1:1,def 3;
hence thesis by A4,A7,A6,A8,RFINSEQ:28;
end;
set A = NAT, D = SCM-Data-Loc;
theorem Th4: ::see SCMPDS_8:2
for s1,s2 being State of SCMPDS st (for a being Int_position
holds s1.a = s2.a) holds Initialize (s1)=Initialize (s2)
proof
let s1,s2 be State of SCMPDS;
assume
for a being Int_position holds s1.a = s2.a;
then DataPart s1 = DataPart s2 by SCMPDS_4:8;
hence thesis by MEMSTR_0:80;
end;
reserve P,Q,U,V for Instruction-Sequence of SCMPDS;
theorem Th5: :: see SCMPDS_7:50
for s being State of SCMPDS, I being halt-free Program of
SCMPDS, j being parahalting shiftable Instruction of SCMPDS
st I is_closed_on s,P
& I is_halting_on s,P holds (I ';' j) is_closed_on s,P
& (I ';' j) is_halting_on s,P
proof
let s be State of SCMPDS,I be halt-free Program of SCMPDS,j be parahalting
shiftable Instruction of SCMPDS;
set Mj = Load j;
A1: Mj is_closed_on IExec(I,P,Initialize s),P &
Mj is_halting_on IExec(I,P,Initialize s),P
by SCMPDS_6:20,21;
assume
I is_closed_on s,P & I is_halting_on s,P;
then (I ';' Mj) is_closed_on s,P & (I ';' Mj) is_halting_on s,P
by A1,SCMPDS_7:24;
hence thesis by SCMPDS_4:def 3;
end;
theorem :: see SCMPDS_7:49
for s being 0-started State of SCMPDS, I being halt-free Program of SCMPDS, J
being shiftable parahalting Program of SCMPDS,a be Int_position st I
is_closed_on s,P & I is_halting_on s,P holds IExec(I ';' J,P,s).a
= IExec(J,P,Initialize IExec(I,P,s)).a
proof
let s be 0-started State of SCMPDS,I be halt-free Program of SCMPDS,
J be shiftable parahalting Program of SCMPDS,a be Int_position;
J is_closed_on IExec(I,P,s),P & J is_halting_on IExec(I,P,s),P
by SCMPDS_6:20,21;
hence thesis by SCMPDS_7:30;
end;
theorem :: see SCMPDS_7:49
for s being 0-started State of SCMPDS, I being halt-free parahalting Program
of SCMPDS , J being shiftable Program of SCMPDS,a be Int_position
st J is_closed_on IExec(I,P,s),P & J is_halting_on IExec(I,P,s),P
holds IExec(I ';' J,P,s).a = IExec(J,P,Initialize IExec(I,P,s)).a
proof
let s be 0-started State of SCMPDS,
I be halt-free parahalting Program of SCMPDS, J
be shiftable Program of SCMPDS,a be Int_position;
I is_closed_on s,P & I is_halting_on s,P by SCMPDS_6:20,21;
hence thesis by SCMPDS_7:30;
end;
theorem :: SCMPDS_7:43
for s being State of SCMPDS, I being Program of SCMPDS,J being
shiftable parahalting Program of SCMPDS st I is_closed_on s,P
& I is_halting_on s,P
holds I ';' J is_closed_on s,P & I ';' J is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS,J be shiftable parahalting
Program of SCMPDS;
A1: J is_closed_on IExec(I,P,Initialize s),P &
J is_halting_on IExec(I,P,Initialize s),P
by SCMPDS_6:20,21;
assume
I is_closed_on s,P & I is_halting_on s,P;
hence thesis by A1,SCMPDS_7:24;
end;
theorem :: SCMPDS_7:43
for s being State of SCMPDS, I being parahalting Program of SCMPDS,J
being shiftable Program of SCMPDS st
J is_closed_on IExec(I,P,Initialize s),P & J
is_halting_on IExec(I,P,Initialize s),P holds I ';' J is_closed_on s,P
& I ';' J is_halting_on s,P
proof
let s be State of SCMPDS,I be parahalting Program of SCMPDS,J be shiftable
Program of SCMPDS;
A1: I is_closed_on s,P & I is_halting_on s,P by SCMPDS_6:20,21;
assume
J is_closed_on IExec(I,P,Initialize s),P &
J is_halting_on IExec(I,P,Initialize s),P;
hence thesis by A1,SCMPDS_7:24;
end;
theorem :: SCMPDS_7:43
for s being State of SCMPDS, I being Program of SCMPDS, j being
parahalting shiftable Instruction of SCMPDS st I is_closed_on s,P & I
is_halting_on s,P holds I ';' j is_closed_on s,P & I ';' j is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS,j be shiftable parahalting
Instruction of SCMPDS;
A1: Load j is_closed_on IExec(I,P,Initialize s),P &
Load j is_halting_on IExec(I,P,Initialize s),P
by SCMPDS_6:20,21;
assume
I is_closed_on s,P & I is_halting_on s,P;
then I ';' Load j is_closed_on s,P & I ';' Load j is_halting_on s,P by A1,
SCMPDS_7:24;
hence thesis by SCMPDS_4:def 3;
end;
Lm1: for a be Int_position,i be Integer,n be Nat, I be Program of
SCMPDS holds card stop for-down(a,i,n,I)= card I+4
proof
let a be Int_position,i be Integer,n be Nat, I be Program of
SCMPDS;
thus card stop for-down(a,i,n,I)= card for-down(a,i,n,I) +1 by COMPOS_1:55
.= card I +3+1 by SCMPDS_7:41
.= card I + 4;
end;
Lm2: for a be Int_position,i be Integer,n be Nat, I be Program of
SCMPDS holds for-down(a,i,n,I)= ((a,i)<=0_goto (card I +3)) ';' (I ';' AddTo(a,
i,-n) ';' goto -(card I+2))
proof
let a be Int_position,i be Integer,n be Nat, I be Program of
SCMPDS;
set i1=(a,i)<=0_goto (card I +3), i2=AddTo(a,i,-n), i3=goto -(card I+2);
thus for-down(a,i,n,I) = i1 ';' I ';' i2 ';' i3 by SCMPDS_7:def 2
.= i1 ';' (I ';' i2 ';' i3) by SCMPDS_7:2;
end;
Lm3: for I being Program of SCMPDS,a being Int_position,i being Integer, n be
Nat holds Shift(I ';' AddTo(a,i,-n),1) c= for-down(a,i,n,I)
proof
let I be Program of SCMPDS,a be Int_position,i be Integer, n be Nat;
set i1=(a,i)<=0_goto (card I+3), i2=AddTo(a,i,-n), i3=goto -(card I+2);
A1: for-down(a,i,n,I) = i1 ';' I ';' i2 ';' i3 by SCMPDS_7:def 2
.= i1 ';' (I ';' i2) ';' i3 by SCMPDS_4:15
.= Load i1 ';' (I ';' i2) ';' i3 by SCMPDS_4:def 2
.= Load i1 ';' (I ';' i2) ';' Load i3 by SCMPDS_4:def 3;
card Load i1=1 by COMPOS_1:54;
hence thesis by A1,SCMPDS_7:3;
end;
begin :: Computing the Execution Result(,) For-loop Program by Loop-Invariant
scheme
ForDownHalt { P[set],
s() -> 0-started State of SCMPDS,
P() -> Instruction-Sequence of SCMPDS,
I() -> halt-free shiftable
Program of SCMPDS, a() -> Int_position,i() -> Integer,n() -> Nat}:
for-down(a(),i(),n(),I()) is_closed_on s(), P()
& for-down(a(),i(),n(),I()) is_halting_on s(), P()
provided
A1: n() > 0 and
A2: P[s()] and
A3: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
holds IExec(I() ';' AddTo(a(),i(),-n()),Q,t).a()=t.a()
& IExec(I() ';' AddTo(a(),i(),-n()),Q,t).DataLoc(s().a(),i())
=t.DataLoc(s().a(),i())-n()
& I() is_closed_on t,Q & I() is_halting_on t,Q
& P[Initialize (IExec(I() ';' AddTo(a(),i(),-n()),Q,t))]
proof
set i1=(a(),i())<=0_goto (card I()+3), J=I() ';' AddTo(a(),i(),-n()), i3=
goto -(card I()+2);
set b=DataLoc(s().a(),i());
set FOR=for-down(a(),i(),n(),I()), pFOR=stop FOR,
pJ= stop J;
defpred Q[Nat] means
for t be 0-started State of SCMPDS,Q st t.b <= $1 & P[t] & t.a()=s().a()
holds FOR is_closed_on t,Q & FOR is_halting_on t,Q;
A4: for k be Nat st Q[k] holds Q[k + 1]
proof
let k be Nat;
assume
A5: Q[k];
now
let t be 0-started State of SCMPDS;
let Q;
A6: Initialize t = t by MEMSTR_0:44;
assume
A7: t.b <= k+1;
assume
A8: P[t];
assume
A9: t.a()=s().a();
per cases;
suppose
t.b <= 0;
hence FOR is_closed_on t,Q & FOR is_halting_on t,Q by A9,SCMPDS_7:44;
end;
suppose
A10: t.b > 0;
A11: 0 in dom pFOR by COMPOS_1:36;
-(-n()) > 0 by A1;
then -n() < 0;
then -n() <= -1 by INT_1:8;
then
A12: -n()+t.b <= -1+t.b by XREAL_1:6;
t.b-1 <= k by A7,XREAL_1:20;
then
A13: -n()+t.b <= k by A12,XXREAL_0:2;
set Q2 = Q +* pJ, Q3 = Q +* pFOR, t4 = Comput(Q3,t,1), Q4 = Q3,
Jt = IExec(J,Q,t);
A14: pJ c= Q2 by FUNCT_4:25;
A15: FOR = i1 ';' (J ';' i3) by Lm2;
A16: Comput(Q3,t,0+1) = Following(Q3,Comput(Q3,t,0)) by EXTPRO_1:3
.= Following(Q3,t) by EXTPRO_1:2
.= Exec(i1,t) by A15,A6,SCMPDS_6:11;
for x holds t.x = t4.x by A16,SCMPDS_2:56;
then
A17: DataPart t = DataPart t4 by SCMPDS_4:8;
A18: Jt.b=t.b-n() by A3,A8,A9,A10;
A19: Jt.a()=t.a() by A3,A8,A9,A10;
set m2=LifeSpan(Q2,t), t5=Comput(Q4,t4,m2), Q5 = Q4,
l1= (card J + 1);
A20: card J = card I()+1 by SCMP_GCD:4;
A21: t.DataLoc(t.a(),i())= t.b by A9;
A22: IC t = 0 by A6,MEMSTR_0:47;
A23: I() is_closed_on t,Q & I() is_halting_on t,Q by A3,A8,A9,A10;
then
A24: J is_closed_on t,Q by Th5;
then
A25: J is_closed_on t,Q2 by A6,SCMPDS_6:24;
card I() + 2 < card I() + 3 by XREAL_1:6;
then
A26: l1 in dom FOR by A20,SCMPDS_7:42;
set m3=m2 +1;
set t6=Comput(Q3,t,m3), Q6 = Q3;
A27: t6=t5 by EXTPRO_1:4;
A28: J is_halting_on t,Q by A23,Th5;
then
A29: Q2 halts_on t by A6,SCMPDS_6:def 3;
Q2+*pJ halts_on t by A28,A6,SCMPDS_6:def 3;
then
A30: J is_halting_on t,Q2 by A6,SCMPDS_6:def 3;
set m4=m3+1, t7=Comput(Q3,t,m4), Q7 = Q3;
A31: pFOR c= Q3 by FUNCT_4:25;
A32: FOR c= pFOR by AFINSQ_1:74;
then
A33: FOR c= Q3 by A31,XBOOLE_1:1;
Shift(J,1) c= FOR by Lm3;
then Shift(J,1) c= pFOR by A32,XBOOLE_1:1;
then
A34: Shift(J,1) c= Q4 by A31,XBOOLE_1:1;
A35: IC t4 = IC t + 1 by A10,A16,A21,SCMPDS_2:56
.= (0+1) by A22;
then
A36: DataPart Comput(Q2,t,m2) = DataPart t5 by A14,A30,A25,A17,A34,
SCMPDS_7:18;
then
A37: DataPart t5 = DataPart(Result(Q2,t)) by A29,EXTPRO_1:23
.= DataPart Jt by SCMPDS_4:def 5;
A38: IC t5=l1 by A14,A30,A25,A35,A17,A34,SCMPDS_7:18;
then
A39: CurInstr(Q6,t6) =Q4.l1 by A27,PBOOLE:143
.=FOR.l1 by A26,A33,GRFUNC_1:2
.=i3 by A20,SCMPDS_7:43;
A40: t7 = Following(Q3,t6) by EXTPRO_1:3
.= Exec(i3,t6) by A39;
IC t7 =ICplusConst(t6,0-(card I()+2)) by A40,SCMPDS_2:54
.= 0 by A20,A38,A27,SCMPDS_7:1;
then
A41: Initialize t7 = t7 by MEMSTR_0:46;
InsCode i3=14 by SCMPDS_2:12;
then InsCode i3 in {0,4,5,6,14} by ENUMSET1:def 3;
then t7 =Initialize (t6) by A40,A41,SCMPDS_8:3
.=Initialize (Jt) by A37,A27,MEMSTR_0:80;
then
A42: P[t7] by A3,A8,A9,A10;
A43: Q7 +* pFOR= Q7;
t5.b=Comput(Q2,t,m2).b by A36,SCMPDS_4:8
.=(Result(Q2,t)).b by A29,EXTPRO_1:23
.=t.b - n() by A18,SCMPDS_4:def 5;
then
A44: t7.b=-n()+t.b by A27,A40,SCMPDS_2:54;
t5.a()=Comput(Q2,t,m2).a() by A36,SCMPDS_4:8
.=(Result(Q2,t)).a() by A29,EXTPRO_1:23
.=s().a() by A9,A19,SCMPDS_4:def 5;
then
A45: t7.a()=s().a() by A27,A40,SCMPDS_2:54;
then
A46: FOR is_closed_on t7,Q7 by A5,A42,A44,A13,A41;
now
let k be Nat;
per cases;
suppose
k < m4;
then
A47: k <= m3 by INT_1:7;
hereby
per cases by A47,NAT_1:8;
suppose
A48: k <= m2;
per cases;
suppose
k=0;
hence IC Comput(Q3,t,k) in dom pFOR by A11,A22,EXTPRO_1:2;
end;
suppose
k<>0;
then consider kn be Nat such that
A49: k=kn+1 by NAT_1:6;
reconsider kn as Nat;
reconsider lm = IC Comput(Q2,t,kn) as Element
of NAT;
kn < k by A49,XREAL_1:29;
then kn < m2 by A48,XXREAL_0:2;
then IC Comput(Q2,t,kn) + 1 = IC Comput(
Q4,t4,kn) by A14,A30,A25,A35,A17,A34,SCMPDS_7:16;
then
A50: IC Comput(Q3,t,k) = (lm+1) by A49,EXTPRO_1:4;
IC Comput(Q2,t,kn) in dom pJ by A24,A6,SCMPDS_6:def 2;
then lm < card pJ by AFINSQ_1:66;
then lm < card J+1 by COMPOS_1:55;
then
A51: lm+1 <= card J +1 by INT_1:7;
card I() + 2 < card I() + 4 by XREAL_1:6;
then lm+1 < card I() +4 by A20,A51,XXREAL_0:2;
then lm+1 < card pFOR by Lm1;
hence IC Comput(Q3,t,k) in dom pFOR by A50,AFINSQ_1:66;
end;
end;
suppose
A52: k=m3;
l1 in dom pFOR by A26,COMPOS_1:62;
hence
IC Comput(Q3,t,k) in dom pFOR by A14,A30,A25,A35,A17,A34,A27
,A52,SCMPDS_7:18;
end;
end;
end;
suppose
k >= m4;
then consider nn be Nat such that
A53: k=m4+nn by NAT_1:10;
reconsider nn as Nat;
Comput(Q3,t,k)
= Comput(Q3,Comput(Q3,t,m4),nn) by A53,EXTPRO_1:4
.= Comput(Q7+*pFOR,t7,nn);
hence IC Comput(Q3,t,k) in dom pFOR by A46,A41,SCMPDS_6:def 2;
end;
end;
hence FOR is_closed_on t,Q by A6,SCMPDS_6:def 2;
FOR is_halting_on t7,Q7 by A5,A45,A42,A44,A13,A41;
then Q7 halts_on t7 by A43,A41,SCMPDS_6:def 3;
then Q3 halts_on t by EXTPRO_1:22;
hence FOR is_halting_on t,Q by A6,SCMPDS_6:def 3;
end;
end;
hence thesis;
end;
A54: Q[0] by SCMPDS_7:44;
A55: for k being Nat holds Q[k] from NAT_1:sch 2(A54,A4);
per cases;
suppose
s().b <= 0;
hence thesis by SCMPDS_7:44;
end;
suppose
s().b > 0;
then reconsider m=s().b as Element of NAT by INT_1:3;
Q[m] by A55;
hence thesis by A2;
end;
end;
scheme
ForDownExec { P[set], s() -> 0-started State of SCMPDS,
P() -> Instruction-Sequence of SCMPDS,
I() -> halt-free shiftable
Program of SCMPDS, a() -> Int_position,i() -> Integer,n() -> Nat}:
IExec(for-down(a(),i(),n(),I()),P(),s())
= IExec(for-down(a(),i(),n(),I()),P(),
Initialize IExec(I() ';' AddTo(a(),i(),-n()),P(), s()))
provided
A1: n() > 0 and
A2: s().DataLoc(s().a(),i()) > 0 and
A3: P[s()] and
A4: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
holds IExec(I() ';' AddTo(a(),i(),-n()),Q,t).a()=t.a() &
IExec(I
() ';' AddTo(a(),i(),-n()),Q,t).DataLoc(s().a(),i())
=t.DataLoc(s().a(),i())-n()
& I() is_closed_on t,Q & I() is_halting_on t,Q
& P[Initialize IExec(I() ';' AddTo(a(),i(),-n()),Q,t)]
proof
set i1=(a(),i())<=0_goto (card I()+3), J=I() ';' AddTo(a(),i(),-n()), i3=
goto -(card I()+2);
set FOR=for-down(a(),i(),n(),I()), pFOR = stop FOR, P1 = P() +* pFOR;
set PJ = P() +* stop J, mJ=LifeSpan(PJ,s()),
m1=mJ+2, s2=Initialize IExec(J,P(),s()), m2= LifeSpan(P1,s2);
A5: stop J c= PJ by FUNCT_4:25;
A6: Initialize s() = s() by MEMSTR_0:44;
A7: I() is_closed_on s(), P() & I() is_halting_on s(), P() by A2,A3,A4;
then J is_closed_on s(), P() by Th5;
then
A8: J is_closed_on s(),PJ by A6,SCMPDS_6:24;
A9: J is_halting_on s(), P() by A7,Th5;
then
A10: PJ halts_on s() by A6,SCMPDS_6:def 3;
PJ+*stop J halts_on Initialize s() by A9,SCMPDS_6:def 3;
then
A11: J is_halting_on s(),PJ by SCMPDS_6:def 3;
A12: FOR = i1 ';' (J ';' i3) by Lm2;
A13: Comput(P1,s(),0+1) = Following(P1,
Comput(P1,s(),0)) by EXTPRO_1:3
.= Following(P1,s()) by EXTPRO_1:2
.= Exec(i1,s()) by A12,A6,SCMPDS_6:11;
set m3=mJ +1;
set s4 = Comput(P1,s(),1), P4 = P1;
set b=DataLoc(s().a(),i());
A14: card J = card I()+1 by SCMP_GCD:4;
set s6=Comput(P1,s(),m3), P6 = P1;
set s5=Comput(P4,s4,mJ), l1= (card J + 1), P5 = P4;
card I() + 2 < card I() + 3 by XREAL_1:6;
then
A15: l1 in dom FOR by A14,SCMPDS_7:42;
A16: s6=s5 by EXTPRO_1:4;
for x holds s().x = s4.x by A13,SCMPDS_2:56;
then
A17: DataPart s() = DataPart s4 by SCMPDS_4:8;
A18: IC s() = 0 by MEMSTR_0:def 12;
A19: pFOR c= P1 by FUNCT_4:25;
A20: FOR c= pFOR by AFINSQ_1:74;
then
A21: FOR c= P1 by A19,XBOOLE_1:1;
Shift(J,1) c= FOR by Lm3;
then Shift(J,1) c= pFOR by A20,XBOOLE_1:1;
then
A22: Shift(J,1) c= P4 by A19,XBOOLE_1:1;
set m0=LifeSpan(P1,s());
set m4=m3+1, s7=Comput(P1,s(),m4);
A23: IC s4 = IC s() + 1 by A2,A13,SCMPDS_2:56
.= (0+1) by A18;
then
A24: IC s5=l1 by A5,A11,A8,A17,A22,SCMPDS_7:18;
then
A25: CurInstr(P6,s6) =P4.l1 by A16,PBOOLE:143
.=FOR.l1 by A15,A21,GRFUNC_1:2
.=i3 by A14,SCMPDS_7:43;
A26: s7 = Following(P1,s6) by EXTPRO_1:3
.= Exec(i3,s6) by A25;
A27: DataPart Comput(PJ,s(),mJ) = DataPart s5 by A5,A11,A8,A23,A17,A22,
SCMPDS_7:18;
now
let x be Int_position;
not x in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A28: s2.x=IExec(J,P(),s()).x by FUNCT_4:11;
s5.x=Comput(PJ,s(),mJ).x by A27,SCMPDS_4:8
.=(Result(PJ,s())).x by A10,EXTPRO_1:23
.=IExec(J,P(),s()).x by SCMPDS_4:def 5;
hence s7.x=s2.x by A16,A26,A28,SCMPDS_2:54;
end;
then
A29: DataPart s7 = DataPart s2 by SCMPDS_4:8;
A30: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=s().a() & t.DataLoc(s().
a(),i()) > 0 holds
IExec(I() ';' AddTo(a(),i(),-n()),Q,t).a()=t.a() &
IExec(I()
';' AddTo(a(),i(),-n()),Q,t).DataLoc(s().a(),i())
=t.DataLoc(s().a(),i())-n() & I
() is_closed_on t,Q & I() is_halting_on t,Q
& P[Initialize (IExec(I() ';' AddTo(a(),i(),-n()),Q,t))] by A4;
A31: P[s()] by A3;
for-down(a(),i(),n(),I()) is_closed_on s(), P() &
for-down(a(),i(),n(),I()) is_halting_on s(), P()
from ForDownHalt(A1,A31,A30);
then
A32: P1 halts_on s() by A6,SCMPDS_6:def 3;
set Es=IExec(J,P(),s()), bj=DataLoc((Initialize Es).a(),i());
(Initialize Es).a() = Es.a() by SCMPDS_5:15
.=s().a() by A2,A3,A4;
then
A33: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=(Initialize Es).a() & t.DataLoc((Initialize Es).a(),i()) > 0
holds IExec(I() ';' AddTo(a(),i(),-n()),Q,t).a()=t.a()
& IExec(I() ';' AddTo(a(),i(),-n()),Q,t).DataLoc((Initialize Es).a(),i())
=t.DataLoc((Initialize Es).a(),i())-n()
& I() is_closed_on t,Q & I() is_halting_on t,Q
& P[Initialize (IExec(I() ';' AddTo(a(),i
(),-n()),Q,t))] by A4;
A34: P[Initialize Es] by A2,A3,A4;
FOR is_closed_on Initialize Es,P() &
FOR is_halting_on Initialize Es,P() from ForDownHalt(A1,A34,A33);
then
A35: P1 halts_on Initialize s2 by SCMPDS_6:def 3;
IC s7 =ICplusConst(s6,0-(card I()+2)) by A26,SCMPDS_2:54
.= 0 by A14,A24,A16,SCMPDS_7:1;
then
A36: IC s2 =IC Comput(P1,s(),m1) by MEMSTR_0:47;
A37: Comput(P1,s(),m1)=s2 by A29,A36,MEMSTR_0:78;
then CurInstr(P1,Comput(P1,s(),m1))=i1
by A12,SCMPDS_6:11;
then m0 > m1 by A32,EXTPRO_1:36,SCMPDS_6:17;
then consider nn be Nat such that
A38: m0=m1+nn by NAT_1:10;
reconsider nn as Nat;
Comput(P1,s(),m1+m2) = Comput(P1,s2,m2) by A37,EXTPRO_1:4;
then CurInstr(P1,Comput(P1,s(),m1+m2))
= halt SCMPDS by A35,EXTPRO_1:def 15;
then m1 + m2 >= m0 by A32,EXTPRO_1:def 15;
then
A39: m2 >= nn by A38,XREAL_1:6;
A40: Comput(P1,s(),m0) = Comput(P1,s2,nn) by A37,A38,EXTPRO_1:4;
then CurInstr(P1,Comput(P1,s2,nn))
=halt SCMPDS by A32,EXTPRO_1:def 15;
then nn >= m2 by A35,EXTPRO_1:def 15;
then nn=m2 by A39,XXREAL_0:1;
then Result(P1,s()) = Comput(P1,s2,m2) by A32,A40,EXTPRO_1:23;
hence IExec(FOR,P(),s()) = Comput(P1,s2,m2) by SCMPDS_4:def 5
.= Result(P1,s2) by A35,EXTPRO_1:23
.= IExec(FOR,P(),Initialize IExec(J,P(),s())) by SCMPDS_4:def 5;
end;
scheme
ForDownEnd { P[set], s() -> 0-started State of SCMPDS,
I() -> halt-free shiftable Program of SCMPDS,
P() -> Instruction-Sequence of SCMPDS,
a() -> Int_position,i() -> Integer,n() -> Nat}:
IExec(for-down(a(),i(),n(),I()),P(),s()).DataLoc(s().a(),i(
)) <= 0 & P[Initialize IExec(for-down(a(),i(),n(),I()),P(),s())]
provided
A1: n() > 0 and
A2: P[s()] and
A3: for t be 0-started State of SCMPDS st P[t] &
t.a()=s().a() & t.DataLoc(s().a(),i()) > 0 holds
IExec(I() ';' AddTo(a(),i(),-n()),Q,t).a()=t.a() & IExec(I
() ';' AddTo(a(),i(),-n()),Q,t).DataLoc(s().a(),i())
=t.DataLoc(s().a(),i())-n()
& I() is_closed_on t,Q & I() is_halting_on t,Q
& P[Initialize (IExec(I() ';' AddTo(a(),i(),-n()),Q,t))]
proof
set b=DataLoc(s().a(),i()), FR=for-down(a(),i(),n(),I());
defpred Q[Nat] means
for t be 0-started State of SCMPDS,Q st t.b <= $1 & t.a()=s().a() &
P[t] holds IExec(FR,Q,t).b <= 0 & P[Initialize IExec(FR,Q,t)];
A4: Q[0 qua Nat]
proof
let t be 0-started State of SCMPDS, Q;
assume that
A5: t.b <= 0 & t.a()=s().a() and
A6: P[t];
A7: Initialize t = t by MEMSTR_0:44;
hence IExec(FR,Q,t).b <= 0 by A5,SCMPDS_7:47;
for x be Int_position holds IExec(FR,Q,t).x = t.x
by A5,A7,SCMPDS_7:47;
hence thesis by A6,Th4,A7;
end;
A8: now
let k be Nat;
assume
A9: Q[k];
thus Q[k+1]
proof
let u be 0-started State of SCMPDS;
let U;
assume that
A10: u.b <= k+1 and
A11: u.a()=s().a() and
A12: P[u];
per cases;
suppose
u.b <= 0;
hence IExec(FR,U,u).b <= 0 &
P[Initialize IExec(FR,U,u)] by A4,A11,A12;
end;
suppose
A13: u.b > 0;
set Ad=AddTo(a(),i(),-n());
set Iu=IExec(I() ';' Ad,U,u);
A14: Iu.a()=s().a() & P[Initialize Iu] by A3,A11,A12,A13;
Iu.b=u.b-n() by A3,A11,A12,A13;
then Iu.b+1 <= u.b by A1,INT_1:7,XREAL_1:44;
then Iu.b+1 <= k+1 by A10,XXREAL_0:2;
then
A15: Iu.b <= k by XREAL_1:6;
A16: P[u] by A12;
A17: for t being 0-started State of SCMPDS,Q
st P[t] & t.a()=u.a() & t.DataLoc(u.a(),i()) > 0
holds IExec(I() ';' Ad,Q,t).a()=t.a() &
IExec(I() ';' Ad,Q,t).DataLoc(u.a(),i()) =t.DataLoc(u.a(),i())-n()
& I() is_closed_on t,Q & I()
is_halting_on t,Q &
P[Initialize (IExec(I() ';' Ad,Q,t))] by A3,A11;
A18: u.DataLoc(u.a(),i()) > 0 by A11,A13;
A19: (Initialize Iu).b = Iu.b by SCMPDS_5:15;
A20: (Initialize Iu).a() = Iu.a() by SCMPDS_5:15;
IExec(FR,U,u) = IExec(FR,U,Initialize Iu)
from ForDownExec(A1,A18,A16,A17);
hence IExec(FR,U,u).b <= 0 &
P[Initialize IExec(FR,U,u)] by A9,A15,A14,A19,A20;
end;
end;
end;
A21: for k being Nat holds Q[k] from NAT_1:sch 2(A4,A8);
per cases;
suppose
s().b > 0;
then reconsider m=s().b as Element of NAT by INT_1:3;
Q[m] by A21;
hence thesis by A2;
end;
suppose
s().b <= 0;
hence thesis by A2,A4;
end;
end;
theorem Th11:
for s being 0-started State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a,x,y be Int_position, i,c be Integer,n be Nat st
n > 0 & s.x >= s.y +c &
for t be 0-started State of SCMPDS,Q st t.x >= t.y +c & t.a=s.a & t
.DataLoc(s.a,i) > 0 holds
IExec(I ';' AddTo(a,i,-n),Q,t).a=t.a & IExec(I ';'
AddTo(a,i,-n),Q,t).DataLoc(s.a,i)=t.DataLoc(s.a,i)-n
& I is_closed_on t,Q & I
is_halting_on t,Q
& IExec(I ';' AddTo(a,i,-n),Q,t).x >=IExec(I ';' AddTo(a,i,-n),Q,t).y+c
holds for-down(a,i,n,I) is_closed_on s,P &
for-down(a,i,n,I) is_halting_on s,P
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, a,x,y
be Int_position, i,c be Integer,n be Nat;
set b=DataLoc(s.a,i), J=I ';' AddTo(a,i,-n);
assume
A1: n > 0;
defpred P[set] means ex t be State of SCMPDS st t=$1 & t.x >= t.y+c;
assume
A2: s.x >= s.y +c;
A3: P[s] by A2;
assume
A4: for t be 0-started State of SCMPDS,Q
st t.x >= t.y +c & t.a=s.a & t.b > 0 holds
IExec(J,Q,t).a=t.a & IExec(J,Q,t).b=t.b-n &
I is_closed_on t,Q
& I is_halting_on t,Q &
IExec(J,Q,t).x>=IExec(J,Q,t).y+c;
A5: now
let t be 0-started State of SCMPDS, Q;
assume that
A6: P[t] and
A7: t.a=s.a & t.b > 0;
consider v be State of SCMPDS such that
A8: v= t and
A9: v.x>=v.y+c by A6;
thus IExec(J,Q,t).a=t.a & IExec(J,Q,t).b=t.b-n &
I is_closed_on t,Q & I
is_halting_on t,Q by A4,A7,A8,A9;
thus P[Initialize IExec(J,Q,t)]
proof
take v=Initialize IExec(J,Q,t);
thus v=Initialize IExec(J,Q,t);
v.x=IExec(J,Q,t).x by SCMPDS_5:15;
then v.x>=IExec(J,Q,t).y+c by A4,A7,A8,A9;
hence thesis by SCMPDS_5:15;
end;
end;
for-down(a,i,n,I) is_closed_on s,P &
for-down(a,i,n,I) is_halting_on s,P
from ForDownHalt(A1,A3,A5);
hence thesis;
end;
theorem Th12:
for s being 0-started State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a,x,y be Int_position, i,c be Integer,n be Nat st
n > 0 & s.x >= s.y +c & s.DataLoc(s.a,i) > 0 &
for t be 0-started State of SCMPDS,Q st t.x
>= t.y +c & t.a=s.a & t.DataLoc(s.a,i) > 0
holds IExec(I ';' AddTo(a,i,-n),Q,t).a
=t.a & IExec(I ';' AddTo(a,i,-n),Q,t).DataLoc(s.a,i)
=t.DataLoc(s.a,i)-n & I
is_closed_on t,Q & I is_halting_on t,Q
& IExec(I ';' AddTo(a,i,-n),Q,t).x>=IExec(I
';' AddTo(a,i,-n),Q,t).y+c
holds IExec(for-down(a,i,n,I),P,s) = IExec(for-down(a,i,
n,I),P,Initialize IExec(I ';' AddTo(a,i,-n),P,s))
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, a,x,y
be Int_position, i,c be Integer,n be Nat;
set b=DataLoc(s.a,i), J=I ';' AddTo(a,i,-n);
assume
A1: n > 0;
defpred P[set] means ex t be State of SCMPDS st t=$1 & t.x>=t.y+c;
assume
A2: s.x >= s.y +c;
A3: P[s] by A2;
assume
A4: s.b > 0;
assume
A5: for t be 0-started State of SCMPDS,Q
st t.x >= t.y +c & t.a=s.a & t.b > 0 holds
IExec(J,Q,t).a=t.a & IExec(J,Q,t).b=t.b-n &
I is_closed_on t,Q & I is_halting_on t,Q & IExec(J,Q,t).x>=IExec(J,Q,t).y+c;
A6: now
let t be 0-started State of SCMPDS, Q;
assume that
A7: P[t] and
A8: t.a=s.a & t.b > 0;
consider v be State of SCMPDS such that
A9: v= t and
A10: v.x>=v.y+c by A7;
thus IExec(J,Q,t).a=t.a & IExec(J,Q,t).b=t.b-n &
I is_closed_on t,Q & I is_halting_on t,Q by A5,A8,A9,A10;
thus P[Initialize IExec(J,Q,t) ]
proof
take v=Initialize IExec(J,Q,t);
thus v=Initialize IExec(J,Q,t);
v.x=IExec(J,Q,t).x by SCMPDS_5:15;
then v.x>=IExec(J,Q,t).y+c by A5,A8,A9,A10;
hence thesis by SCMPDS_5:15;
end;
end;
IExec(for-down(a,i,n,I),P,s)
= IExec(for-down(a,i,n,I),P,
Initialize IExec(I ';' AddTo(a,i,-n),P,s))
from ForDownExec(A1,A4,A3,A6);
hence thesis;
end;
theorem
for s being 0-started State of SCMPDS,I being halt-free shiftable Program of
SCMPDS , a be Int_position, i be Integer,n be Nat
st s.DataLoc(s.a,i) > 0 & n > 0 & a <> DataLoc(s.a,i) &
(for t be 0-started State of SCMPDS,Q st t.a=s.a
holds IExec(I,Q,t).a=t.a
& IExec(I,Q,t).DataLoc(s.a,i)=t.DataLoc(s.a,i) & I
is_closed_on t,Q & I is_halting_on t,Q) holds
for-down(a,i,n,I) is_closed_on s,P &
for-down(a,i,n,I) is_halting_on s,P
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS,
a be Int_position, i be Integer,n be Nat;
assume that
A1: s.DataLoc(s.a,i) > 0 & n > 0 & a <> DataLoc(s.a,i) and
A2: for t be 0-startedState of SCMPDS,Q
st t.a=s.a holds IExec(I,Q,t).a=t.a
& IExec(I,Q,t).DataLoc(s.a,i)=t.DataLoc(s.a,i) & I is_closed_on t,Q
& I is_halting_on t,Q;
for t being 0-started State of SCMPDS,Q st
(for x be Int_position st x in {} holds t.x=s.x) & t.a=s.a
holds IExec(I,Q,t).a=t.a
& IExec(I,Q,t).DataLoc(s.a,i)=t.DataLoc(
s.a,i) & I is_closed_on t,Q & I is_halting_on t,Q
& for y be Int_position st y in
{} holds IExec(I,Q,t).y=t.y by A2;
hence thesis by A1,SCMPDS_7:48;
end;
begin :: A Program for Insert Sort
:: n -> intpos 2, x1 -> intpos 3
definition
let n,p0 be Nat;
func insert-sort(n,p0) -> Program of SCMPDS 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;
end;
set j1= AddTo(GBP,3,1), j2= (GBP,4):=(GBP,3), j3= AddTo(GBP,1,1), j4= (GBP,6)
:=(GBP,1), k1= (GBP,5):=(intpos 4,-1), k2= SubFrom(GBP,5,intpos 4,0), k3= (GBP,
5):=(intpos 4,-1), k4= (intpos 4,-1):=(intpos 4,0), k5= (intpos 4,0 ):=(GBP,5),
k6= AddTo(GBP,4,-1), k7= AddTo(GBP,6,-1), FA= Load ((GBP,6):=0), 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)), IF= if>0(GBP,5, TR,FA), B1= ((GBP,
5):=(intpos 4,-1)) ';' (SubFrom(GBP,5,intpos 4,0)) ';' (if>0(GBP,5, TR,FA)),
WH = while>0(GBP,6,B1),
J4= j1 ';' j2 ';' j3 ';' j4, B2= J4 ';' WH, FR= for-down(
GBP,2,1,B2);
Lm4: card B1=10
proof
thus card B1=card (k1 ';' k2)+card IF by AFINSQ_1:17
.=2+card IF by SCMP_GCD:5
.=2+(card TR+card FA+2) by SCMPDS_6:65
.=2+(card (k3 ';' k4 ';' k5 ';' k6) +1+card FA+2) by SCMP_GCD:4
.=2+(card (k3 ';' k4 ';' k5)+1 +1+card FA+2) by SCMP_GCD:4
.=2+(card (k3 ';' k4)+1+1 +1+card FA+2) by SCMP_GCD:4
.=2+(2+1+1 +1+card FA+2) by SCMP_GCD:5
.=2+(2+1+1+1+1+2) by COMPOS_1:54
.=10;
end;
Lm5: card B2=16
proof
thus card B2=card (j1 ';' j2 ';' j3 ';' j4) + card WH by AFINSQ_1:17
.=card (j1 ';' j2 ';' j3)+1+ card WH by SCMP_GCD:4
.=card (j1 ';' j2 )+1+1+ card WH by SCMP_GCD:4
.=2+1+1+ card WH by SCMP_GCD:5
.=2+1+1+(10+2) by Lm4,SCMPDS_8:17
.=16;
end;
set a1=intpos 1, a2=intpos 2, a3=intpos 3, a4=intpos 4, a5=intpos 5,
a6=intpos 6;
Lm6: for s being 0-started State of SCMPDS
st s.a4 >= 7+s.a6 & s.GBP=0 & s.a6 > 0 holds
IExec(B1,P,s).GBP=0 & IExec(B1,P,s).a1=s.a1
proof
let s be 0-started State of SCMPDS;
set a=GBP, x=DataLoc(s.a4,-1), y=DataLoc(s.a4,0);
assume that
A1: s.a4 >= 7+s.a6 and
A2: s.a=0 and
A3: s.a6 > 0;
A4: 7+s.a6>7+0 by A3,XREAL_1:6;
set t0=s, t1=Exec(k1, t0), t2=IExec(k1 ';' k2,P,s),
Q2 = P;
A5: DataLoc(t0.a,5)=intpos (0+5) by A2,SCMP_GCD:1;
then
A6: t1.a=0 by A2,AMI_3:10,SCMPDS_2:47;
then
A7: DataLoc(t1.a,5)=intpos (0+5) by SCMP_GCD:1;
A8: t1.a4=s.a4 by A5,AMI_3:10,SCMPDS_2:47;
A9: s.a4>=1+(6+s.a6) by A1;
then
A10: s.a4-1 >= 6+s.a6 by XREAL_1:19;
set Fi= (a,6):=0, t02=Initialize t2, Q02 = Q2,
t3=IExec(k3 ';' k4 ';' k5 ';' k6,Q2,Initialize t2),
t4=IExec(k3 ';' k4 ';' k5,Q2,Initialize t2),
t5=IExec(k3 ';' k4,Q2,Initialize t2),
t6=Exec(k3,t02);
t2.a=Exec(k2,t1).a by SCMPDS_5:42
.=0 by A6,A7,AMI_3:10,SCMPDS_2:50;
then
A11: t02.a=0 by SCMPDS_5:15;
then
A12: DataLoc(t02.a,5)=intpos (0+5) by SCMP_GCD:1;
then
A13: t6.a=0 by A11,AMI_3:10,SCMPDS_2:47;
t2.a4=Exec(k2,t1).a4 by SCMPDS_5:42
.=s.a4 by A8,A7,AMI_3:10,SCMPDS_2:50;
then t02.a4=s.a4 by SCMPDS_5:15;
then
A14: t6.a4=s.a4 by A12,AMI_3:10,SCMPDS_2:47;
A15: 6+s.a6>6+0 by A3,XREAL_1:6;
then 0<>|.t6.a4+-1.| by A10,A14,ABSVALUE:def 1;
then
A16: a<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
s.a4-1 > 0 by A3,A9,XREAL_1:19;
then
A17: |.t6.a4+-1.| =s.a4-1 by A14,ABSVALUE:def 1;
then 4<>|.t6.a4+-1.| by A10,A15,XXREAL_0:2;
then
A18: a4<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
A19: t5.a4 =Exec(k4, t6).a4 by SCMPDS_5:42
.=s.a4 by A14,A18,SCMPDS_2:47;
then 0<>|.t5.a4+0 .| by A1,A4,ABSVALUE:def 1;
then
A20: a<>DataLoc(t5.a4,0) by XTUPLE_0:1;
A21: t5.a =Exec(k4, t6).a by SCMPDS_5:42
.=0 by A13,A16,SCMPDS_2:47;
A22: t4.a=Exec(k5,t5).a by SCMPDS_5:41
.=0 by A21,A20,SCMPDS_2:47;
then
A23: a<>DataLoc(t4.a,4) by AMI_3:10,SCMP_GCD:1;
A24: t1.a1=s.a1 by A5,AMI_3:10,SCMPDS_2:47;
t2.a1=Exec(k2, t1).a1 by SCMPDS_5:42
.=s.a1 by A24,A7,AMI_3:10,SCMPDS_2:50;
then
A25: t02.a1=s.a1 by SCMPDS_5:15;
then
A26: t6.a1=s.a1 by A12,AMI_3:10,SCMPDS_2:47;
A27: t3.a=Exec(k6,t4).a by SCMPDS_5:41
.=0 by A22,A23,SCMPDS_2:48;
then
A28: DataLoc(t3.a,6)=intpos (0+6) by SCMP_GCD:1;
A29: DataLoc(t02.a,6)=intpos (0+6) by A11,SCMP_GCD:1;
now
per cases;
suppose
(Initialize t2).DataLoc((Initialize t2).a,5) <= 0;
hence IExec(IF,Q2,Initialize t2).a=IExec(FA,Q2,Initialize t2).a
by SCMPDS_6:74
.=Exec(Fi,t02).a by SCMPDS_5:40
.=0 by A11,A29,AMI_3:10,SCMPDS_2:46;
end;
suppose (Initialize t2).DataLoc((Initialize t2).a,5) > 0;
hence IExec(IF,Q2,Initialize t2).a=IExec(TR,Q2,Initialize t2).a
by SCMPDS_6:73
.=Exec(k7,t3).a by SCMPDS_5:41
.=0 by A27,A28,AMI_3:10,SCMPDS_2:48;
end;
end;
hence IExec(B1,P,s).a=0 by SCMPDS_5:35;
A30: a1<>DataLoc(t4.a,4) by A22,AMI_3:10,SCMP_GCD:1;
|.t5.a4+0 .| = s.a4 by A1,A4,A19,ABSVALUE:def 1;
then 1<>|.t5.a4+0 .| by A1,A4,XXREAL_0:2;
then
A31: a1<>DataLoc(t5.a4,0) by XTUPLE_0:1;
1<>|.t6.a4+-1.| by A10,A15,A17,XXREAL_0:2;
then
A32: a1<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
A33: t5.a1 =Exec(k4, t6).a1 by SCMPDS_5:42
.=s.a1 by A26,A32,SCMPDS_2:47;
A34: t4.a1=Exec(k5,t5).a1 by SCMPDS_5:41
.=s.a1 by A33,A31,SCMPDS_2:47;
A35: t3.a1=Exec(k6,t4).a1 by SCMPDS_5:41
.=s.a1 by A34,A30,SCMPDS_2:48;
now
per cases;
suppose
(Initialize t2).DataLoc((Initialize t2).a,5) <= 0;
hence IExec(IF,Q2,Initialize t2).a1=IExec(FA,Q2,Initialize t2).a1
by SCMPDS_6:74
.=Exec(Fi,t02).a1 by SCMPDS_5:40
.=s.a1 by A25,A29,AMI_3:10,SCMPDS_2:46;
end;
suppose
(Initialize t2).DataLoc((Initialize t2).a,5) > 0;
hence IExec(IF,Q2,Initialize t2).a1=IExec(TR,Q2,Initialize t2).a1
by SCMPDS_6:73
.=Exec(k7,t3).a1 by SCMPDS_5:41
.=s.a1 by A35,A28,AMI_3:10,SCMPDS_2:48;
end;
end;
hence thesis by SCMPDS_5:35;
end;
Lm7: for s being 0-started State of SCMPDS
st s.a4 >= 7+s.a6 & s.GBP=0 & s.a6 > 0 holds
IExec(B1,P,s).a2=s.a2 & IExec(B1,P,s).a3=s.a3 &
IExec(B1,P,s).a6 < s.a6
& IExec(B1,P,s).a4 >= 7+IExec(B1,P,s).a6 & (for i be Nat
st i>=7 & i<>s.a4-1 & i<>s.a4 holds
IExec(B1,P,s).intpos i=s.intpos i) &
(s.DataLoc(s.a4,-1) > s.DataLoc(s.a4,0)
implies IExec(B1,P,s).DataLoc(s.a4,-1)=s.DataLoc(s.a4,0)
& IExec(B1,P,s).DataLoc(s.a4,0) =s.DataLoc(s.a4,-1)
& IExec(B1,P,s).a6=s.a6-1
& IExec(B1,P,s).a4=s.a4-1 )
& (s.DataLoc(s.a4,-1) <= s.DataLoc(s.a4,0)
implies IExec(B1,P,s).DataLoc(s.a4,-1)
=s.DataLoc(s.a4,-1) & IExec(B1,P,s).DataLoc(s.a4,0) =s.DataLoc(s.a4,0)
& IExec(B1,P,s).a6=0)
proof
let s be 0-started State of SCMPDS;
set a=GBP, x=DataLoc(s.a4,-1), y=DataLoc(s.a4,0);
assume that
A1: s.a4 >= 7+s.a6 and
A2: s.a=0 and
A3: s.a6 > 0;
set t0=s, t1=Exec(k1, t0),
t2=IExec(k1 ';' k2,P,s), Q2 = P;
A4: 7+s.a6>7+0 by A3,XREAL_1:6;
then
A5: |.s.a4.|=s.a4 by A1,ABSVALUE:def 1;
set Fi= (a,6):=0, t02=Initialize t2, Q02 = Q2,
t3=IExec(k3 ';' k4 ';' k5 ';' k6,Q2,Initialize t2),
t4=IExec(k3 ';' k4 ';' k5,Q2,Initialize t2),
t5=IExec(k3 ';' k4,Q2,Initialize t2),
t6=Exec(k3, t02);
A6: DataLoc(t0.a,5)=intpos (0+5) by A2,SCMP_GCD:1;
then
A7: t1.a=0 by A2,AMI_3:10,SCMPDS_2:47;
then
A8: DataLoc(t1.a,5)=intpos (0+5) by SCMP_GCD:1;
then
A9: |.t1.a+5.|=0+5 by XTUPLE_0:1;
then |.s.a4+0.|<>|.t1.a+5.| by A1,A4,A5,XXREAL_0:2;
then
A10: y<>DataLoc(t1.a,5) by XTUPLE_0:1;
A11: |.t0.a+5.|=0+5 by A6,XTUPLE_0:1;
then |.s.a4+0.|<>|.t0.a+5.| by A1,A4,A5,XXREAL_0:2;
then t0.y=s.y & y<>DataLoc(t0.a,5) by XTUPLE_0:1;
then
A12: t1.y=s.y by SCMPDS_2:47;
A13: t1.a5=s.x by A6,SCMPDS_2:47;
A14: t1.a4=s.a4 by A6,AMI_3:10,SCMPDS_2:47;
t2.y=Exec(k2, t1).y by SCMPDS_5:42
.=s.y by A12,A10,SCMPDS_2:50;
then
A15: t02.y=s.y by SCMPDS_5:15;
A16: t02.a = t2.a by SCMPDS_5:15
.=Exec(k2, t1).a by SCMPDS_5:42
.=0 by A7,A8,AMI_3:10,SCMPDS_2:50;
A17: DataLoc(t02.a,5)=intpos (0+5) by A16,SCMP_GCD:1;
then
A18: t6.a=0 by A16,AMI_3:10,SCMPDS_2:47;
|.t02.a+5.|=0+5 by A17,XTUPLE_0:1;
then |.s.a4+0.|<>|.t02.a+5.| by A1,A4,A5,XXREAL_0:2;
then y<>DataLoc(t02.a,5) by XTUPLE_0:1;
then
A19: t6.y=s.y by A15,SCMPDS_2:47;
t2.a4=Exec(k2, t1).a4 by SCMPDS_5:42
.=s.a4 by A14,A8,AMI_3:10,SCMPDS_2:50;
then
A20: t02.a4=s.a4 by SCMPDS_5:15;
then
A21: t6.a4=s.a4 by A17,AMI_3:10,SCMPDS_2:47;
then
A22: t5.x =Exec(k4, t6).DataLoc(t6.a4,-1) by SCMPDS_5:42
.=s.y by A21,A19,SCMPDS_2:47;
A23: t1.a3=s.a3 by A6,AMI_3:10,SCMPDS_2:47;
t2.a3=Exec(k2, t1).a3 by SCMPDS_5:42
.=s.a3 by A23,A8,AMI_3:10,SCMPDS_2:50;
then
A24: t02.a3=s.a3 by SCMPDS_5:15;
then
A25: t6.a3=s.a3 by A17,AMI_3:10,SCMPDS_2:47;
A26: s.a4>=1+(6+s.a6) by A1;
then
A27: s.a4-1 >= 6+s.a6 by XREAL_1:19;
A28: t1.a2=s.a2 by A6,AMI_3:10,SCMPDS_2:47;
t2.a2=Exec(k2, t1).a2 by SCMPDS_5:42
.=s.a2 by A28,A8,AMI_3:10,SCMPDS_2:50;
then
A29: t02.a2=s.a2 by SCMPDS_5:15;
then
A30: t6.a2=s.a2 by A17,AMI_3:10,SCMPDS_2:47;
A31: t1.a6=s.a6 by A6,AMI_3:10,SCMPDS_2:47;
t2.a6=Exec(k2, t1).a6 by SCMPDS_5:42
.=s.a6 by A31,A8,AMI_3:10,SCMPDS_2:50;
then t02.a6=s.a6 by SCMPDS_5:15;
then
A32: t6.a6=s.a6 by A17,AMI_3:10,SCMPDS_2:47;
A33: DataLoc(t02.a,6)=intpos (0+6) by A16,SCMP_GCD:1;
A34: now
assume
t02.DataLoc(t02.a,5) <= 0;
then IExec(IF,Q2,Initialize t2).a6=IExec(FA,Q2,Initialize t2).a6
by SCMPDS_6:74
.=Exec(Fi,t02).a6 by SCMPDS_5:40
.=0 by A33,SCMPDS_2:46;
hence IExec(B1,P,s).a6 =0 by SCMPDS_5:35;
end;
A35: 6+s.a6>6+0 by A3,XREAL_1:6;
then 0<>|.t6.a4+-1.| by A27,A21,ABSVALUE:def 1;
then
A36: a<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
A37: s.a4-1 > 0 by A3,A26,XREAL_1:19;
then
A38: |.t6.a4+-1.| =s.a4-1 by A21,ABSVALUE:def 1;
then 4<>|.t6.a4+-1.| by A27,A35,XXREAL_0:2;
then
A39: a4<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
A40: t5.a4 =Exec(k4, t6).a4 by SCMPDS_5:42
.=s.a4 by A21,A39,SCMPDS_2:47;
then
A41: |.t5.a4+0 .| = s.a4 by A1,A4,ABSVALUE:def 1;
then 4<>|.t5.a4+0 .| by A1,A4,XXREAL_0:2;
then
A42: a4<>DataLoc(t5.a4,0) by XTUPLE_0:1;
3<>|.t6.a4+-1.| by A27,A35,A38,XXREAL_0:2;
then
A43: a3<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
3<>|.t5.a4+0 .| by A1,A4,A41,XXREAL_0:2;
then
A44: a3<>DataLoc(t5.a4,0) by XTUPLE_0:1;
A45: t5.a3 =Exec(k4, t6).a3 by SCMPDS_5:42
.=s.a3 by A25,A43,SCMPDS_2:47;
A46: t4.a3=Exec(k5,t5).a3 by SCMPDS_5:41
.=s.a3 by A45,A44,SCMPDS_2:47;
2<>|.t5.a4+0 .| by A1,A4,A41,XXREAL_0:2;
then
A47: a2<>DataLoc(t5.a4,0) by XTUPLE_0:1;
A48: t4.a4=Exec(k5,t5).a4 by SCMPDS_5:41
.=s.a4 by A40,A42,SCMPDS_2:47;
A49: t5.a =Exec(k4, t6).a by SCMPDS_5:42
.=0 by A18,A36,SCMPDS_2:47;
A50: 2*|.(s.a4+-1).|+1=2*(s.a4-1)+1 by A27,A35,ABSVALUE:def 1;
then |.s.a4+-1.|<>|.t1.a+5.| by A3,A27,A9,XREAL_1:6;
then
A51: x<>DataLoc(t1.a,5) by XTUPLE_0:1;
0<>|.t5.a4+0 .| by A1,A4,A40,ABSVALUE:def 1;
then
A52: a<>DataLoc(t5.a4,0) by XTUPLE_0:1;
A53: t4.a=Exec(k5,t5).a by SCMPDS_5:41
.=0 by A49,A52,SCMPDS_2:47;
then
A54: a<>DataLoc(t4.a,4) by AMI_3:10,SCMP_GCD:1;
2<>|.t6.a4+-1.| by A27,A35,A38,XXREAL_0:2;
then
A55: a2<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
A56: t5.a2 =Exec(k4, t6).a2 by SCMPDS_5:42
.=s.a2 by A30,A55,SCMPDS_2:47;
A57: t4.a2=Exec(k5,t5).a2 by SCMPDS_5:41
.=s.a2 by A56,A47,SCMPDS_2:47;
A58: a2<>DataLoc(t4.a,4) by A53,AMI_3:10,SCMP_GCD:1;
t3.a=Exec(k6,t4).a by SCMPDS_5:41
.=0 by A53,A54,SCMPDS_2:48;
then
A59: DataLoc(t3.a,6)=intpos (0+6) by SCMP_GCD:1;
then
A60: |.t3.a+6.|=0+6 by XTUPLE_0:1;
A61: DataLoc(t4.a,4)=intpos (0+4) by A53,SCMP_GCD:1;
then
A62: |.t4.a+4.|=0+4 by XTUPLE_0:1;
then |.s.a4+-1.|<>|.t4.a+4.| by A27,A35,A50,XXREAL_0:2;
then
A63: x<>DataLoc(t4.a,4) by XTUPLE_0:1;
A64: t3.a2=Exec(k6,t4).a2 by SCMPDS_5:41
.=s.a2 by A57,A58,SCMPDS_2:48;
now
per cases;
suppose
t02.DataLoc(t02.a,5) <= 0;
hence IExec(IF,Q2,Initialize t2).a2=IExec(FA,Q2,Initialize t2).a2
by SCMPDS_6:74
.=Exec(Fi,t02).a2 by SCMPDS_5:40
.=s.a2 by A29,A33,AMI_3:10,SCMPDS_2:46;
end;
suppose
t02.DataLoc(t02.a,5) > 0;
hence IExec(IF,Q2,Initialize t2).a2=IExec(TR,Q2,Initialize t2).a2
by SCMPDS_6:73
.=Exec(k7,t3).a2 by SCMPDS_5:41
.=s.a2 by A64,A59,AMI_3:10,SCMPDS_2:48;
end;
end;
hence IExec(B1,P,s).a2=s.a2 by SCMPDS_5:35;
A65: a3<>DataLoc(t4.a,4) by A53,AMI_3:10,SCMP_GCD:1;
A66: t3.a3=Exec(k6,t4).a3 by SCMPDS_5:41
.=s.a3 by A46,A65,SCMPDS_2:48;
now
per cases;
suppose
t02.DataLoc(t02.a,5) <= 0;
hence IExec(IF,Q2,Initialize t2).a3=IExec(FA,Q2,Initialize t2).a3
by SCMPDS_6:74
.=Exec(Fi,t02).a3 by SCMPDS_5:40
.=s.a3 by A24,A33,AMI_3:10,SCMPDS_2:46;
end;
suppose
t02.DataLoc(t02.a,5) > 0;
hence IExec(IF,Q2,Initialize t2).a3=IExec(TR,Q2,Initialize t2).a3
by SCMPDS_6:73
.=Exec(k7,t3).a3 by SCMPDS_5:41
.=s.a3 by A66,A59,AMI_3:10,SCMPDS_2:48;
end;
end;
hence IExec(B1,P,s).a3=s.a3 by SCMPDS_5:35;
A67: a6<>DataLoc(t4.a,4) by A53,AMI_3:10,SCMP_GCD:1;
6<>|.t6.a4+-1.| by A26,A35,A38,XREAL_1:19;
then
A68: a6<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
A69: t5.a6 =Exec(k4, t6).a6 by SCMPDS_5:42
.=s.a6 by A32,A68,SCMPDS_2:47;
6<>|.t5.a4+0 .| by A1,A4,A41,XXREAL_0:2;
then
A70: a6<>DataLoc(t5.a4,0) by XTUPLE_0:1;
A71: t4.a6=Exec(k5,t5).a6 by SCMPDS_5:41
.=s.a6 by A69,A70,SCMPDS_2:47;
A72: t3.a6=Exec(k6,t4).a6 by SCMPDS_5:41
.=s.a6 by A71,A67,SCMPDS_2:48;
A73: t3.a4=Exec(k6,t4).a4 by SCMPDS_5:41
.=t4.a4+-1 by A61,SCMPDS_2:48
.=s.a4-1 by A48;
A74: now
assume
A75: t02.DataLoc(t02.a,5) > 0;
then IExec(IF,Q2,Initialize t2).a6=IExec(TR,Q2,Initialize t2).a6
by SCMPDS_6:73
.=Exec(k7,t3).a6 by SCMPDS_5:41
.=s.a6+ -1 by A72,A59,SCMPDS_2:48
.=s.a6-1;
hence IExec(B1,P,s).a6=s.a6-1 by SCMPDS_5:35;
IExec(IF,Q2,Initialize t2).a4=IExec(TR,Q2,Initialize t2).a4
by A75,SCMPDS_6:73
.=Exec(k7,t3).a4 by SCMPDS_5:41
.=s.a4-1 by A73,A59,AMI_3:10,SCMPDS_2:48;
hence IExec(B1,P,s).a4=s.a4-1 by SCMPDS_5:35;
end;
hereby
per cases;
suppose
t02.DataLoc(t02.a,5) <= 0;
hence IExec(B1,P,s).a6 < s.a6 by A3,A34;
end;
suppose
t02.DataLoc(t02.a,5) > 0;
hence IExec(B1,P,s).a6 < s.a6 by A74,XREAL_1:146;
end;
end;
hereby
per cases;
suppose
A76: t02.DataLoc(t02.GBP,5) <= 0;
then IExec(IF,Q2,Initialize t2).a4=IExec(FA,Q2,Initialize t2).a4
by SCMPDS_6:74
.=Exec(Fi,t02).a4 by SCMPDS_5:40
.=s.a4 by A20,A33,AMI_3:10,SCMPDS_2:46;
then IExec(B1,P,s).a4=s.a4 by SCMPDS_5:35;
hence IExec(B1,P,s).a4 >= 7+IExec(B1,P,s).a6
by A1,A4,A34,A76,XXREAL_0:2;
end;
suppose
A77: t02.DataLoc(t02.a,5) > 0;
s.a4-1 >= 7+s.a6-1 by A1,XREAL_1:9;
hence IExec(B1,P,s).a4 >= 7+IExec(B1,P,s).a6
by A74,A77;
end;
end;
A78: now
let i be Nat;
assume that
A79: i>=7 and
i<>s.a4-1 and
i <> s.a4;
i>5 by A79,XXREAL_0:2;
hence t1.intpos i =s.intpos i by A6,AMI_3:10,SCMPDS_2:47;
end;
A80: now
let i be Nat;
assume that
A81: i>=7 and
A82: i<>s.a4-1 & i <> s.a4;
A83: i>5 by A81,XXREAL_0:2;
thus t2.intpos i=Exec(k2, t1).intpos i by SCMPDS_5:42
.=t1.intpos i by A8,A83,AMI_3:10,SCMPDS_2:50
.=s.intpos i by A78,A81,A82;
end;
A84: now
let i be Nat;
assume that
A85: i>=7 and
A86: i<>s.a4-1 & i <> s.a4;
i>5 by A85,XXREAL_0:2;
hence t6.intpos i=t02.intpos i by A17,AMI_3:10,SCMPDS_2:47
.=t2.intpos i by SCMPDS_5:15
.=s.intpos i by A80,A85,A86;
end;
A87: now
let i be Nat;
assume that
A88: i>=7 and
A89: i<>s.a4-1 and
A90: i <> s.a4;
A91: intpos i <> DataLoc(t6.a4,-1)
proof
assume
intpos i=DataLoc(t6.a4,-1);
then i =|.t6.a4+-1.| by XTUPLE_0:1;
hence contradiction by A37,A21,A89,ABSVALUE:def 1;
end;
thus t5.intpos i=Exec(k4, t6).intpos i by SCMPDS_5:42
.=t6.intpos i by A91,SCMPDS_2:47
.=s.intpos i by A84,A88,A89,A90;
end;
A92: now
let i be Nat;
assume that
A93: i>=7 & i<>s.a4-1 and
A94: i <> s.a4;
A95: intpos i <> DataLoc(t5.a4,0)
proof
assume
intpos i=DataLoc(t5.a4,0);
then i=|.t5.a4+0 .| by XTUPLE_0:1;
hence contradiction by A1,A4,A40,A94,ABSVALUE:def 1;
end;
thus t4.intpos i=Exec(k5, t5).intpos i by SCMPDS_5:41
.=t5.intpos i by A95,SCMPDS_2:47
.=s.intpos i by A87,A93,A94;
end;
A96: now
let i be Nat;
assume that
A97: i>=7 and
A98: i<>s.a4-1 & i <> s.a4;
i>4 by A97,XXREAL_0:2;
then
A99: intpos i <> DataLoc(t4.a,4) by A53,AMI_3:10,SCMP_GCD:1;
thus t3.intpos i=Exec(k6, t4).intpos i by SCMPDS_5:41
.=t4.intpos i by A99,SCMPDS_2:48
.=s.intpos i by A92,A97,A98;
end;
hereby
let i be Nat;
set xi=intpos i;
assume that
A100: i>=7 and
A101: i<>s.a4-1 & i <> s.a4;
A102: i>6 by A100,XXREAL_0:2;
per cases;
suppose
t02.DataLoc(t02.a,5) <= 0;
then IExec(IF,Q2,Initialize t2).xi=IExec(FA,Q2,Initialize t2).xi
by SCMPDS_6:74
.=Exec(Fi,t02).xi by SCMPDS_5:40
.=t02.xi by A33,A102,AMI_3:10,SCMPDS_2:46
.=t2.xi by SCMPDS_5:15
.=s.xi by A80,A100,A101;
hence IExec(B1,P,s).xi=s.xi by SCMPDS_5:35;
end;
suppose
t02.DataLoc(t02.a,5) > 0;
then IExec(IF,Q2,Initialize t2).xi=IExec(TR,Q2,Initialize t2).xi
by SCMPDS_6:73
.=Exec(k7,t3).xi by SCMPDS_5:41
.=t3.xi by A59,A102,AMI_3:10,SCMPDS_2:48
.=s.xi by A96,A100,A101;
hence IExec(B1,P,s).xi=s.xi by SCMPDS_5:35;
end;
end;
A103: t02.a5 = t2.a5 by SCMPDS_5:15
.=Exec(k2, t1).a5 by SCMPDS_5:42
.=s.x-s.y by A14,A13,A12,A8,SCMPDS_2:50;
then
A104: t02.DataLoc(t02.a,5)=s.x-s.y by A16,SCMP_GCD:1;
|.s.a4+-1.|<>|.t0.a+5.| by A3,A27,A50,A11,XREAL_1:6;
then x<>DataLoc(t0.a,5) by XTUPLE_0:1;
then
A105: t1.x=s.x by SCMPDS_2:47;
t2.x=Exec(k2, t1).x by SCMPDS_5:42
.=s.x by A105,A51,SCMPDS_2:50;
then
A106: t02.x=s.x by SCMPDS_5:15;
then
A107: t6.a5=s.x by A20,A17,SCMPDS_2:47;
5<>|.t6.a4+-1.| by A27,A35,A38,XXREAL_0:2;
then
A108: a5<>DataLoc(t6.a4,-1) by XTUPLE_0:1;
A109: t5.a5 =Exec(k4, t6).a5 by SCMPDS_5:42
.=s.x by A107,A108,SCMPDS_2:47;
|.s.a4+0.|<>|.t4.a+4.| by A1,A4,A5,A62,XXREAL_0:2;
then
A110: y<>DataLoc(t4.a,4) by XTUPLE_0:1;
A111: t4.y =Exec(k5, t5).DataLoc(t5.a4,0) by A40,SCMPDS_5:41
.=t5.DataLoc(t5.a,5) by SCMPDS_2:47
.=s.x by A49,A109,SCMP_GCD:1;
A112: t3.y=Exec(k6, t4).y by SCMPDS_5:41
.=s.x by A111,A110,SCMPDS_2:48;
|.s.a4+-1.|<>|.t5.a4+0 .| by A50,A41;
then
A113: x<>DataLoc(t5.a4,0) by XTUPLE_0:1;
A114: t4.x=Exec(k5,t5).x by SCMPDS_5:41
.=s.y by A22,A113,SCMPDS_2:47;
A115: t3.x=Exec(k6, t4).x by SCMPDS_5:41
.=s.y by A114,A63,SCMPDS_2:48;
hereby
A116: x<>DataLoc(t3.a,6) by A27,A35,A50,A59,XTUPLE_0:1;
assume
s.x > s.y;
then
A117: s.x-s.y > s.y-s.y by XREAL_1:9;
then IExec(IF,Q2,Initialize t2).x=IExec(TR,Q2,Initialize t2).x
by A104,SCMPDS_6:73
.=Exec(k7,t3).x by SCMPDS_5:41
.=s.y by A115,A116,SCMPDS_2:48;
hence IExec(B1,P,s).x=s.y by SCMPDS_5:35;
|.s.a4+0.|<>|.t3.a+6.| by A1,A4,A5,A60,XXREAL_0:2;
then
A118: y<>DataLoc(t3.a,6) by XTUPLE_0:1;
IExec(IF,Q2,Initialize t2).y=IExec(TR,Q2,Initialize t2).y
by A104,A117,SCMPDS_6:73
.=Exec(k7,t3).y by SCMPDS_5:41
.=s.x by A112,A118,SCMPDS_2:48;
hence IExec(B1,P,s).y=s.x by SCMPDS_5:35;
thus IExec(B1,P,s).a6=s.a6-1 &
IExec(B1,P,s).a4=s.a4-1
by A16,A103,A74,A117,SCMP_GCD:1;
end;
A119: |.t02.a+6.|=0+6 by A33,XTUPLE_0:1;
hereby
A120: x<>DataLoc(t02.a,6) by A27,A35,A50,A33,XTUPLE_0:1;
assume
s.x <= s.y;
then
A121: s.x-s.y <= s.y-s.y by XREAL_1:9;
then IExec(IF,Q2,Initialize t2).x=IExec(FA,Q2,Initialize t2).x
by A104,SCMPDS_6:74
.=Exec(Fi,t02).x by SCMPDS_5:40
.=s.x by A106,A120,SCMPDS_2:46;
hence IExec(B1,P,s).x=s.x by SCMPDS_5:35;
|.s.a4+0.|<>|.t02.a+6.| by A1,A4,A5,A119,XXREAL_0:2;
then
A122: y<>DataLoc(t02.a,6) by XTUPLE_0:1;
IExec(IF,Q2,Initialize t2).y=IExec(FA,Q2,Initialize t2).y
by A104,A121,SCMPDS_6:74
.=Exec(Fi,t02).y by SCMPDS_5:40
.=s.y by A15,A122,SCMPDS_2:46;
hence IExec(B1,P,s).y=s.y by SCMPDS_5:35;
thus IExec(B1,P,s).a6 =0 by A16,A103,A34,A121,SCMP_GCD:1;
end;
end;
Lm8: for s being 0-started State of SCMPDS
st s.a4 >= 7+s.DataLoc(s.GBP,6) & s.GBP=0
holds WH is_closed_on s,P & WH is_halting_on s,P
proof
let s be 0-started State of SCMPDS;
set a=GBP, b=DataLoc(s.a,6);
assume that
A1: s.a4 >= 7+s.b and
A2: s.a=0;
A3: b=intpos(0+6) by A2,SCMP_GCD:1;
A4: now
let t be 0-started State of SCMPDS;
let Q;
assume that
A5: for x st x in {a4} holds t.x >= 7+t.b and
A6: t.a=s.a & t.b >0;
set Bt=IExec(B1,Q,t);
A7: a4 in {a4} by TARSKI:def 1;
then
A8: t.a4 >= 7+t.a6 by A3,A5;
hence IExec(B1,Q,t).a=t.a by A2,A3,A6,Lm6;
thus B1 is_closed_on t,Q & B1 is_halting_on t,Q by SCMPDS_6:20,21;
thus IExec(B1,Q,t).b < t.b by A2,A3,A6,A8,Lm7;
t.a4 >= 7+t.b by A5,A7;
then Bt.a4 >= 7+Bt.a6 by A2,A3,A6,Lm7;
hence for x st x in {a4} holds IExec(B1,Q,t).x >=
7+IExec(B1,Q,t).b by A3,TARSKI:def 1;
end;
for x st x in {a4} holds s.x >= 7+s.b by A1,TARSKI:def 1;
hence thesis by A4,SCMPDS_8:29;
end;
Lm9: for s being 0-started State of SCMPDS
st s.a4 >= 7+s.DataLoc(s.GBP,6) & s.GBP=0
holds IExec(WH,P,s).GBP=0 & IExec(WH,P,s).a1=s.a1 &
IExec(WH,P,s).a2=s.a2 & IExec(WH,P,s).a3=s.a3
proof
let s be 0-started State of SCMPDS;
set b=DataLoc(s.GBP,6), a=GBP;
assume that
A1: s.a4 >= 7+s.b and
A2: s.a=0;
A3: b=intpos (0+6) by A2,SCMP_GCD:1;
defpred P[Nat] means for t be 0-started State of SCMPDS,Q
st t.a6 <= $1 & t.a4 >= 7+t.a6
& t.a=0 holds IExec(WH,Q,t).a=0 &
IExec(WH,Q,t).a1=t.a1 & IExec(WH,Q,t).a2=t.a2 &
IExec(WH,Q,t).a3=t.a3;
A4: P[0 qua Nat]
proof
let t be 0-started State of SCMPDS, Q;
assume that
A5: t.a6 <= 0 and
t.a4 >= 7+t.a6 and
A6: t.a=0;
A7: DataLoc(t.a,6)=intpos (0+6) by A6,SCMP_GCD:1;
hence IExec(WH,Q,t).a=0 by A5,A6,SCMPDS_8:23;
thus thesis by A5,A7,SCMPDS_8:23;
end;
A8: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A9: P[k];
thus P[k+1]
proof
let t be 0-started State of SCMPDS, Q;
set bt=DataLoc(t.a,6);
assume that
A10: t.a6 <= k+1 and
A11: t.a4 >= 7+t.a6 and
A12: t.a=0;
A13: bt=intpos (0+6) by A12,SCMP_GCD:1;
per cases;
suppose
t.bt <= 0;
hence thesis by A12,SCMPDS_8:23;
end;
suppose
A14: t.bt > 0;
A15:
(for v be 0-started State of SCMPDS,Q st
(for x st x in {a4} holds v.x >= 7+v.DataLoc(t.GBP,6)) & v.GBP=t.GBP &
v.DataLoc(t.GBP,6) > 0
holds
IExec(B1,Q,v).GBP=v.GBP & B1 is_closed_on v,Q & B1 is_halting_on v,Q
& IExec(B1,Q,v).DataLoc(t.GBP,6) < v.DataLoc(t.GBP,6) & for x st x in {a4}
holds IExec(B1,Q,v).x >= 7+IExec(B1,Q,v).DataLoc(t.GBP,6))
proof
let v be 0-started State of SCMPDS;
let V;
A16: Initialize v = v by MEMSTR_0:44;
assume that
A17: for x st x in {a4} holds v.x >= 7+v.bt and
A18: v.a=t.a & v.bt > 0;
set Iv=IExec(B1,V,Initialize Initialize v);
A19: v.a = (Initialize v).a by SCMPDS_5:15;
A20: v.a4 = (Initialize v).a4 by SCMPDS_5:15;
A21: v.a6 = (Initialize v).a6 by SCMPDS_5:15;
A22: a4 in {a4} by TARSKI:def 1;
then
A23: v.a4 >= 7+v.a6 by A13,A17;
hence IExec(B1,V,v).a=v.a
by A12,A13,A18,Lm6;
thus B1 is_closed_on v,V & B1 is_halting_on v,V by SCMPDS_6:20,21;
thus IExec(B1,V,v).bt < v.bt
by A12,A13,A18,A23,Lm7;
v.a4 >= 7+v.bt by A17,A22;
then Iv.a4 >= 7+Iv.a6 by A12,A13,A18,Lm7,A19,A20,A21;
hence for x st x in {a4}
holds IExec(B1,V,v).x >= 7+IExec(B1,V,v).bt
by A13,A16,TARSKI:def 1;
end;
set It=IExec(B1,Q,t), IT = Q;
A24: It.a1 = (Initialize It).a1 by SCMPDS_5:15;
A25: It.a6 = (Initialize It).a6 by SCMPDS_5:15;
A26: It.a4 = (Initialize It).a4 by SCMPDS_5:15;
A27: It.GBP = (Initialize It).GBP by SCMPDS_5:15;
A28: It.a2 = (Initialize It).a2 by SCMPDS_5:15;
A29: It.a3 = (Initialize It).a3 by SCMPDS_5:15;
It.a6 < t.a6 by A11,A12,A13,A14,Lm7;
then It.a6 +1 <= t.a6 by INT_1:7;
then It.a6 +1 <= k+1 by A10,XXREAL_0:2;
then
A30: It.a6 <= k by XREAL_1:6;
A31: It.GBP=0 & It.a4 >= 7+It.a6 by A11,A12,A13,A14,Lm6,Lm7;
then
A32: IExec(WH,IT,Initialize It).a1=It.a1 by A9,A30,A24,A25,A26,A27;
A33: IExec(WH,IT,Initialize It).a3=It.a3 by A9,A31,A30,A25,A26,A27,A29;
A34: IExec(WH,IT,Initialize It).a2=It.a2 by A9,A31,A30,A25,A26,A27,A28;
A35: for x st x in {a4} holds t.x >= 7+t.bt by A11,A13,TARSKI:def 1;
IExec(WH,IT,Initialize It).a=0 by A9,A31,A30,A25,A26,A27;
hence IExec(WH,Q,t).a=0 by A14,A35,A15,SCMPDS_8:29;
It.a1=t.a1 by A11,A12,A13,A14,Lm6;
hence IExec(WH,Q,t).a1=t.a1
by A14,A35,A15,A32,SCMPDS_8:29;
It.a2=t.a2 by A11,A12,A13,A14,Lm7;
hence IExec(WH,Q,t).a2=t.a2
by A14,A35,A15,A34,SCMPDS_8:29;
It.a3=t.a3 by A11,A12,A13,A14,Lm7;
hence thesis by A14,A35,A15,A33,SCMPDS_8:29;
end;
end;
end;
per cases;
suppose
s.a6 <= 0;
hence thesis by A2,A3,SCMPDS_8:23;
end;
suppose
s.a6 > 0;
then reconsider m=s.a6 as Element of NAT by INT_1:3;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A8);
then P[m];
hence thesis by A1,A2,A3;
end;
end;
Lm10: for s being 0-started State of SCMPDS
st s.GBP=0 holds IExec(J4,P,s).GBP =0 &
IExec(J4,P,s).a1 = s.a1+1 &
IExec(J4,P,s).a2=s.a2 &
IExec(J4,P,s).a3 =s.a3+1 & IExec(J4,P,s).
a4 =s.a3+1 & IExec(J4,P,s).a6 =s.a1+1
& for i be Nat st i >= 7 holds
IExec(J4,P,s).intpos i=s.intpos i
proof
set a=GBP;
let s be 0-started State of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
set t0=Initialize s, t1=IExec(J4,P,s),
t2=IExec(j1 ';' j2 ';' j3,P,s), t3=IExec(j1 ';' j2,P,s), t4=Exec(j1,s);
assume
A2: s.a=0;
then
A3: t0.a=0 by SCMPDS_5:15;
then
A4: DataLoc(t0.a,3)=intpos (0+3) by SCMP_GCD:1;
then
A5: t4.a=0 by A3,A2,AMI_3:10,SCMPDS_2:48;
then
A6: DataLoc(t4.a,4)=intpos (0+4) by SCMP_GCD:1;
A7: t4.a2=s.a2 by A4,A2,A3,AMI_3:10,SCMPDS_2:48;
A8: t3.a2 =Exec(j2, t4).a2 by SCMPDS_5:42
.=s.a2 by A7,A6,AMI_3:10,SCMPDS_2:47;
A9: t4.a1=s.a1 by A4,A2,A3,AMI_3:10,SCMPDS_2:48;
A10: t3.a1 =Exec(j2, t4).a1 by SCMPDS_5:42
.=s.a1 by A9,A6,AMI_3:10,SCMPDS_2:47;
A11: t4.a3=s.a3+1 by A4,A1,SCMPDS_2:48;
A12: t3.a =Exec(j2, t4).a by SCMPDS_5:42
.=0 by A5,A6,AMI_3:10,SCMPDS_2:47;
then
A13: DataLoc(t3.a,1)=intpos (0+1) by SCMP_GCD:1;
A14: DataLoc(t4.a,3)=intpos (0+3) by A5,SCMP_GCD:1;
A15: t3.a4 =Exec(j2,t4).a4 by SCMPDS_5:42
.=s.a3+1 by A11,A6,A14,SCMPDS_2:47;
A16: t2.a4 =Exec(j3, t3).a4 by SCMPDS_5:41
.=s.a3+1 by A15,A13,AMI_3:10,SCMPDS_2:48;
A17: t2.a2 =Exec(j3, t3).a2 by SCMPDS_5:41
.=s.a2 by A8,A13,AMI_3:10,SCMPDS_2:48;
A18: t2.a1 =Exec(j3, t3).a1 by SCMPDS_5:41
.=s.a1+1 by A10,A13,SCMPDS_2:48;
A19: t3.a3 =Exec(j2, t4).a3 by SCMPDS_5:42
.=s.a3+1 by A11,A6,AMI_3:10,SCMPDS_2:47;
A20: t2.a3 =Exec(j3, t3).a3 by SCMPDS_5:41
.=s.a3+1 by A19,A13,AMI_3:10,SCMPDS_2:48;
A21: t2.a =Exec(j3, t3).a by SCMPDS_5:41
.=0 by A12,A13,AMI_3:10,SCMPDS_2:48;
then
A22: DataLoc(t2.a,6)=intpos (0+6) by SCMP_GCD:1;
thus t1.a =Exec(j4, t2).a by SCMPDS_5:41
.=0 by A21,A22,AMI_3:10,SCMPDS_2:47;
thus t1.a1 =Exec(j4, t2).a1 by SCMPDS_5:41
.=s.a1+1 by A18,A22,AMI_3:10,SCMPDS_2:47;
thus t1.a2 =Exec(j4, t2).a2 by SCMPDS_5:41
.=s.a2 by A17,A22,AMI_3:10,SCMPDS_2:47;
A23: DataLoc(t2.a,1)=intpos (0+1) by A21,SCMP_GCD:1;
thus t1.a3 =Exec(j4, t2).a3 by SCMPDS_5:41
.=s.a3+1 by A20,A22,AMI_3:10,SCMPDS_2:47;
thus t1.a4 =Exec(j4, t2).a4 by SCMPDS_5:41
.=s.a3+1 by A16,A22,AMI_3:10,SCMPDS_2:47;
thus t1.a6 =Exec(j4, t2).a6 by SCMPDS_5:41
.=s.a1+1 by A18,A22,A23,SCMPDS_2:47;
A24: now
let i be Nat;
assume
i >= 7;
then i > 3 by XXREAL_0:2;
hence t4.intpos i=t0.intpos i by A4,A1,AMI_3:10,SCMPDS_2:48
.=s.intpos i by SCMPDS_5:15;
end;
A25: now
let i be Nat;
assume
A26: i >= 7;
then
A27: i > 4 by XXREAL_0:2;
thus t3.intpos i =Exec(j2, t4).intpos i by SCMPDS_5:42
.=t4.intpos i by A6,A27,AMI_3:10,SCMPDS_2:47
.=s.intpos i by A24,A26;
end;
A28: now
let i be Nat;
assume
A29: i >= 7;
then
A30: i > 1 by XXREAL_0:2;
thus t2.intpos i =Exec(j3, t3).intpos i by SCMPDS_5:41
.=t3.intpos i by A13,A30,AMI_3:10,SCMPDS_2:48
.=s.intpos i by A25,A29;
end;
hereby
let i be Nat;
assume
A31: i >= 7;
then
A32: i > 6 by XXREAL_0:2;
thus t1.intpos i =Exec(j4, t2).intpos i by SCMPDS_5:41
.=t2.intpos i by A22,A32,AMI_3:10,SCMPDS_2:47
.=s.intpos i by A28,A31;
end;
end;
set jf=AddTo(GBP,2,-1), B3=B2 ';' jf;
Lm11: for s being 0-started State of SCMPDS
st s.a3 >= s.a1+7 & s.GBP=0 holds IExec(B3,P,s).GBP=0 &
IExec(B3,P,s).a2=s.a2-1 & IExec(B3,P,s).a3=s.a3+1 &
IExec(B3,P,s).a1=s.a1+1
& for i be Nat st i <> 2
holds IExec(B3,P,s).intpos i
=IExec(WH,P,Initialize IExec(J4,P,s)).intpos i
proof
set a=GBP;
let s be 0-started State of SCMPDS;
set s1=IExec(J4,P,s),
Bt=IExec(B2,P,s), P1 = P;
A1: Initialize s = s by MEMSTR_0:44;
A2: s1.a = (Initialize s1).a by SCMPDS_5:15;
A3: s1.a4 = (Initialize s1).a4 by SCMPDS_5:15;
A4: s1.a6 = (Initialize s1).a6 by SCMPDS_5:15;
A5: s1.a3 = (Initialize s1).a3 by SCMPDS_5:15;
A6: s1.a1 = (Initialize s1).a1 by SCMPDS_5:15;
A7: s1.a2 = (Initialize s1).a2 by SCMPDS_5:15;
assume that
A8: s.a3 >= s.a1+7 and
A9: s.a=0;
A10: s1.a1 = s.a1+1 by A9,Lm10;
A11: s1.a3 =s.a3+1 by A9,Lm10;
A12: s1.a2=s.a2 by A9,Lm10;
s1.a6 =s.a1+1 & s.a3+1 >= 7+s.a1+1 by A8,A9,Lm10,XREAL_1:6;
then
A13: s1.a4 >= 7+s1.a6 by A9,Lm10;
A14: s1.GBP =0 by A9,Lm10;
then
A15: DataLoc(s1.a,6)=intpos (0+6) by SCMP_GCD:1;
then WH is_closed_on Initialize s1,P1 & WH is_halting_on Initialize s1,P1
by A14,A13,Lm8,A2,A3,A4;
then
A16: WH is_closed_on s1,P1 & WH is_halting_on s1,P1 by SCMPDS_6:125,126;
A17: J4 is_closed_on s,P & J4 is_halting_on s,P by SCMPDS_6:20,21;
then
A18: Bt.a =IExec(WH,P1,Initialize s1).a by A16,SCMPDS_7:30
.=0 by A14,A15,A13,Lm9,A2,A3,A4;
then
A19: DataLoc(Bt.a,2)=intpos (0+2) by SCMP_GCD:1;
A20: B2 is_closed_on s,P & B2 is_halting_on s,P by A16,A17,A1,SCMPDS_7:24;
hence IExec(B3,P,s).a=Exec(jf, Bt).a by SCMPDS_7:31
.=0 by A18,A19,AMI_3:10,SCMPDS_2:48;
thus IExec(B3,P,s).a2=Exec(jf, Bt).a2 by A20,SCMPDS_7:31
.=Bt.a2+ -1 by A19,SCMPDS_2:48
.=Bt.a2-1
.=IExec(WH,P1,Initialize s1).a2 -1 by A16,A17,SCMPDS_7:30
.=s.a2-1 by A14,A12,A15,A13,Lm9,A2,A3,A4,A7;
thus IExec(B3,P,s).a3=Exec(jf, Bt).a3 by A20,SCMPDS_7:31
.=Bt.a3 by A19,AMI_3:10,SCMPDS_2:48
.=IExec(WH,P1,Initialize s1).a3 by A16,A17,SCMPDS_7:30
.=s.a3+1 by A14,A11,A15,A13,Lm9,A2,A3,A4,A5;
thus IExec(B3,P,s).a1=Exec(jf, Bt).a1 by A20,SCMPDS_7:31
.=Bt.a1 by A19,AMI_3:10,SCMPDS_2:48
.=IExec(WH,P1,Initialize s1).a1 by A16,A17,SCMPDS_7:30
.=s.a1+1 by A14,A10,A15,A13,Lm9,A2,A3,A4,A6;
hereby
let i be Nat;
assume
A21: i<> 2;
thus IExec(B3,P,s).intpos i=Exec(jf, Bt).intpos i
by A20,SCMPDS_7:31
.=Bt.intpos i by A19,A21,AMI_3:10,SCMPDS_2:48
.=IExec(WH,P1,Initialize s1).intpos i by A16,A17,SCMPDS_7:30;
end;
end;
Lm12: for s being 0-started State of SCMPDS st s.a3 >= s.a1+7 & s.GBP=0
holds FR is_closed_on s,P & FR is_halting_on s,P
proof
let s be 0-started State of SCMPDS;
set a=GBP, b=DataLoc(s.a,2);
assume that
A1: s.a3 >= s.a1+7 and
A2: s.a=0;
A3: b=intpos(0+2) by A2,SCMP_GCD:1;
now
let t be 0-started State of SCMPDS;
let Q;
A4: Initialize t = t by MEMSTR_0:44;
assume that
A5: t.a3 >= t.a1+7 and
A6: t.a=s.a and
t.b >0;
set t1=IExec(J4,Q,t), Q1 = Q;
A7: t1.a = (Initialize t1).a by SCMPDS_5:15;
A8: t1.a4 = (Initialize t1).a4 by SCMPDS_5:15;
A9: t1.a6 = (Initialize t1).a6 by SCMPDS_5:15;
A10: t.a3+1 >= 7+t.a1+1 by A5,XREAL_1:6;
thus IExec(B3,Q,t).a=t.a by A2,A5,A6,Lm11;
thus IExec(B3,Q,t).b=t.b-1 by A2,A3,A5,A6,Lm11;
A11: J4 is_closed_on t,Q & J4 is_halting_on t,Q by SCMPDS_6:20,21;
t1.a6 =t.a1+1 by A2,A6,Lm10;
then
A12: t1.a4 >= 7+t1.a6 by A2,A6,A10,Lm10;
A13: t1.a =0 by A2,A6,Lm10;
then DataLoc(t1.a,6)=intpos (0+6) by SCMP_GCD:1;
then WH is_closed_on Initialize t1,Q1 & WH is_halting_on Initialize t1,Q1
by A13,A12,Lm8,A8,A9,A7;
then WH is_closed_on t1,Q1 & WH is_halting_on t1,Q1 by SCMPDS_6:125,126;
hence B2 is_closed_on t,Q & B2 is_halting_on t,Q by A11,A4,SCMPDS_7:24;
IExec(B3,Q,t).a1=t.a1+1 by A2,A5,A6,Lm11;
hence IExec(B3,Q,t).a3>=IExec(B3,Q,t).a1+7
by A2,A5,A6,A10,Lm11;
end;
hence thesis by A1,Th11;
end;
Lm13: for s being 0-started State of SCMPDS
st s.a3 >= s.a1+7 & s.GBP=0 & s.a2 > 0 holds
IExec(FR,P,s) = IExec(FR,P,Initialize IExec(B3,P,s))
proof
let s be 0-started State of SCMPDS;
set a=GBP, b=DataLoc(s.a,2);
assume that
A1: s.a3 >= s.a1+7 and
A2: s.a=0 and
A3: s.a2 > 0;
A4: b=intpos(0+2) by A2,SCMP_GCD:1;
now
let t be 0-started State of SCMPDS;
let Q;
A5: Initialize t = t by MEMSTR_0:44;
assume that
A6: t.a3 >= t.a1+7 and
A7: t.a=s.a and
t.b >0;
set t1=IExec(J4,Q,t), Q1 = Q;
A8: t.a3+1 >= 7+t.a1+1 by A6,XREAL_1:6;
thus IExec(B3,Q,t).a=t.a by A2,A6,A7,Lm11;
thus IExec(B3,Q,t).b=t.b-1
by A2,A4,A6,A7,Lm11;
A9: J4 is_closed_on t,Q & J4 is_halting_on t,Q by SCMPDS_6:20,21;
t1.a6 =t.a1+1 by A2,A7,Lm10;
then
A10: t1.a4 >= 7+t1.a6 by A2,A7,A8,Lm10;
A11: t1.a = (Initialize t1).a by SCMPDS_5:15;
A12: t1.a4 = (Initialize t1).a4 by SCMPDS_5:15;
A13: t1.a6 = (Initialize t1).a6 by SCMPDS_5:15;
A14: t1.a =0 by A2,A7,Lm10;
then DataLoc(t1.a,6)=intpos (0+6) by SCMP_GCD:1;
then WH is_closed_on Initialize t1,Q1 & WH is_halting_on Initialize t1,Q1
by A14,A10,Lm8,A11,A12,A13;
then WH is_closed_on t1,Q1 & WH is_halting_on t1,Q1 by SCMPDS_6:125,126;
hence B2 is_closed_on t,Q & B2 is_halting_on t,Q by A9,A5,SCMPDS_7:24;
IExec(B3,Q,t).a1=t.a1+1 by A2,A6,A7,Lm11;
hence IExec(B3,Q,t).a3>=IExec(B3,Q,t).a1+7
by A2,A6,A7,A8,Lm11;
end;
hence thesis by A1,A3,A4,Th12;
end;
begin :: The Property of Insert Sort and Its Correctness
theorem
card insert-sort (n,p0) = 23
proof
set i1= GBP:=0, i2= (GBP,1):=0, i3= (GBP,2):=(n-1), i4= (GBP,3):=p0;
thus card insert-sort (n,p0) =card(i1 ';' i2 ';' i3 ';' i4) + card FR by
AFINSQ_1:17
.=card(i1 ';' i2 ';' i3)+1 + card FR by SCMP_GCD:4
.=card(i1 ';' i2)+1+1 + card FR by SCMP_GCD:4
.=2+1+1+card FR by SCMP_GCD:5
.=4+(card B2+3) by SCMPDS_7:41
.=23 by Lm5;
end;
theorem
p0 >= 7 implies insert-sort (n,p0) is parahalting
proof
set a=GBP, i1= a:=0, i2= (a,1):=0, i3= (a,2):=(n-1), i4= (a,3):=p0, I= i1
';' i2 ';' i3 ';' i4;
assume
A1: p0 >= 7;
now
let s be State of SCMPDS;
let P;
set s1=IExec(I,P,Initialize s),
s2=IExec(i1 ';' i2 ';' i3,P,Initialize s), P1 = P,
s3=IExec(i1 ';' i2,P,Initialize s), s4
=Exec(i1, Initialize s);
A2: s1.a = (Initialize s1).a by SCMPDS_5:15;
A3: s1.a1 = (Initialize s1).a1 by SCMPDS_5:15;
A4: s1.a3 = (Initialize s1).a3 by SCMPDS_5:15;
A5: I is_closed_on s,P & I is_halting_on s,P by SCMPDS_6:20,21;
A6: s4.a=0 by SCMPDS_2:45;
then
A7: DataLoc(s4.a,1)=intpos (0+1) by SCMP_GCD:1;
A8: s3.a=Exec(i2,s4).a by SCMPDS_5:42
.=0 by A6,A7,AMI_3:10,SCMPDS_2:46;
then
A9: DataLoc(s3.a,2)=intpos (0+2) by SCMP_GCD:1;
A10: s3.a1=Exec(i2,s4).a1 by SCMPDS_5:42
.=0 by A7,SCMPDS_2:46;
A11: s2.a1=Exec(i3,s3).a1 by SCMPDS_5:41
.=0 by A10,A9,AMI_3:10,SCMPDS_2:46;
A12: s2.a=Exec(i3,s3).a by SCMPDS_5:41
.=0 by A8,A9,AMI_3:10,SCMPDS_2:46;
then
A13: DataLoc(s2.a,3)=intpos (0+3) by SCMP_GCD:1;
A14: s1.a3=Exec(i4,s2).a3 by SCMPDS_5:41
.=p0 by A13,SCMPDS_2:46;
s1.a1=Exec(i4,s2).a1 by SCMPDS_5:41
.=0 by A11,A13,AMI_3:10,SCMPDS_2:46;
then
A15: s1.a3 >= s1.a1+7 by A1,A14;
s1.a=Exec(i4,s2).a by SCMPDS_5:41
.=0 by A12,A13,AMI_3:10,SCMPDS_2:46;
then FR is_closed_on Initialize s1,P1 & FR is_halting_on Initialize s1,P1
by A15,Lm12,A2,A3,A4;
then FR is_closed_on s1,P1 & FR is_halting_on s1,P1 by SCMPDS_6:125,126;
hence insert-sort (n,p0) is_halting_on s,P by A5,SCMPDS_7:24;
end;
hence thesis by SCMPDS_6:21;
end;
Lm14: for s being 0-started State of SCMPDS
st s.a4 >= 7+s.a6 & s.GBP=0 & s.a6 >0 holds
IExec(WH,P,s) =IExec(WH,P,Initialize IExec(B1,P,s))
proof
let s be 0-started State of SCMPDS;
set a=GBP, b=DataLoc(s.a,6);
assume that
A1: s.a4 >= 7+s.a6 and
A2: s.a=0 and
A3: s.a6 > 0;
A4: b=intpos(0+6) by A2,SCMP_GCD:1;
A5: now
let t be 0-started State of SCMPDS;
let Q;
A6: Initialize t = t by MEMSTR_0:44;
assume that
A7: for x st x in {a4} holds t.x >= 7+t.b and
A8: t.a=s.a & t.b >0;
set Bt=IExec(B1,Q,Initialize t);
A9: a4 in {a4} by TARSKI:def 1;
then
A10: t.a4 >= 7+t.a6 by A4,A7;
hence IExec(B1,Q,t).a=t.a by A2,A4,A8,Lm6;
thus B1 is_closed_on t,Q & B1 is_halting_on t,Q by SCMPDS_6:20,21;
thus IExec(B1,Q,t).b < t.b by A2,A4,A8,A10,Lm7;
t.a4 >= 7+t.b by A7,A9;
then Bt.a4 >= 7+Bt.a6 by A2,A4,A8,Lm7,A6;
hence for x st x in {a4} holds IExec(B1,Q,t).x
>= 7+IExec(B1,Q,t).b by A4,A6,TARSKI:def 1;
end;
for x st x in {a4} holds s.x >= 7+s.b by A1,A4,TARSKI:def 1;
hence thesis by A3,A4,A5,SCMPDS_8:29;
end;
theorem Th16:
for s being 0-started State of SCMPDS,
f,g be FinSequence of INT, k0,k being 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)))),P,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 be Nat st i>k+1 & i <= len f
holds f.i=g.i) & for i be Nat st 1 <= i & i <= k+1 holds ex j be
Nat st 1 <= j & j <= k+1 & g.i=f.j
proof
set a=GBP;
let s be 0-started State of SCMPDS,
f,g be FinSequence of INT,m,n be Nat;
assume
A1: s.a4 >= 7+s.a6 & s.a=0 & n=s.a6 & m=s.a4-s.a6-1;
defpred P[Nat] means for t be 0-started State of SCMPDS,Q
for f1,f2 be
FinSequence of INT st t.a4 >= 7+t.a6 & t.a=0 & $1=t.a6 & m=t.a4-t.a6-1 & f1
is_FinSequence_on t,m & f2 is_FinSequence_on IExec(WH,Q,t),m
& len f1=len f2 &
len f1 > $1 & f1 is_non_decreasing_on 1,$1 holds f1,f2 are_fiberwise_equipotent
& f2 is_non_decreasing_on 1,$1+1 & (for i be Nat st i>$1+1 & i <=
len f1 holds f1.i=f2.i) & (for i be Nat st 1 <= i & i <= $1+1 ex j
be Nat st 1 <= j & j <= $1+1 & f2.i=f1.j);
assume
A2: f is_FinSequence_on s,m & g is_FinSequence_on IExec(WH,P,s),m;
A3: now
let k be Nat;
assume
A4: P[k];
thus P[k+1 qua Nat]
proof
let t be 0-started State of SCMPDS,Q;
let f1,f2 be FinSequence of INT;
A5: Initialize t = t by MEMSTR_0:44;
assume that
A6: t.a4 >= 7+t.a6 and
A7: t.a=0 and
A8: k+1=t.a6 and
A9: m=t.a4-t.a6-1 and
A10: f1 is_FinSequence_on t,m and
A11: f2 is_FinSequence_on IExec(WH,Q,t),m and
A12: len f1=len f2 and
A13: len f1 > k+1 and
A14: f1 is_non_decreasing_on 1,k+1;
set Bt=IExec(B1,Q,t), x=DataLoc(t.a4,-1), y=DataLoc(t.a4,0);
A15: Bt.a=0 by A6,A7,A8,Lm6;
m+1+(k+1) >= 7+t.a6 by A6,A8,A9;
then
A16: m+1 >= 7 by A8,XREAL_1:6;
A17: x=DataLoc(m,k+1) by A8,A9
.=intpos(m+(k+1)) by SCMP_GCD:1;
A18: Bt.a6 = (Initialize Bt).a6 by SCMPDS_5:15;
A19: Bt.a4 = (Initialize Bt).a4 by SCMPDS_5:15;
A20: (Initialize Bt).a = Bt.a by SCMPDS_5:15;
A21: t.x > t.y implies Bt.x=t.y & Bt.y =t.x & Bt.a6=t.a6-1
& Bt.a4=t.a4-1 by A6,A7,A8,Lm7;
A22: t.x <= t.y implies Bt.x=t.x & Bt.y =t.y & Bt.a6=0
by A6,A7,A8,Lm7;
A23: y=intpos(m+(k+2)) by A8,A9,SCMP_GCD:1;
A24: Bt.a4 >= 7+Bt.a6 by A6,A7,A8,Lm7;
per cases;
suppose
A25: t.x > t.y;
now
let i be Nat;
assume
1<=i & i <= len f2;
hence f2.i=IExec(WH,Q,t).intpos(m+i) by A11
.=IExec(WH,Q,Initialize Bt).intpos(m+i) by A6,A7,A8,Lm14;
end;
then
A26: f2 is_FinSequence_on IExec(WH,Q,Initialize Bt),m;
A27: k+1 < k+2 by XREAL_1:6;
consider h be FinSequence of INT such that
A28: len h=len f1 and
A29: for i be Nat st 1<=i & i <= len h holds h.i=Bt.
intpos(m+ i) by Th1;
k+1 > k by XREAL_1:29;
then
A30: len h > k by A13,A28,XXREAL_0:2;
A31: now
let i be Nat;
assume that
A32: i <> k+1 & i<>k+2 and
A33: 1 <= i and
A34: i <= len f1;
A35: m+i <> t.a4-1 & m+i <> t.a4 by A8,A9,A32;
m+i >= m+1 by A33,XREAL_1:6;
then
A36: m+i >= 7 by A16,XXREAL_0:2;
thus h.i=Bt.intpos(m+i) by A28,A29,A33,A34
.=t.intpos(m+i) by A6,A7,A8,A36,A35,Lm7
.=f1.i by A10,A33,A34;
end;
now
let i,j be Nat;
assume that
A37: 1 <= i and
A38: i <= j and
A39: j <= k;
A40: j <= len f1 by A28,A30,A39,XXREAL_0:2;
then
A41: i <= len f1 by A38,XXREAL_0:2;
A42: k < k+1 by XREAL_1:29;
then
A43: j < k+1 by A39,XXREAL_0:2;
k+1 < k+1+1 by XREAL_1:29;
then
A44: k < k+1+1 by A42,XXREAL_0:2;
j >= 1 by A37,A38,XXREAL_0:2;
then
A45: h.j=f1.j by A31,A39,A42,A44,A40;
j < k+2 by A39,A44,XXREAL_0:2;
then h.i=f1.i by A31,A37,A38,A43,A41;
hence h.i <= h.j by A14,A37,A38,A43,A45,FINSEQ_6:def 9;
end;
then
A46: h is_non_decreasing_on 1,k by FINSEQ_6:def 9;
A47: len f1 >= k+1+1 by A13,INT_1:7;
A48: 1 <= k+1 by NAT_1:11;
then
A49: 1 <= k+2 by A27,XXREAL_0:2;
then
A50: h.(k+2)=t.x by A23,A21,A25,A28,A29,A47;
then
A51: h.(k+2)=f1.(k+1) by A10,A13,A17,A48;
A52: Bt.a4-Bt.a6-1=m by A9,A21,A25;
A53: h.(k+1)=t.y by A13,A17,A21,A25,A28,A29,NAT_1:11;
then h.(k+1)=f1.(k+2) by A10,A23,A49,A47;
then
A54: f1,h are_fiberwise_equipotent by A13,A28,A31,A48,A49,A47,A51,Th3;
A55: h is_FinSequence_on Initialize Bt,m
proof let i be Nat;
assume 1 <= i & i <= len h;
then h.i=Bt.intpos(m+i) by A29;
hence thesis by SCMPDS_5:15;
end;
h,f2 are_fiberwise_equipotent
by A4,A8,A12,A15,A24,A21,A25,A28,A52,A26,A30,A46,A55,A18,A19,A20;
hence f1,f2 are_fiberwise_equipotent by A54,CLASSES1:76;
A56: f2 is_non_decreasing_on 1, k+1
by A4,A8,A12,A15,A24,A21,A25,A28,A52,A55,A18,A19,A20,A26,A30,A46;
now
let i,j be Nat;
assume that
A57: 1 <= i and
A58: i <= j and
A59: j <= (k+1)+1;
per cases by A59,NAT_1:8;
suppose
j <= k+1;
hence f2.i <= f2.j by A56,A57,A58,FINSEQ_6:def 9;
end;
suppose
A60: j = k+1+1;
hereby
per cases;
suppose
i=j;
hence f2.i <= f2.j;
end;
suppose
i<>j;
then i < j by A58,XXREAL_0:1;
then i <= k+1 by A60,NAT_1:13;
then consider mm be Nat such that
A61: 1 <= mm and
A62: mm <= k+1 and
A63: f2.i=h.mm by A4,A8,A12,A15,A24,A21,A25,A28,A52,A55,A26,A30,A46
,A57,A18,A19,A20;
A64: f2.j=h.(k+2) by A4,A8,A12,A15,A24,A21,A25,A28,A52,A55,A26,A30
,A46,A27,A47,A60,A18,A19,A20;
hereby
per cases;
suppose
mm=k+1;
hence
f2.i <= f2.j by A13,A17,A21,A22,A28,A29,A50,A61,A63,A64;
end;
suppose
A65: mm<>k+1;
mm < k+2 by A27,A62,XXREAL_0:2;
then mm < len h by A28,A47,XXREAL_0:2;
then
A66: h.mm=f1.mm by A28,A31,A27,A61,A62,A65;
f2.j=f1.(k+1) by A10,A13,A17,A48,A50,A64;
hence f2.i <= f2.j by A14,A61,A62,A63,A66,FINSEQ_6:def 9;
end;
end;
end;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k+1)+1 by FINSEQ_6:def 9;
hereby
let i be Nat;
assume that
A67: i>(k+1)+1 and
A68: i <= len f1;
A69: k+1 < k+1+1 by XREAL_1:29;
then
A70: i > k+1 by A67,XXREAL_0:2;
1 <= k+1 by NAT_1:11;
then
A71: 1 <= i by A70,XXREAL_0:2;
thus f2.i=h.i by A4,A8,A12,A15,A24,A21,A25,A28,A52,A55,A26,A30,A46
,A68,A70,A18,A19,A20
.=f1.i by A31,A67,A68,A69,A71;
end;
hereby
let i be Nat;
assume that
A72: 1 <= i and
A73: i <= (k+1)+1;
per cases;
suppose
A74: i=k+1+1;
reconsider j=k+1 as Nat;
take j;
thus 1 <= j by NAT_1:11;
thus j <= (k+1)+1 by NAT_1:11;
thus f2.i=f1.j by A4,A8,A12,A15,A24,A21,A25,A28,A52,A55,A26,A30,A46
,A27,A47,A51,A74,A18,A19,A20;
end;
suppose
i<>k+1+1;
then i < k+1+1 by A73,XXREAL_0:1;
then i <= k+1 by NAT_1:13;
then consider mm be Nat such that
A75: 1 <= mm and
A76: mm <= k+1 and
A77: f2.i=h.mm by A4,A8,A12,A15,A24,A21,A25,A28,A52,A55,A26,A30,A46,A72
,A18,A19,A20;
hereby
A78: k+2=(k+1)+1;
per cases;
suppose
A79: mm=k+1;
reconsider j=k+2 as Nat;
take j;
thus 1 <= j by A78,NAT_1:11;
thus j <= k+1+1;
thus f2.i=f1.j by A10,A23,A49,A47,A53,A77,A79;
end;
suppose
A80: mm<>k+1;
reconsider mm as Nat;
take mm;
thus 1 <= mm by A75;
thus mm <= k+1+1 by A27,A76,XXREAL_0:2;
mm < k+2 by A27,A76,XXREAL_0:2;
then mm < len f1 by A47,XXREAL_0:2;
hence f2.i=f1.mm by A31,A27,A75,A76,A77,A80;
end;
end;
end;
end;
end;
suppose
A81: t.x <= t.y;
A82: now
let i be Nat;
assume that
A83: i>=1 and
A84: i <= len f1;
A85: f1.i=t.intpos(m+i) by A10,A83,A84;
Bt.DataLoc(Bt.a,6) =0 by A15,A22,A81,SCMP_GCD:1;
then
A86: (Initialize Bt).DataLoc(Bt.a,6) =0 by SCMPDS_5:15;
m+i >= m+1 by A83,XREAL_1:6;
then
A87: m+i >= 7 by A16,XXREAL_0:2;
A88: (Initialize Bt).intpos(m+i) = Bt.intpos(m+i) by SCMPDS_5:15;
A89: (Initialize Bt).DataLoc((Initialize Bt).GBP,6) <= 0 by A86,SCMPDS_5:15;
per cases;
suppose
A90: m+i=t.a4-1;
hence f1.i=IExec(WH,Q,Initialize Bt).x
by A8,A9,A17,A22,A81,A85,A88,A89,SCMPDS_8:23
.=IExec(WH,Q,Initialize t).x by A6,A7,A8,Lm14,A5
.=f2.i by A8,A9,A11,A12,A13,A17,A83,A90,A5;
end;
suppose
A91: m+i=t.a4;
hence f1.i=IExec(WH,Q,Initialize Bt).y
by A8,A9,A23,A22,A81,A85,A88,A89,SCMPDS_8:23
.=IExec(WH,Q,Initialize t).y by A6,A7,A8,Lm14,A5
.=f2.i by A8,A9,A11,A12,A23,A83,A84,A91,A5;
end;
suppose
m+i<>t.a4-1 & m+i<>t.a4;
hence f1.i=Bt.intpos (m+i)
by A6,A7,A8,A87,A85,Lm7
.=IExec(WH,Q,Initialize Bt).intpos (m+i) by A88,A89,SCMPDS_8:23
.=IExec(WH,Q,Initialize t).intpos (m+i) by A6,A7,A8,Lm14,A5
.=f2.i by A11,A12,A83,A84,A5;
end;
end;
then
A92: f1=f2 by A12,FINSEQ_1:14;
thus f1,f2 are_fiberwise_equipotent by A12,A82,FINSEQ_1:14;
now
let i, j be Nat;
assume that
A93: 1 <= i and
A94: i <= j and
A95: j <= (k+1)+1;
per cases by A95,NAT_1:8;
suppose
j <= k+1;
hence f1.i <= f1.j by A14,A93,A94,FINSEQ_6:def 9;
end;
suppose
A96: j = k+1+1;
hereby
per cases;
suppose
i=j;
hence f1.i <= f1.j;
end;
suppose
i<>j;
then i < j by A94,XXREAL_0:1;
then i <= k+1 by A96,NAT_1:13;
then
A97: f1.i <= f1.(k+1) by A14,A93,FINSEQ_6:def 9;
1<=k+1 by NAT_1:11;
then
A98: f1.(k+1)=t.x by A10,A13,A17;
1<=(k+1)+1 & j<=len f1 by A13,A96,INT_1:7,NAT_1:11;
then f1.j=t.y by A10,A23,A96;
hence f1.i <= f1.j by A81,A97,A98,XXREAL_0:2;
end;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k+1)+1 by A92,FINSEQ_6:def 9;
thus for i be Nat st i>(k+1)+1 & i <= len f1 holds f1.i=f2.
i by A12,A82,FINSEQ_1:14;
thus for i be Nat st 1 <= i & i <= (k+1)+1
ex j be Nat st 1 <= j & j <= (k+1)+1 & f2.i=f1.j by A92;
end;
end;
end;
A99: P[0 qua Nat]
proof
let t be 0-started State of SCMPDS, Q;
let f1,f2 be FinSequence of INT;
A100: Initialize t = t by MEMSTR_0:44;
assume that
t.a4 >= 7+t.a6 and
A101: t.a=0 & 0=t.a6 and
m=t.a4-t.a6-1 and
A102: f1 is_FinSequence_on t,m and
A103: f2 is_FinSequence_on IExec(WH,Q,t),m and
A104: len f1=len f2 and
len f1 > 0 and
f1 is_non_decreasing_on 1,0;
A105: t.DataLoc(t.a,6) =0 by A101,SCMP_GCD:1;
A106: now
let i be Nat;
assume
A107: 1 <= i & i <= len f1;
thus f1.i=t.intpos(m+i) by A102,A107
.=IExec(WH,Q,Initialize t).intpos(m+i) by A105,A100,SCMPDS_8:23
.=f2.i by A103,A104,A107,A100;
end;
hence f1,f2 are_fiberwise_equipotent by A104,FINSEQ_1:14;
thus f2 is_non_decreasing_on 1,0+1 by FINSEQ_6:165;
thus for i be Nat st i>0+1 & i <= len f1 holds f1.i=f2.i by A106;
f1=f2 by A104,A106,FINSEQ_1:14;
hence thesis;
end;
A108: for k be Nat holds P[k] from NAT_1:sch 2(A99,A3);
assume
len f= len g & len f > n & f is_non_decreasing_on 1,n;
hence thesis by A1,A2,A108;
end;
Lm15: for s being 0-started State of SCMPDS,
f,g be FinSequence of INT, p0,n being
Nat st s.GBP=0 & s.a2=n-1 & s.a3=p0+1 & s.a1=0 & p0 >= 6 & f
is_FinSequence_on s,p0 & g is_FinSequence_on IExec(FR,P,s),p0
& len f=n & len g =
n holds f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n
proof
set a=GBP;
let s be 0-started State of SCMPDS,
f,g be FinSequence of INT,p0,n be Nat;
assume that
A1: s.a=0 and
A2: s.a2=n-1 and
A3: s.a3=p0+1 and
A4: s.a1=0 and
A5: p0 >= 6 and
A6: f is_FinSequence_on s,p0 & g is_FinSequence_on IExec(FR,P,s),p0 and
A7: len f=n and
A8: len g = n;
per cases;
suppose
A9: n=0;
then g={} by A8;
hence f,g are_fiberwise_equipotent by A7,A9;
thus thesis by A9,FINSEQ_6:165;
end;
suppose
n<>0;
then n >= 1+0 by INT_1:7;
then n-1 >= 0 by XREAL_1:19;
then reconsider n1=n-1 as Element of NAT by INT_1:3;
defpred P[Nat] means for t be 0-started State of SCMPDS,Q
for f1,f2 be FinSequence of INT, m be Nat
st t.a=0 & t.a2+t.a1=n-1 & t.a2=$1 & m=n-t.a2 & p0=t.a3-t.
a1-1 & f1 is_FinSequence_on t,p0
& f2 is_FinSequence_on IExec(FR,Q,t),p0 & f1
is_non_decreasing_on 1,m & len f1=n & len f2 = n holds f1,f2
are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n;
A10: s.a2+s.a1=n-1+0 & 1=n-s.a2 by A2,A4;
A11: now
let k be Nat;
assume
A12: P[k];
now
let t be 0-started State of SCMPDS,
f1,f2 be FinSequence of INT, m be Nat;
let Q;
assume that
A13: t.a=0 and
A14: t.a2+t.a1=n-1 and
A15: t.a2=k+1 and
A16: m=n-t.a2 and
A17: p0=t.a3-t.a1-1 and
A18: f1 is_FinSequence_on t,p0 and
A19: f2 is_FinSequence_on IExec(FR,Q,t),p0 and
A20: f1 is_non_decreasing_on 1,m & len f1=n and
A21: len f2 = n;
set t1=IExec(J4,Q,t), Bt=IExec(B3,Q,t), Q1 = Q;
A22: t1.a = (Initialize t1).a by SCMPDS_5:15;
A23: t1.a4 = (Initialize t1).a4 by SCMPDS_5:15;
A24: t1.a6 = (Initialize t1).a6 by SCMPDS_5:15;
A25: t1.a4 =t.a3+1 by A13,Lm10;
p0+(t.a1+1)=t.a3 by A17;
then t.a3 >= 6+(t.a1+1) by A5,XREAL_1:6;
then
A26: t.a3 >= 6+1+t.a1;
then
A27: Bt.a=0 by A13,Lm11;
A28: Bt.a2=t.a2-1 by A13,A26,Lm11;
then
A29: n-Bt.a2=m+1 by A16;
A30: Bt.a1=t.a1+1 by A13,A26,Lm11;
then
A31: Bt.a2+Bt.a1=n-1 by A14,A28;
Bt.a3=t.a3+1 by A13,A26,Lm11;
then
A32: Bt.a3-Bt.a1-1=p0 by A17,A30;
A33: t1.a6 =t.a1+1 by A13,Lm10;
then
A34: p0=t1.a4-t1.a6-1 by A17,A25;
now
let i be Nat;
assume
1 <= i & i <= len f2;
hence f2.i=IExec(FR,Q,t).intpos(p0+i) by A19
.= IExec(FR,Q,Initialize Bt).intpos(p0+i)
by A13,A15,A26,Lm13;
end;
then
A35: f2 is_FinSequence_on IExec(FR,Q,Initialize Bt),p0;
A36: now
A37: p0+1 >= 6+1 by A5,XREAL_1:6;
let i be Nat;
assume that
A38: 1 <= i and
A39: i <= len f1;
p0+1 <= p0+i by A38,XREAL_1:6;
then
A40: p0+i >= 7 by A37,XXREAL_0:2;
thus f1.i=t.intpos(p0+i) by A18,A38,A39
.= t1.intpos(p0+i)
by A13,A40,Lm10;
end;
t1.a4=p0+(t1.a6+1) by A17,A25,A33;
then t1.a4 >= 6+(t1.a6+1) by A5,XREAL_1:6;
then
A41: t1.a4 >= 6+1+t1.a6;
m+(k+1)=n by A15,A16;
then
A42: n > 0+m by XREAL_1:6;
consider h be FinSequence of INT such that
A43: len h=n and
A44: for i be Nat st 1<=i & i <= len h holds h.i=IExec(
WH,Q1,Initialize t1) .intpos(p0+i) by Th1;
A45: h is_FinSequence_on IExec(WH,Q1,Initialize t1),p0 by A44;
A46: now
A47: p0+1 >= 6+1 by A5,XREAL_1:6;
let i be Nat;
assume that
A48: 1 <= i and
A49: i <= len h;
p0+1 <= p0+i by A48,XREAL_1:6;
then p0+i >= 7 by A47,XXREAL_0:2;
then
A50: p0+i > 2 by XXREAL_0:2;
thus h.i=IExec(WH,Q1,Initialize t1).intpos(p0+i) by A44,A48,A49
.= Bt.intpos(p0+i) by A13,A26,A50,Lm11;
end;
A51: f1 is_FinSequence_on (Initialize t1),p0
proof let i be Nat;
assume 1 <= i & i <= len f1;
then f1.i=t1.intpos(p0+i) by A36;
hence thesis by SCMPDS_5:15;
end;
A52: t1.a =0 by A13,Lm10;
then
A53: f1,h are_fiberwise_equipotent by A14,A16,A17,A20,A25,A43,A34,A41,A45
,A42,Th16,A23,A24,A22,A51;
A54: h is_non_decreasing_on 1,m +1 by A14,A16,A17,A20,A25,A43,A34,A41,A45
,A42,Th16,A23,A24,A22,A51,A52;
A55: (Initialize Bt).a = Bt.a by SCMPDS_5:15;
A56: (Initialize Bt).a1 = Bt.a1 by SCMPDS_5:15;
A57: (Initialize Bt).a2 = Bt.a2 by SCMPDS_5:15;
A58: (Initialize Bt).a3 = Bt.a3 by SCMPDS_5:15;
A59: h is_FinSequence_on (Initialize Bt),p0
proof let i be Nat such that
A60: 1 <= i & i <= len h;
thus h.i=Bt.intpos(p0+i) by A60,A46
.=(Initialize Bt).intpos(p0+i) by SCMPDS_5:15;
end;
then h,f2 are_fiberwise_equipotent by A12,A15,A16,A21,A43,A27,A31,A29
,A32,A35,A54,A55,A56,A57,A58;
hence f1,f2 are_fiberwise_equipotent by A53,CLASSES1:76;
thus f2 is_non_decreasing_on 1,n by A12,A15,A16,A21,A43,A54,A27,A31,A29
,A32,A35,A55,A56,A57,A58,A59;
end;
hence P[k+1];
end;
A61: P[0 qua Nat]
proof
let t be 0-started State of SCMPDS, Q;
let f1,f2 be FinSequence of INT, m be Nat;
A62: Initialize t = t by MEMSTR_0:44;
assume that
A63: t.a=0 and
t.a2+t.a1=n-1 and
A64: t.a2=0 and
A65: m=n-t.a2 and
p0=t.a3-t.a1-1 and
A66: f1 is_FinSequence_on t,p0 and
A67: f2 is_FinSequence_on IExec(FR,Q,t),p0 and
A68: f1 is_non_decreasing_on 1,m and
A69: len f1=n & len f2 = n;
A70: t.DataLoc(t.a,2)=0 by A63,A64,SCMP_GCD:1;
A71: now
let i be Nat;
assume
A72: 1 <= i & i <= len f2;
thus f2.i=IExec(FR,Q,Initialize t).intpos(p0+i) by A67,A72,A62
.=t.intpos(p0+i) by A70,SCMPDS_7:47
.=f1.i by A66,A69,A72;
end;
hence f1,f2 are_fiberwise_equipotent by A69,FINSEQ_1:14;
thus thesis by A64,A65,A68,A69,A71,FINSEQ_1:14;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A61,A11);
then
A73: P[n1];
p0=s.a3-s.a1-1 & f is_non_decreasing_on 1,1 by A3,A4,FINSEQ_6:165;
hence thesis by A1,A6,A7,A8,A10,A73;
end;
end;
theorem
for s being 0-started State of SCMPDS,f,g be FinSequence of INT,p0,
n being Nat
st p0 >= 6 & len f=n & len g = n & f is_FinSequence_on s,p0 &
g is_FinSequence_on IExec(insert-sort(n,p0+1),P,s),p0
holds f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n
proof
set a=GBP;
let s be 0-started State of SCMPDS,f,g be FinSequence of INT,p0,
n be Nat;
assume that
A1: p0 >= 6 and
A2: len f=n & len g = n and
A3: f is_FinSequence_on s,p0 and
A4: g is_FinSequence_on IExec(insert-sort(n,p0+1),P,s),p0;
A5: p0+1 >= 6+1 by A1,XREAL_1:6;
set i1= GBP:=0, i2= (GBP,1):=0, i3= (GBP,2):=(n-1), i4= (GBP,3):=(p0+1);
set I4=i1 ';' i2 ';' i3 ';' i4, t1=IExec(I4,P,s),
t2=IExec(i1 ';' i2 ';' i3,P,s), t3=IExec(i1 ';' i2,P,s), t4=Exec(i1,s);
A6: t4.a=0 by SCMPDS_2:45;
then
A7: DataLoc(t4.a,1)=intpos (0+1) by SCMP_GCD:1;
A8: t3.a =Exec(i2, t4).a by SCMPDS_5:42
.=0 by A6,A7,AMI_3:10,SCMPDS_2:46;
then
A9: DataLoc(t3.a,2)=intpos (0+2) by SCMP_GCD:1;
A10: t2.a =Exec(i3, t3).a by SCMPDS_5:41
.=0 by A8,A9,AMI_3:10,SCMPDS_2:46;
then
A11: DataLoc(t2.a,3)=intpos (0+3) by SCMP_GCD:1;
A12: now
let i be Nat;
assume
A13: i > 3;
then
A14: i > 1 by XXREAL_0:2;
thus t3.intpos i =Exec(i2, t4).intpos i by SCMPDS_5:42
.=t4.intpos i by A7,A14,AMI_3:10,SCMPDS_2:46
.=s.intpos i by A13,AMI_3:10,SCMPDS_2:45;
end;
A15: now
let i be Nat;
assume
A16: i > 3;
then
A17: i > 2 by XXREAL_0:2;
thus t2.intpos i =Exec(i3, t3).intpos i by SCMPDS_5:41
.=t3.intpos i by A9,A17,AMI_3:10,SCMPDS_2:46
.=s.intpos i by A12,A16;
end;
now
let i be Nat;
assume that
A18: 1 <= i and
A19: i <= len f;
set pi=p0+i;
pi >= p0+1 by A18,XREAL_1:6;
then pi >= 7 by A5,XXREAL_0:2;
then
A20: pi > 3 by XXREAL_0:2;
thus (Initialize t1).intpos pi = t1.intpos pi by SCMPDS_5:15
.=Exec(i4, t2).intpos pi by SCMPDS_5:41
.=t2.intpos pi by A11,A20,AMI_3:10,SCMPDS_2:46
.=s.intpos pi by A15,A20
.=f.i by A3,A18,A19;
end;
then
A21: f is_FinSequence_on Initialize t1,p0;
A22: t3.a1 =Exec(i2, t4).a1 by SCMPDS_5:42
.=0 by A7,SCMPDS_2:46;
A23: t2.a1 =Exec(i3, t3).a1 by SCMPDS_5:41
.=0 by A22,A9,AMI_3:10,SCMPDS_2:46;
A24: I4 is_closed_on s,P & I4 is_halting_on s,P by SCMPDS_6:20,21;
A25: t1.a =Exec(i4, t2).a by SCMPDS_5:41
.=0 by A10,A11,AMI_3:10,SCMPDS_2:46;
A26: t2.a2 =Exec(i3, t3).a2 by SCMPDS_5:41
.=n-1 by A9,SCMPDS_2:46;
A27: t1.a3 =Exec(i4, t2).a3 by SCMPDS_5:41
.=p0+1 by A11,SCMPDS_2:46;
A28: t1.a3 = (Initialize t1).a3 by SCMPDS_5:15;
A29: t1.a1 = (Initialize t1).a1 by SCMPDS_5:15;
A30: t1.a = (Initialize t1).a by SCMPDS_5:15;
A31: t1.a2 = (Initialize t1).a2 by SCMPDS_5:15;
A32: t1.a1 =Exec(i4, t2).a1 by SCMPDS_5:41
.=0 by A23,A11,AMI_3:10,SCMPDS_2:46;
then t1.a3 >= t1.a1+7 by A27,A5;
then FR is_closed_on Initialize t1,P & FR is_halting_on Initialize t1,P
by A25,Lm12,A28,A29,A30;
then
A33: FR is_closed_on t1,P & FR is_halting_on t1,P by SCMPDS_6:125,126;
now
let i be Nat;
assume
1 <= i & i <= len g;
hence g.i=IExec(I4 ';' FR,P,s).intpos(p0+i) by A4
.=IExec(FR,P,Initialize t1).intpos(p0+i) by A24,A33,SCMPDS_7:30;
end;
then
A34: g is_FinSequence_on IExec(FR,P,Initialize t1),p0;
t1.a2 =Exec(i4, t2).a2 by SCMPDS_5:41
.=n-1 by A26,A11,AMI_3:10,SCMPDS_2:46;
hence thesis by A1,A2,A25,A32,A27,A21,A34,Lm15,A28,A29,A30,A31;
end;