Copyright (c) 2000 Association of Mizar Users
environ
vocabulary AMI_3, SCMPDS_2, AMI_1, SCMPDS_4, CARD_1, SCMFSA6A, FINSEQ_1,
INT_1, FUNCT_1, SCMP_GCD, RFUNCT_2, RELAT_1, RFINSEQ, AMI_2, SCMPDS_8,
SCMPDS_5, SCMFSA6B, UNIALG_2, SCMFSA7B, SCMFSA_7, SCMPDS_7, ARYTM_1,
RELOC, FUNCT_4, SCMPDS_3, FUNCT_7, SCM_1, BOOLE, AMI_5, SCMISORT,
SCMFSA_9, SCMFSA8B, ABSVALUE, SCPISORT;
notation XBOOLE_0, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_4, INT_1, NAT_1,
AMI_1, AMI_2, AMI_3, AMI_5, FUNCT_7, SCMPDS_2, SCMPDS_3, CARD_1,
SCMPDS_4, SCM_1, SCMPDS_5, SCMPDS_6, SCMP_GCD, DOMAIN_1, FINSEQ_1,
SCMPDS_7, SCMPDS_8, ABSVALUE, SFMASTR3, RFINSEQ;
constructors REAL_1, DOMAIN_1, AMI_5, SCMPDS_4, SCM_1, SCMPDS_5, SCMPDS_6,
SCMP_GCD, SCMPDS_7, SCMPDS_8, SFMASTR3, RFINSEQ, NAT_1, MEMBERED, RAT_1;
clusters AMI_1, INT_1, FUNCT_1, RELSET_1, SCMPDS_2, SCMFSA_4, SCMPDS_4,
SCMPDS_5, SCMPDS_6, SCMPDS_7, SCMPDS_8, WSIERP_1, NAT_1, FRAENKEL,
XREAL_0, MEMBERED;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
theorems AMI_1, AMI_3, NAT_1, REAL_1, TARSKI, FUNCT_4, INT_1, AMI_5, SCMPDS_2,
SCMPDS_3, GRFUNC_1, AXIOMS, SCM_1, SCMFSA6B, SCMPDS_4, SCMPDS_5,
SCMPDS_6, ENUMSET1, SCMP_GCD, SCMPDS_7, SCMPDS_8, ABSVALUE, FINSEQ_1,
SFMASTR3, FINSEQ_2, SCMBSORT, RFINSEQ, SQUARE_1, RELAT_1, XBOOLE_1,
XCMPLX_0, XCMPLX_1;
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
:Def1: for i be Nat st 1 <= i & i <= len f holds f.i=s.intpos(m+i);
end;
Lm1:
for f being FinSequence of INT,k be Nat holds f is_non_decreasing_on k,k
proof
let f be FinSequence of INT,k be Nat;
now
let i, j be Nat;
assume A1: k <= i & i <= j & j <= k;
then k <= j by AXIOMS:22;
then j=k by A1,AXIOMS:21;
hence f.i <= f.j by A1,AXIOMS:21;
end;
hence thesis by SFMASTR3:def 4;
end;
theorem Th1:
for f being FinSequence of INT,m,n be Nat st m >= n holds
f is_non_decreasing_on m,n
proof
let f be FinSequence of INT,m,n be Nat;
assume A1: m>=n;
per cases by A1,AXIOMS:21;
suppose m=n;
hence thesis by Lm1;
suppose A2:m>n;
now
let i, j be Nat;
assume A3: m <= i & i <= j & j <= n;
assume f.i > f.j;
m <= j by A3,AXIOMS:22;
hence contradiction by A2,A3,AXIOMS:22;
end;
hence thesis by SFMASTR3:def 4;
end;
theorem Th2:
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 Seg n holds f.i=U(i) from SeqLambda;
now
let i be Nat;
assume i in dom f;
then i in Seg n by A1,FINSEQ_1:def 3;
then f.i = s.intpos (m+i) by A1;
hence f.i in INT by INT_1:12;
end;
then reconsider f as FinSequence of INT by FINSEQ_2:14;
take f;
thus len f=n by A1;
hereby
let i be Nat;
assume 1<=i & i <= len f;
then i in Seg n by A1,FINSEQ_1:3;
hence f.i = s.intpos (m+i) by A1;
end;
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 & for i be Nat st 1<=i & i <= len f holds
f.i=s.intpos(m+i) by Th2;
take f;
thus len f=n by A1;
thus f is_FinSequence_on s,m by A1,Def1;
end;
theorem Th4:
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 A1: 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;
A2: Seg (len f) = dom f by FINSEQ_1:def 3;
A3: m in Seg (len f) by A1,FINSEQ_1:3;
A4: n in dom f by A1,A2,FINSEQ_1:3;
A5: dom f=dom g by A1,A2,FINSEQ_1:def 3;
now
let k be set;
assume A6: k<>m & k<>n & k in dom f;
then reconsider i=k as Nat;
1 <= i & i <= len f by A2,A6,FINSEQ_1:3;
hence f.k=g.k by A1,A6;
end;
hence thesis by A1,A2,A3,A4,A5,SCMBSORT:7;
end;
set A = the Instruction-Locations of SCMPDS,
D = SCM-Data-Loc;
theorem Th5: ::see SCMPDS_8:2
for s1,s2 being State of SCMPDS st
(for a being Int_position holds s1.a = s2.a)
holds Dstate(s1)=Dstate(s2)
proof
let s1,s2 be State of SCMPDS;
assume for a being Int_position holds s1.a = s2.a;
then s1 | D = s2 | D by SCMPDS_4:23;
hence thesis by SCMPDS_8:2;
end;
theorem Th6: :: see SCMPDS_7:50
for s being State of SCMPDS, I being No-StopCode Program-block,
j being parahalting shiftable Instruction of SCMPDS st
I is_closed_on s & I is_halting_on s
holds (I ';' j) is_closed_on s & (I ';' j) is_halting_on s
proof
let s be State of SCMPDS,I be No-StopCode Program-block,j be parahalting
shiftable Instruction of SCMPDS;
assume A1: I is_closed_on s & I is_halting_on s;
set Mj = Load j;
A2: Mj is_closed_on IExec(I,s) by SCMPDS_6:34;
Mj is_halting_on IExec(I,s) by SCMPDS_6:35;
then (I ';' Mj) is_closed_on s & (I ';' Mj) is_halting_on s
by A1,A2,SCMPDS_7:43;
hence thesis by SCMPDS_4:def 5;
end;
theorem :: see SCMPDS_7:49
for s being State of SCMPDS, I being No-StopCode Program-block,
J being shiftable parahalting Program-block,a be Int_position st
I is_closed_on s & I is_halting_on s
holds IExec(I ';' J, s).a = IExec(J,IExec(I,s)).a
proof
let s be State of SCMPDS,I be No-StopCode Program-block,
J be shiftable parahalting Program-block,a be Int_position;
assume A1: I is_closed_on s & I is_halting_on s;
J is_closed_on IExec(I,s) & J is_halting_on IExec(I,s)
by SCMPDS_6:34,35;
hence thesis by A1,SCMPDS_7:49;
end;
theorem :: see SCMPDS_7:49
for s being State of SCMPDS, I being No-StopCode parahalting Program-block,
J being shiftable Program-block,a be Int_position st J is_closed_on
IExec(I,s) & J is_halting_on IExec(I,s) holds
IExec(I ';' J, s).a = IExec(J,IExec(I,s)).a
proof
let s be State of SCMPDS,I be No-StopCode parahalting Program-block,
J be shiftable Program-block,a be Int_position;
assume A1: J is_closed_on IExec(I,s) & J is_halting_on IExec(I,s);
I is_closed_on s & I is_halting_on s by SCMPDS_6:34,35;
hence thesis by A1,SCMPDS_7:49;
end;
theorem :: SCMPDS_7:43
for s being State of SCMPDS, I being Program-block,J being shiftable
parahalting Program-block st I is_closed_on s & I is_halting_on s
holds I ';' J is_closed_on s & I ';' J is_halting_on s
proof
let s be State of SCMPDS,I be Program-block,J be shiftable parahalting
Program-block;
assume A1: I is_closed_on s & I is_halting_on s;
J is_closed_on IExec(I,s) & J is_halting_on IExec(I,s)
by SCMPDS_6:34,35;
hence thesis by A1,SCMPDS_7:43;
end;
theorem :: SCMPDS_7:43
for s being State of SCMPDS, I being parahalting Program-block,J being
shiftable Program-block st J is_closed_on IExec(I,s) & J is_halting_on
IExec(I,s) holds
I ';' J is_closed_on s & I ';' J is_halting_on s
proof
let s be State of SCMPDS,I be parahalting Program-block,J be shiftable
Program-block;
assume A1: J is_closed_on IExec(I,s) & J is_halting_on IExec(I,s);
I is_closed_on s & I is_halting_on s by SCMPDS_6:34,35;
hence thesis by A1,SCMPDS_7:43;
end;
theorem :: SCMPDS_7:43
for s being State of SCMPDS, I being Program-block, j being parahalting
shiftable Instruction of SCMPDS st I is_closed_on s & I is_halting_on s
holds I ';' j is_closed_on s & I ';' j is_halting_on s
proof
let s be State of SCMPDS,I be Program-block,j be shiftable parahalting
Instruction of SCMPDS;
assume A1: I is_closed_on s & I is_halting_on s;
Load j is_closed_on IExec(I,s) & Load j is_halting_on IExec(I,s)
by SCMPDS_6:34,35;
then I ';' Load j is_closed_on s & I ';' Load j is_halting_on s
by A1,SCMPDS_7:43;
hence thesis by SCMPDS_4:def 5;
end;
Lm2:
for a be Int_position,i be Integer,n be Nat,I be Program-block 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-block;
thus card stop for-down(a,i,n,I)= card for-down(a,i,n,I) +1 by SCMPDS_5:7
.= card I +3+1 by SCMPDS_7:60
.= card I +(3+1) by XCMPLX_1:1
.= card I + 4;
end;
Lm3:
for a be Int_position,i be Integer,n be Nat,
I be Program-block 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-block;
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:15;
end;
Lm4:
for I being Program-block,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-block,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: card Load i1=1 by SCMPDS_5:6;
for-down(a,i,n,I) = i1 ';' I ';' i2 ';' i3 by SCMPDS_7:def 2
.= i1 ';' (I ';' i2) ';' i3 by SCMPDS_4:51
.= Load i1 ';' (I ';' i2) ';' i3 by SCMPDS_4:def 4
.= Load i1 ';' (I ';' i2) ';' Load i3 by SCMPDS_4:def 5;
hence thesis by A1,SCMPDS_7:16;
end;
begin :: Computing the Execution Result of For-loop Program by Loop-Invariant
scheme ForDownHalt { P[set],
s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
a() -> Int_position,i() -> Integer,n() -> Nat}:
(P[s()] or not P[s()]) &
for-down(a(),i(),n(),I()) is_closed_on s() &
for-down(a(),i(),n(),I()) is_halting_on s()
provided
A1: n() > 0 and
A2: P[Dstate s()] and
A3: for t be State of SCMPDS st
P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
holds IExec(I() ';' AddTo(a(),i(),-n()),t).a()=t.a() &
IExec(I() ';' AddTo(a(),i(),-n()),t).DataLoc(s().a(),i())
=t.DataLoc(s().a(),i())-n() &
I() is_closed_on t & I() is_halting_on t &
P[Dstate(IExec(I() ';' AddTo(a(),i(),-n()),t))]
proof
set b=DataLoc(s().a(),i());
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,
iFOR=Initialized pFOR,
pJ=stop J ,
IsJ= Initialized pJ;
defpred Q[Nat] means
for t be State of SCMPDS st t.b <= $1 &
P[Dstate t] & t.a()=s().a()
holds FOR is_closed_on t & FOR is_halting_on t;
A4: Q[0] by SCMPDS_7:63;
A5: for k be Nat st Q[k] holds Q[k + 1]
proof
let k be Nat;
assume A6: Q[k];
now
let t be State of SCMPDS;
assume A7: t.b <= k+1;
assume A8: P[Dstate t];
assume A9: t.a()=s().a();
per cases;
suppose t.b <= 0;
hence FOR is_closed_on t & FOR is_halting_on t
by A9,SCMPDS_7:63;
suppose A10: t.b > 0;
set t2 = t +* IsJ,
t3 = t +* iFOR,
C3 = Computation t3,
t4 = C3.1,
Jt = IExec(J,t);
A11: card J = card I()+1 by SCMP_GCD:8;
then A12: card J > 0 by NAT_1:19;
A13: Jt.a()=t.a() & Jt.b=t.b-n()
& I() is_closed_on t & I() is_halting_on t & P[Dstate Jt]
by A3,A8,A9,A10;
then A14: J is_closed_on t & J is_halting_on t by Th6;
A15: IsJ c= t2 by FUNCT_4:26;
A16: t2 is halting by A14,SCMPDS_6:def 3;
then t2 +* IsJ is halting by A15,AMI_5:10;
then A17: J is_halting_on t2 by SCMPDS_6:def 3;
A18: J is_closed_on t2 by A14,SCMPDS_6:38;
A19: inspos 0 in dom pFOR by SCMPDS_4:75;
A20: IC t3 =inspos 0 by SCMPDS_6:21;
FOR = i1 ';' (J ';' i3) by Lm3;
then A21: CurInstr t3 = i1 by SCMPDS_6:22;
A22: (Computation t3).(0 + 1) = Following (Computation t3).0 by AMI_1:def
19
.= Following t3 by AMI_1:def 19
.= Exec(i1,t3) by A21,AMI_1:def 18;
A23: not a() in dom iFOR & a() in dom t by SCMPDS_2:49,SCMPDS_4:31;
A24: not b in dom iFOR & b in dom t by SCMPDS_2:49,SCMPDS_4:31;
A25: t3.DataLoc(t3.a(),i())= t3.b by A9,A23,FUNCT_4:12
.= t.b by A24,FUNCT_4:12;
A26: IC t4 = t4.IC SCMPDS by AMI_1:def 15
.= Next IC t3 by A10,A22,A25,SCMPDS_2:68
.= inspos(0+1) by A20,SCMPDS_4:70;
t2,t3 equal_outside A by SCMPDS_4:36;
then A27: t2 | D = t3 | D by SCMPDS_4:24;
now let x;
thus t2.x = t3.x by A27,SCMPDS_4:23
.= t4.x by A22,SCMPDS_2:68;
end;
then A28: t2 | D = t4 | D by SCMPDS_4:23;
set m2=LifeSpan t2,
t5=(Computation t4).m2,
l1=inspos (card J + 1);
A29: IExec(J,t) = Result t2 +* t | A by SCMPDS_4:def 8;
A30: dom (t | A) = A by SCMPDS_6:1;
then A31: not a() in dom (t | A) by SCMPDS_2:53;
A32: not b in dom (t | A) by A30,SCMPDS_2:53;
A33: l1=inspos (card I()+(1+1)) by A11,XCMPLX_1:1;
card I() + 2 < card I() + 3 by REAL_1:53;
then A34: l1 in dom FOR by A33,SCMPDS_7:61;
A35: FOR c= iFOR by SCMPDS_6:17;
iFOR c= t3 by FUNCT_4:26;
then A36: FOR c= t3 by A35,XBOOLE_1:1;
Shift(J,1) c= FOR by Lm4;
then Shift(J,1) c= t3 by A36,XBOOLE_1:1;
then A37: Shift(J,1) c= t4 by AMI_3:38;
then A38: (Computation t2).m2 | D = t5 | D
by A12,A15,A17,A18,A26,A28,SCMPDS_7:36;
A39: dom (t | A) = A by SCMPDS_6:1;
A40: t5|D =(Result t2)|D by A16,A38,SCMFSA6B:16
.= (Result t2 +* t | A)|D by A39,AMI_5:7,SCMPDS_2:10
.= Jt | D by SCMPDS_4:def 8;
A41: t5.a()=(Computation t2).m2.a() by A38,SCMPDS_4:23
.=(Result t2).a() by A16,SCMFSA6B:16
.=s().a() by A9,A13,A29,A31,FUNCT_4:12;
A42: t5.b=(Computation t2).m2.b by A38,SCMPDS_4:23
.=(Result t2).b by A16,SCMFSA6B:16
.=t.b - n() by A13,A29,A32,FUNCT_4:12;
set m3=m2 +1;
set t6=(Computation t3).m3;
A43: IC t5=l1 by A12,A15,A17,A18,A26,A28,A37,SCMPDS_7:36;
A44: t6=t5 by AMI_1:51;
then A45: CurInstr t6=t5.l1 by A43,AMI_1:def 17
.=t4.l1 by AMI_1:54
.=t3.l1 by AMI_1:54
.=FOR.l1 by A34,A36,GRFUNC_1:8
.=i3 by A33,SCMPDS_7:62;
set m4=m3+1,
t7=(Computation t3).m4;
A46: t7 = Following t6 by AMI_1:def 19
.= Exec(i3,t6) by A45,AMI_1:def 18;
A47: IC t7=t7.IC SCMPDS by AMI_1:def 15
.=ICplusConst(t6,-(card I()+2)) by A46,SCMPDS_2:66
.=ICplusConst(t6,0-(card I()+2)) by XCMPLX_1:150
.=inspos 0 by A33,A43,A44,SCMPDS_7:1;
A48: t7.a()=s().a() by A41,A44,A46,SCMPDS_2:66;
InsCode i3=0 by SCMPDS_2:21;
then InsCode i3 in {0,4,5,6} by ENUMSET1:19;
then Dstate(t7)=Dstate(t6) by A46,SCMPDS_8:3
.=Dstate(Jt) by A40,A44,SCMPDS_8:2;
then A49: P[Dstate t7] by A3,A8,A9,A10;
A50: t7.b=t.b-n() by A42,A44,A46,SCMPDS_2:66
.=-n()+t.b by XCMPLX_0:def 8;
-(-n()) > 0 by A1;
then -n() < 0 by REAL_1:66;
then -n() <= -1 by INT_1:21;
then -n()+t.b <= -1+t.b by AXIOMS:24;
then A51: -n()+t.b <= t.b-1 by XCMPLX_0:def 8;
t.b-1 <= k by A7,REAL_1:86;
then -n()+t.b <= k by A51,AXIOMS:22;
then A52: FOR is_closed_on t7 & FOR is_halting_on t7 by A6,A48,A49,A50;
A53: t7 +* iFOR=t7 by A47,SCMPDS_7:37;
now
let k be Nat;
per cases;
suppose k < m4;
then A54: k <= m3 by INT_1:20;
hereby
per cases by A54,NAT_1:26;
suppose A55:k <= m2;
hereby
per cases;
suppose k=0;
hence IC (Computation t3).k in dom pFOR by A19,A20,AMI_1:def
19;
suppose k<>0;
then consider kn be Nat such that
A56: k=kn+1 by NAT_1:22;
kn < k by A56,REAL_1:69;
then kn < m2 by A55,AXIOMS:22;
then A57: IC (Computation t2).kn + 1 = IC (Computation t4).kn
by A12,A15,A17,A18,A26,A28,A37,SCMPDS_7:34;
A58: IC (Computation t2).kn in dom pJ by A14,SCMPDS_6:def 2;
consider lm be Nat such that
A59: IC (Computation t2).kn=inspos lm by SCMPDS_3:32;
lm < card pJ by A58,A59,SCMPDS_4:1;
then lm < card J+1 by SCMPDS_5:7;
then lm+1 <= card J +1 by INT_1:20;
then A60: lm+1 <= card I()+(1+1) by A11,XCMPLX_1:1;
card I() + 2 < card I() + 4 by REAL_1:53;
then lm+1 < card I() +4 by A60,AXIOMS:22;
then A61: lm+1 < card pFOR by Lm2;
IC (Computation t3).k=inspos lm +1 by A56,A57,A59,AMI_1:51
.=inspos (lm+1) by SCMPDS_3:def 3;
hence IC (Computation t3).k in dom pFOR by A61,SCMPDS_4:1;
end;
suppose A62:k=m3;
l1 in dom pFOR by A34,SCMPDS_6:18;
hence IC (Computation t3).k in dom pFOR by A12,A15,A17,A18,A26,
A28,A37,A44,A62,SCMPDS_7:36;
end;
suppose k >= m4;
then consider nn be Nat such that
A63: k=m4+nn by NAT_1:28;
C3.k=(Computation (t7 +* iFOR)).nn by A53,A63,AMI_1:51;
hence IC (Computation t3).k in dom pFOR by A52,SCMPDS_6:def 2;
end;
hence FOR is_closed_on t by SCMPDS_6:def 2;
t7 is halting by A52,A53,SCMPDS_6:def 3;
then t3 is halting by SCM_1:27;
hence FOR is_halting_on t by SCMPDS_6:def 3;
end;
hence Q[k+1];
end;
A64: for k being Nat holds Q[k] from Ind(A4,A5);
thus P[s()] or not P[s()];
per cases;
suppose s().b <= 0;
hence FOR is_closed_on s() & FOR is_halting_on s() by SCMPDS_7:63;
suppose s().b > 0;
then reconsider m=s().b as Nat by INT_1:16;
Q[m] by A64;
hence FOR is_closed_on s() & FOR is_halting_on s() by A2;
end;
scheme ForDownExec { P[set],
s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
a() -> Int_position,i() -> Integer,n() -> Nat}:
(P[s()] or not P[s()]) &
IExec(for-down(a(),i(),n(),I()),s()) =
IExec(for-down(a(),i(),n(),I()),IExec(I() ';' AddTo(a(),i(),-n()),s()))
provided
A1: n() > 0 and
A2: s().DataLoc(s().a(),i()) > 0 and
A3: P[Dstate s()] and
A4: for t be State of SCMPDS st
P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
holds IExec(I() ';' AddTo(a(),i(),-n()),t).a()=t.a() &
IExec(I() ';' AddTo(a(),i(),-n()),t).DataLoc(s().a(),i())
=t.DataLoc(s().a(),i())-n() &
I() is_closed_on t & I() is_halting_on t &
P[Dstate(IExec(I() ';' AddTo(a(),i(),-n()),t))]
proof
set b=DataLoc(s().a(),i());
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()),
iFOR=Initialized stop FOR,
iJ= Initialized stop J,
s1= s() +* iFOR,
C1=Computation s1,
ps= s() | A;
defpred X[set] means P[$1];
A5: X[Dstate s()] by A3;
A6: for t be State of SCMPDS st
X[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
holds IExec(I() ';' AddTo(a(),i(),-n()),t).a()=t.a() &
IExec(I() ';' AddTo(a(),i(),-n()),t).DataLoc(s().a(),i())
=t.DataLoc(s().a(),i())-n() &
I() is_closed_on t & I() is_halting_on t &
X[Dstate(IExec(I() ';' AddTo(a(),i(),-n()),t))] by A4;
(X[s()] or not X[s()]) &
for-down(a(),i(),n(),I()) is_closed_on s() &
for-down(a(),i(),n(),I()) is_halting_on s()
from ForDownHalt(A1,A5,A6);
then A7: s1 is halting by SCMPDS_6:def 3;
set sJ= s() +* iJ,
mJ=LifeSpan sJ,
m1=mJ+2,
s2=IExec(J,s()) +* iFOR,
C2=Computation s2,
m2=LifeSpan s2;
set Es=IExec(J,s()),
bj=DataLoc(Es.a(),i());
A8: card J = card I()+1 by SCMP_GCD:8;
then A9: card J > 0 by NAT_1:19;
A10: Es.a()=s().a() & Es.b =s().b-n() &
I() is_closed_on s() & I() is_halting_on s() &
P[Dstate Es] by A2,A5,A6;
then A11: J is_closed_on s() & J is_halting_on s() by Th6;
A12: X[Dstate Es] by A2,A5,A6;
A13: for t being State of SCMPDS st
X[Dstate t] & t.a()=Es.a() & t.bj > 0 holds
IExec(J,t).a()=t.a() & IExec(J,t).bj=t.bj-n() &
I() is_closed_on t & I() is_halting_on t &
X[Dstate IExec(J,t) ] by A6,A10;
A14: (X[Es] or not X[Es]) & FOR is_closed_on Es & FOR is_halting_on Es
from ForDownHalt(A1,A12,A13);
set s4 = C1.1;
A15: iJ c= sJ by FUNCT_4:26;
A16: sJ is halting by A11,SCMPDS_6:def 3;
then sJ +* iJ is halting by A15,AMI_5:10;
then A17: J is_halting_on sJ by SCMPDS_6:def 3;
A18: J is_closed_on sJ by A11,SCMPDS_6:38;
A19: IC s1 =inspos 0 by SCMPDS_6:21;
A20: FOR = i1 ';' (J ';' i3) by Lm3;
then A21: CurInstr s1 = i1 by SCMPDS_6:22;
A22: (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
.= Following s1 by AMI_1:def 19
.= Exec(i1,s1) by A21,AMI_1:def 18;
A23: not a() in dom iFOR & a() in dom s() by SCMPDS_2:49,SCMPDS_4:31;
A24: not b in dom iFOR & b in dom s() by SCMPDS_2:49,SCMPDS_4:31;
A25: s1.DataLoc(s1.a(),i())=s1.b by A23,FUNCT_4:12
.= s().b by A24,FUNCT_4:12;
A26: IC s4 = s4.IC SCMPDS by AMI_1:def 15
.= Next IC s1 by A2,A22,A25,SCMPDS_2:68
.= inspos(0+1) by A19,SCMPDS_4:70;
sJ,s1 equal_outside A by SCMPDS_4:36;
then A27: sJ | D = s1 | D by SCMPDS_4:24;
now let x;
thus sJ.x = s1.x by A27,SCMPDS_4:23
.= s4.x by A22,SCMPDS_2:68;
end;
then A28: sJ | D = s4 | D by SCMPDS_4:23;
set s5=(Computation s4).mJ,
l1=inspos (card J + 1);
A29: IExec(J,s()) = Result sJ +* s() | A by SCMPDS_4:def 8;
A30: dom (s() | A) = A by SCMPDS_6:1;
A31: l1=inspos (card I()+(1+1)) by A8,XCMPLX_1:1;
card I() + 2 < card I() + 3 by REAL_1:53;
then A32: l1 in dom FOR by A31,SCMPDS_7:61;
A33: FOR c= iFOR by SCMPDS_6:17;
iFOR c= s1 by FUNCT_4:26;
then A34: FOR c= s1 by A33,XBOOLE_1:1;
Shift(J,1) c= FOR by Lm4;
then Shift(J,1) c= s1 by A34,XBOOLE_1:1;
then A35: Shift(J,1) c= s4 by AMI_3:38;
then A36: (Computation sJ).mJ | D = s5 | D
by A9,A15,A17,A18,A26,A28,SCMPDS_7:36;
set m3=mJ +1;
set s6=(Computation s1).m3;
A37: IC s5=l1 by A9,A15,A17,A18,A26,A28,A35,SCMPDS_7:36;
A38: s6=s5 by AMI_1:51;
then A39: CurInstr s6=s5.l1 by A37,AMI_1:def 17
.=s4.l1 by AMI_1:54
.=s1.l1 by AMI_1:54
.=FOR.l1 by A32,A34,GRFUNC_1:8
.=i3 by A31,SCMPDS_7:62;
set m4=m3+1,
s7=(Computation s1).m4;
A40: s7 = Following s6 by AMI_1:def 19
.= Exec(i3,s6) by A39,AMI_1:def 18;
A41: IC s7=s7.IC SCMPDS by AMI_1:def 15
.=ICplusConst(s6,-(card I()+2)) by A40,SCMPDS_2:66
.=ICplusConst(s6,0-(card I()+2)) by XCMPLX_1:150
.=inspos 0 by A31,A37,A38,SCMPDS_7:1;
A42: m4=mJ+(1+1) by XCMPLX_1:1
.=mJ+2;
now
let x be Int_position;
not x in dom iFOR & x in dom IExec(J,s())
by SCMPDS_2:49,SCMPDS_4:31;
then A43: s2.x=IExec(J,s()).x by FUNCT_4:12;
A44: not x in dom (s() | A) by A30,SCMPDS_2:53;
s5.x=(Computation sJ).mJ.x by A36,SCMPDS_4:23
.=(Result sJ).x by A16,SCMFSA6B:16
.=IExec(J,s()).x by A29,A44,FUNCT_4:12;
hence s7.x=s2.x by A38,A40,A43,SCMPDS_2:66;
end;
then A45: s7 | D = s2 | D by SCMPDS_4:23;
A46: IC s2 =IC C1.m1 by A41,A42,SCMPDS_6:21;
A47: s2 is halting by A14,SCMPDS_6:def 3;
A48: dom ps = dom s() /\ A by RELAT_1:90
.= ({IC SCMPDS} \/ D \/ A) /\ A by SCMPDS_4:19
.= A by XBOOLE_1:21;
s2 | A= (Result sJ +* ps +* iFOR) | A by SCMPDS_4:def 8
.=(Result sJ +* ps)|A +* iFOR | A by AMI_5:6
.= ps +* iFOR | A by A48,FUNCT_4:24
.= s1 | A by AMI_5:6
.= C1.m1 | A by SCMPDS_7:6;
then A49: C1.m1=s2 by A42,A45,A46,SCMPDS_7:7;
then CurInstr C1.m1=i1 by A20,SCMPDS_6:22;
then A50: CurInstr C1.m1 <> halt SCMPDS by SCMPDS_6:30;
set m0=LifeSpan s1;
m0 > m1 by A7,A50,SCMPDS_6:2;
then consider nn be Nat such that
A51: m0=m1+nn by NAT_1:28;
A52: C1.m0 = C2.nn by A49,A51,AMI_1:51;
then CurInstr C2.nn =halt SCMPDS by A7,SCM_1:def 2;
then A53: nn >= m2 by A47,SCM_1:def 2;
C1.(m1 + m2) = C2.m2 by A49,AMI_1:51;
then CurInstr C1.(m1 + m2) = halt SCMPDS by A47,SCM_1:def 2;
then m1 + m2 >= m0 by A7,SCM_1:def 2;
then m2 >= nn by A51,REAL_1:53;
then nn=m2 by A53,AXIOMS:21;
then A54: Result s1 = C2.m2 by A7,A52,SCMFSA6B:16;
A55: IExec(J,s()) | A= (Result sJ +* ps) | A by SCMPDS_4:def 8
.= ps by A48,FUNCT_4:24;
thus P[s()] or not P[s()];
thus IExec(FOR,s())
= C2.m2 +* ps by A54,SCMPDS_4:def 8
.= Result s2 +* IExec(J,s()) | A by A47,A55,SCMFSA6B:16
.= IExec(FOR,IExec(J,s())) by SCMPDS_4:def 8;
end;
scheme ForDownEnd { P[set],
s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
a() -> Int_position,i() -> Integer,n() -> Nat}:
(P[s()] or not P[s()]) &
IExec(for-down(a(),i(),n(),I()),s()).DataLoc(s().a(),i()) <= 0 &
P[Dstate IExec(for-down(a(),i(),n(),I()),s())]
provided
A1: n() > 0 and
A2: P[Dstate s()] and
A3: for t be State of SCMPDS st
P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
holds IExec(I() ';' AddTo(a(),i(),-n()),t).a()=t.a() &
IExec(I() ';' AddTo(a(),i(),-n()),t).DataLoc(s().a(),i())
=t.DataLoc(s().a(),i())-n() &
I() is_closed_on t & I() is_halting_on t &
P[Dstate(IExec(I() ';' AddTo(a(),i(),-n()),t))]
proof
set b=DataLoc(s().a(),i()),
FR=for-down(a(),i(),n(),I());
defpred Q[Nat] means
for t be State of SCMPDS st t.b <= $1 & t.a()=s().a() & P[Dstate t]
holds IExec(FR,t).b <= 0 & P[Dstate IExec(FR,t)];
A4: Q[0]
proof
let t be State of SCMPDS;
assume A5: t.b <= 0 & t.a()=s().a() & P[Dstate t];
then A6: for x be Int_position holds IExec(FR,t).x = t.x by SCMPDS_7:66;
thus IExec(FR,t).b <= 0 by A5,SCMPDS_7:66;
thus P[Dstate IExec(FR,t)] by A5,A6,Th5;
end;
A7: now
let k be Nat;
assume A8:Q[k];
now
let u be State of SCMPDS;
assume A9: u.b <= k+1 & u.a()=s().a() & P[Dstate u];
per cases;
suppose u.b <= 0;
hence IExec(FR,u).b <= 0 & P[Dstate IExec(FR,u)] by A4,A9;
suppose A10: u.b > 0;
then A11: u.DataLoc(u.a(),i()) > 0 by A9;
defpred X[set] means P[$1];
A12: X[Dstate u] by A9;
set Ad=AddTo(a(),i(),-n());
A13: for t being State of SCMPDS st
X[Dstate t] & t.a()=u.a() & t.DataLoc(u.a(),i()) > 0 holds
IExec(I() ';' Ad,t).a()=t.a() &
IExec(I() ';' Ad,t).DataLoc(u.a(),i())
=t.DataLoc(u.a(),i())-n() &
I() is_closed_on t & I() is_halting_on t &
X[Dstate(IExec(I() ';' Ad,t))] by A3,A9;
set Iu=IExec(I() ';' Ad,u);
A14: (X[u] or not X[u]) &
IExec(FR,u) = IExec(FR,Iu) from ForDownExec(A1,A11,A12,A13);
A15: Iu.b=u.b-n() by A3,A9,A10;
u.b-n() < u.b by A1,SQUARE_1:29;
then Iu.b+1 <= u.b by A15,INT_1:20;
then Iu.b+1 <= k+1 by A9,AXIOMS:22;
then A16: Iu.b <= k by REAL_1:53;
A17: Iu.a()=s().a() by A3,A9,A10;
P[Dstate Iu] by A3,A9,A10;
hence IExec(FR,u).b <= 0 & P[Dstate IExec(FR,u)] by A8,A14,A16,A17;
end;
hence Q[k+1];
end;
A18: for k being Nat holds Q[k] from Ind(A4,A7);
thus (P[s()] or not P[s()]);
per cases;
suppose s().b > 0;
then reconsider m=s().b as Nat by INT_1:16;
Q[m] by A18;
hence thesis by A2;
suppose s().b <= 0;
hence thesis by A2,A4;
end;
theorem Th12:
for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
a,x,y be Int_position, i,c be Integer,n be Nat st
n > 0 & s.x >= s.y +c &
for t be State of SCMPDS st
t.x >= t.y +c & t.a=s.a & t.DataLoc(s.a,i) > 0
holds IExec(I ';' AddTo(a,i,-n),t).a=t.a &
IExec(I ';' AddTo(a,i,-n),t).DataLoc(s.a,i)=t.DataLoc(s.a,i)-n &
I is_closed_on t & I is_halting_on t &
IExec(I ';' AddTo(a,i,-n),t).x>=IExec(I ';' AddTo(a,i,-n),t).y+c
holds
for-down(a,i,n,I) is_closed_on s & for-down(a,i,n,I) is_halting_on s
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
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;
assume A2: s.x >= s.y +c;
assume A3: for t be State of SCMPDS st
t.x >= t.y +c & t.a=s.a & t.b > 0
holds IExec(J,t).a=t.a & IExec(J,t).b=t.b-n &
I is_closed_on t & I is_halting_on t &
IExec(J,t).x>=IExec(J,t).y+c;
defpred P[set] means ex t be State of SCMPDS st
t=$1 & t.x >= t.y+c;
A4: P[Dstate s]
proof
take t=Dstate s;
thus t=Dstate s;
t.x>= s.y+c by A2,SCMPDS_8:4;
hence t.x>=t.y+c by SCMPDS_8:4;
end;
A5: now
let t be State of SCMPDS;
assume A6: P[Dstate t] & t.a=s.a & t.b > 0;
then consider v be State of SCMPDS such that
A7: v=Dstate t & v.x>=v.y+c;
t.x=v.x by A7,SCMPDS_8:4;
then A8: t.x>=t.y+c by A7,SCMPDS_8:4;
hence IExec(J,t).a=t.a & IExec(J,t).b=t.b-n &
I is_closed_on t & I is_halting_on t by A3,A6;
thus P[Dstate IExec(J,t)]
proof
take v=Dstate IExec(J,t);
thus v=Dstate IExec(J,t);
v.x=IExec(J,t).x by SCMPDS_8:4;
then v.x>=IExec(J,t).y+c by A3,A6,A8;
hence v.x>=v.y+c by SCMPDS_8:4;
end;
end;
(P[s] or not P[s]) &
for-down(a,i,n,I) is_closed_on s &
for-down(a,i,n,I) is_halting_on s
from ForDownHalt(A1,A4,A5);
hence thesis;
end;
theorem Th13:
for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
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 State of SCMPDS st
t.x >= t.y +c & t.a=s.a & t.DataLoc(s.a,i) > 0
holds IExec(I ';' AddTo(a,i,-n),t).a=t.a &
IExec(I ';' AddTo(a,i,-n),t).DataLoc(s.a,i)=t.DataLoc(s.a,i)-n &
I is_closed_on t & I is_halting_on t &
IExec(I ';' AddTo(a,i,-n),t).x>=IExec(I ';' AddTo(a,i,-n),t).y+c
holds
IExec(for-down(a,i,n,I),s) =
IExec(for-down(a,i,n,I),IExec(I ';' AddTo(a,i,-n),s))
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
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;
assume A2: s.x >= s.y +c;
assume A3: s.b > 0;
assume A4: for t be State of SCMPDS st
t.x >= t.y +c & t.a=s.a & t.b > 0
holds IExec(J,t).a=t.a & IExec(J,t).b=t.b-n &
I is_closed_on t & I is_halting_on t &
IExec(J,t).x>=IExec(J,t).y+c;
defpred P[set] means ex t be State of SCMPDS st
t=$1 & t.x>=t.y+c;
A5: P[Dstate s]
proof
take t=Dstate s;
thus t=Dstate s;
t.x>= s.y+c by A2,SCMPDS_8:4;
hence t.x>=t.y+c by SCMPDS_8:4;
end;
A6: now
let t be State of SCMPDS;
assume A7: P[Dstate t] & t.a=s.a & t.b > 0;
then consider v be State of SCMPDS such that
A8: v=Dstate t & v.x>=v.y+c;
t.x=v.x by A8,SCMPDS_8:4;
then A9: t.x>=t.y+c by A8,SCMPDS_8:4;
hence IExec(J,t).a=t.a & IExec(J,t).b=t.b-n &
I is_closed_on t & I is_halting_on t by A4,A7;
thus P[Dstate IExec(J,t) ]
proof
take v=Dstate IExec(J,t);
thus v=Dstate IExec(J,t);
v.x=IExec(J,t).x by SCMPDS_8:4;
then v.x>=IExec(J,t).y+c by A4,A7,A9;
hence v.x>=v.y+c by SCMPDS_8:4;
end;
end;
(P[s] or not P[s]) &
IExec(for-down(a,i,n,I),s) =
IExec(for-down(a,i,n,I),IExec(I ';' AddTo(a,i,-n),s))
from ForDownExec(A1,A3,A5,A6);
hence thesis;
end;
theorem
for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
a be Int_position, i be Integer,n be Nat
st s.DataLoc(s.a,i) > 0 & n > 0 & card I > 0 &
a <> DataLoc(s.a,i) & (for t be State of SCMPDS st t.a=s.a
holds IExec(I,t).a=t.a & IExec(I,t).DataLoc(s.a,i)=t.DataLoc(s.a,i) &
I is_closed_on t & I is_halting_on t)
holds
for-down(a,i,n,I) is_closed_on s & for-down(a,i,n,I) is_halting_on s
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position, i be Integer,n be Nat;
assume A1: s.DataLoc(s.a,i) > 0 & n > 0 & card I > 0 &
a <> DataLoc(s.a,i) & (for t be State of SCMPDS st t.a=s.a
holds IExec(I,t).a=t.a & IExec(I,t).DataLoc(s.a,i)=t.DataLoc(s.a,i) &
I is_closed_on t & I is_halting_on t);
then for t being State of SCMPDS
st (for x be Int_position st x in {} holds t.x=s.x) & t.a=s.a holds
IExec(I,t).a=t.a & IExec(I,t).DataLoc(s.a,i)=t.DataLoc(s.a,i) &
I is_closed_on t & I is_halting_on t &
for y be Int_position st y in {} holds IExec(I,t).y=t.y;
hence thesis by A1,SCMPDS_7:67;
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-block equals :Def2:
((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=k3 ';' k4 ';' k5 ';' k6 ';' k7,
IF= if>0(GBP,5, TR,FA),
B1= k1 ';' k2 ';' IF,
WH= while>0(GBP,6,B1),
J4= j1 ';' j2 ';' j3 ';' j4,
B2= J4 ';' WH,
FR= for-down(GBP,2,1,B2);
Lm5:
card B1=10
proof
thus card B1=card (k1 ';' k2)+card IF by SCMPDS_4:45
.=2+card IF by SCMP_GCD:9
.=2+(card TR+card FA+2) by SCMPDS_6:79
.=2+(card (k3 ';' k4 ';' k5 ';' k6) +1+card FA+2) by SCMP_GCD:8
.=2+(card (k3 ';' k4 ';' k5)+1 +1+card FA+2) by SCMP_GCD:8
.=2+(card (k3 ';' k4)+1+1 +1+card FA+2) by SCMP_GCD:8
.=2+(2+1+1 +1+card FA+2) by SCMP_GCD:9
.=2+(2+1+1+1+1+2) by SCMPDS_5:6
.=10;
end;
Lm6:
card B2=16
proof
thus card B2=card (j1 ';' j2 ';' j3 ';' j4) + card WH by SCMPDS_4:45
.=card (j1 ';' j2 ';' j3)+1+ card WH by SCMP_GCD:8
.=card (j1 ';' j2 )+1+1+ card WH by SCMP_GCD:8
.=2+1+1+ card WH by SCMP_GCD:9
.=2+1+1+(10+2) by Lm5,SCMPDS_8:17
.=16;
end;
set a1=intpos 1,
a2=intpos 2,
a3=intpos 3,
a4=intpos 4,
a5=intpos 5,
a6=intpos 6;
Lm7:
for s being State of SCMPDS st s.a4 >= 7+s.a6 & s.GBP=0 & s.a6 > 0
holds
IExec(B1,s).GBP=0 & IExec(B1,s).a1=s.a1 &
IExec(B1,s).a2=s.a2 & IExec(B1,s).a3=s.a3 &
IExec(B1,s).a6 < s.a6 &
IExec(B1,s).a4 >= 7+IExec(B1,s).a6 &
(for i be Nat st i>=7 & i<>s.a4-1 & i<>s.a4 holds
IExec(B1,s).intpos i=s.intpos i) &
(s.DataLoc(s.a4,-1) > s.DataLoc(s.a4,0) implies
IExec(B1,s).DataLoc(s.a4,-1)=s.DataLoc(s.a4,0) &
IExec(B1,s).DataLoc(s.a4,0) =s.DataLoc(s.a4,-1) &
IExec(B1,s).a6=s.a6-1 & IExec(B1,s).a4=s.a4-1 ) &
(s.DataLoc(s.a4,-1) <= s.DataLoc(s.a4,0) implies
IExec(B1,s).DataLoc(s.a4,-1)=s.DataLoc(s.a4,-1) &
IExec(B1,s).DataLoc(s.a4,0) =s.DataLoc(s.a4,0) & IExec(B1,s).a6=0)
proof
let s be State of SCMPDS;
set a=GBP,
x=DataLoc(s.a4,-1),
y=DataLoc(s.a4,0);
assume A1: s.a4 >= 7+s.a6 & s.a=0 & s.a6 > 0;
set t0=Initialized s,
t1=Exec(k1, t0),
t2=IExec(k1 ';' k2,s);
s.a4>=(1+6)+s.a6 by A1;
then s.a4>=1+(6+s.a6) by XCMPLX_1:1;
then A2: s.a4-1 >= 6+s.a6 by REAL_1:84;
A3: 6+s.a6>6+0 by A1,REAL_1:53;
then 6+s.a6>= 6+1 by INT_1:20;
then s.a4-1 >= 7 by A2,AXIOMS:22;
then 2*(s.a4-1) >= 2*7 by AXIOMS:25;
then A4: 2*(s.a4-1)+1 >= 14+1 by AXIOMS:24;
A5: s.a4-1 > 0 by A2,A3,AXIOMS:22;
A6: 2*abs((s.a4+-1))+1=2*abs(s.a4-1)+1 by XCMPLX_0:def 8
.=2*(s.a4-1)+1 by A5,ABSVALUE:def 1;
then A7: x=2*(s.a4-1)+1 by SCMPDS_2:def 4;
A8: 7+s.a6>7+0 by A1,REAL_1:53;
then s.a4 > 7 by A1,AXIOMS:22;
then 2*(s.a4) > 2*7 by REAL_1:70;
then A9: 2*(s.a4)+1>14+1 by REAL_1:53;
A10: s.a4 > 0 by A1,A8,AXIOMS:22;
A11: y=2*abs((s.a4+0))+1 by SCMPDS_2:def 4
.=2*(s.a4)+1 by A10,ABSVALUE:def 1;
A12: a=dl.0 by SCMP_GCD:def 1,def 2
.=2*0+1 by AMI_3:def 19
.=1;
A13: a1=dl.1 by SCMP_GCD:def 1
.=2*1+1 by AMI_3:def 19
.=3;
A14: a2=dl.2 by SCMP_GCD:def 1
.=2*2+1 by AMI_3:def 19
.=5;
A15: a3=dl.3 by SCMP_GCD:def 1
.=2*3+1 by AMI_3:def 19
.=7;
A16: a4=dl.4 by SCMP_GCD:def 1
.=2*4+1 by AMI_3:def 19
.=9;
A17: a5=dl.5 by SCMP_GCD:def 1
.=2*5+1 by AMI_3:def 19
.=11;
A18: a6=dl.6 by SCMP_GCD:def 1
.=2*6+1 by AMI_3:def 19
.=13;
A19: t0.a=0 by A1,SCMPDS_5:40;
A20: t0.a1=s.a1 by SCMPDS_5:40;
A21: t0.a2=s.a2 by SCMPDS_5:40;
A22: t0.a3=s.a3 by SCMPDS_5:40;
A23: t0.a4=s.a4 by SCMPDS_5:40;
A24: t0.a6=s.a6 by SCMPDS_5:40;
A25: t0.x=s.x by SCMPDS_5:40;
A26: t0.y=s.y by SCMPDS_5:40;
A27: DataLoc(t0.a,5)=intpos (0+5) by A19,SCMP_GCD:5;
then a<>DataLoc(t0.a,5) by SCMP_GCD:4,def 2;
then A28: t1.a=0 by A19,SCMPDS_2:59;
a1<>DataLoc(t0.a,5) by A27,SCMP_GCD:4;
then A29: t1.a1=s.a1 by A20,SCMPDS_2:59;
a2<>DataLoc(t0.a,5) by A27,SCMP_GCD:4;
then A30: t1.a2=s.a2 by A21,SCMPDS_2:59;
a3<>DataLoc(t0.a,5) by A27,SCMP_GCD:4;
then A31: t1.a3=s.a3 by A22,SCMPDS_2:59;
a4<>DataLoc(t0.a,5) by A27,SCMP_GCD:4;
then A32: t1.a4=s.a4 by A23,SCMPDS_2:59;
A33: t1.a5=s.x by A23,A25,A27,SCMPDS_2:59;
a6<>DataLoc(t0.a,5) by A27,SCMP_GCD:4;
then A34: t1.a6=s.a6 by A24,SCMPDS_2:59;
x<>DataLoc(t0.a,5) by A4,A7,A17,A27;
then A35: t1.x=s.x by A25,SCMPDS_2:59;
y<>DataLoc(t0.a,5) by A9,A11,A17,A27;
then A36: t1.y=s.y by A26,SCMPDS_2:59;
A37: now let i be Nat;
assume i>=7 & i<>s.a4-1 & i <> s.a4;
then i>5 by AXIOMS:22;
then intpos i <> DataLoc(t0.a,5) by A27,SCMP_GCD:4;
hence t1.intpos i=t0.intpos i by SCMPDS_2:59
.=s.intpos i by SCMPDS_5:40;
end;
A38: DataLoc(t1.a,5)=intpos (0+5) by A28,SCMP_GCD:5;
then A39: a<>DataLoc(t1.a,5) by SCMP_GCD:4,def 2;
A40: t2.a=Exec(k2, t1).a by SCMPDS_5:47
.=0 by A28,A39,SCMPDS_2:62;
A41: a1<>DataLoc(t1.a,5) by A38,SCMP_GCD:4;
A42: t2.a1=Exec(k2, t1).a1 by SCMPDS_5:47
.=s.a1 by A29,A41,SCMPDS_2:62;
A43: a2<>DataLoc(t1.a,5) by A38,SCMP_GCD:4;
A44: t2.a2=Exec(k2, t1).a2 by SCMPDS_5:47
.=s.a2 by A30,A43,SCMPDS_2:62;
A45: a3<>DataLoc(t1.a,5) by A38,SCMP_GCD:4;
A46: t2.a3=Exec(k2, t1).a3 by SCMPDS_5:47
.=s.a3 by A31,A45,SCMPDS_2:62;
A47: a4<>DataLoc(t1.a,5) by A38,SCMP_GCD:4;
A48: t2.a4=Exec(k2, t1).a4 by SCMPDS_5:47
.=s.a4 by A32,A47,SCMPDS_2:62;
A49: t2.a5=Exec(k2, t1).a5 by SCMPDS_5:47
.=s.x-s.y by A32,A33,A36,A38,SCMPDS_2:62;
A50: t2.DataLoc(t2.a,5)=t2.intpos (0+5) by A40,SCMP_GCD:5
.=s.x-s.y by A49;
A51: a6<>DataLoc(t1.a,5) by A38,SCMP_GCD:4;
A52: t2.a6=Exec(k2, t1).a6 by SCMPDS_5:47
.=s.a6 by A34,A51,SCMPDS_2:62;
A53: x<>DataLoc(t1.a,5) by A4,A7,A17,A38;
A54: t2.x=Exec(k2, t1).x by SCMPDS_5:47
.=s.x by A35,A53,SCMPDS_2:62;
A55: y<>DataLoc(t1.a,5) by A9,A11,A17,A38;
A56: t2.y=Exec(k2, t1).y by SCMPDS_5:47
.=s.y by A36,A55,SCMPDS_2:62;
A57: now let i be Nat;
assume A58: i>=7 & i<>s.a4-1 & i <> s.a4;
then i>5 by AXIOMS:22;
then A59: intpos i <> DataLoc(t1.a,5) by A38,SCMP_GCD:4;
thus t2.intpos i=Exec(k2, t1).intpos i by SCMPDS_5:47
.=t1.intpos i by A59,SCMPDS_2:62
.=s.intpos i by A37,A58;
end;
set Fi= (a,6):=0,
t02=Initialized t2,
t3=IExec(k3 ';' k4 ';' k5 ';' k6,t2),
t4=IExec(k3 ';' k4 ';' k5,t2),
t5=IExec(k3 ';' k4,t2),
t6=Exec(k3, t02);
A60: t02.a=0 by A40,SCMPDS_5:40;
A61: t02.a1=s.a1 by A42,SCMPDS_5:40;
A62: t02.a2=s.a2 by A44,SCMPDS_5:40;
A63: t02.a3=s.a3 by A46,SCMPDS_5:40;
A64: t02.a4=s.a4 by A48,SCMPDS_5:40;
A65: t02.a6=s.a6 by A52,SCMPDS_5:40;
A66: t02.x=s.x by A54,SCMPDS_5:40;
A67: t02.y=s.y by A56,SCMPDS_5:40;
A68: DataLoc(t02.a,5)=intpos (0+5) by A60,SCMP_GCD:5;
then a<>DataLoc(t02.a,5) by SCMP_GCD:4,def 2;
then A69: t6.a=0 by A60,SCMPDS_2:59;
a1<>DataLoc(t02.a,5) by A68,SCMP_GCD:4;
then A70: t6.a1=s.a1 by A61,SCMPDS_2:59;
a2<>DataLoc(t02.a,5) by A68,SCMP_GCD:4;
then A71: t6.a2=s.a2 by A62,SCMPDS_2:59;
a3<>DataLoc(t02.a,5) by A68,SCMP_GCD:4;
then A72: t6.a3=s.a3 by A63,SCMPDS_2:59;
a4<>DataLoc(t02.a,5) by A68,SCMP_GCD:4;
then A73: t6.a4=s.a4 by A64,SCMPDS_2:59;
A74: t6.a5=s.x by A64,A66,A68,SCMPDS_2:59;
a6<>DataLoc(t02.a,5) by A68,SCMP_GCD:4;
then A75: t6.a6=s.a6 by A65,SCMPDS_2:59;
y<>DataLoc(t02.a,5) by A9,A11,A17,A68;
then A76: t6.y=s.y by A67,SCMPDS_2:59;
A77: now let i be Nat;
assume A78: i>=7 & i<>s.a4-1 & i <> s.a4;
then i>5 by AXIOMS:22;
then intpos i <> DataLoc(t02.a,5) by A68,SCMP_GCD:4;
hence t6.intpos i=t02.intpos i by SCMPDS_2:59
.=t2.intpos i by SCMPDS_5:40
.=s.intpos i by A57,A78;
end;
A79: DataLoc(t6.a4,-1) =2*(s.a4-1)+1 by A6,A73,SCMPDS_2:def 4;
then A80: a<>DataLoc(t6.a4,-1) by A4,A12;
A81: t5.a =Exec(k4, t6).a by SCMPDS_5:47
.=0 by A69,A80,SCMPDS_2:59;
A82: a1<>DataLoc(t6.a4,-1) by A4,A13,A79;
A83: t5.a1 =Exec(k4, t6).a1 by SCMPDS_5:47
.=s.a1 by A70,A82,SCMPDS_2:59;
A84: a2<>DataLoc(t6.a4,-1) by A4,A14,A79;
A85: t5.a2 =Exec(k4, t6).a2 by SCMPDS_5:47
.=s.a2 by A71,A84,SCMPDS_2:59;
A86: a3<>DataLoc(t6.a4,-1) by A4,A15,A79;
A87: t5.a3 =Exec(k4, t6).a3 by SCMPDS_5:47
.=s.a3 by A72,A86,SCMPDS_2:59;
A88: a4<>DataLoc(t6.a4,-1) by A4,A16,A79;
A89: t5.a4 =Exec(k4, t6).a4 by SCMPDS_5:47
.=s.a4 by A73,A88,SCMPDS_2:59;
A90: a5<>DataLoc(t6.a4,-1) by A4,A17,A79;
A91: t5.a5 =Exec(k4, t6).a5 by SCMPDS_5:47
.=s.x by A74,A90,SCMPDS_2:59;
A92: a6<>DataLoc(t6.a4,-1) by A4,A18,A79;
A93: t5.a6 =Exec(k4, t6).a6 by SCMPDS_5:47
.=s.a6 by A75,A92,SCMPDS_2:59;
A94: t5.x =Exec(k4, t6).DataLoc(t6.a4,-1) by A73,SCMPDS_5:47
.=s.y by A73,A76,SCMPDS_2:59;
A95: now let i be Nat;
assume A96: i>=7 & i<>s.a4-1 & i <> s.a4;
A97: intpos i <> DataLoc(t6.a4,-1)
proof
assume A98:intpos i=DataLoc(t6.a4,-1);
intpos i=dl.i by SCMP_GCD:def 1
.=2*i+1 by AMI_3:def 19;
then 2*i=2*(s.a4-1) by A79,A98,XCMPLX_1:2;
hence contradiction by A96,XCMPLX_1:5;
end;
thus t5.intpos i=Exec(k4, t6).intpos i by SCMPDS_5:47
.=t6.intpos i by A97,SCMPDS_2:59
.=s.intpos i by A77,A96;
end;
A99: DataLoc(t5.a4,0) =2*abs((s.a4+0))+1 by A89,SCMPDS_2:def 4
.=2*(s.a4)+1 by A10,ABSVALUE:def 1;
then A100: a<>DataLoc(t5.a4,0) by A9,A12;
A101: t4.a=Exec(k5,t5).a by SCMPDS_5:46
.=0 by A81,A100,SCMPDS_2:59;
A102: a1<>DataLoc(t5.a4,0) by A9,A13,A99;
A103: t4.a1=Exec(k5,t5).a1 by SCMPDS_5:46
.=s.a1 by A83,A102,SCMPDS_2:59;
A104: a2<>DataLoc(t5.a4,0) by A9,A14,A99;
A105: t4.a2=Exec(k5,t5).a2 by SCMPDS_5:46
.=s.a2 by A85,A104,SCMPDS_2:59;
A106: a3<>DataLoc(t5.a4,0) by A9,A15,A99;
A107: t4.a3=Exec(k5,t5).a3 by SCMPDS_5:46
.=s.a3 by A87,A106,SCMPDS_2:59;
A108: a4<>DataLoc(t5.a4,0) by A9,A16,A99;
A109: t4.a4=Exec(k5,t5).a4 by SCMPDS_5:46
.=s.a4 by A89,A108,SCMPDS_2:59;
A110: a6<>DataLoc(t5.a4,0) by A9,A18,A99;
A111: t4.a6=Exec(k5,t5).a6 by SCMPDS_5:46
.=s.a6 by A93,A110,SCMPDS_2:59;
A112: x<>DataLoc(t5.a4,0)
proof
assume x=DataLoc(t5.a4,0);
then 2*(s.a4-1)=2*(s.a4) by A7,A99,XCMPLX_1:2;
then s.a4-1=s.a4 by XCMPLX_1:5;
then -1+s.a4=0+s.a4 by XCMPLX_0:def 8;
hence contradiction by XCMPLX_1:2;
end;
A113: t4.x=Exec(k5,t5).x by SCMPDS_5:46
.=s.y by A94,A112,SCMPDS_2:59;
A114: t4.y =Exec(k5, t5).DataLoc(t5.a4,0) by A89,SCMPDS_5:46
.=t5.DataLoc(t5.a,5) by SCMPDS_2:59
.=t5.intpos(0+5) by A81,SCMP_GCD:5
.=s.x by A91;
A115: now let i be Nat;
assume A116: i>=7 & i<>s.a4-1 & i <> s.a4;
A117: intpos i <> DataLoc(t5.a4,0)
proof
assume A118:intpos i=DataLoc(t5.a4,0);
intpos i=dl.i by SCMP_GCD:def 1
.=2*i+1 by AMI_3:def 19;
then 2*i=2*(s.a4) by A99,A118,XCMPLX_1:2;
hence contradiction by A116,XCMPLX_1:5;
end;
thus t4.intpos i=Exec(k5, t5).intpos i by SCMPDS_5:46
.=t5.intpos i by A117,SCMPDS_2:59
.=s.intpos i by A95,A116;
end;
A119: DataLoc(t4.a,4)=intpos (0+4) by A101,SCMP_GCD:5;
then A120: a<>DataLoc(t4.a,4) by SCMP_GCD:4,def 2;
A121: t3.a=Exec(k6,t4).a by SCMPDS_5:46
.=0 by A101,A120,SCMPDS_2:60;
A122: a1<>DataLoc(t4.a,4) by A119,SCMP_GCD:4;
A123: t3.a1=Exec(k6,t4).a1 by SCMPDS_5:46
.=s.a1 by A103,A122,SCMPDS_2:60;
A124: a2<>DataLoc(t4.a,4) by A119,SCMP_GCD:4;
A125: t3.a2=Exec(k6,t4).a2 by SCMPDS_5:46
.=s.a2 by A105,A124,SCMPDS_2:60;
A126: a3<>DataLoc(t4.a,4) by A119,SCMP_GCD:4;
A127: t3.a3=Exec(k6,t4).a3 by SCMPDS_5:46
.=s.a3 by A107,A126,SCMPDS_2:60;
A128: t3.a4=Exec(k6,t4).a4 by SCMPDS_5:46
.=t4.a4+-1 by A119,SCMPDS_2:60
.=s.a4-1 by A109,XCMPLX_0:def 8;
A129: a6<>DataLoc(t4.a,4) by A119,SCMP_GCD:4;
A130: t3.a6=Exec(k6,t4).a6 by SCMPDS_5:46
.=s.a6 by A111,A129,SCMPDS_2:60;
A131: x<>DataLoc(t4.a,4) by A4,A7,A16,A119;
A132: t3.x=Exec(k6, t4).x by SCMPDS_5:46
.=s.y by A113,A131,SCMPDS_2:60;
A133: y<>DataLoc(t4.a,4) by A9,A11,A16,A119;
A134: t3.y=Exec(k6, t4).y by SCMPDS_5:46
.=s.x by A114,A133,SCMPDS_2:60;
A135: now let i be Nat;
assume A136: i>=7 & i<>s.a4-1 & i <> s.a4;
then i>4 by AXIOMS:22;
then A137: intpos i <> DataLoc(t4.a,4) by A119,SCMP_GCD:4;
thus t3.intpos i=Exec(k6, t4).intpos i by SCMPDS_5:46
.=t4.intpos i by A137,SCMPDS_2:60
.=s.intpos i by A115,A136;
end;
A138: DataLoc(t3.a,6)=intpos (0+6) by A121,SCMP_GCD:5;
then A139: a<>DataLoc(t3.a,6) by SCMP_GCD:4,def 2;
A140: DataLoc(t02.a,6)=intpos (0+6) by A60,SCMP_GCD:5;
now per cases;
suppose A141: t2.DataLoc(t2.a,5) <= 0;
A142: a<>DataLoc(t02.a,6) by A140,SCMP_GCD:4,def 2;
thus IExec(IF,t2).a=IExec(FA,t2).a by A141,SCMPDS_6:88
.=Exec(Fi,t02).a by SCMPDS_5:45
.=0 by A60,A142,SCMPDS_2:58;
suppose t2.DataLoc(t2.a,5) > 0;
hence IExec(IF,t2).a=IExec(TR,t2).a by SCMPDS_6:87
.=Exec(k7,t3).a by SCMPDS_5:46
.=0 by A121,A139,SCMPDS_2:60;
end;
hence IExec(B1,s).a=0 by SCMPDS_5:39;
now
per cases;
suppose A143: t2.DataLoc(t2.a,5) <= 0;
A144: a1<>DataLoc(t02.a,6) by A140,SCMP_GCD:4;
thus IExec(IF,t2).a1=IExec(FA,t2).a1 by A143,SCMPDS_6:88
.=Exec(Fi,t02).a1 by SCMPDS_5:45
.=s.a1 by A61,A144,SCMPDS_2:58;
suppose A145:t2.DataLoc(t2.a,5) > 0;
A146: a1<>DataLoc(t3.a,6) by A138,SCMP_GCD:4;
thus IExec(IF,t2).a1=IExec(TR,t2).a1 by A145,SCMPDS_6:87
.=Exec(k7,t3).a1 by SCMPDS_5:46
.=s.a1 by A123,A146,SCMPDS_2:60;
end;
hence IExec(B1,s).a1=s.a1 by SCMPDS_5:39;
now
per cases;
suppose A147: t2.DataLoc(t2.a,5) <= 0;
A148: a2<>DataLoc(t02.a,6) by A140,SCMP_GCD:4;
thus IExec(IF,t2).a2=IExec(FA,t2).a2 by A147,SCMPDS_6:88
.=Exec(Fi,t02).a2 by SCMPDS_5:45
.=s.a2 by A62,A148,SCMPDS_2:58;
suppose A149: t2.DataLoc(t2.a,5) > 0;
A150: a2<>DataLoc(t3.a,6) by A138,SCMP_GCD:4;
thus IExec(IF,t2).a2=IExec(TR,t2).a2 by A149,SCMPDS_6:87
.=Exec(k7,t3).a2 by SCMPDS_5:46
.=s.a2 by A125,A150,SCMPDS_2:60;
end;
hence IExec(B1,s).a2=s.a2 by SCMPDS_5:39;
now
per cases;
suppose A151: t2.DataLoc(t2.a,5) <= 0;
A152: a3<>DataLoc(t02.a,6) by A140,SCMP_GCD:4;
thus IExec(IF,t2).a3=IExec(FA,t2).a3 by A151,SCMPDS_6:88
.=Exec(Fi,t02).a3 by SCMPDS_5:45
.=s.a3 by A63,A152,SCMPDS_2:58;
suppose A153: t2.DataLoc(t2.a,5) > 0;
A154: a3<>DataLoc(t3.a,6) by A138,SCMP_GCD:4;
thus IExec(IF,t2).a3=IExec(TR,t2).a3 by A153,SCMPDS_6:87
.=Exec(k7,t3).a3 by SCMPDS_5:46
.=s.a3 by A127,A154,SCMPDS_2:60;
end;
hence IExec(B1,s).a3=s.a3 by SCMPDS_5:39;
A155: now
assume t2.DataLoc(t2.a,5) <= 0;
then IExec(IF,t2).a6=IExec(FA,t2).a6 by SCMPDS_6:88
.=Exec(Fi,t02).a6 by SCMPDS_5:45
.=0 by A140,SCMPDS_2:58;
hence IExec(B1,s).a6 =0 by SCMPDS_5:39;
end;
A156: now
assume A157: t2.DataLoc(t2.a,5) > 0;
then IExec(IF,t2).a6=IExec(TR,t2).a6 by SCMPDS_6:87
.=Exec(k7,t3).a6 by SCMPDS_5:46
.=s.a6+ -1 by A130,A138,SCMPDS_2:60
.=s.a6-1 by XCMPLX_0:def 8;
hence IExec(B1,s).a6=s.a6-1 by SCMPDS_5:39;
A158: a4<>DataLoc(t3.a,6) by A138,SCMP_GCD:4;
IExec(IF,t2).a4=IExec(TR,t2).a4 by A157,SCMPDS_6:87
.=Exec(k7,t3).a4 by SCMPDS_5:46
.=s.a4-1 by A128,A158,SCMPDS_2:60;
hence IExec(B1,s).a4=s.a4-1 by SCMPDS_5:39;
end;
hereby
per cases;
suppose t2.DataLoc(t2.a,5) <= 0;
hence IExec(B1,s).a6 < s.a6 by A1,A155;
suppose t2.DataLoc(t2.a,5) > 0;
hence IExec(B1,s).a6 < s.a6 by A156,INT_1:26;
end;
hereby
per cases;
suppose A159:t2.DataLoc(t2.GBP,5) <= 0;
A160: a4<>DataLoc(t02.a,6) by A140,SCMP_GCD:4;
IExec(IF,t2).a4=IExec(FA,t2).a4 by A159,SCMPDS_6:88
.=Exec(Fi,t02).a4 by SCMPDS_5:45
.=s.a4 by A64,A160,SCMPDS_2:58;
then IExec(B1,s).a4=s.a4 by SCMPDS_5:39;
hence IExec(B1,s).a4 >= 7+IExec(B1,s).a6 by A1,A8,A155,A159,AXIOMS:22;
suppose A161:t2.DataLoc(t2.a,5) > 0;
s.a4-1 >= 7+s.a6-1 by A1,REAL_1:49;
hence IExec(B1,s).a4 >= 7+IExec(B1,s).a6 by A156,A161,XCMPLX_1:29;
end;
hereby let i be Nat;
set xi=intpos i;
assume A162: i>=7 & i<>s.a4-1 & i <> s.a4;
then A163: i>6 by AXIOMS:22;
per cases;
suppose A164: t2.DataLoc(t2.a,5) <= 0;
A165: xi<>DataLoc(t02.a,6) by A140,A163,SCMP_GCD:4;
IExec(IF,t2).xi=IExec(FA,t2).xi by A164,SCMPDS_6:88
.=Exec(Fi,t02).xi by SCMPDS_5:45
.=t02.xi by A165,SCMPDS_2:58
.=t2.xi by SCMPDS_5:40
.=s.xi by A57,A162;
hence IExec(B1,s).xi=s.xi by SCMPDS_5:39;
suppose A166: t2.DataLoc(t2.a,5) > 0;
A167: xi<>DataLoc(t3.a,6) by A138,A163,SCMP_GCD:4;
IExec(IF,t2).xi=IExec(TR,t2).xi by A166,SCMPDS_6:87
.=Exec(k7,t3).xi by SCMPDS_5:46
.=t3.xi by A167,SCMPDS_2:60
.=s.xi by A135,A162;
hence IExec(B1,s).xi=s.xi by SCMPDS_5:39;
end;
hereby
assume s.x > s.y;
then A168: s.x-s.y > s.y-s.y by REAL_1:54;
then A169: s.x-s.y > 0 by XCMPLX_1:14;
A170: x<>DataLoc(t3.a,6) by A4,A7,A18,A138;
IExec(IF,t2).x=IExec(TR,t2).x by A50,A169,SCMPDS_6:87
.=Exec(k7,t3).x by SCMPDS_5:46
.=s.y by A132,A170,SCMPDS_2:60;
hence IExec(B1,s).x=s.y by SCMPDS_5:39;
A171: y<>DataLoc(t3.a,6) by A9,A11,A18,A138;
IExec(IF,t2).y=IExec(TR,t2).y by A50,A169,SCMPDS_6:87
.=Exec(k7,t3).y by SCMPDS_5:46
.=s.x by A134,A171,SCMPDS_2:60;
hence IExec(B1,s).y=s.x by SCMPDS_5:39;
thus IExec(B1,s).a6=s.a6-1 & IExec(B1,s).a4=s.a4-1 by A50,A156,A168,
XCMPLX_1:14;
end;
hereby
assume s.x <= s.y;
then A172: s.x-s.y <= s.y-s.y by REAL_1:49;
then A173: s.x-s.y <= 0 by XCMPLX_1:14;
A174: x<>DataLoc(t02.a,6) by A4,A7,A18,A140;
IExec(IF,t2).x=IExec(FA,t2).x by A50,A173,SCMPDS_6:88
.=Exec(Fi,t02).x by SCMPDS_5:45
.=s.x by A66,A174,SCMPDS_2:58;
hence IExec(B1,s).x=s.x by SCMPDS_5:39;
A175: y<>DataLoc(t02.a,6) by A9,A11,A18,A140;
IExec(IF,t2).y=IExec(FA,t2).y by A50,A173,SCMPDS_6:88
.=Exec(Fi,t02).y by SCMPDS_5:45
.=s.y by A67,A175,SCMPDS_2:58;
hence IExec(B1,s).y=s.y by SCMPDS_5:39;
thus IExec(B1,s).a6 =0 by A50,A155,A172,XCMPLX_1:14;
end;
end;
Lm8:
for s being State of SCMPDS st s.a4 >= 7+s.DataLoc(s.GBP,6) & s.GBP=0
holds WH is_closed_on s & WH is_halting_on s
proof
let s be State of SCMPDS;
set a=GBP,
b=DataLoc(s.a,6);
assume A1: s.a4 >= 7+s.b & s.a=0;
then A2: b=intpos(0+6) by SCMP_GCD:5;
A3: for x st x in {a4} holds s.x >= 7+s.b by A1,TARSKI:def 1;
now
let t be State of SCMPDS;
assume A4:
(for x st x in {a4} holds t.x >= 7+t.b) & t.a=s.a & t.b >0;
A5: a4 in {a4} by TARSKI:def 1;
then A6: t.a4 >= 7+t.b by A4;
A7: t.a4 >= 7+t.a6 by A2,A4,A5;
set Bt=IExec(B1,t);
A8: Bt.a=0 & Bt.a6 < t.a6 & Bt.a4 >= 7+Bt.a6 by A1,A2,A4,A6,Lm7;
thus IExec(B1,t).a=t.a by A1,A2,A4,A7,Lm7;
thus B1 is_closed_on t & B1 is_halting_on t by SCMPDS_6:34,35;
thus IExec(B1,t).b < t.b by A1,A2,A4,A7,Lm7;
thus for x st x in {a4} holds
IExec(B1,t).x >= 7+IExec(B1,t).b by A2,A8,TARSKI:def 1;
end;
hence thesis by A3,Lm5,SCMPDS_8:29;
end;
Lm9:
for s being State of SCMPDS st s.a4 >= 7+s.DataLoc(s.GBP,6) & s.GBP=0
holds
IExec(WH,s).GBP=0 & IExec(WH,s).a1=s.a1 &
IExec(WH,s).a2=s.a2 & IExec(WH,s).a3=s.a3
proof
let s be State of SCMPDS;
set b=DataLoc(s.GBP,6),
a=GBP;
assume A1: s.a4 >= 7+s.b & s.a=0;
defpred P[Nat] means
for t be State of SCMPDS st t.a6 <= $1 & t.a4 >= 7+t.a6 & t.a=0 holds
IExec(WH,t).a=0 & IExec(WH,t).a1=t.a1 &
IExec(WH,t).a2=t.a2 & IExec(WH,t).a3=t.a3;
A2: P[0]
proof
let t be State of SCMPDS;
assume A3: t.a6 <= 0 & t.a4 >= 7+t.a6 & t.a=0;
then A4: DataLoc(t.a,6)=intpos (0+6) by SCMP_GCD:5;
hence IExec(WH,t).a=0 by A3,SCMPDS_8:23;
thus IExec(WH,t).a1=t.a1 &
IExec(WH,t).a2=t.a2 & IExec(WH,t).a3=t.a3 by A3,A4,SCMPDS_8:23;
end;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6:P[k];
thus P[k+1]
proof
let t be State of SCMPDS;
set bt=DataLoc(t.a,6);
assume A7: t.a6 <= k+1 & t.a4 >= 7+t.a6 & t.a=0;
then A8: bt=intpos (0+6) by SCMP_GCD:5;
per cases;
suppose t.bt <= 0;
hence thesis by A7,SCMPDS_8:23;
suppose A9: t.bt > 0;
A10: for x st x in {a4} holds t.x >= 7+t.bt by A7,A8,TARSKI:def 1;
A11: now
let v be State of SCMPDS;
assume A12:
(for x st x in {a4} holds v.x >= 7+v.bt) &
v.a=t.a & v.bt > 0;
A13: a4 in {a4} by TARSKI:def 1;
then A14: v.a4 >= 7+v.bt by A12;
A15: v.a4 >= 7+v.a6 by A8,A12,A13;
set Iv=IExec(B1,v);
A16: Iv.a=0 & Iv.a6 < v.a6 & Iv.a4 >= 7+Iv.a6 by A7,A8,A12,A14,Lm7;
thus IExec(B1,v).a=v.a by A7,A8,A12,A15,Lm7;
thus B1 is_closed_on v & B1 is_halting_on v by SCMPDS_6:34,35;
thus IExec(B1,v).bt < v.bt by A7,A8,A12,A15,Lm7;
thus for x st x in {a4} holds IExec(B1,v).x >= 7+IExec(B1,v).bt
by A8,A16,TARSKI:def 1;
end;
set It=IExec(B1,t);
A17: It.GBP=0 & It.a1=t.a1 & It.a2=t.a2 & It.a3=t.a3 &
It.a6 < t.a6 & It.a4 >= 7+It.a6 by A7,A8,A9,Lm7;
then It.a6 +1 <= t.a6 by INT_1:20;
then It.a6 +1 <= k+1 by A7,AXIOMS:22;
then It.a6 <= k by REAL_1:53;
then A18: IExec(WH,It).a=0 & IExec(WH,It).a1=It.a1 &
IExec(WH,It).a2=It.a2 & IExec(WH,It).a3=It.a3 by A6,A17;
hence IExec(WH,t).a=0 by A9,A10,A11,Lm5,SCMPDS_8:29;
thus IExec(WH,t).a1=t.a1 by A9,A10,A11,A17,A18,Lm5,SCMPDS_8:29;
thus IExec(WH,t).a2=t.a2 by A9,A10,A11,A17,A18,Lm5,SCMPDS_8:29;
thus IExec(WH,t).a3=t.a3 by A9,A10,A11,A17,A18,Lm5,SCMPDS_8:29;
end;
end;
A19: b=intpos (0+6) by A1,SCMP_GCD:5;
per cases;
suppose s.a6 <= 0;
hence thesis by A1,A19,SCMPDS_8:23;
suppose s.a6 > 0;
then reconsider m=s.a6 as Nat by INT_1:16;
for k be Nat holds P[k] from Ind(A2,A5);
then P[m];
hence thesis by A1,A19;
end;
Lm10:
for s being State of SCMPDS st s.GBP=0 holds
IExec(J4,s).GBP =0 & IExec(J4,s).a1 = s.a1+1 &
IExec(J4,s).a2=s.a2 & IExec(J4,s).a3 =s.a3+1 &
IExec(J4,s).a4 =s.a3+1 & IExec(J4,s).a6 =s.a1+1 &
for i be Nat st i >= 7 holds IExec(J4,s).intpos i=s.intpos i
proof
let s be State of SCMPDS;
set a=GBP;
set t0=Initialized s,
t1=IExec(J4,s),
t2=IExec(j1 ';' j2 ';' j3,s),
t3=IExec(j1 ';' j2,s),
t4=Exec(j1, t0);
assume s.a=0;
then A1: t0.a=0 by SCMPDS_5:40;
A2: t0.a1=s.a1 by SCMPDS_5:40;
A3: t0.a2=s.a2 by SCMPDS_5:40;
A4: t0.a3=s.a3 by SCMPDS_5:40;
A5: DataLoc(t0.a,3)=intpos (0+3) by A1,SCMP_GCD:5;
then a<>DataLoc(t0.a,3) by SCMP_GCD:4,def 2;
then A6: t4.a=0 by A1,SCMPDS_2:60;
a1<>DataLoc(t0.a,3) by A5,SCMP_GCD:4;
then A7: t4.a1=s.a1 by A2,SCMPDS_2:60;
a2<>DataLoc(t0.a,3) by A5,SCMP_GCD:4;
then A8: t4.a2=s.a2 by A3,SCMPDS_2:60;
A9: t4.a3=s.a3+1 by A4,A5,SCMPDS_2:60;
A10: now let i be Nat;
assume i >= 7;
then i > 3 by AXIOMS:22;
then intpos i<>DataLoc(t0.a,3) by A5,SCMP_GCD:4;
hence t4.intpos i=t0.intpos i by SCMPDS_2:60
.=s.intpos i by SCMPDS_5:40;
end;
A11: DataLoc(t4.a,4)=intpos (0+4) by A6,SCMP_GCD:5;
A12: DataLoc(t4.a,3)=intpos (0+3) by A6,SCMP_GCD:5;
A13: a<>DataLoc(t4.a,4) by A11,SCMP_GCD:4,def 2;
A14: t3.a =Exec(j2, t4).a by SCMPDS_5:47
.=0 by A6,A13,SCMPDS_2:59;
A15: a1<>DataLoc(t4.a,4) by A11,SCMP_GCD:4;
A16: t3.a1 =Exec(j2, t4).a1 by SCMPDS_5:47
.=s.a1 by A7,A15,SCMPDS_2:59;
A17: a2<>DataLoc(t4.a,4) by A11,SCMP_GCD:4;
A18: t3.a2 =Exec(j2, t4).a2 by SCMPDS_5:47
.=s.a2 by A8,A17,SCMPDS_2:59;
A19: a3<>DataLoc(t4.a,4) by A11,SCMP_GCD:4;
A20: t3.a3 =Exec(j2, t4).a3 by SCMPDS_5:47
.=s.a3+1 by A9,A19,SCMPDS_2:59;
A21: t3.a4 =Exec(j2,t4).a4 by SCMPDS_5:47
.=s.a3+1 by A9,A11,A12,SCMPDS_2:59;
A22: now let i be Nat;
assume A23:i >= 7;
then i > 4 by AXIOMS:22;
then A24: intpos i<>DataLoc(t4.a,4) by A11,SCMP_GCD:4;
thus t3.intpos i =Exec(j2, t4).intpos i by SCMPDS_5:47
.=t4.intpos i by A24,SCMPDS_2:59
.=s.intpos i by A10,A23;
end;
A25: DataLoc(t3.a,1)=intpos (0+1) by A14,SCMP_GCD:5;
then A26: a<>DataLoc(t3.a,1) by SCMP_GCD:4,def 2;
A27: t2.a =Exec(j3, t3).a by SCMPDS_5:46
.=0 by A14,A26,SCMPDS_2:60;
A28: t2.a1 =Exec(j3, t3).a1 by SCMPDS_5:46
.=s.a1+1 by A16,A25,SCMPDS_2:60;
A29: a2<>DataLoc(t3.a,1) by A25,SCMP_GCD:4;
A30: t2.a2 =Exec(j3, t3).a2 by SCMPDS_5:46
.=s.a2 by A18,A29,SCMPDS_2:60;
A31: a3<>DataLoc(t3.a,1) by A25,SCMP_GCD:4;
A32: t2.a3 =Exec(j3, t3).a3 by SCMPDS_5:46
.=s.a3+1 by A20,A31,SCMPDS_2:60;
A33: a4<>DataLoc(t3.a,1) by A25,SCMP_GCD:4;
A34: t2.a4 =Exec(j3, t3).a4 by SCMPDS_5:46
.=s.a3+1 by A21,A33,SCMPDS_2:60;
A35: now let i be Nat;
assume A36:i >= 7;
then i > 1 by AXIOMS:22;
then A37: intpos i<>DataLoc(t3.a,1) by A25,SCMP_GCD:4;
thus t2.intpos i =Exec(j3, t3).intpos i by SCMPDS_5:46
.=t3.intpos i by A37,SCMPDS_2:60
.=s.intpos i by A22,A36;
end;
A38: DataLoc(t2.a,6)=intpos (0+6) by A27,SCMP_GCD:5;
then A39: a<>DataLoc(t2.a,6) by SCMP_GCD:4,def 2;
thus t1.a =Exec(j4, t2).a by SCMPDS_5:46
.=0 by A27,A39,SCMPDS_2:59;
A40: a1<>DataLoc(t2.a,6) by A38,SCMP_GCD:4;
thus t1.a1 =Exec(j4, t2).a1 by SCMPDS_5:46
.=s.a1+1 by A28,A40,SCMPDS_2:59;
A41: a2<>DataLoc(t2.a,6) by A38,SCMP_GCD:4;
thus t1.a2 =Exec(j4, t2).a2 by SCMPDS_5:46
.=s.a2 by A30,A41,SCMPDS_2:59;
A42: a3<>DataLoc(t2.a,6) by A38,SCMP_GCD:4;
thus t1.a3 =Exec(j4, t2).a3 by SCMPDS_5:46
.=s.a3+1 by A32,A42,SCMPDS_2:59;
A43: a4 <> DataLoc(t2.a,6) by A38,SCMP_GCD:4;
thus t1.a4 =Exec(j4, t2).a4 by SCMPDS_5:46
.=s.a3+1 by A34,A43,SCMPDS_2:59;
A44: DataLoc(t2.a,1)=intpos (0+1) by A27,SCMP_GCD:5;
thus t1.a6 =Exec(j4, t2).a6 by SCMPDS_5:46
.=s.a1+1 by A28,A38,A44,SCMPDS_2:59;
hereby let i be Nat;
assume A45:i >= 7;
then i > 6 by AXIOMS:22;
then A46: intpos i<>DataLoc(t2.a,6) by A38,SCMP_GCD:4;
thus t1.intpos i =Exec(j4, t2).intpos i by SCMPDS_5:46
.=t2.intpos i by A46,SCMPDS_2:59
.=s.intpos i by A35,A45;
end;
end;
set jf=AddTo(GBP,2,-1),
B3=B2 ';' jf;
Lm11:
for s being State of SCMPDS st s.a3 >= s.a1+7 & s.GBP=0
holds
IExec(B3,s).GBP=0 & IExec(B3,s).a2=s.a2-1 &
IExec(B3,s).a3=s.a3+1 & IExec(B3,s).a1=s.a1+1 &
for i be Nat st i <> 2 holds
IExec(B3,s).intpos i=IExec(WH,IExec(J4,s)).intpos i
proof
let s be State of SCMPDS;
set a=GBP;
set s1=IExec(J4,s),
Bt=IExec(B2, s);
assume A1: s.a3 >= s.a1+7 & s.a=0;
then A2: s1.GBP =0 & s1.a1 = s.a1+1 &
s1.a2=s.a2 & s1.a3 =s.a3+1 &
s1.a4 =s.a3+1 & s1.a6 =s.a1+1 by Lm10;
then A3: DataLoc(s1.a,6)=intpos (0+6) by SCMP_GCD:5;
s.a3+1 >= 7+s.a1+1 by A1,AXIOMS:24;
then A4: s1.a4 >= 7+s1.a6 by A2,XCMPLX_1:1;
then A5: WH is_closed_on s1 & WH is_halting_on s1 by A2,A3,Lm8;
A6: J4 is_closed_on s & J4 is_halting_on s by SCMPDS_6:34,35;
then A7: Bt.a =IExec(WH,s1).a by A5,SCMPDS_7:49
.=0 by A2,A3,A4,Lm9;
then A8: DataLoc(Bt.a,2)=intpos (0+2) by SCMP_GCD:5;
then A9: a<>DataLoc(Bt.a,2) by SCMP_GCD:4,def 2;
A10: B2 is_closed_on s & B2 is_halting_on s by A5,A6,SCMPDS_7:43;
hence IExec(B3,s).a=Exec(jf, Bt).a by SCMPDS_7:50
.=0 by A7,A9,SCMPDS_2:60;
thus IExec(B3,s).a2=Exec(jf, Bt).a2 by A10,SCMPDS_7:50
.=Bt.a2+ -1 by A8,SCMPDS_2:60
.=Bt.a2-1 by XCMPLX_0:def 8
.=IExec(WH,s1).a2 -1 by A5,A6,SCMPDS_7:49
.=s.a2-1 by A2,A3,A4,Lm9;
A11: a3<>DataLoc(Bt.a,2) by A8,SCMP_GCD:4;
thus IExec(B3,s).a3=Exec(jf, Bt).a3 by A10,SCMPDS_7:50
.=Bt.a3 by A11,SCMPDS_2:60
.=IExec(WH,s1).a3 by A5,A6,SCMPDS_7:49
.=s.a3+1 by A2,A3,A4,Lm9;
A12: a1<>DataLoc(Bt.a,2) by A8,SCMP_GCD:4;
thus IExec(B3,s).a1=Exec(jf, Bt).a1 by A10,SCMPDS_7:50
.=Bt.a1 by A12,SCMPDS_2:60
.=IExec(WH,s1).a1 by A5,A6,SCMPDS_7:49
.=s.a1+1 by A2,A3,A4,Lm9;
hereby
let i be Nat;
assume i<> 2;
then A13: intpos i<>DataLoc(Bt.a,2) by A8,SCMP_GCD:4;
thus IExec(B3,s).intpos i=Exec(jf, Bt).intpos i by A10,SCMPDS_7:50
.=Bt.intpos i by A13,SCMPDS_2:60
.=IExec(WH,s1).intpos i by A5,A6,SCMPDS_7:49;
end;
end;
Lm12:
for s being State of SCMPDS st s.a3 >= s.a1+7 & s.GBP=0
holds FR is_closed_on s & FR is_halting_on s
proof
let s be State of SCMPDS;
set a=GBP,
b=DataLoc(s.a,2);
assume A1: s.a3 >= s.a1+7 & s.a=0;
then A2: b=intpos(0+2) by SCMP_GCD:5;
now
let t be State of SCMPDS;
assume A3: t.a3 >= t.a1+7 & t.a=s.a & t.b >0;
set t1=IExec(J4,t);
A4: t1.a =0 & t1.a1 = t.a1+1 &
t1.a2=t.a2 & t1.a3 =t.a3+1 &
t1.a4 =t.a3+1 & t1.a6 =t.a1+1 by A1,A3,Lm10;
A5: IExec(B3,t).a=0 & IExec(B3,t).a2=t.a2-1 &
IExec(B3,t).a3=t.a3+1 & IExec(B3,t).a1=t.a1+1 by A1,A3,Lm11;
thus IExec(B3,t).a=t.a by A1,A3,Lm11;
thus IExec(B3,t).b=t.b-1 by A1,A2,A3,Lm11;
A6: DataLoc(t1.a,6)=intpos (0+6) by A4,SCMP_GCD:5;
A7: t.a3+1 >= 7+t.a1+1 by A3,AXIOMS:24;
then t1.a4 >= 7+t1.a6 by A4,XCMPLX_1:1;
then A8: WH is_closed_on t1 & WH is_halting_on t1 by A4,A6,Lm8;
J4 is_closed_on t & J4 is_halting_on t by SCMPDS_6:34,35;
hence B2 is_closed_on t & B2 is_halting_on t by A8,SCMPDS_7:43;
thus IExec(B3,t).a3>=IExec(B3,t).a1+7 by A5,A7,XCMPLX_1:1;
end;
hence thesis by A1,Th12;
end;
Lm13:
for s being State of SCMPDS st s.a3 >= s.a1+7 & s.GBP=0 & s.a2 > 0 holds
IExec(FR,s) = IExec(FR,IExec(B3,s))
proof
let s be State of SCMPDS;
set a=GBP,
b=DataLoc(s.a,2);
assume A1: s.a3 >= s.a1+7 & s.a=0 & s.a2 > 0;
then A2: b=intpos(0+2) by SCMP_GCD:5;
now
let t be State of SCMPDS;
assume A3: t.a3 >= t.a1+7 & t.a=s.a & t.b >0;
set t1=IExec(J4,t);
A4: t1.a =0 & t1.a1 = t.a1+1 &
t1.a2=t.a2 & t1.a3 =t.a3+1 &
t1.a4 =t.a3+1 & t1.a6 =t.a1+1 by A1,A3,Lm10;
A5: IExec(B3,t).a=0 & IExec(B3,t).a2=t.a2-1 &
IExec(B3,t).a3=t.a3+1 & IExec(B3,t).a1=t.a1+1 by A1,A3,Lm11;
thus IExec(B3,t).a=t.a by A1,A3,Lm11;
thus IExec(B3,t).b=t.b-1 by A1,A2,A3,Lm11;
A6: DataLoc(t1.a,6)=intpos (0+6) by A4,SCMP_GCD:5;
A7: t.a3+1 >= 7+t.a1+1 by A3,AXIOMS:24;
then t1.a4 >= 7+t1.a6 by A4,XCMPLX_1:1;
then A8: WH is_closed_on t1 & WH is_halting_on t1 by A4,A6,Lm8;
J4 is_closed_on t & J4 is_halting_on t by SCMPDS_6:34,35;
hence B2 is_closed_on t & B2 is_halting_on t by A8,SCMPDS_7:43;
thus IExec(B3,t).a3>=IExec(B3,t).a1+7 by A5,A7,XCMPLX_1:1;
end;
hence thesis by A1,A2,Th13;
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 ';' FR) by Def2
.=card(i1 ';' i2 ';' i3 ';' i4) + card FR by SCMPDS_4:45
.=card(i1 ';' i2 ';' i3)+1 + card FR by SCMP_GCD:8
.=card(i1 ';' i2)+1+1 + card FR by SCMP_GCD:8
.=2+1+1+card FR by SCMP_GCD:9
.=4+(card B2+3) by SCMPDS_7:60
.=23 by Lm6;
end;
theorem
p0 >= 7 implies insert-sort (n,p0) is parahalting
proof
assume A1: p0 >= 7;
set a=GBP,
i1= a:=0,
i2= (a,1):=0,
i3= (a,2):=(n-1),
i4= (a,3):=p0,
I= i1 ';' i2 ';' i3 ';' i4;
now
let s be State of SCMPDS;
set s1=IExec(I,s),
s2=IExec(i1 ';' i2 ';' i3,s),
s3=IExec(i1 ';' i2,s),
s4=Exec(i1, Initialized s);
A2: s4.a=0 by SCMPDS_2:57;
then A3: DataLoc(s4.a,1)=intpos (0+1) by SCMP_GCD:5;
then A4: a<>DataLoc(s4.a,1) by SCMP_GCD:4,def 2;
A5: s3.a=Exec(i2,s4).a by SCMPDS_5:47
.=0 by A2,A4,SCMPDS_2:58;
A6: s3.a1=Exec(i2,s4).a1 by SCMPDS_5:47
.=0 by A3,SCMPDS_2:58;
A7: DataLoc(s3.a,2)=intpos (0+2) by A5,SCMP_GCD:5;
then A8: a<>DataLoc(s3.a,2) by SCMP_GCD:4,def 2;
A9: s2.a=Exec(i3,s3).a by SCMPDS_5:46
.=0 by A5,A8,SCMPDS_2:58;
A10: a1<>DataLoc(s3.a,2) by A7,SCMP_GCD:4;
A11: s2.a1=Exec(i3,s3).a1 by SCMPDS_5:46
.=0 by A6,A10,SCMPDS_2:58;
A12: DataLoc(s2.a,3)=intpos (0+3) by A9,SCMP_GCD:5;
then A13: a<>DataLoc(s2.a,3) by SCMP_GCD:4,def 2;
A14: s1.a=Exec(i4,s2).a by SCMPDS_5:46
.=0 by A9,A13,SCMPDS_2:58;
A15: a1<>DataLoc(s2.a,3) by A12,SCMP_GCD:4;
A16: s1.a1=Exec(i4,s2).a1 by SCMPDS_5:46
.=0 by A11,A15,SCMPDS_2:58;
A17: s1.a3=Exec(i4,s2).a3 by SCMPDS_5:46
.=p0 by A12,SCMPDS_2:58;
A18: I is_closed_on s & I is_halting_on s by SCMPDS_6:34,35;
s1.a3 >= s1.a1+7 by A1,A16,A17;
then FR is_closed_on s1 & FR is_halting_on s1 by A14,Lm12;
then I ';' FR is_halting_on s by A18,SCMPDS_7:43;
hence insert-sort (n,p0) is_halting_on s by Def2;
end;
hence thesis by SCMPDS_6:35;
end;
Lm14:
for s being State of SCMPDS st s.a4 >= 7+s.a6 & s.GBP=0 & s.a6 >0
holds IExec(WH,s) =IExec(WH,IExec(B1,s))
proof
let s be State of SCMPDS;
set a=GBP,
b=DataLoc(s.a,6);
assume A1: s.a4 >= 7+s.a6 & s.a=0 & s.a6 > 0;
then A2: b=intpos(0+6) by SCMP_GCD:5;
then A3: for x st x in {a4} holds s.x >= 7+s.b by A1,TARSKI:def 1;
now
let t be State of SCMPDS;
assume A4:
(for x st x in {a4} holds t.x >= 7+t.b) & t.a=s.a & t.b >0;
A5: a4 in {a4} by TARSKI:def 1;
then A6: t.a4 >= 7+t.b by A4;
A7: t.a4 >= 7+t.a6 by A2,A4,A5;
set Bt=IExec(B1,t);
A8: Bt.a=0 & Bt.a6 < t.a6 & Bt.a4 >= 7+Bt.a6 by A1,A2,A4,A6,Lm7;
thus IExec(B1,t).a=t.a by A1,A2,A4,A7,Lm7;
thus B1 is_closed_on t & B1 is_halting_on t by SCMPDS_6:34,35;
thus IExec(B1,t).b < t.b by A1,A2,A4,A7,Lm7;
thus for x st x in {a4} holds
IExec(B1,t).x >= 7+IExec(B1,t).b by A2,A8,TARSKI:def 1;
end;
hence thesis by A1,A2,A3,Lm5,SCMPDS_8:29;
end;
set Insert_the_k1_item=WH;
theorem Th17:
for s being State of SCMPDS,f,g be FinSequence of INT,k0,k being Nat
st s.a4 >= 7+s.a6 & s.GBP=0 & k=s.a6 & k0=s.a4-s.a6-1 &
f is_FinSequence_on s,k0 &
g is_FinSequence_on IExec(Insert_the_k1_item,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
let s be State of SCMPDS,f,g be FinSequence of INT,m,n be Nat;
set a=GBP;
assume A1: s.a4 >= 7+s.a6 & s.a=0 & n=s.a6 & m=s.a4-s.a6-1;
assume A2: f is_FinSequence_on s,m & g is_FinSequence_on IExec(WH,s),m;
assume A3: len f= len g & len f > n & f is_non_decreasing_on 1,n;
defpred P[Nat] means
for t be State of SCMPDS,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,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 holds ex j be Nat st
1 <= j & j <= $1+1 & f2.i=f1.j);
A4: P[0]
proof
let t be State of SCMPDS,f1,f2 be FinSequence of INT;
assume A5: t.a4 >= 7+t.a6 & t.a=0 & 0=t.a6 & m=t.a4-t.a6-1 &
f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec(WH,t),m &
len f1=len f2 & len f1 > 0 & f1 is_non_decreasing_on 1,0;
then A6: t.DataLoc(t.a,6) =t.intpos(0+6) by SCMP_GCD:5
.=0 by A5;
A7: now
let i be Nat;
assume A8: 1 <= i & i <= len f1;
hence f1.i=t.intpos(m+i) by A5,Def1
.=IExec(WH,t).intpos(m+i) by A6,SCMPDS_8:23
.=f2.i by A5,A8,Def1;
end;
then A9: f1=f2 by A5,FINSEQ_1:18;
thus f1,f2 are_fiberwise_equipotent by A5,A7,FINSEQ_1:18;
thus f2 is_non_decreasing_on 1,0+1 by Th1;
thus for i be Nat st i>0+1 & i <= len f1 holds f1.i=f2.i by A7;
thus for i be Nat st 1 <= i & i <= 0+1
ex j be Nat st 1 <= j & j <= 0+1 & f2.i=f1.j by A9;
end;
A10: now let k be Nat;
assume A11:P[k];
now
let t be State of SCMPDS,f1,f2 be FinSequence of INT;
assume A12: t.a4 >= 7+t.a6 & t.a=0 & k+1=t.a6 & m=t.a4-t.a6-1 &
f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec(WH,t),m &
len f1=len f2 & len f1 > k+1 & f1 is_non_decreasing_on 1,k+1;
set Bt=IExec(B1,t),
x=DataLoc(t.a4,-1),
y=DataLoc(t.a4,0);
A13: t.a6 > 0 by A12,NAT_1:19;
A14: t.a4-1=t.a4+ -t.a6 +t.a6-1 by XCMPLX_1:139
.=t.a4+ -t.a6 + t.a6+-1 by XCMPLX_0:def 8
.=t.a4+ -t.a6 +-1+t.a6 by XCMPLX_1:1
.=t.a4-t.a6 +-1+t.a6 by XCMPLX_0:def 8
.=m+(k+1) by A12,XCMPLX_0:def 8;
A15: x=2*abs((t.a4+-1))+1 by SCMPDS_2:def 4
.=2*abs(m+(k+1))+1 by A14,XCMPLX_0:def 8
.=DataLoc(m,k+1) by SCMPDS_2:def 4
.=intpos(m+(k+1)) by SCMP_GCD:5;
A16: t.a4=t.a4+-1+1 by XCMPLX_1:139
.=m+(k+1)+1 by A14,XCMPLX_0:def 8;
then A17: t.a4=m+k+1+1 by XCMPLX_1:1
.=m+k+(1+1) by XCMPLX_1:1
.=m+(k+2) by XCMPLX_1:1;
A18: y=2*abs((t.a4+0))+1 by SCMPDS_2:def 4
.=DataLoc(m,k+2) by A17,SCMPDS_2:def 4
.=intpos(m+(k+2)) by SCMP_GCD:5;
m+1+(k+1) >= 7+t.a6 by A12,A16,XCMPLX_1:1;
then A19: m+1 >= 7 by A12,REAL_1:53;
A20: Bt.a=0 & Bt.a1=t.a1 & Bt.a4 >= 7+Bt.a6 &
(for i be Nat st i>=7 & i<>t.a4-1 & i<>t.a4 holds
Bt.intpos i=t.intpos i) &
(t.x > t.y implies Bt.x=t.y & Bt.y =t.x &
Bt.a6=t.a6-1 & Bt.a4=t.a4-1) &
(t.x <= t.y implies Bt.x=t.x & Bt.y =t.y & Bt.a6=0) by A12,A13,Lm7;
per cases;
suppose A21: t.x > t.y;
consider h be FinSequence of INT such that
A22: len h=len f1 & for i be Nat st 1<=i & i <= len h
holds h.i=Bt.intpos(m+i) by Th2;
A23: Bt.a6=k by A12,A20,A21,XCMPLX_1:26;
then A24: Bt.a4-Bt.a6-1=m+(k+1)-(k+1) by A14,A20,A21,XCMPLX_1:36
.=m by XCMPLX_1:26;
A25: h is_FinSequence_on Bt,m by A22,Def1;
now
let i be Nat;
assume 1<=i & i <= len f2;
hence f2.i=IExec(WH,t).intpos(m+i) by A12,Def1
.=IExec(WH,Bt).intpos(m+i) by A12,A13,Lm14;
end;
then A26: f2 is_FinSequence_on IExec(WH,Bt),m by Def1;
k+1 > k by REAL_1:69;
then A27: len h > k by A12,A22,AXIOMS:22;
A28: now
let i be Nat;
assume A29: i <> k+1 & i<>k+2 & 1 <= i & i <= len f1;
then m+i >= m+1 by AXIOMS:24;
then A30: m+i >= 7 by A19,AXIOMS:22;
A31: m+i <> t.a4-1 by A14,A29,XCMPLX_1:2;
A32: m+i <> t.a4 by A17,A29,XCMPLX_1:2;
thus h.i=Bt.intpos(m+i) by A22,A29
.=t.intpos(m+i) by A12,A13,A30,A31,A32,Lm7
.=f1.i by A12,A29,Def1;
end;
now
let i,j be Nat;
assume A33: 1 <= i & i <= j & j <= k;
A34: k < k+1 by REAL_1:69;
k+1 < k+1+1 by REAL_1:69;
then k < k+1+1 by A34,AXIOMS:22;
then A35: k < k+(1+1) by XCMPLX_1:1;
A36: j < k+1 by A33,A34,AXIOMS:22;
A37: j < k+2 by A33,A35,AXIOMS:22;
A38: j <= len f1 by A22,A27,A33,AXIOMS:22;
j >= 1 by A33,AXIOMS:22;
then A39: h.j=f1.j by A28,A33,A34,A35,A38;
i <= len f1 by A33,A38,AXIOMS:22;
then h.i=f1.i by A28,A33,A36,A37;
hence h.i <= h.j by A12,A33,A36,A39,SFMASTR3:def 4;
end;
then A40: h is_non_decreasing_on 1,k by SFMASTR3:def 4;
then A41: h,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,k+1 &
(for i be Nat st i>k+1 & i <= len h holds h.i=f2.i) &
(for i be Nat st 1 <= i & i <= k+1 holds ex j be Nat st
1 <= j & j <= k+1 & f2.i=h.j)
by A11,A12,A20,A22,A23,A24,A25,A26,A27;
A42: 1 <= k+1 by NAT_1:29;
A43: k+1 < k+2 by REAL_1:53;
then A44: 1 <= k+2 by A42,AXIOMS:22;
len f1 >= k+1+1 by A12,INT_1:20;
then A45: len f1 >= k+(1+1) by XCMPLX_1:1;
A46: h.(k+1)=t.y by A12,A15,A20,A21,A22,A42;
then A47: h.(k+1)=f1.(k+2) by A12,A18,A44,A45,Def1;
A48: h.(k+2)=t.x by A18,A20,A21,A22,A44,A45;
then A49: h.(k+2)=f1.(k+1) by A12,A15,A42,Def1;
then f1,h are_fiberwise_equipotent by A12,A22,A28,A42,A44,A45,A47,
Th4
;
hence f1,f2 are_fiberwise_equipotent by A41,RFINSEQ:2;
now
let i,j be Nat;
assume A50: 1 <= i & i <= j & j <= (k+1)+1;
per cases by A50,NAT_1:26;
suppose j <= k+1;
hence f2.i <= f2.j by A41,A50,SFMASTR3:def 4;
suppose A51:j = k+1+1;
hereby
per cases;
suppose i=j;
hence f2.i <= f2.j;
suppose i<>j;
then i < j by A50,REAL_1:def 5;
then i <= k+1 by A51,NAT_1:38;
then consider mm be Nat such that
A52: 1 <= mm & mm <= k+1 & f2.i=h.mm by A11,A12,A20,A22,A23,A24
,A25,A26,A27,A40,A50;
j=k+(1+1) by A51,XCMPLX_1:1;
then A53: f2.j=h.(k+2) by A11,A12,A20,A22,A23,A24,A25,A26,A27,
A40,A43,A45;
hereby
per cases;
suppose mm=k+1;
hence f2.i <= f2.j by A12,A15,A20,A22,A48,A52,A53;
suppose A54: mm<>k+1;
mm < k+2 by A43,A52,AXIOMS:22;
then mm < len h by A22,A45,AXIOMS:22;
then A55: h.mm=f1.mm by A22,A28,A43,A52,A54;
f2.j=f1.(k+1) by A12,A15,A42,A48,A53,Def1;
hence f2.i <= f2.j by A12,A52,A55,SFMASTR3:def 4;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k+1)+1 by SFMASTR3:def 4;
hereby
let i be Nat;
assume A56: i>(k+1)+1 & i <= len f1;
A57: k+1 < k+1+1 by REAL_1:69;
then A58: i > k+1 by A56,AXIOMS:22;
A59: i > k+(1+1) by A56,XCMPLX_1:1;
1 <= k+1 by NAT_1:29;
then A60: 1 <= i by A58,AXIOMS:22;
thus f2.i=h.i by A11,A12,A20,A22,A23,A24,A25,A26,A27,A40,A56,A58
.=f1.i by A28,A56,A57,A59,A60;
end;
hereby
let i be Nat;
assume A61: 1 <= i & i <= (k+1)+1;
per cases;
suppose i=k+1+1;
then A62: i=k+(1+1) by XCMPLX_1:1;
take j=k+1;
thus 1 <= j by NAT_1:29;
thus j <= (k+1)+1 by NAT_1:29;
thus f2.i=f1.j by A11,A12,A20,A22,A23,A24,A25,A26,A27,A40,A43,
A45,A49,A62;
suppose i<>k+1+1;
then i < k+1+1 by A61,REAL_1:def 5;
then i <= k+1 by NAT_1:38;
then consider mm be Nat such that
A63: 1 <= mm & mm <= k+1 & f2.i=h.mm by A11,A12,A20,A22,A23,A24,A25,
A26,A27,A40,A61;
hereby
A64: k+2=k+(1+1) .=(k+1)+1 by XCMPLX_1:1;
per cases;
suppose A65: mm=k+1;
take j=k+2;
thus 1 <= j by A64,NAT_1:29;
thus j <= k+1+1 by A64;
thus f2.i=f1.j by A12,A18,A44,A45,A46,A63,A65,Def1;
suppose A66: mm<>k+1;
mm < k+2 by A43,A63,AXIOMS:22;
then A67: mm < len f1 by A45,AXIOMS:22;
take mm;
thus 1 <= mm by A63;
thus mm <= k+1+1 by A43,A63,A64,AXIOMS:22;
thus f2.i=f1.mm by A28,A43,A63,A66,A67;
end;
end;
suppose A68: t.x <= t.y;
A69: now let i be Nat;
assume A70: i>=1 & i <= len f1;
then m+i >= m+1 by AXIOMS:24;
then A71: m+i >= 7 by A19,AXIOMS:22;
A72: f1.i=t.intpos(m+i) by A12,A70,Def1;
A73: Bt.DataLoc(Bt.a,6) = Bt.intpos(0+6) by A20,SCMP_GCD:5
.=0 by A12,A13,A68,Lm7;
per cases;
suppose A74: m+i=t.a4-1;
hence f1.i=IExec(WH,Bt).x by A14,A15,A20,A68,A72,A73,SCMPDS_8:23
.=IExec(WH,t).x by A12,A13,Lm14
.=f2.i by A12,A14,A15,A70,A74,Def1;
suppose A75: m+i=t.a4;
hence f1.i=IExec(WH,Bt).y by A17,A18,A20,A68,A72,A73,SCMPDS_8:23
.=IExec(WH,t).y by A12,A13,Lm14
.=f2.i by A12,A17,A18,A70,A75,Def1;
suppose m+i<>t.a4-1 & m+i<>t.a4;
hence f1.i=Bt.intpos (m+i) by A12,A13,A71,A72,Lm7
.=IExec(WH,Bt).intpos (m+i) by A73,SCMPDS_8:23
.=IExec(WH,t).intpos (m+i) by A12,A13,Lm14
.=f2.i by A12,A70,Def1;
end;
then A76: f1=f2 by A12,FINSEQ_1:18;
thus f1,f2 are_fiberwise_equipotent by A12,A69,FINSEQ_1:18;
now
let i, j be Nat;
assume A77: 1 <= i & i <= j & j <= (k+1)+1;
per cases by A77,NAT_1:26;
suppose j <= k+1;
hence f1.i <= f1.j by A12,A77,SFMASTR3:def 4;
suppose A78:j = k+1+1;
hereby
per cases;
suppose i=j;
hence f1.i <= f1.j;
suppose i<>j;
then i < j by A77,REAL_1:def 5;
then i <= k+1 by A78,NAT_1:38;
then A79: f1.i <= f1.(k+1) by A12,A77,SFMASTR3:def 4;
A80: j=k+(1+1) by A78,XCMPLX_1:1;
1<=k+1 by NAT_1:29;
then A81: f1.(k+1)=t.x by A12,A15,Def1;
A82: 1<=(k+1)+1 by NAT_1:29;
j<=len f1 by A12,A78,INT_1:20;
then f1.j=t.y by A12,A18,A78,A80,A82,Def1;
hence f1.i <= f1.j by A68,A79,A81,AXIOMS:22;
end;
end;
hence f2 is_non_decreasing_on 1,(k+1)+1 by A76,SFMASTR3:def 4;
thus for i be Nat st i>(k+1)+1 & i <= len f1 holds f1.i=f2.i by A12,
A69,FINSEQ_1:18;
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 A76;
end;
hence P[k+1];
end;
for k be Nat holds P[k] from Ind(A4,A10);
hence thesis by A1,A2,A3;
end;
Lm15:
for s being 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,s),p0 &
len f=n & len g = n holds
f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n
proof
let s be State of SCMPDS,f,g be FinSequence of INT,p0,n be Nat;
set a=GBP;
assume A1:s.a=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,s),p0 &
len f=n & len g = n;
per cases;
suppose A2: n=0;
then g={} & f={} by A1,FINSEQ_1:25;
hence f,g are_fiberwise_equipotent;
thus g is_non_decreasing_on 1,n by A2,Th1;
suppose n<>0;
then A3: n>0 by NAT_1:19;
defpred P[Nat] means
for t be State of SCMPDS,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,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;
A4: P[0]
proof
let t be State of SCMPDS,f1,f2 be FinSequence of INT,m be Nat;
assume A5: t.a=0 & t.a2+t.a1=n-1 & t.a2=0 & m=n-t.a2 &
p0=t.a3-t.a1-1 & f1 is_FinSequence_on t,p0 &
f2 is_FinSequence_on IExec(FR,t),p0 &
f1 is_non_decreasing_on 1,m & len f1=n & len f2 = n;
then A6: t.DataLoc(t.a,2)=t.intpos(0+2) by SCMP_GCD:5
.=0 by A5;
A7: now let i be Nat;
assume A8: 1 <= i & i <= len f2;
hence f2.i=IExec(FR,t).intpos(p0+i) by A5,Def1
.=t.intpos(p0+i) by A6,SCMPDS_7:66
.=f1.i by A5,A8,Def1;
end;
hence f1,f2 are_fiberwise_equipotent by A5,FINSEQ_1:18;
thus f2 is_non_decreasing_on 1,n by A5,A7,FINSEQ_1:18;
end;
A9: now
let k be Nat;
assume A10:P[k];
now
let t be State of SCMPDS,f1,f2 be FinSequence of INT,m be Nat;
assume A11: t.a=0 & t.a2+t.a1=n-1 & t.a2=k+1 & m=n-t.a2 &
p0=t.a3-t.a1-1 & f1 is_FinSequence_on t,p0 &
f2 is_FinSequence_on IExec(FR,t),p0 &
f1 is_non_decreasing_on 1,m & len f1=n & len f2 = n;
set t1=IExec(J4,t),
Bt=IExec(B3,t);
A12: t1.a =0 & t1.a1 = t.a1+1 &
t1.a2=t.a2 & t1.a3 =t.a3+1 &
t1.a4 =t.a3+1 & t1.a6 =t.a1+1 &
for i be Nat st i >= 7 holds t1.intpos i=t.intpos i by A11,Lm10;
consider h be FinSequence of INT such that
A13: len h=n & for i be Nat st 1<=i & i <= len h holds
h.i=IExec(WH,t1).intpos(p0+i) by Th2;
A14: p0=t1.a4-t1.a6-1 by A11,A12,XCMPLX_1:32;
then p0=t1.a4-(t1.a6+1) by XCMPLX_1:36;
then t1.a4=p0+(t1.a6+1) by XCMPLX_1:27;
then t1.a4 >= 6+(t1.a6+1) by A1,AXIOMS:24;
then A15: t1.a4 >= 6+1+t1.a6 by XCMPLX_1:1;
t.a1=n-1-t.a2 by A11,XCMPLX_1:26;
then t.a1=m-1 by A11,XCMPLX_1:21;
then A16: m=t1.a6 by A12,XCMPLX_1:27;
now
let i be Nat;
assume A17: 1 <= i & i <= len f1;
then A18: p0+1 <= p0+i by AXIOMS:24;
p0+1 >= 6+1 by A1,AXIOMS:24;
then A19: p0+i >= 7 by A18,AXIOMS:22;
thus f1.i=t.intpos(p0+i) by A11,A17,Def1
.= t1.intpos(p0+i) by A11,A19,Lm10;
end;
then A20: f1 is_FinSequence_on t1,p0 by Def1;
A21: h is_FinSequence_on IExec(WH,t1),p0 by A13,Def1;
A22: m+(k+1)=n by A11,XCMPLX_1:27;
k+1 > 0 by NAT_1:19;
then n > 0+m by A22,REAL_1:53;
then A23: f1,h are_fiberwise_equipotent & h is_non_decreasing_on 1,m+1
by A11,A12,A13,A14,A15,A16,A20,A21,Th17;
p0=t.a3-(t.a1+1) by A11,XCMPLX_1:36;
then p0+(t.a1+1)=t.a3 by XCMPLX_1:27;
then t.a3 >= 6+(t.a1+1) by A1,AXIOMS:24;
then A24: t.a3 >= 6+1+t.a1 by XCMPLX_1:1;
then A25: Bt.a=0 & Bt.a2=t.a2-1 & Bt.a3=t.a3+1 & Bt.a1=t.a1+1 &
for i be Nat st i <> 2 holds Bt.intpos i=IExec(WH,t1).intpos i
by A11,Lm11;
then A26: Bt.a2+Bt.a1=n-1 by A11,XCMPLX_1:28;
A27: Bt.a2=k by A11,A25,XCMPLX_1:26;
A28: n-Bt.a2=m+1 by A11,A25,XCMPLX_1:37;
A29: Bt.a3-Bt.a1-1=p0 by A11,A25,XCMPLX_1:32;
now
let i be Nat;
assume A30: 1 <= i & i <= len h;
then A31: p0+1 <= p0+i by AXIOMS:24;
p0+1 >= 6+1 by A1,AXIOMS:24;
then p0+i >= 7 by A31,AXIOMS:22;
then A32: p0+i > 2 by AXIOMS:22;
thus h.i=IExec(WH,t1).intpos(p0+i) by A13,A30
.= Bt.intpos(p0+i) by A11,A24,A32,Lm11;
end;
then A33: h is_FinSequence_on Bt,p0 by Def1;
now
let i be Nat;
assume A34: 1 <= i & i <= len f2;
A35: t.a2 > 0 by A11,NAT_1:19;
thus f2.i=IExec(FR,t).intpos(p0+i) by A11,A34,Def1
.= IExec(FR,Bt).intpos(p0+i) by A11,A24,A35,Lm13;
end;
then A36: f2 is_FinSequence_on IExec(FR,Bt),p0 by Def1;
then h,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n
by A10,A11,A13,A23,A25,A26,A27,A28,A29,A33;
hence f1,f2 are_fiberwise_equipotent by A23,RFINSEQ:2;
thus f2 is_non_decreasing_on 1,n by A10,A11,A13,A23,A25,A26,A27,
A28,A29,A33,A36;
end;
hence P[k+1];
end;
A37: for k being Nat holds P[k] from Ind(A4,A9);
n >= 1+0 by A3,INT_1:20;
then n-1 >= 0 by REAL_1:84;
then reconsider n1=n-1 as Nat by INT_1:16;
A38: s.a2+s.a1=n-1+0 by A1;
A39: 1=n-s.a2 by A1,XCMPLX_1:18;
A40: p0=s.a3-s.a1-1 by A1,XCMPLX_1:26;
A41: f is_non_decreasing_on 1,1 by Th1;
P[n1] by A37;
hence thesis by A1,A38,A39,A40,A41;
end;
theorem
for s being 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),s),p0 holds
f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n
proof
let s be State of SCMPDS,f,g be FinSequence of INT,p0,n be Nat;
assume A1: p0 >= 6 & len f=n & len g = n & f is_FinSequence_on s,p0 &
g is_FinSequence_on IExec(insert-sort(n,p0+1),s),p0;
set a=GBP;
set i1= GBP:=0,
i2= (GBP,1):=0,
i3= (GBP,2):=(n-1),
i4= (GBP,3):=(p0+1);
set t0=Initialized s,
I4=i1 ';' i2 ';' i3 ';' i4,
t1=IExec(I4,s),
t2=IExec(i1 ';' i2 ';' i3,s),
t3=IExec(i1 ';' i2,s),
t4=Exec(i1, t0);
A2: t4.a=0 by SCMPDS_2:57;
A3: now let i be Nat;
assume i > 3;
then i > 0 by AXIOMS:22;
then intpos i<> a by SCMP_GCD:4,def 2;
hence t4.intpos i=t0.intpos i by SCMPDS_2:57
.=s.intpos i by SCMPDS_5:40;
end;
A4: DataLoc(t4.a,1)=intpos (0+1) by A2,SCMP_GCD:5;
then A5: a<>DataLoc(t4.a,1) by SCMP_GCD:4,def 2;
A6: t3.a =Exec(i2, t4).a by SCMPDS_5:47
.=0 by A2,A5,SCMPDS_2:58;
A7: t3.a1 =Exec(i2, t4).a1 by SCMPDS_5:47
.=0 by A4,SCMPDS_2:58;
A8: now let i be Nat;
assume A9:i > 3;
then i > 1 by AXIOMS:22;
then A10: intpos i<> DataLoc(t4.a,1) by A4,SCMP_GCD:4;
thus t3.intpos i =Exec(i2, t4).intpos i by SCMPDS_5:47
.=t4.intpos i by A10,SCMPDS_2:58
.=s.intpos i by A3,A9;
end;
A11: DataLoc(t3.a,2)=intpos (0+2) by A6,SCMP_GCD:5;
then A12: a<>DataLoc(t3.a,2) by SCMP_GCD:4,def 2;
A13: t2.a =Exec(i3, t3).a by SCMPDS_5:46
.=0 by A6,A12,SCMPDS_2:58;
A14: a1<>DataLoc(t3.a,2) by A11,SCMP_GCD:4;
A15: t2.a1 =Exec(i3, t3).a1 by SCMPDS_5:46
.=0 by A7,A14,SCMPDS_2:58;
A16: t2.a2 =Exec(i3, t3).a2 by SCMPDS_5:46
.=n-1 by A11,SCMPDS_2:58;
A17: now let i be Nat;
assume A18:i > 3;
then i > 2 by AXIOMS:22;
then A19: intpos i<> DataLoc(t3.a,2) by A11,SCMP_GCD:4;
thus t2.intpos i =Exec(i3, t3).intpos i by SCMPDS_5:46
.=t3.intpos i by A19,SCMPDS_2:58
.=s.intpos i by A8,A18;
end;
A20: DataLoc(t2.a,3)=intpos (0+3) by A13,SCMP_GCD:5;
then A21: a<>DataLoc(t2.a,3) by SCMP_GCD:4,def 2;
A22: t1.a =Exec(i4, t2).a by SCMPDS_5:46
.=0 by A13,A21,SCMPDS_2:58;
A23: a1<>DataLoc(t2.a,3) by A20,SCMP_GCD:4;
A24: t1.a1 =Exec(i4, t2).a1 by SCMPDS_5:46
.=0 by A15,A23,SCMPDS_2:58;
A25: a2<>DataLoc(t2.a,3) by A20,SCMP_GCD:4;
A26: t1.a2 =Exec(i4, t2).a2 by SCMPDS_5:46
.=n-1 by A16,A25,SCMPDS_2:58;
A27: t1.a3 =Exec(i4, t2).a3 by SCMPDS_5:46
.=p0+1 by A20,SCMPDS_2:58;
A28: p0+1 >= 6+1 by A1,AXIOMS:24;
now
let i be Nat;
assume A29: 1 <= i & i <= len f;
set pi=p0+i;
pi >= p0+1 by A29,AXIOMS:24;
then pi >= 7 by A28,AXIOMS:22;
then A30: pi > 3 by AXIOMS:22;
then A31: intpos pi<> DataLoc(t2.a,3) by A20,SCMP_GCD:4;
thus t1.intpos pi =Exec(i4, t2).intpos pi by SCMPDS_5:46
.=t2.intpos pi by A31,SCMPDS_2:58
.=s.intpos pi by A17,A30
.=f.i by A1,A29,Def1;
end;
then A32: f is_FinSequence_on t1,p0 by Def1;
A33: I4 is_closed_on s & I4 is_halting_on s by SCMPDS_6:34,35;
t1.a3 >= t1.a1+7 by A24,A27,A28;
then A34: FR is_closed_on t1 & FR is_halting_on t1 by A22,Lm12;
now
let i be Nat;
assume 1 <= i & i <= len g;
hence g.i=IExec(insert-sort(n,p0+1),s).intpos(p0+i) by A1,Def1
.=IExec(I4 ';' FR,s).intpos(p0+i) by Def2
.=IExec(FR,t1).intpos(p0+i) by A33,A34,SCMPDS_7:49;
end;
then g is_FinSequence_on IExec(FR,t1),p0 by Def1;
hence thesis by A1,A22,A24,A26,A27,A32,Lm15;
end;