Copyright (c) 2000 Association of Mizar Users
environ
vocabulary AMI_3, SCMPDS_2, AMI_1, SCMPDS_4, SCMFSA6A, SCMFSA8A, SCMFSA_7,
INT_1, SCMFSA8B, CARD_1, SCMPDS_5, FUNCT_1, UNIALG_2, SCMFSA7B, SCMFSA6B,
FUNCT_4, SCMPDS_3, RELAT_1, AMI_2, SCMFSA_9, ARYTM_1, RELOC, SCM_1,
FUNCT_7, BOOLE, FUNCOP_1, CARD_3, SCMPDS_8, FINSEQ_1, RFUNCT_2, RFINSEQ,
FUNCT_2, SCPISORT, SCMP_GCD, SCPQSORT;
notation TARSKI, XBOOLE_0, FUNCT_2, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1,
FUNCT_1, FUNCT_4, RECDEF_1, 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, CARD_3, FINSEQ_1, SCMPDS_8, SFMASTR3, RFINSEQ, SCPISORT;
constructors AMI_5, SCMPDS_4, SCM_1, SCMPDS_5, SCMPDS_6, SCMP_GCD, SCMPDS_8,
SFMASTR3, RFINSEQ, SCPISORT, RECDEF_1, NAT_1, MEMBERED, RAT_1;
clusters AMI_1, INT_1, FUNCT_1, RELSET_1, FINSEQ_1, SCMPDS_2, SCMFSA_4,
SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMPDS_8, RFINSEQ, WSIERP_1, NAT_1,
FRAENKEL, XREAL_0, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
theorems AMI_1, AMI_3, NAT_1, REAL_1, TARSKI, FUNCT_4, INT_1, AMI_5, SCMPDS_2,
FUNCT_7, GRFUNC_1, AXIOMS, SCM_1, SCMFSA6B, SCMPDS_4, SCMPDS_5, REAL_2,
SCMPDS_6, SCMP_GCD, SCMPDS_7, SCMPDS_8, FINSEQ_1, SFMASTR3, FINSEQ_2,
RFINSEQ, FUNCT_2, FINSEQ_3, RELAT_1, SCMFSA6A, SCPISORT, XBOOLE_0,
XBOOLE_1, SQUARE_1, XCMPLX_0, XCMPLX_1;
schemes NAT_1, SCMPDS_8;
begin :: The Several Properties of "while" Program and Finite Sequence
reserve x for Int_position,
n,p0 for Nat;
Lm1:
for s being State of SCMPDS, I,J being shiftable Program-block,n being Nat
holds I ';' Goto n ';' J is shiftable
proof
let s be State of SCMPDS, I,J be shiftable Program-block,n be Nat;
I ';' Goto n ';' J = I ';' Load (goto n) ';' J by SCMPDS_6:def 1;
hence thesis;
end;
definition
let I,J be shiftable Program-block,
a be Int_position,k1 be Integer;
cluster if>0(a,k1,I,J) -> shiftable;
correctness
proof
set i = (a,k1)<=0_goto (card I + 2),
G =Goto (card J+1);
reconsider IJ=I ';' G ';' J as shiftable Program-block by Lm1;
if>0(a,k1,I,J) = i ';' I ';' G ';' J by SCMPDS_6:def 5
.=i ';' (I ';' G) ';' J by SCMPDS_4:50
.=i ';' IJ by SCMPDS_4:50
.=Load i ';' IJ by SCMPDS_4:def 4;
hence thesis;
end;
end;
theorem Th1: :: see SCMPDS_6:87
for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
J being shiftable Program-block,a ,b be Int_position,k1 being Integer
st s.DataLoc(s.a,k1) > 0 & I is_closed_on s & I is_halting_on s
holds IExec(if>0(a,k1,I,J),s).b = IExec(I,s).b
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
J be shiftable Program-block,a,b be Int_position,k1 be Integer;
assume s.DataLoc(s.a,k1)>0 & I is_closed_on s & I is_halting_on s;
then A1: IExec(if>0(a,k1,I,J),s) =
IExec(I,s) +* Start-At inspos (card I + card J + 2) by SCMPDS_6:84;
not b in dom Start-At inspos (card I + card J + 2) by SCMPDS_4:59;
hence IExec(if>0(a,k1,I,J),s).b = IExec(I,s).b by A1,FUNCT_4:12;
end;
set A = the Instruction-Locations of SCMPDS,
D = SCM-Data-Loc;
Lm2:
for a be Int_position,i be Integer,I be Program-block holds
while>0(a,i,I)= ((a,i)<=0_goto (card I +2)) ';' (I ';'
goto -(card I+1))
proof
let a be Int_position,i be Integer,I be Program-block;
set i1=(a,i)<=0_goto (card I +2),
i2=goto -(card I+1);
thus while>0(a,i,I) = i1 ';' I ';' i2 by SCMPDS_8:def 3
.= i1 ';' (I ';' i2) by SCMPDS_4:51;
end;
Lm3:
for I being Program-block,a being Int_position,i being Integer
holds Shift(I,1) c= while>0(a,i,I)
proof
let I be Program-block,a be Int_position,i be Integer;
set i1=(a,i)<=0_goto (card I+2),
i2=goto -(card I+1);
A1: card Load i1=1 by SCMPDS_5:6;
while>0(a,i,I) = i1 ';' I ';' i2 by SCMPDS_8:def 3
.= i1 ';' I ';' Load i2 by SCMPDS_4:def 5
.= Load i1 ';' I ';' Load i2 by SCMPDS_4:def 4;
hence thesis by A1,SCMPDS_7:16;
end;
theorem Th2:
for s,sm be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position,i be Integer, m be Nat st card I>0 & I is_closed_on s &
I is_halting_on s & s.DataLoc(s.a,i) > 0 &
m=LifeSpan (s +* Initialized stop I)+2 &
sm=(Computation(s +* Initialized stop while>0(a,i,I))).m holds
sm | SCM-Data-Loc =IExec(I,s)|SCM-Data-Loc &
sm +*Initialized stop while>0(a,i,I)=sm
proof
let s,sm be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position,i be Integer,m be Nat;
set b=DataLoc(s.a,i);
set WH =while>0(a,i,I),
iWH=Initialized stop WH,
IsI=Initialized stop I;
set i1=(a,i)<=0_goto (card I+2),
i2=goto -(card I+1);
set s2 = s +* IsI,
s3 = s +* iWH,
s4 = (Computation s3).1;
assume A1: card I>0 & I is_closed_on s & I is_halting_on s & s.b > 0 &
m=LifeSpan s2+2 & sm=(Computation(s +* iWH)).m;
A2: IsI c= s2 by FUNCT_4:26;
A3: s2 is halting by A1,SCMPDS_6:def 3;
then s2 +* IsI is halting by A2,AMI_5:10;
then A4: I is_halting_on s2 by SCMPDS_6:def 3;
A5: I is_closed_on s2 by A1,SCMPDS_6:38;
A6: IC s3 =inspos 0 by SCMPDS_6:21;
WH = i1 ';' (I ';' i2) by Lm2;
then A7: CurInstr s3 = i1 by SCMPDS_6:22;
A8: (Computation s3).(0 + 1) = Following (Computation s3).0 by AMI_1:def 19
.= Following s3 by AMI_1:def 19
.= Exec(i1,s3) by A7,AMI_1:def 18;
A9: s3.DataLoc(s3.a,i)= s3.b by SCMPDS_5:19
.= s.b by SCMPDS_5:19;
A10: IC s4 = s4.IC SCMPDS by AMI_1:def 15
.= Next IC s3 by A1,A8,A9,SCMPDS_2:68
.= inspos(0+1) by A6,SCMPDS_4:70;
s2,s3 equal_outside A by SCMPDS_4:36;
then A11: s2 | D = s3 | D by SCMPDS_4:24;
now let x;
thus s2.x = s3.x by A11,SCMPDS_4:23
.= s4.x by A8,SCMPDS_2:68;
end;
then A12: s2 | D = s4 | D by SCMPDS_4:23;
set m2=LifeSpan s2,
s5=(Computation s4).m2,
l1=inspos (card I + 1);
A13: dom (s | A) = A by SCMPDS_6:1;
card I + 1 < card I + 2 by REAL_1:53;
then A14: l1 in dom WH by SCMPDS_8:18;
A15: WH c= iWH by SCMPDS_6:17;
iWH c= s3 by FUNCT_4:26;
then A16: WH c= s3 by A15,XBOOLE_1:1;
Shift(I,1) c= WH by Lm3;
then Shift(I,1) c= s3 by A16,XBOOLE_1:1;
then A17: Shift(I,1) c= s4 by AMI_3:38;
then (Computation s2).m2 | D = s5 | D by A1,A2,A4,A5,A10,A12,SCMPDS_7:36;
then A18: s5|D =(Result s2)|D by A3,SCMFSA6B:16
.= (Result s2 +* s | A)|D by A13,AMI_5:7,SCMPDS_2:10
.=IExec(I,s)|D by SCMPDS_4:def 8;
set m3=m2 +1;
set s6=(Computation s3).m3;
A19: IC s5=l1 by A1,A2,A4,A5,A10,A12,A17,SCMPDS_7:36;
A20: s6=s5 by AMI_1:51;
then A21: CurInstr s6=s5.l1 by A19,AMI_1:def 17
.=s4.l1 by AMI_1:54
.=s3.l1 by AMI_1:54
.=WH.l1 by A14,A16,GRFUNC_1:8
.=i2 by SCMPDS_8:19;
set s7=(Computation s3).(m3+ 1);
A22: s7 = Following s6 by AMI_1:def 19
.= Exec(i2,s6) by A21,AMI_1:def 18;
A23: IC s7=s7.IC SCMPDS by AMI_1:def 15
.=ICplusConst(s6,-(card I+1)) by A22,SCMPDS_2:66
.=ICplusConst(s6,0-(card I+1)) by XCMPLX_1:150
.=inspos 0 by A19,A20,SCMPDS_7:1;
A24: s7=(Computation s3).(m2+(1+1)) by XCMPLX_1:1
.=sm by A1;
now let x;
thus sm.x=s6.x by A22,A24,SCMPDS_2:66
.=s5.x by AMI_1:51;
end;
hence sm | D =IExec(I,s)|D by A18,SCMPDS_4:23;
thus sm +* iWH=sm by A23,A24,SCMPDS_7:37;
end;
theorem Th3:
for s be State of SCMPDS,I be Program-block st
for t be State of SCMPDS st
t | SCM-Data-Loc =s | SCM-Data-Loc holds I is_halting_on t
holds I is_closed_on s
proof
let s be State of SCMPDS,I be Program-block;
assume A1: for t be State of SCMPDS st t | D =s | D
holds I is_halting_on t;
set pI=stop I,
II=Initialized pI,
sI=s +* II;
defpred X[Nat] means not IC (Computation sI).$1 in dom pI;
assume not I is_closed_on s;
then A2: ex k be Nat st X[k] by SCMPDS_6:def 2;
consider n such that
A3: X[n] and
A4: for m be Nat st X[m] holds n <= m from Min(A2);
A5: not Next IC (Computation sI).n in dom pI by A3,SCMPDS_4:71;
set s2 = (Computation sI).n,
Ig = ((IC s2,Next IC s2) --> (goto 1, goto -1)),
s0 = sI +* Ig,
s1 = s2 +* Ig,
t1= sI +* (IC s2,goto 1),
t2= t1 +* (Next IC s2,goto -1),
t3= s2 +* (IC s2,goto 1),
t4= t3 +* (Next IC s2,goto -1),
IL=the Instruction-Locations of SCMPDS;
set IAt = pI +* Start-At inspos 0;
dom stop(I) misses dom Start-At inspos 0 by SCMPDS_4:54;
then A6: pI c= IAt by FUNCT_4:33;
A7: II = IAt by SCMPDS_4:def 2;
(IAt) | IL = pI by SCMPDS_4:58;
then A8: dom stop (I) = dom(IAt) /\ IL by RELAT_1:90;
then A9: not IC s2 in dom IAt by A3,XBOOLE_0:def 3;
A10: not Next IC s2 in dom IAt by A5,A8,XBOOLE_0:def 3;
A11: II c= sI by FUNCT_4:26;
then IAt c= t1 by A7,A9,SCMFSA6A:1;
then IAt c= t2 by A10,SCMFSA6A:1;
then A12: IAt c= s0 by SCMPDS_4:69;
A13: sI,t1 equal_outside IL by SCMFSA6A:3;
t1,t2 equal_outside IL by SCMFSA6A:3;
then sI,t2 equal_outside IL by A13,FUNCT_7:29;
then A14: sI,s0 equal_outside IL by SCMPDS_4:69;
then A15: s0,sI equal_outside IL by FUNCT_7:28;
A16: for a be Int_position holds s.a = sI.a by SCMPDS_5:19;
s0 | D = sI | D by A14,SCMPDS_4:24
.= s | D by A16,SCMPDS_4:23;
then I is_halting_on s0 by A1;
then A17: s0 +* II is halting by SCMPDS_6:def 3;
A18: s0 +* II=s0 by A7,A12,AMI_5:10;
A19: stop I c= s0 by A6,A12,XBOOLE_1:1;
A20: stop I c= sI by A6,A7,A11,XBOOLE_1:1;
for m be Nat st m < n holds IC((Computation sI).m) in dom pI by A4;
then A21: (Computation s0).n,s2 equal_outside IL by A15,A19,A20,SCMPDS_4:67;
A22: s2,t3 equal_outside IL by SCMFSA6A:3;
t3,t4 equal_outside IL by SCMFSA6A:3;
then s2,t4 equal_outside IL by A22,FUNCT_7:29;
then s2,s1 equal_outside IL by SCMPDS_4:69;
then A23: (Computation s0).n, s1 equal_outside IL by A21,FUNCT_7:29;
sI | IL = s2 | IL by SCMFSA6B:17;
then t1 | IL = t3 | IL by SCMFSA6A:5;
then t2 | IL = t4 | IL by SCMFSA6A:5;
then s0 | IL = t4 | IL by SCMPDS_4:69;
then s0 | IL = s1 | IL by SCMPDS_4:69;
then (Computation s0).n | IL = s1 | IL by SCMFSA6B:17;
then A24: (Computation s0).n = s1 by A23,SCMFSA6A:2;
s1 is not halting by SCMPDS_4:66;
hence contradiction by A17,A18,A24,SCM_1:27;
end;
theorem Th4:
for i1,i2,i3,i4 be Instruction of SCMPDS holds
card (i1 ';' i2 ';' i3 ';' i4)=4
proof
let x1,x2,x3,x4 be Instruction of SCMPDS;
thus card (x1 ';' x2 ';' x3 ';' x4)=card (x1 ';' x2 ';' x3)+1 by SCMP_GCD:8
.=card (x1 ';' x2 )+1+1 by SCMP_GCD:8
.=2+1+1 by SCMP_GCD:9
.=4;
end;
theorem Th5:
for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
a,x,y be Int_position, i,c be Integer st card I > 0 &
s.x >= c+s.DataLoc(s.a,i) &
(for t be State of SCMPDS st t.x >= c+t.DataLoc(s.a,i) & t.y=s.y &
t.a=s.a & t.DataLoc(s.a,i) > 0 holds
IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
IExec(I,t).DataLoc(s.a,i) < t.DataLoc(s.a,i) &
IExec(I,t).x >= c+IExec(I,t).DataLoc(s.a,i) & IExec(I,t).y=t.y)
holds
while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s &
(s.DataLoc(s.a,i) > 0 implies
IExec(while>0(a,i,I),s) =IExec(while>0(a,i,I),IExec(I,s)))
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a,x1,y1 be Int_position, i,c be Integer;
set b=DataLoc(s.a,i);
assume A1: card I > 0;
assume A2: s.x1 >= c+s.b;
assume A3: for t be State of SCMPDS st t.x1 >= c+t.b & t.y1=s.y1 &
t.a=s.a & t.b > 0 holds
IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
IExec(I,t).b < t.b & IExec(I,t).x1 >= c+IExec(I,t).b &
IExec(I,t).y1=t.y1;
A4: for x st x in {x1} holds
s.x >= c+s.b by A2,TARSKI:def 1;
now
let t be State of SCMPDS;
assume A5: (for x st x in {x1} holds t.x >= c+t.b) &
(for x st x in {y1} holds t.x=s.x) & t.a=s.a & t.b > 0;
x1 in {x1} by TARSKI:def 1;
then A6: t.x1 >= c+t.b by A5;
y1 in {y1} by TARSKI:def 1;
then A7: t.y1=s.y1 by A5;
hence IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
IExec(I,t).b < t.b by A3,A5,A6;
hereby
let x;
assume A8: x in {x1};
IExec(I,t).x1 >= c+IExec(I,t).b by A3,A5,A6,A7;
hence IExec(I,t).x >= c+IExec(I,t).b by A8,TARSKI:def 1;
end;
hereby
let x;
assume A9: x in {y1};
hence IExec(I,t).x=IExec(I,t).y1 by TARSKI:def 1
.=t.y1 by A3,A5,A6,A7
.=t.x by A9,TARSKI:def 1;
end;
end;
hence thesis by A1,A4,SCMPDS_8:27;
end;
theorem Th6:
for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
a,x,y be Int_position, i,c be Integer st card I > 0 & s.x >= c &
(for t be State of SCMPDS st t.x >= c & t.y=s.y &
t.a=s.a & t.DataLoc(s.a,i) > 0 holds
IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
IExec(I,t).DataLoc(s.a,i) < t.DataLoc(s.a,i) &
IExec(I,t).x >= c & IExec(I,t).y=t.y)
holds
while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s &
( s.DataLoc(s.a,i) > 0 implies
IExec(while>0(a,i,I),s) =IExec(while>0(a,i,I),IExec(I,s)))
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a,x,y be Int_position, i,c be Integer;
set b=DataLoc(s.a,i);
assume A1: card I > 0;
assume A2: s.x >= c;
assume A3: for t be State of SCMPDS st t.x >= c & t.y=s.y &
t.a=s.a & t.b > 0
holds IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
IExec(I,t).b < t.b & IExec(I,t).x >= c & IExec(I,t).y=t.y;
defpred P[set] means ex t be State of SCMPDS st
t=$1 & t.x >= c & t.y=s.y;
consider f be Function of product the Object-Kind of SCMPDS,NAT such that
A4: for s be State of SCMPDS holds
(s.b <= 0 implies f.s =0) & (s.b > 0 implies f.s=s.b)
by SCMPDS_8:5;
deffunc F(State of SCMPDS) = f.$1;
A5: for t be State of SCMPDS holds F(Dstate t)=0 iff t.b <= 0
proof
let t be State of SCMPDS;
thus F(Dstate t)=0 implies t.b <= 0
proof
assume A6: F(Dstate t)=0;
assume t.b > 0;
then (Dstate t).b > 0 by SCMPDS_8:4;
hence contradiction by A4,A6;
end;
assume t.b <= 0;
then (Dstate t).b <= 0 by SCMPDS_8:4;
hence thesis by A4;
end;
then A7: for t be State of SCMPDS st
P[Dstate t] & F(Dstate t)=0 holds t.b <= 0;
A8: P[Dstate s]
proof
take t=Dstate s;
thus t=Dstate s;
thus t.x >= c by A2,SCMPDS_8:4;
thus t.y=s.y by SCMPDS_8:4;
end;
A9: now
let t be State of SCMPDS;
assume A10:P[Dstate t] & t.a=s.a & t.b > 0;
then consider v be State of SCMPDS such that
A11: v=Dstate t & v.x >= c & v.y=s.y;
A12: t.x >= c by A11,SCMPDS_8:4;
A13: t.y=s.y by A11,SCMPDS_8:4;
hence IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t
by A3,A10,A12;
set It=IExec(I,t),
t2=Dstate It,
t1=Dstate t;
thus F(t2) < F(t1)
proof
assume A14: F(t2) >= F(t1);
t1.b > 0 by A10,SCMPDS_8:4;
then A15: F(t1)=t1.b by A4
.=t.b by SCMPDS_8:4;
then It.b > 0 by A5,A10,A14;
then t2.b > 0 by SCMPDS_8:4;
then F(t2)=t2.b by A4
.=It.b by SCMPDS_8:4;
hence contradiction by A3,A10,A12,A13,A14,A15;
end;
thus P[Dstate It]
proof
take v=Dstate It;
thus v=Dstate It;
It.x >= c by A3,A10,A12,A13;
hence v.x >= c by SCMPDS_8:4;
It.y=t.y by A3,A10,A12,A13;
hence v.y=s.y by A13,SCMPDS_8:4;
end;
end;
(F(s)=F(s) or P[s]) & while>0(a,i,I) is_closed_on s &
while>0(a,i,I) is_halting_on s from WhileGHalt(A1,A7,A8,A9);
hence while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s;
assume A16: s.b > 0;
(F(s)=F(s) or P[s]) &
IExec(while>0(a,i,I),s) = IExec(while>0(a,i,I),IExec(I,s))
from WhileGExec(A1,A16,A7,A8,A9);
hence thesis;
end;
theorem Th7:
for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
a,x1,x2,x3,x4 be Int_position, i,c,md be Integer st
card I > 0 & s.x4=s.x3-c+s.x1 & md <= s.x3-c &
(for t be State of SCMPDS st t.x4=t.x3-c+t.x1 & md <= t.x3-c &
t.x2=s.x2 & t.a=s.a & t.DataLoc(s.a,i) > 0 holds
IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
IExec(I,t).DataLoc(s.a,i) < t.DataLoc(s.a,i) &
IExec(I,t).x4=IExec(I,t).x3-c+IExec(I,t).x1 &
md <= IExec(I,t).x3-c & IExec(I,t).x2=t.x2)
holds
while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s &
( s.DataLoc(s.a,i) > 0 implies
IExec(while>0(a,i,I),s) =IExec(while>0(a,i,I),IExec(I,s)) )
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a,x1,x2,x3,x4 be Int_position, i,c,md be Integer;
set b=DataLoc(s.a,i);
assume A1: card I > 0;
assume A2: s.x4=s.x3-c+s.x1 & md <= s.x3-c;
assume A3: for t be State of SCMPDS st t.x4=t.x3-c+t.x1 & md <= t.x3-c &
t.x2=s.x2 & t.a=s.a & t.DataLoc(s.a,i) > 0 holds
IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
IExec(I,t).DataLoc(s.a,i) < t.DataLoc(s.a,i) &
IExec(I,t).x4=IExec(I,t).x3-c+IExec(I,t).x1 &
md <= IExec(I,t).x3-c & IExec(I,t).x2=t.x2;
defpred P[set] means ex t be State of SCMPDS st
t=$1 & t.x4=t.x3-c+t.x1 & md <= t.x3-c & t.x2=s.x2;
consider f be Function of product the Object-Kind of SCMPDS,NAT such that
A4: for s be State of SCMPDS holds
(s.b <= 0 implies f.s =0) & (s.b > 0 implies f.s=s.b)
by SCMPDS_8:5;
deffunc F(State of SCMPDS) = f.$1;
A5: for t be State of SCMPDS holds F(Dstate t)=0 iff t.b <= 0
proof
let t be State of SCMPDS;
thus F(Dstate t)=0 implies t.b <= 0
proof
assume A6: F(Dstate t)=0;
assume t.b > 0;
then (Dstate t).b > 0 by SCMPDS_8:4;
hence contradiction by A4,A6;
end;
assume t.b <= 0;
then (Dstate t).b <= 0 by SCMPDS_8:4;
hence thesis by A4;
end;
then A7: for t be State of SCMPDS st P[Dstate t] & F(Dstate t)=0 holds t.b <=
0;
A8: P[Dstate s]
proof
take t=Dstate s;
thus t=Dstate s;
t.x4=s.x3-c+s.x1 by A2,SCMPDS_8:4;
then t.x4=t.x3-c+s.x1 by SCMPDS_8:4;
hence t.x4=t.x3-c+t.x1 by SCMPDS_8:4;
thus md <= t.x3-c by A2,SCMPDS_8:4;
thus t.x2=s.x2 by SCMPDS_8:4;
end;
A9: now
let t be State of SCMPDS;
assume A10:P[Dstate t] & t.a=s.a & t.b > 0;
then consider v be State of SCMPDS such that
A11: v=Dstate t & v.x4=v.x3-c+v.x1 & md <= v.x3-c &
v.x2=s.x2;
t.x4=v.x3-c+v.x1 by A11,SCMPDS_8:4;
then t.x4=t.x3-c+v.x1 by A11,SCMPDS_8:4;
then A12: t.x4=t.x3-c+t.x1 by A11,SCMPDS_8:4;
A13: md <= t.x3-c by A11,SCMPDS_8:4;
A14: t.x2=s.x2 by A11,SCMPDS_8:4;
hence IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t
by A3,A10,A12,A13;
set It=IExec(I,t),
t2=Dstate It,
t1=Dstate t;
thus F(t2) < F(t1)
proof
assume A15: F(t2) >= F(t1);
t1.b > 0 by A10,SCMPDS_8:4;
then A16: F(t1)=t1.b by A4
.=t.b by SCMPDS_8:4;
then It.b > 0 by A5,A10,A15;
then t2.b > 0 by SCMPDS_8:4;
then F(t2)=t2.b by A4
.=It.b by SCMPDS_8:4;
hence contradiction by A3,A10,A12,A13,A14,A15,A16;
end;
thus P[Dstate It]
proof
take v=Dstate It;
thus v=Dstate It;
It.x4=It.x3-c+It.x1 by A3,A10,A12,A13,A14;
then v.x4=It.x3-c+It.x1 by SCMPDS_8:4;
then v.x4=v.x3-c+It.x1 by SCMPDS_8:4;
hence v.x4=v.x3-c+v.x1 by SCMPDS_8:4;
md <= It.x3-c by A3,A10,A12,A13,A14;
hence md <= v.x3-c by SCMPDS_8:4;
It.x2=t.x2 by A3,A10,A12,A13,A14;
hence v.x2=s.x2 by A14,SCMPDS_8:4;
end;
end;
(F(s)=F(s) or P[s]) & while>0(a,i,I) is_closed_on s &
while>0(a,i,I) is_halting_on s from WhileGHalt(A1,A7,A8,A9);
hence while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s;
assume A17: s.b > 0;
(F(s)=F(s) or P[s]) &
IExec(while>0(a,i,I),s) = IExec(while>0(a,i,I),IExec(I,s))
from WhileGExec(A1,A17,A7,A8,A9);
hence thesis;
end;
theorem Th8:
for f being FinSequence of INT,m,k1,k,n be Nat st m<=k & k <= n &
k1=k-1 & f is_non_decreasing_on m,k1 & f is_non_decreasing_on k+1,n &
(for i be Nat st m <= i & i < k holds f.i <= f.k) &
(for i be Nat st k < i & i <= n holds f.k <= f.i)
holds
f is_non_decreasing_on m,n
proof
let f be FinSequence of INT,m,k1,k,n be Nat;
assume A1: m<=k & k <= n & k1=k-1;
assume A2: f is_non_decreasing_on m,k1;
assume A3: f is_non_decreasing_on k+1,n;
assume A4: for i be Nat st m <= i & i < k holds f.i <= f.k;
assume A5: for i be Nat st k < i & i <= n holds f.k <= f.i;
now
let i,j be Nat;
assume A6: m <= i & i <= j & j <= n;
per cases by REAL_1:def 5;
suppose j < k;
then j+1 <= k by INT_1:20;
then j <= k1 by A1,REAL_1:84;
hence f.i <= f.j by A2,A6,SFMASTR3:def 4;
suppose A7: j = k;
hereby
per cases;
suppose i=j;
hence f.i <= f.j;
suppose i<>j;
then i<j by A6,REAL_1:def 5;
hence f.i <= f.j by A4,A6,A7;
end;
suppose A8: j > k;
hereby
per cases by REAL_1:def 5;
suppose A9: i < k;
A10: f.j >= f.k by A5,A6,A8;
f.k >= f.i by A4,A6,A9;
hence f.i <= f.j by A10,AXIOMS:22;
suppose A11: i = k;
hereby
per cases;
suppose i=j;
hence f.i <= f.j;
suppose i<>j;
then i<j by A6,REAL_1:def 5;
hence f.i <= f.j by A5,A6,A11;
end;
suppose i > k;
then i >= k+1 by INT_1:20;
hence f.i <= f.j by A3,A6,SFMASTR3:def 4;
end;
end;
hence thesis by SFMASTR3:def 4;
end;
theorem Th9: :: RFINSEQ:17
for f,g be FinSequence,x be set st x in dom g & f,g are_fiberwise_equipotent
holds ex y be set st y in dom g & f.x=g.y
proof
let f,g be FinSequence,x be set;
assume A1:x in dom g & f,g are_fiberwise_equipotent;
then consider P be Permutation of dom g such that
A2: f = g*P by RFINSEQ:17;
take y=P.x;
thus y in dom g by A1,FUNCT_2:7;
thus f.x=g.y by A1,A2,FUNCT_2:70;
end;
theorem Th10: ::RFINSEQ:14
for f,g,h be FinSequence holds
f,g are_fiberwise_equipotent iff h^f, h^g are_fiberwise_equipotent
proof
let f,g,h be FinSequence;
thus f,g are_fiberwise_equipotent implies h^f, h^g are_fiberwise_equipotent
proof assume
A1: f,g are_fiberwise_equipotent;
now let y be set;
card (f"{y}) = card (g"{y}) by A1,RFINSEQ:def 1;
hence card ((h^f)"{y}) = card(g"{y}) + card(h"{y}) by FINSEQ_3:63
.= card((h^g)"{y}) by FINSEQ_3:63;
end;
hence thesis by RFINSEQ:def 1;
end; assume
A2: h^f,h^g are_fiberwise_equipotent;
now let x be set;
card((h^f)"{x}) = card(f"{x})+card(h"{x}) &
card((h^g)"{x}) = card(g"{x})+card(h"{x}) &
card((h^f)"{x}) = card((h^g)"{x}) by A2,FINSEQ_3:63,RFINSEQ:def 1;
hence card(f"{x}) = card(g"{x}) by XCMPLX_1:2;
end;
hence thesis by RFINSEQ:def 1;
end;
theorem Th11:
for f,g be FinSequence,m,n,j be Nat st f,g are_fiberwise_equipotent &
m<=n & n <= len f & (for i be Nat st 1<=i & i<=m holds f.i=g.i) &
(for i be Nat st n<i & i<=len f holds f.i=g.i) & (m<j & j<=n)
holds ex k be Nat st m<k & k<=n & f.j=g.k
proof
let f,g be FinSequence,m,n,j be Nat;
assume A1: f,g are_fiberwise_equipotent;
assume A2: m<=n & n <= len f;
assume A3: for i be Nat st 1<=i & i<=m holds f.i=g.i;
assume A4: for i be Nat st n<i & i<=len f holds f.i=g.i;
assume A5: m<j & j<=n;
A6: len f=len g by A1,RFINSEQ:16;
n-m >= 0 by A2,SQUARE_1:12;
then reconsider m2=n-m as Nat by INT_1:16;
len f-n >= 0 by A2,SQUARE_1:12;
then reconsider m3=len f-n as Nat by INT_1:16;
A7: len f=len f+n-n by XCMPLX_1:26
.=n+m3 by XCMPLX_1:29;
A8: len g=len f+n-n by A6,XCMPLX_1:26
.=n+m3 by XCMPLX_1:29;
consider s1,r1 be FinSequence such that
A9: len s1 = n & len r1 = m3 & f = s1^r1 by A7,FINSEQ_2:25;
consider s2,r2 be FinSequence such that
A10: len s2 = n & len r2 = m3 & g = s2^r2 by A8,FINSEQ_2:25;
len s1=n+m-m by A9,XCMPLX_1:26
.=m+m2 by XCMPLX_1:29;
then consider p1,q1 be FinSequence such that
A11: len p1 = m & len q1 = m2 & s1 = p1^q1 by FINSEQ_2:25;
len s2=n+m-m by A10,XCMPLX_1:26
.=m+m2 by XCMPLX_1:29;
then consider p2,q2 be FinSequence such that
A12: len p2 = m & len q2 = m2 & s2 = p2^q2 by FINSEQ_2:25;
A13: f=p1^(q1^r1) by A9,A11,FINSEQ_1:45;
A14: g=p2^(q2^r2) by A10,A12,FINSEQ_1:45;
A15: Seg m = dom p1 by A11,FINSEQ_1:def 3;
A16: Seg m = dom p2 by A12,FINSEQ_1:def 3;
now
let i be Nat;
assume A17: i in Seg m3;
then A18: i in dom r1 by A9,FINSEQ_1:def 3;
A19: i in dom r2 by A10,A17,FINSEQ_1:def 3;
A20: 1 <= i & i <= m3 by A17,FINSEQ_1:3;
then A21: n+1 <= n+i by AXIOMS:24;
n < n+1 by REAL_1:69;
then A22: n< i+n by A21,AXIOMS:22;
A23: len s1+i <= len f by A7,A9,A20,AXIOMS:24;
thus r1.i=f.(len s1+i) by A9,A18,FINSEQ_1:def 7
.=g.(len s2+i) by A4,A9,A10,A22,A23
.=r2.i by A10,A19,FINSEQ_1:def 7;
end;
then r1=r2 by A9,A10,FINSEQ_2:10;
then A24: s1,s2 are_fiberwise_equipotent by A1,A9,A10,RFINSEQ:14;
now
let i be Nat;
assume A25: i in Seg m;
then A26: 1<= i & i <= m by FINSEQ_1:3;
thus p1.i=f.i by A13,A15,A25,FINSEQ_1:def 7
.=g.i by A3,A26
.=p2.i by A14,A16,A25,FINSEQ_1:def 7;
end;
then p1=p2 by A11,A12,FINSEQ_2:10;
then A27: q1,q2 are_fiberwise_equipotent by A11,A12,A24,Th10;
A28: j-len p1 > 0 by A5,A11,SQUARE_1:11;
then reconsider x=j-len p1 as Nat by INT_1:16;
A29: Seg m2 = dom q1 by A11,FINSEQ_1:def 3;
A30: Seg m2 = dom q2 by A12,FINSEQ_1:def 3;
A31: 1+ 0<= x by A28,INT_1:20;
A32: x <= n-len p1 by A5,REAL_1:49;
then x in dom q2 by A11,A30,A31,FINSEQ_1:3;
then consider y be set such that
A33: y in dom q2 & q1.x=q2.y by A27,Th9;
reconsider y as Nat by A33;
A34: 1<=y & y<=m2 by A30,A33,FINSEQ_1:3;
take k=len p2+y;
A35: k>=len p2+1 by A34,AXIOMS:24;
m+1 > m by REAL_1:69;
hence m<k by A12,A35,AXIOMS:22;
k <= m2+len p2 by A34,AXIOMS:24;
then k <= n+-m+m by A12,XCMPLX_0:def 8;
hence k<=n by XCMPLX_1:139;
A36: j=len p1+x by XCMPLX_1:27;
A37: x in dom q1 by A11,A29,A31,A32,FINSEQ_1:3;
then A38: len p1 + x in dom s1 by A11,FINSEQ_1:41;
A39: len p2 + y in dom s2 by A12,A33,FINSEQ_1:41;
thus f.j=s1.(len p1+x) by A9,A36,A38,FINSEQ_1:def 7
.=q2.y by A11,A33,A37,FINSEQ_1:def 7
.=s2.(len p2+y) by A12,A33,FINSEQ_1:def 7
.=g.k by A10,A39,FINSEQ_1:def 7;
end;
Lm4:
for s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position, i,c be Integer,f,g be FinSequence of INT,m,n,m1
be Nat st card I> 0 & s.a=c & len f=n & len g=n & f is_FinSequence_on s,m &
g is_FinSequence_on IExec(while>0(a,i,I),s),m & 1=s.DataLoc(c,i) &
m1=m+n+1 & m+1=s.intpos m1 & m+n=s.intpos(m1+1) &
(for t be State of SCMPDS,f1,f2 be FinSequence of INT,k1,k2,y1,yn be Nat
st t.a=c & 2*k1+1=t.DataLoc(c,i) & k2=m+n+2*k1+1 & m+y1=t.intpos k2 &
m+yn=t.intpos(k2+1) & (1 <= y1 & yn <= n or y1 >= yn)
holds I is_closed_on t & I is_halting_on t & IExec(I,t).a=t.a &
(for j be Nat st (1<=j & j<2*k1+1) holds
IExec(I,t).intpos(m+n+j)=t.intpos(m+n+j)) &
(y1>=yn implies IExec(I,t).DataLoc(c,i)=2*k1-1 &
(for j be Nat st (1<=j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j))) &
(y1<yn implies IExec(I,t).DataLoc(c,i)=2*k1+3 &
(for j be Nat st (1<=j & j<y1) or (yn<j & j <= n) holds
IExec(I,t).intpos(m+j) = t.intpos (m+j)) &
(ex ym be Nat st y1 <= ym & ym <= yn & m+y1=IExec(I,t).intpos k2 &
m+ym-1=IExec(I,t).intpos (k2+1) & m+ym+1=IExec(I,t).intpos (k2+2) &
m+yn=IExec(I,t).intpos (k2+3) &
(for j be Nat st y1 <= j & j < ym holds
IExec(I,t).intpos (m+j) <= IExec(I,t).intpos (m+ym)) &
(for j be Nat st ym < j & j <= yn holds
IExec(I,t).intpos (m+j) >= IExec(I,t).intpos (m+ym)))) &
(f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec(I,t),m &
len f1=n & len f2=n implies f1,f2 are_fiberwise_equipotent))
holds
while>0(a,i,I) is_halting_on s &
f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position, i,c be Integer,f,g be FinSequence of INT,
m,n,m1 be Nat;
set b=DataLoc(c,i);
assume A1: card I>0 & s.a=c & len f=n & len g=n;
assume A2: f is_FinSequence_on s,m;
assume A3: g is_FinSequence_on IExec(while>0(a,i,I),s),m;
assume A4: 1=s.b;
assume A5: m1=m+n+1 & m+1=s.intpos m1 & m+n=s.intpos(m1+1);
assume A6: for t be State of SCMPDS,f1,f2 be FinSequence of INT,
k1,k2,y1,yn be Nat st t.a=c & 2*k1+1=t.b & k2=m+n+2*k1+1 &
m+y1=t.intpos k2 & m+yn=t.intpos(k2+1) & (1 <= y1 & yn <= n or y1 >= yn)
holds I is_closed_on t & I is_halting_on t & IExec(I,t).a=t.a &
(for j be Nat st (1<=j & j<2*k1+1) holds
IExec(I,t).intpos(m+n+j)=t.intpos(m+n+j)) &
(y1>=yn implies IExec(I,t).b=2*k1-1 &
(for j be Nat st (1<=j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j))) &
(y1<yn implies IExec(I,t).b=2*k1+3 &
(for j be Nat st (1<=j & j<y1) or (yn<j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j)) &
(ex ym be Nat st y1 <= ym & ym <= yn & m+y1=IExec(I,t).intpos k2 &
m+ym-1=IExec(I,t).intpos (k2+1) & m+ym+1=IExec(I,t).intpos (k2+2) &
m+yn=IExec(I,t).intpos (k2+3) &
(for j be Nat st y1 <= j & j < ym holds
IExec(I,t).intpos(m+j) <= IExec(I,t).intpos(m+ym)) &
(for j be Nat st ym < j & j <= yn holds
IExec(I,t).intpos(m+j) >= IExec(I,t).intpos(m+ym)))) &
(f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec(I,t),m &
len f1=n & len f2=n implies f1,f2 are_fiberwise_equipotent);
set WH =while>0(a,i,I),
sWH=stop WH,
iWH=Initialized sWH;
defpred P[Nat] means
for t be State of SCMPDS,f1 be FinSequence of INT, k1,k2,y1,yn be
Nat st t.a=c & 2*k1+1=t.b & k2=m+n+2*k1+1 &
(1 <= y1 & yn <= n or y1 >= yn) & m+y1=t.intpos k2 &
m+yn=t.intpos(k2+1) & yn-y1<=$1 & f1 is_FinSequence_on t,m &
len f1=n holds ex k be Nat,f2 be FinSequence of INT st
(Computation(t +*iWH)).k+*iWH=(Computation(t +*iWH)).k &
f2 is_FinSequence_on (Computation(t +*iWH)).k,m & len f2=n &
f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn &
(for j be Nat st y1<yn & (1<=j & j<y1 or yn<j & j<= n) holds
f2.j= t.intpos(m+j)) &
(for j be Nat st y1>=yn & 1<=j & j<= n holds f2.j= t.intpos(m+j)) &
(for j be Nat st (1<=j & j<2*k1+1) holds
(Computation(t +*iWH)).k.intpos(m+n+j)=t.intpos(m+n+j)) &
(Computation(t +*iWH)).k.b=t.b-2 & (Computation(t +*iWH)).k.a=c;
A7: P[0]
proof
let t be State of SCMPDS,f1 be FinSequence of INT,k1,k2,y1,yn be
Nat;
assume A8: t.a=c & 2*k1+1=t.b & k2=m+n+2*k1+1 &
(1 <= y1 & yn <= n or y1 >= yn) & m+y1=t.intpos k2 &
m+yn=t.intpos(k2+1) & yn-y1<=0 &
f1 is_FinSequence_on t,m & len f1=n;
then A9: t.b > 0 by NAT_1:19;
A10: I is_closed_on t & I is_halting_on t & IExec(I,t).a=t.a by A6,A8;
A11: y1>=yn implies IExec(I,t).b=2*k1-1 & (for j be Nat st (1<=j & j <= n)
holds IExec(I,t).intpos (m+j) = t.intpos (m+j)) by A6,A8;
A12: y1>=yn by A8,SQUARE_1:11;
A13: IExec(I,t).b=2*k1+1-1-1 by A8,A11,SQUARE_1:11,XCMPLX_1:26
.=t.b-(1+1) by A8,XCMPLX_1:36;
take k=LifeSpan (t +* Initialized stop I)+2;
set tk=(Computation(t +* iWH)).k;
A14: tk | D =IExec(I,t) | D by A1,A8,A9,A10,Th2;
consider f2 be FinSequence of INT such that
A15: len f2=n & for i be Nat st 1<=i & i <= len f2 holds
f2.i=IExec(I,t).intpos(m+i) by SCPISORT:2;
A16: f2 is_FinSequence_on IExec(I,t),m by A15,SCPISORT:def 1;
take f2;
thus tk+*iWH =tk by A1,A8,A9,A10,Th2;
now
let i be Nat;
assume 1<=i & i <= len f2;
hence f2.i=IExec(I,t).intpos(m+i) by A15
.=tk.intpos(m+i) by A14,SCMPDS_4:23;
end;
hence f2 is_FinSequence_on tk,m by SCPISORT:def 1;
thus len f2=n by A15;
thus f1,f2 are_fiberwise_equipotent by A6,A8,A15,A16;
thus f2 is_non_decreasing_on y1,yn by A12,SCPISORT:1;
thus for j be Nat st y1<yn & (1<=j & j<y1 or yn<j & j<= n) holds
f2.j= t.intpos(m+j) by A8,SQUARE_1:11;
hereby
let j be Nat;
assume A17: y1>=yn & 1<=j & j<= n;
hence f2.j=IExec(I,t).intpos (m+j) by A15
.=t.intpos(m+j) by A6,A8,A17;
end;
hereby
let j be Nat;
assume A18: 1<=j & j<2*k1+1;
thus tk.intpos(m+n+j)=IExec(I,t).intpos(m+n+j) by A14,SCMPDS_4:23
.=t.intpos(m+n+j) by A6,A8,A18;
end;
thus tk.b=t.b-2 by A13,A14,SCMPDS_4:23;
thus tk.a=c by A8,A10,A14,SCMPDS_4:23;
end;
A19: now let k be Nat;
assume A20:P[k];
now let t be State of SCMPDS,f1 be FinSequence of INT,
k1,k2,y1,ym,yn be Nat;
assume A21: t.a=c & 2*k1+1=t.b & k2=m+n+2*k1+1 &
(1 <= y1 & yn <= n or y1 >= yn) & m+y1=t.intpos k2 &
m+yn=t.intpos(k2+1) & yn-y1<=k+1 &
f1 is_FinSequence_on t,m & len f1=n;
per cases;
suppose yn-y1<=0;
hence ex kk be Nat,f2 be FinSequence of INT st
(Computation(t +*iWH)).kk+*iWH=(Computation(t +*iWH)).kk &
f2 is_FinSequence_on (Computation(t +*iWH)).kk,m & len f2=n &
f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn &
(for j be Nat st y1<yn & (1<=j & j<y1 or yn<j & j<= n) holds
f2.j= t.intpos(m+j)) &
(for j be Nat st y1>=yn & 1<=j & j<= n holds
f2.j= t.intpos(m+j)) &
(for j be Nat st (1<=j & j<2*k1+1) holds
(Computation(t +*iWH)).kk.intpos(m+n+j)=t.intpos(m+n+j)) &
(Computation(t +*iWH)).kk.b=t.b-2 &
(Computation(t +*iWH)).kk.a=c by A7,A21;
suppose A22: yn-y1>0;
then A23: yn>y1 by REAL_2:106;
A24: t.b > 0 by A21,NAT_1:19;
A25: I is_closed_on t & I is_halting_on t & IExec(I,t).a=t.a
by A6,A21;
set It=IExec(I,t);
A26: y1<yn implies It.b=2*k1+3 &
(for j be Nat st (1<=j & j<y1) or (yn<j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j)) &
(ex ym be Nat st y1 <= ym & ym <= yn & m+y1=It.intpos k2 &
m+ym-1=It.intpos (k2+1) & m+ym+1=It.intpos (k2+2) &
m+yn=It.intpos (k2+3) &
(for j be Nat st y1 <= j & j < ym holds
IExec(I,t).intpos(m+j) <= IExec(I,t).intpos(m+ym)) &
(for j be Nat st ym < j & j <= yn holds
IExec(I,t).intpos(m+j) >= IExec(I,t).intpos(m+ym))) by A6,A21;
set m1=LifeSpan (t +* Initialized stop I)+2;
set t1=(Computation(t +* iWH)).m1;
A27: t1 | D =IExec(I,t) | D & t1+*iWH =t1 by A1,A21,A24,A25,Th2;
consider ym be Nat such that
A28: y1 <= ym & ym <= yn & m+y1=It.intpos k2 &
m+ym-1=It.intpos (k2+1) & m+ym+1=It.intpos (k2+2) &
m+yn=It.intpos (k2+3) &
(for j be Nat st y1 <= j & j < ym holds
IExec(I,t).intpos(m+j) <= IExec(I,t).intpos(m+ym)) &
(for j be Nat st ym < j & j <= yn holds
IExec(I,t).intpos(m+j) >= IExec(I,t).intpos(m+ym)) by A22,A26,
REAL_2:106;
set k3=m+n+2*(k1+1)+1,
yd=ym+1;
A29: t1.a=c by A21,A25,A27,SCMPDS_4:23;
A30: t1.b=2*k1+3 by A22,A26,A27,REAL_2:106,SCMPDS_4:23;
A31: t1.b=2*k1+(2*1+1) by A22,A26,A27,REAL_2:106,SCMPDS_4:23
.=2*k1+2*1+1 by XCMPLX_1:1
.=2*(k1+1)+1 by XCMPLX_1:8;
A32: yd > ym by REAL_1:69;
then A33: yd >= y1 by A28,AXIOMS:22;
then A34: yd >= 1 by A21,A22,AXIOMS:22,REAL_2:106;
A35: k3=m+n+(2*k1+2*1)+1 by XCMPLX_1:8
.=m+n+2*k1+2*1+1 by XCMPLX_1:1
.=k2+2 by A21,XCMPLX_1:1;
then A36: t1.intpos k3=It.intpos (k2+2) by A27,SCMPDS_4:23
.=m+yd by A28,XCMPLX_1:1;
k3+1=k2+(2+1) by A35,XCMPLX_1:1;
then A37: t1.intpos(k3+1)=m+yn by A27,A28,SCMPDS_4:23;
ym+(1+k) >= y1+(1+k) by A28,AXIOMS:24;
then A38: yd+k >= y1+(1+k) by XCMPLX_1:1;
yn <= y1+(k+1) by A21,REAL_1:86;
then yn <= yd+k by A38,AXIOMS:22;
then A39: yn-yd<=k by REAL_1:86;
consider f2 be FinSequence of INT such that
A40: len f2=n & for i be Nat st 1<=i & i <= len f2 holds
f2.i=t1.intpos(m+i) by SCPISORT:2;
f2 is_FinSequence_on t1,m by A40,SCPISORT:def 1;
then consider kl be Nat,f3 be FinSequence of INT such that
A41: (Computation(t1 +*iWH)).kl+*iWH=(Computation(t1 +*iWH)).kl &
f3 is_FinSequence_on (Computation(t1 +*iWH)).kl,m & len f3=n &
f2,f3 are_fiberwise_equipotent &
f3 is_non_decreasing_on yd,yn &
(for j be Nat st yd<yn & (1<=j & j<yd or yn<j & j<= n) holds
f3.j= t1.intpos(m+j)) &
(for j be Nat st yd>=yn & 1<=j & j<= n
holds f3.j=t1.intpos(m+j)) &
(for j be Nat st (1<=j & j<2*(k1+1)+1) holds
(Computation(t1 +*iWH)).kl.intpos(m+n+j)=t1.intpos(m+n+j)) &
(Computation(t1 +*iWH)).kl.b=t1.b-2 &
(Computation(t1 +*iWH)).kl.a=c by A20,A21,A22,A29,A31,A34,A36,A37,
A39,A40,REAL_2:106;
set t2=(Computation(t1 +*iWH)).kl;
A42: ym >= 1 by A21,A22,A28,AXIOMS:22,REAL_2:106;
then ym-1 >= 0 by SQUARE_1:12;
then reconsider yc=ym-1 as Nat by INT_1:16;
A43: t2.b=2*k1+(1+2-2) by A30,A41,XCMPLX_1:29
.=2*k1+1;
A44: yc < ym by INT_1:26;
then A45: yc <= yn by A28,AXIOMS:22;
then A46: yc <= n by A21,A22,AXIOMS:22,REAL_2:106;
set jj=2*k1+1;
A47: k2=m+n+jj by A21,XCMPLX_1:1;
A48: jj >= 1 by NAT_1:29;
A49: 2*k1+3=2*k1+(2*1+1)
.=2*k1+2*1+1 by XCMPLX_1:1
.=2*(k1+1)+1 by XCMPLX_1:8;
then jj < 2*(k1+1)+1 by REAL_1:53;
then A50: t2.intpos k2=t1.intpos(m+n+jj) by A41,A47,A48
.=m+y1 by A27,A28,A47,SCMPDS_4:23;
set jj=2*k1+2;
A51: k2+1=m+n+2*k1+(1+1) by A21,XCMPLX_1:1
.=m+n+jj by XCMPLX_1:1;
jj >= 2 by NAT_1:29;
then A52: jj >= 1 by AXIOMS:22;
jj < 2*(k1+1)+1 by A49,REAL_1:53;
then A53: t2.intpos (k2+1)=t1.intpos(m+n+jj) by A41,A51,A52
.=m+ym-1 by A27,A28,A51,SCMPDS_4:23
.=m+yc by XCMPLX_1:29;
yc <= yn-1 by A28,REAL_1:49;
then yc-y1 <= yn-1-y1 by REAL_1:49;
then A54: yc-y1 <= yn-y1-1 by XCMPLX_1:21;
yn-y1-1 <= k+1-1 by A21,REAL_1:49;
then yn-y1-1 <= k by XCMPLX_1:26;
then yc-y1<=k by A54,AXIOMS:22;
then consider km be Nat,f4 be FinSequence of INT such that
A55: (Computation(t2 +*iWH)).km+*iWH=(Computation(t2 +*iWH)).km &
f4 is_FinSequence_on (Computation(t2 +*iWH)).km,m & len f4=n &
f3,f4 are_fiberwise_equipotent &
f4 is_non_decreasing_on y1,yc &
(for j be Nat st y1<yc & (1<=j & j<y1 or yc<j & j<= n) holds
f4.j= t2.intpos(m+j)) &
(for j be Nat st y1>=yc & 1<=j & j<= n
holds f4.j=t2.intpos(m+j)) &
(for j be Nat st (1<=j & j<2*k1+1) holds
(Computation(t2 +*iWH)).km.intpos(m+n+j)=t2.intpos(m+n+j)) &
(Computation(t2 +*iWH)).km.b=t2.b-2 &
(Computation(t2 +*iWH)).km.a=c by A20,A21,A22,A41,A43,A46,A50,A53,
REAL_2:106;
take mm=m1+(kl+km);
set tm=(Computation(t +* iWH)).mm;
take f4;
A56: tm=(Computation (t1+*iWH)).(kl+km) by A27,AMI_1:51
.=(Computation (t2+*iWH)).km by A41,AMI_1:51;
hence tm+*iWH =tm by A55;
thus f4 is_FinSequence_on tm,m by A55,A56;
thus len f4=n by A55;
now
let i be Nat;
assume 1<=i & i <= len f2;
hence f2.i=t1.intpos(m+i) by A40
.=IExec(I,t).intpos(m+i) by A27,SCMPDS_4:23;
end;
then f2 is_FinSequence_on IExec(I,t),m by SCPISORT:def 1;
then f1,f2 are_fiberwise_equipotent by A6,A21,A40;
then f1,f3 are_fiberwise_equipotent by A41,RFINSEQ:2;
hence f1,f4 are_fiberwise_equipotent by A55,RFINSEQ:2;
A57: yc < yd by A32,A44,AXIOMS:22;
A58: now
let j be Nat;
assume A59: yd<=j & j<=yn;
then A60: j <= n by A21,A22,AXIOMS:22,REAL_2:106;
A61: yc < j by A57,A59,AXIOMS:22;
A62: 1<=j by A34,A59,AXIOMS:22;
now
per cases;
suppose y1<yc;
hence f4.j=t2.intpos(m+j) by A55,A60,A61;
suppose y1>=yc;
hence f4.j=t2.intpos(m+j) by A55,A60,A62;
end;
hence f4.j=f3.j by A41,A60,A62,SCPISORT:def 1;
end;
now let i,j be Nat;
assume A63: yd <= i & i <= j & j <= yn;
then A64: i <= yn by AXIOMS:22;
A65: yd <= j by A63,AXIOMS:22;
A66: f4.i=f3.i by A58,A63,A64;
f4.j=f3.j by A58,A63,A65;
hence f4.i <= f4.j by A41,A63,A66,SFMASTR3:def 4;
end;
then A67: f4 is_non_decreasing_on yd,yn by SFMASTR3:def 4;
y1-1 >= 0 by A21,A22,REAL_2:106,SQUARE_1:12;
then reconsider y0=y1-1 as Nat by INT_1:16;
A68: y0 <= yc by A28,REAL_1:49;
A69: now let i be Nat;
assume A70:1<=i & i<=y0;
i-1 < i by INT_1:26;
then i-1 < y1-1 by A70,AXIOMS:22;
then A71:i<y1 by REAL_1:49;
y1 <= n by A21,A23,AXIOMS:22;
then A72:i<=n by A71,AXIOMS:22;
now
per cases;
suppose y1<yc;
hence f4.i= t2.intpos(m+i) by A55,A70,A71;
suppose y1>=yc;
hence f4.i= t2.intpos(m+i) by A55,A70,A72;
end;
hence f4.i=f3.i by A41,A70,A72,SCPISORT:def 1;
end;
A73: now let i be Nat;
assume A74: yc<i & i<=len f4;
0 <= yc by NAT_1:18;
then A75: 1+0 <= i by A74,INT_1:20;
now
per cases;
suppose y1<yc;
hence f4.i= t2.intpos(m+i) by A55,A74;
suppose y1>=yc;
hence f4.i= t2.intpos(m+i) by A55,A74,A75;
end;
hence f4.i=f3.i by A41,A55,A74,A75,SCPISORT:def 1;
end;
A76: ym <= n by A21,A22,A28,AXIOMS:22,REAL_2:106;
then A77: f4.ym=f3.ym by A44,A55,A73;
now
per cases;
suppose yd<yn;
hence f3.ym= t1.intpos(m+ym) by A32,A41,A42;
suppose yd>=yn;
hence f3.ym= t1.intpos(m+ym) by A41,A42,A76;
end;
then A78: f4.ym=IExec(I,t).intpos(m+ym) by A27,A77,SCMPDS_4:23;
A79: now let i be Nat;
assume A80:y1 <= i & i < ym;
y0 < y1 by INT_1:26;
then A81: y0 < i by A80,AXIOMS:22;
i+1 <= ym by A80,INT_1:20;
then i<=yc by REAL_1:84;
then consider j be Nat such that
A82: y0<j & j<=yc & f4.i=f3.j by A46,A55,A68,A69,A73,A81,Th11;
0 <= y0 by NAT_1:18;
then A83: 1+0 <= j by A82,INT_1:20;
A84: j<yd by A57,A82,AXIOMS:22;
A85: j<= n by A46,A82,AXIOMS:22;
y1-1+1 <= j by A82,INT_1:20;
then y1-1 <= j-1 by REAL_1:84;
then A86: y1 <= j by REAL_1:54;
yc < ym by INT_1:26;
then A87: j < ym by A82,AXIOMS:22;
now
per cases;
suppose yd<yn;
hence f3.j= t1.intpos(m+j) by A41,A83,A84;
suppose yd>=yn;
hence f3.j= t1.intpos(m+j) by A41,A83,A85;
end;
then f4.i=IExec(I,t).intpos(m+j) by A27,A82,SCMPDS_4:23;
hence f4.i <= f4.ym by A28,A78,A86,A87;
end;
A88: now let i be Nat;
assume A89: 1<=i & i<=ym;
then A90: i<yd by A32,AXIOMS:22;
A91: i<=n by A76,A89,AXIOMS:22;
now
per cases;
suppose yd<yn;
hence f3.i= t1.intpos(m+i) by A41,A89,A90;
suppose yd>=yn;
hence f3.i= t1.intpos(m+i) by A41,A89,A91;
end;
hence f3.i=f2.i by A40,A89,A91;
end;
A92: now let i be Nat;
assume A93: yn<i & i<=len f3;
yn>=0 by NAT_1:18;
then A94: 1+0<=i by A93,INT_1:20;
now
per cases;
suppose yd<yn;
hence f3.i= t1.intpos(m+i) by A41,A93;
suppose yd>=yn;
hence f3.i= t1.intpos(m+i) by A41,A93,A94;
end;
hence f3.i=f2.i by A40,A41,A93,A94;
end;
now let i be Nat;
assume A95: ym < i & i <= yn;
then A96: yc < i by A44,AXIOMS:22;
A97: i<=len f4 by A21,A22,A55,A95,AXIOMS:22,REAL_2:106;
consider j be Nat such that
A98: ym<j & j<=yn & f3.i=f2.j by A21,A22,A28,A41,A88,A92,A95,Th11,
REAL_2:106;
A99: 1<=j by A42,A98,AXIOMS:22;
A100: j<=len f2 by A21,A22,A40,A98,AXIOMS:22,REAL_2:106;
f4.i=f2.j by A73,A96,A97,A98
.=t1.intpos(m+j) by A40,A99,A100
.=IExec(I,t).intpos(m+j) by A27,SCMPDS_4:23;
hence f4.ym <= f4.i by A28,A78,A98;
end;
hence f4 is_non_decreasing_on y1,yn by A28,A55,A67,A79,Th8;
thus for j be Nat st y1<yn & (1<=j & j<y1 or yn<j & j<= n) holds
f4.j= t.intpos(m+j)
proof
let j be Nat;
assume A101: y1<yn & (1<=j & j<y1 or yn<j & j<= n);
A102: 1<=j & j<y1 or yc<j & j<= n
proof
per cases by A101;
suppose 1<=j & j<y1;
hence thesis;
suppose yn<j & j<=n;
hence thesis by A45,AXIOMS:22;
end;
A103: 1<=j & j<= n
proof
per cases by A101;
suppose A104:1<=j & j<y1;
then j<yn by A101,AXIOMS:22;
hence thesis by A21,A22,A104,AXIOMS:22,REAL_2:106;
suppose A105: yn<j & j<=n;
then y1 < j by A101,AXIOMS:22;
hence thesis by A21,A22,A105,AXIOMS:22,REAL_2:106;
end;
A106: 1<=j & j<yd or yn<j & j<= n
proof
per cases by A101;
suppose 1<=j & j<y1;
hence thesis by A33,AXIOMS:22;
suppose yn<j & j<=n;
hence thesis;
end;
A107: now
per cases;
suppose yd<yn;
hence f3.j=t1.intpos(m+j) by A41,A106;
suppose yd>=yn;
hence f3.j=t1.intpos(m+j) by A41,A103;
end;
now
per cases;
suppose y1<yc;
hence f4.j=t2.intpos(m+j) by A55,A102;
suppose y1>=yc;
hence f4.j=t2.intpos(m+j) by A55,A103;
end;
hence f4.j=f3.j by A41,A103,SCPISORT:def 1
.=IExec(I,t).intpos(m+j) by A27,A107,SCMPDS_4:23
.=t.intpos(m+j) by A6,A21,A101;
end;
thus for j be Nat st y1>=yn & 1<=j & j<= n holds
f4.j=t.intpos(m+j) by A22,REAL_2:106;
hereby
let j be Nat;
assume A108: 1<=j & j<2*k1+1;
2*k1+1 < 2*(k1+1)+1 by A49,REAL_1:53;
then A109: j < 2*(k1+1)+1 by A108,AXIOMS:22;
thus tm.intpos(m+n+j)=t2.intpos(m+n+j) by A55,A56,A108
.=t1.intpos(m+n+j) by A41,A108,A109
.=IExec(I,t).intpos(m+n+j) by A27,SCMPDS_4:23
.=t.intpos(m+n+j) by A6,A21,A108;
end;
thus tm.b=2*k1+(1+2-2)-2 by A30,A41,A55,A56,XCMPLX_1:29
.=t.b-2 by A21;
thus tm.a=c by A55,A56;
end;
hence P[k+1];
end;
A110: for k being Nat holds P[k] from Ind(A7,A19);
A111: m1=m+n+2*0+1 by A5;
ex k be Nat,f2 be FinSequence of INT st
(Computation(s +*iWH)).k+*iWH=(Computation(s +*iWH)).k &
f2 is_FinSequence_on (Computation(s +*iWH)).k,m & len f2=n &
f,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n &
(for j be Nat st 1<n & (1<=j & j<1 or n<j & j<= n) holds
f2.j= s.intpos(m+j)) &
(for j be Nat st 1>=n & 1<=j & j<= n holds f2.j= s.intpos(m+j)) &
(for j be Nat st (1<=j & j<2*0+1) holds
(Computation(s +*iWH)).k.intpos(m+n+j)=s.intpos(m+n+j)) &
(Computation(s +*iWH)).k.b=s.b-2 & (Computation(s +*iWH)).k.a=c
proof
per cases;
suppose n-1<=0;
hence thesis by A1,A2,A4,A5,A110,A111;
suppose n-1>0;
then reconsider nn=n-1 as Nat by INT_1:16;
P[nn] by A110;
hence thesis by A1,A2,A4,A5,A111;
end;
then consider k be Nat,f2 be FinSequence of INT such that
A112: (Computation(s +*iWH)).k+*iWH=(Computation(s +*iWH)).k &
f2 is_FinSequence_on (Computation(s +*iWH)).k,m & len f2=n &
f,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n &
(Computation(s +*iWH)).k.b=s.b-2 &
(Computation(s +*iWH)).k.a=c;
set sk=(Computation(s +*iWH)).k,
s1 = sk +* iWH,
s2 = (Computation s1).1;
set i1=(a,i)<=0_goto (card I+2),
i2=goto -(card I+1);
A113: IC s1 =inspos 0 by SCMPDS_6:21;
WH = i1 ';' (I ';' i2 ) by Lm2;
then A114: CurInstr s1 = i1 by SCMPDS_6:22;
A115: (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
.= Following s1 by AMI_1:def 19
.= Exec(i1,s1) by A114,AMI_1:def 18;
iWH c= s1 by FUNCT_4:26;
then sWH c= s1 by SCMPDS_4:57;
then A116: sWH c= s2 by AMI_3:38;
A117: card WH=card I+2 by SCMPDS_8:17;
then A118: inspos(card I+2) in dom sWH by SCMPDS_6:25;
A119: IC s2 = s2.IC SCMPDS by AMI_1:def 15
.= ICplusConst(s1,(card I+2)) by A4,A112,A115,SCMPDS_2:68
.= inspos(0+(card I+2)) by A113,SCMPDS_6:23;
s2.inspos(card I+2) = sWH.inspos(card I+2) by A116,A118,GRFUNC_1:8
.=halt SCMPDS by A117,SCMPDS_6:25;
then A120: CurInstr s2 = halt SCMPDS by A119,AMI_1:def 17;
A121: s2=(Computation(s +*iWH)).(k+1) by A112,AMI_1:51;
then A122: s +* iWH is halting by A120,AMI_1:def 20;
then A123: Result (s +* iWH)=s2 by A120,A121,AMI_1:def 22;
thus WH is_halting_on s by A122,SCMPDS_6:def 3;
now let i be Nat;
assume i in Seg n;
then A124: 1 <= i & i <= n by FINSEQ_1:3;
A125: IExec(WH,s)=s2 +* s | A by A123,SCMPDS_4:def 8;
set xi=intpos (m+i);
dom (s | A) = A by SCMPDS_6:1;
then A126: not xi in dom (s | A) by SCMPDS_2:53;
thus g.i=(s2 +* s | A).xi by A1,A3,A124,A125,SCPISORT:def 1
.=s2.xi by A126,FUNCT_4:12
.=s1.xi by A115,SCMPDS_2:68
.=f2.i by A112,A124,SCPISORT:def 1;
end;
hence thesis by A1,A112,FINSEQ_2:10;
end;
Lm5:
for s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position, i,c be Integer,m,n,m1 be Nat st card I> 0 & s.a=c &
1=s.DataLoc(c,i) & m1=m+n+1 & m+1=s.intpos m1 & m+n=s.intpos(m1+1) &
(for t be State of SCMPDS,f1,f2 be FinSequence of INT,k1,k2,y1,yn be Nat
st t.a=c & 2*k1+1=t.DataLoc(c,i) & k2=m+n+2*k1+1 & m+y1=t.intpos k2 &
m+yn=t.intpos(k2+1) & (1 <= y1 & yn <= n or y1 >= yn)
holds I is_closed_on t & I is_halting_on t & IExec(I,t).a=t.a &
(for j be Nat st (1<=j & j<2*k1+1) holds
IExec(I,t).intpos(m+n+j)=t.intpos(m+n+j)) &
(y1>=yn implies IExec(I,t).DataLoc(c,i)=2*k1-1 &
(for j be Nat st (1<=j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j))) &
(y1<yn implies IExec(I,t).DataLoc(c,i)=2*k1+3 &
(for j be Nat st (1<=j & j<y1) or (yn<j & j <= n) holds
IExec(I,t).intpos(m+j) = t.intpos (m+j)) &
(ex ym be Nat st y1 <= ym & ym <= yn & m+y1=IExec(I,t).intpos k2 &
m+ym-1=IExec(I,t).intpos (k2+1) & m+ym+1=IExec(I,t).intpos (k2+2) &
m+yn=IExec(I,t).intpos (k2+3) &
(for j be Nat st y1 <= j & j < ym holds
IExec(I,t).intpos (m+j) <= IExec(I,t).intpos (m+ym)) &
(for j be Nat st ym < j & j <= yn holds
IExec(I,t).intpos (m+j) >= IExec(I,t).intpos (m+ym)))) &
(f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec(I,t),m &
len f1=n & len f2=n implies f1,f2 are_fiberwise_equipotent))
holds
while>0(a,i,I) is_halting_on s
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position, i,c be Integer,m,n,m1 be Nat;
set b=DataLoc(c,i);
assume A1: card I>0 & s.a=c;
assume A2: 1=s.b;
assume A3: m1=m+n+1 & m+1=s.intpos m1 & m+n=s.intpos(m1+1);
assume A4: for t be State of SCMPDS,f1,f2 be FinSequence of INT,
k1,k2,y1,yn be Nat st t.a=c & 2*k1+1=t.b & k2=m+n+2*k1+1 &
m+y1=t.intpos k2 & m+yn=t.intpos(k2+1) & (1 <= y1 & yn <= n or y1 >= yn)
holds I is_closed_on t & I is_halting_on t & IExec(I,t).a=t.a &
(for j be Nat st (1<=j & j<2*k1+1) holds
IExec(I,t).intpos(m+n+j)=t.intpos(m+n+j)) &
(y1>=yn implies IExec(I,t).b=2*k1-1 &
(for j be Nat st (1<=j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j))) &
(y1<yn implies IExec(I,t).b=2*k1+3 &
(for j be Nat st (1<=j & j<y1) or (yn<j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j)) &
(ex ym be Nat st y1 <= ym & ym <= yn & m+y1=IExec(I,t).intpos k2 &
m+ym-1=IExec(I,t).intpos (k2+1) & m+ym+1=IExec(I,t).intpos (k2+2) &
m+yn=IExec(I,t).intpos (k2+3) &
(for j be Nat st y1 <= j & j < ym holds
IExec(I,t).intpos(m+j) <= IExec(I,t).intpos(m+ym)) &
(for j be Nat st ym < j & j <= yn holds
IExec(I,t).intpos(m+j) >= IExec(I,t).intpos(m+ym)))) &
(f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec(I,t),m &
len f1=n & len f2=n implies f1,f2 are_fiberwise_equipotent);
consider f be FinSequence of INT such that
A5: len f=n & for i be Nat st 1<=i & i <= len f holds
f.i=s.intpos(m+i) by SCPISORT:2;
A6: f is_FinSequence_on s,m by A5,SCPISORT:def 1;
set ss=IExec(while>0(a,i,I),s);
consider g be FinSequence of INT such that
A7: len g=n & for i be Nat st 1<=i & i <= len g holds
g.i=ss.intpos(m+i) by SCPISORT:2;
g is_FinSequence_on ss,m by A7,SCPISORT:def 1;
hence thesis by A1,A2,A3,A4,A5,A6,A7,Lm4;
end;
Lm6:
for s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position, i,c be Integer,m,n,m1 be Nat st card I> 0 & s.a=c &
1=s.DataLoc(c,i) & m1=m+n+1 & m+1=s.intpos m1 & m+n=s.intpos(m1+1) &
(for t be State of SCMPDS,f1,f2 be FinSequence of INT,k1,k2,y1,yn be Nat
st t.a=c & 2*k1+1=t.DataLoc(c,i) & k2=m+n+2*k1+1 & m+y1=t.intpos k2 &
m+yn=t.intpos(k2+1) & (1 <= y1 & yn <= n or y1 >= yn)
holds I is_closed_on t & I is_halting_on t & IExec(I,t).a=t.a &
(for j be Nat st (1<=j & j<2*k1+1) holds
IExec(I,t).intpos(m+n+j)=t.intpos(m+n+j)) &
(y1>=yn implies IExec(I,t).DataLoc(c,i)=2*k1-1 &
(for j be Nat st (1<=j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j))) &
(y1<yn implies IExec(I,t).DataLoc(c,i)=2*k1+3 &
(for j be Nat st (1<=j & j<y1) or (yn<j & j <= n) holds
IExec(I,t).intpos(m+j) = t.intpos (m+j)) &
(ex ym be Nat st y1 <= ym & ym <= yn & m+y1=IExec(I,t).intpos k2 &
m+ym-1=IExec(I,t).intpos (k2+1) & m+ym+1=IExec(I,t).intpos (k2+2) &
m+yn=IExec(I,t).intpos (k2+3) &
(for j be Nat st y1 <= j & j < ym holds
IExec(I,t).intpos (m+j) <= IExec(I,t).intpos (m+ym)) &
(for j be Nat st ym < j & j <= yn holds
IExec(I,t).intpos (m+j) >= IExec(I,t).intpos (m+ym)))) &
(f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec(I,t),m &
len f1=n & len f2=n implies f1,f2 are_fiberwise_equipotent))
holds
while>0(a,i,I) is_halting_on s & while>0(a,i,I) is_closed_on s
proof
let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
a be Int_position, i,c be Integer,m,n,m1 be Nat;
set b=DataLoc(c,i);
assume A1: card I>0;
assume A2: s.a=c;
assume A3: 1=s.b;
assume A4: m1=m+n+1 & m+1=s.intpos m1 & m+n=s.intpos(m1+1);
assume A5: for t be State of SCMPDS,f1,f2 be FinSequence of INT,
k1,k2,y1,yn be Nat st t.a=c & 2*k1+1=t.b & k2=m+n+2*k1+1 &
m+y1=t.intpos k2 & m+yn=t.intpos(k2+1) & (1 <= y1 & yn <= n or y1 >= yn)
holds I is_closed_on t & I is_halting_on t & IExec(I,t).a=t.a &
(for j be Nat st (1<=j & j<2*k1+1) holds
IExec(I,t).intpos(m+n+j)=t.intpos(m+n+j)) &
(y1>=yn implies IExec(I,t).b=2*k1-1 &
(for j be Nat st (1<=j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j))) &
(y1<yn implies IExec(I,t).b=2*k1+3 &
(for j be Nat st (1<=j & j<y1) or (yn<j & j <= n) holds
IExec(I,t).intpos (m+j) = t.intpos (m+j)) &
(ex ym be Nat st y1 <= ym & ym <= yn & m+y1=IExec(I,t).intpos k2 &
m+ym-1=IExec(I,t).intpos (k2+1) & m+ym+1=IExec(I,t).intpos (k2+2) &
m+yn=IExec(I,t).intpos (k2+3) &
(for j be Nat st y1 <= j & j < ym holds
IExec(I,t).intpos(m+j) <= IExec(I,t).intpos(m+ym)) &
(for j be Nat st ym < j & j <= yn holds
IExec(I,t).intpos(m+j) >= IExec(I,t).intpos(m+ym)))) &
(f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec(I,t),m &
len f1=n & len f2=n implies f1,f2 are_fiberwise_equipotent);
A6: now let v be State of SCMPDS;
assume A7: v | D =s | D;
then A8: v.a =c by A2,SCMPDS_4:23;
A9: 1 =v.b by A3,A7,SCMPDS_4:23;
A10: m+1 =v.intpos m1 by A4,A7,SCMPDS_4:23;
m+n =v.intpos (m1+1) by A4,A7,SCMPDS_4:23;
hence while>0(a,i,I) is_halting_on v by A1,A4,A5,A8,A9,A10,Lm5;
end;
hence while>0(a,i,I) is_halting_on s;
thus while>0(a,i,I) is_closed_on s by A6,Th3;
end;
begin :: Program Partition is to split a sequence into a "smaller" and
:: a "larger" subsequence
:: a5=a7=length a2=mid(x[1]), a3=x[2], a4=x[n], a6=save
definition
func Partition -> Program-block equals
:Def1:
((GBP,5):=(GBP,4) ';'
SubFrom(GBP,5,GBP,2) ';'
(GBP,3):=(GBP,2) ';'
AddTo(GBP,3,1)) ';'
while>0(GBP,5,
while>0(GBP,5,
(GBP,7):=(GBP,5) ';' AddTo(GBP,5,-1) ';'
(GBP,6):=(intpos 4,0) ';'
SubFrom(GBP,6,intpos 2,0) ';'
if>0(GBP,6, AddTo(GBP,4,-1) ';' AddTo(GBP,7,-1),
Load (GBP,5):=0 )
) ';'
while>0(GBP,7,
(GBP,5):=(GBP,7) ';' AddTo(GBP,7,-1) ';'
(GBP,6):=(intpos 2,0) ';'
SubFrom(GBP,6,intpos 3,0) ';'
if>0(GBP,6, AddTo(GBP,3,1) ';' AddTo(GBP,5,-1),
Load (GBP,7):=0 )
) ';'
if>0(GBP,5,((GBP,6):=(intpos 4,0) ';'
(intpos 4,0):=(intpos 3,0) ';'
(intpos 3,0):=(GBP,6) ';' AddTo(GBP,5,-2) ';'
AddTo(GBP,3,1)) ';' AddTo(GBP,4,-1)
)
) ';'
(GBP,6):=(intpos 4,0) ';'
(intpos 4,0):=(intpos 2,0) ';'
(intpos 2,0):=(GBP,6);
coherence;
end;
begin :: The Construction of Quick Sort
:: a0=global, a1=stack, a2=stack depth
definition
let n,p0 be Nat;
set pn=p0+n;
func QuickSort(n,p0) -> Program-block equals
:Def2:
((GBP:=0) ';'
(SBP:=1) ';'
(SBP,pn):=(p0+1) ';'
(SBP,pn+1):=pn) ';'
while>0(GBP,1,
(GBP,2):=(SBP,pn+1) ';'
SubFrom(GBP,2,SBP,pn) ';'
if>0(GBP,2, (GBP,2):=(SBP,pn) ';'
(GBP,4):=(SBP,pn+1) ';'
Partition ';'
(((SBP,pn+3):=(SBP,pn+1) ';'
(SBP,pn+1):=(GBP,4) ';'
(SBP,pn+2):=(GBP,4) ';'
AddTo(SBP,pn+1,-1)) ';'
AddTo(SBP,pn+2,1) ';'
AddTo(GBP,1,2)),
Load AddTo(GBP,1,-2)
)
);
coherence;
end;
set i1= (GBP,7):=(GBP,5),
i2= AddTo(GBP,5,-1),
i3= (GBP,6):=(intpos 4,0),
i4= SubFrom(GBP,6,intpos 2,0),
i5= AddTo(GBP,4,-1),
i6= AddTo(GBP,7,-1),
i7= Load (GBP,5):=0,
IF1= if>0(GBP,6,i5 ';' i6,i7),
WB1= i1 ';' i2 ';' i3 ';' i4 ';' IF1,
WH1= while>0(GBP,5,WB1),
j1= (GBP,5):=(GBP,7),
j2= AddTo(GBP,7,-1),
j3= (GBP,6):=(intpos 2,0),
j4= SubFrom(GBP,6,intpos 3,0),
j5= AddTo(GBP,3,1),
j6= AddTo(GBP,5,-1),
j7= Load (GBP,7):=0,
IF2= if>0(GBP,6,j5 ';' j6, j7),
WB2= j1 ';' j2 ';' j3 ';' j4 ';' IF2,
WH2= while>0(GBP,7,WB2),
k1 = (GBP,5):=(GBP,4),
k2 = SubFrom(GBP,5,GBP,2),
k3 = (GBP,3):=(GBP,2),
k4 = AddTo(GBP,3,1),
K4 = k1 ';' k2 ';' k3 ';' k4,
k5 = (GBP,6):=(intpos 4,0),
k6 = (intpos 4,0):=(intpos 3,0),
k7 = (intpos 3,0):=(GBP,6),
k8 = AddTo(GBP,5,-2),
k9 = AddTo(GBP,3,1),
k0 = AddTo(GBP,4,-1),
IF3= if>0(GBP,5, k5 ';' k6 ';' k7 ';' k8 ';' k9 ';' k0),
WB3= WH1 ';' WH2 ';' IF3,
WH3= while>0(GBP,5,WB3),
j8 = (GBP,6):=(intpos 4,0),
j9 = (intpos 4,0):=(intpos 2,0),
j0 = (intpos 2,0):=(GBP,6);
set a1=intpos 1,
a2=intpos 2,
a3=intpos 3,
a4=intpos 4,
a5=intpos 5,
a6=intpos 6,
a7=intpos 7;
Lm7:
card WB1=9
proof
thus card WB1= card (i1 ';' i2 ';' i3 ';' i4) + card IF1 by SCMPDS_4:45
.= 4+card IF1 by Th4
.= 4+(card (i5 ';' i6)+card i7+2) by SCMPDS_6:79
.= 4+(2+card i7+2) by SCMP_GCD:9
.= 4+(2+1+2) by SCMPDS_5:6
.= 9;
end;
Lm8:
for s being State of SCMPDS,md,me be Nat st s.a2=md & s.a4=me &
md >= 8 & me >= 8 & s.GBP=0 & s.a5 > 0 holds
IExec(WB1,s).GBP=0 & IExec(WB1,s).a1=s.a1 &
IExec(WB1,s).a2=s.a2 & IExec(WB1,s).a3=s.a3 &
(for i be Nat st i >= 8 holds IExec(WB1,s).intpos i=s.intpos i) &
(s.intpos md < s.intpos me implies IExec(WB1,s).a5=s.a5-1 &
IExec(WB1,s).a4=s.a4-1 & IExec(WB1,s).a7=s.a5-1) &
(s.intpos md >= s.intpos me implies IExec(WB1,s).a5=0 &
IExec(WB1,s).a4=s.a4 & IExec(WB1,s).a7=s.a5)
proof
let s be State of SCMPDS,md,me be Nat;
set a=GBP;
assume A1: s.a2=md & s.a4=me & md >= 8 & me >= 8 & s.a=0 & s.a5 > 0;
set t0=Initialized s,
t1=IExec(i1 ';' i2 ';' i3 ';' i4,s),
t2=IExec(i1 ';' i2 ';' i3,s),
t3=IExec(i1 ';' i2,s),
t4=Exec(i1, t0);
A2: t0.a=0 by A1,SCMPDS_5:40;
A3: t0.a1=s.a1 by SCMPDS_5:40;
A4: t0.a2=md by A1,SCMPDS_5:40;
A5: t0.a3=s.a3 by SCMPDS_5:40;
A6: t0.a4=me by A1,SCMPDS_5:40;
A7: t0.a5=s.a5 by SCMPDS_5:40;
A8: DataLoc(t0.a,7)=intpos (0+7) by A2,SCMP_GCD:5;
then a<>DataLoc(t0.a,7) by SCMP_GCD:4,def 2;
then A9: t4.a =0 by A2,SCMPDS_2:59;
a1<>DataLoc(t0.a,7) by A8,SCMP_GCD:4;
then A10: t4.a1 =s.a1 by A3,SCMPDS_2:59;
a2<>DataLoc(t0.a,7) by A8,SCMP_GCD:4;
then A11: t4.a2 =md by A4,SCMPDS_2:59;
a3<>DataLoc(t0.a,7) by A8,SCMP_GCD:4;
then A12: t4.a3 =s.a3 by A5,SCMPDS_2:59;
a4<>DataLoc(t0.a,7) by A8,SCMP_GCD:4;
then A13: t4.a4 =me by A6,SCMPDS_2:59;
a5<>DataLoc(t0.a,7) by A8,SCMP_GCD:4;
then A14: t4.a5 =s.a5 by A7,SCMPDS_2:59;
DataLoc(t0.a,5)=intpos (0+5) by A2,SCMP_GCD:5;
then A15: t4.a7 =s.a5 by A7,A8,SCMPDS_2:59;
A16: now let i be Nat;
assume i>=8;
then i > 7 by AXIOMS:22;
then intpos i <> DataLoc(t0.a,7) by A8,SCMP_GCD:4;
hence t4.intpos i=t0.intpos i by SCMPDS_2:59
.=s.intpos i by SCMPDS_5:40;
end;
A17: DataLoc(t4.a,5)=intpos (0+5) by A9,SCMP_GCD:5;
then A18: a<>DataLoc(t4.a,5) by SCMP_GCD:4,def 2;
A19: t3.a =Exec(i2, t4).a by SCMPDS_5:47
.=0 by A9,A18,SCMPDS_2:60;
A20: a1<>DataLoc(t4.a,5) by A17,SCMP_GCD:4;
A21: t3.a1 =Exec(i2, t4).a1 by SCMPDS_5:47
.=s.a1 by A10,A20,SCMPDS_2:60;
A22: a2<>DataLoc(t4.a,5) by A17,SCMP_GCD:4;
A23: t3.a2 =Exec(i2, t4).a2 by SCMPDS_5:47
.=md by A11,A22,SCMPDS_2:60;
A24: a3<>DataLoc(t4.a,5) by A17,SCMP_GCD:4;
A25: t3.a3 =Exec(i2, t4).a3 by SCMPDS_5:47
.=s.a3 by A12,A24,SCMPDS_2:60;
A26: a4<>DataLoc(t4.a,5) by A17,SCMP_GCD:4;
A27: t3.a4 =Exec(i2, t4).a4 by SCMPDS_5:47
.=me by A13,A26,SCMPDS_2:60;
A28: t3.a5 =Exec(i2, t4).a5 by SCMPDS_5:47
.=t4.a5+ -1 by A17,SCMPDS_2:60
.=s.a5-1 by A14,XCMPLX_0:def 8;
A29: a7<>DataLoc(t4.a,5) by A17,SCMP_GCD:4;
A30: t3.a7 =Exec(i2, t4).a7 by SCMPDS_5:47
.=s.a5 by A15,A29,SCMPDS_2:60;
A31: now let i be Nat;
assume A32:i>=8;
then i > 5 by AXIOMS:22;
then A33: intpos i <> DataLoc(t4.a,5) by A17,SCMP_GCD:4;
thus t3.intpos i =Exec(i2, t4).intpos i by SCMPDS_5:47
.=t4.intpos i by A33,SCMPDS_2:60
.=s.intpos i by A16,A32;
end;
A34: DataLoc(t3.a,6)=intpos (0+6) by A19,SCMP_GCD:5;
then A35: a<>DataLoc(t3.a,6) by SCMP_GCD:4,def 2;
A36: t2.a =Exec(i3, t3).a by SCMPDS_5:46
.=0 by A19,A35,SCMPDS_2:59;
A37: a1<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A38: t2.a1 =Exec(i3, t3).a1 by SCMPDS_5:46
.=s.a1 by A21,A37,SCMPDS_2:59;
A39: a2<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A40: t2.a2 =Exec(i3, t3).a2 by SCMPDS_5:46
.=md by A23,A39,SCMPDS_2:59;
A41: a3<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A42: t2.a3 =Exec(i3, t3).a3 by SCMPDS_5:46
.=s.a3 by A25,A41,SCMPDS_2:59;
A43: a4<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A44: t2.a4 =Exec(i3, t3).a4 by SCMPDS_5:46
.=me by A27,A43,SCMPDS_2:59;
A45: a5<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A46: t2.a5 =Exec(i3, t3).a5 by SCMPDS_5:46
.=s.a5-1 by A28,A45,SCMPDS_2:59;
A47: DataLoc(t3.a4,0)=intpos (me+0) by A27,SCMP_GCD:5;
A48: t2.a6 =Exec(i3, t3).a6 by SCMPDS_5:46
.=t3.intpos me by A34,A47,SCMPDS_2:59
.=s.intpos me by A1,A31;
A49: a7<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A50: t2.a7 =Exec(i3, t3).a7 by SCMPDS_5:46
.=s.a5 by A30,A49,SCMPDS_2:59;
A51: now let i be Nat;
assume A52:i>=8;
then i > 6 by AXIOMS:22;
then A53: intpos i <> DataLoc(t3.a,6) by A34,SCMP_GCD:4;
thus t2.intpos i=Exec(i3, t3).intpos i by SCMPDS_5:46
.=t3.intpos i by A53,SCMPDS_2:59
.=s.intpos i by A31,A52;
end;
A54: DataLoc(t2.a,6)=intpos (0+6) by A36,SCMP_GCD:5;
then A55: a<>DataLoc(t2.a,6) by SCMP_GCD:4,def 2;
A56: t1.a =Exec(i4, t2).a by SCMPDS_5:46
.=0 by A36,A55,SCMPDS_2:62;
A57: a1<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A58: t1.a1 =Exec(i4, t2).a1 by SCMPDS_5:46
.=s.a1 by A38,A57,SCMPDS_2:62;
A59: a2<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A60: t1.a2 =Exec(i4, t2).a2 by SCMPDS_5:46
.=md by A40,A59,SCMPDS_2:62;
A61: a3<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A62: t1.a3 =Exec(i4, t2).a3 by SCMPDS_5:46
.=s.a3 by A42,A61,SCMPDS_2:62;
A63: a4<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A64: t1.a4 =Exec(i4, t2).a4 by SCMPDS_5:46
.=me by A44,A63,SCMPDS_2:62;
A65: a5<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A66: t1.a5 =Exec(i4, t2).a5 by SCMPDS_5:46
.=s.a5-1 by A46,A65,SCMPDS_2:62;
A67: t1.a6 =Exec(i4, t2).a6 by SCMPDS_5:46
.=t2.a6-t2.DataLoc(t2.a2,0) by A54,SCMPDS_2:62
.=t2.a6-t2.intpos(md+0) by A40,SCMP_GCD:5
.=s.intpos me - s.intpos md by A1,A48,A51;
A68: a7<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A69: t1.a7 =Exec(i4, t2).a7 by SCMPDS_5:46
.=s.a5 by A50,A68,SCMPDS_2:62;
A70: now let i be Nat;
assume A71:i>=8;
then i > 6 by AXIOMS:22;
then A72: intpos i <> DataLoc(t2.a,6) by A54,SCMP_GCD:4;
thus t1.intpos i=Exec(i4, t2).intpos i by SCMPDS_5:46
.=t2.intpos i by A72,SCMPDS_2:62
.=s.intpos i by A51,A71;
end;
set t01=Initialized t1,
ii7= (GBP,5):=0,
t5=Exec(i5,t01);
A73: t01.a=0 by A56,SCMPDS_5:40;
A74: t01.a1=s.a1 by A58,SCMPDS_5:40;
A75: t01.a2=s.a2 by A1,A60,SCMPDS_5:40;
A76: t01.a3=s.a3 by A62,SCMPDS_5:40;
A77: t01.a7=s.a5 by A69,SCMPDS_5:40;
A78: DataLoc(t01.a,5)=intpos(0+5) by A73,SCMP_GCD:5;
A79: DataLoc(t01.a,4)=intpos(0+4) by A73,SCMP_GCD:5;
then a<>DataLoc(t01.a,4) by SCMP_GCD:4,def 2;
then A80: t5.a=0 by A73,SCMPDS_2:60;
a1<>DataLoc(t01.a,4) by A79,SCMP_GCD:4;
then A81: t5.a1=s.a1 by A74,SCMPDS_2:60;
a2<>DataLoc(t01.a,4) by A79,SCMP_GCD:4;
then A82: t5.a2=s.a2 by A75,SCMPDS_2:60;
a3<>DataLoc(t01.a,4) by A79,SCMP_GCD:4;
then A83: t5.a3=s.a3 by A76,SCMPDS_2:60;
A84: DataLoc(t5.a,7)=intpos(0+7) by A80,SCMP_GCD:5;
A85: now
per cases;
suppose A86: t1.DataLoc(t1.a,6) <= 0;
A87: a<>DataLoc(t01.a,5) by A78,SCMP_GCD:4,def 2;
thus IExec(IF1,t1).a=IExec(i7,t1).a by A86,SCMPDS_6:88
.=Exec(ii7,t01).a by SCMPDS_5:45
.=0 by A73,A87,SCMPDS_2:58;
A88: a1<>DataLoc(t01.a,5) by A78,SCMP_GCD:4;
thus IExec(IF1,t1).a1=IExec(i7,t1).a1 by A86,SCMPDS_6:88
.=Exec(ii7,t01).a1 by SCMPDS_5:45
.=s.a1 by A74,A88,SCMPDS_2:58;
A89: a2<>DataLoc(t01.a,5) by A78,SCMP_GCD:4;
thus IExec(IF1,t1).a2=IExec(i7,t1).a2 by A86,SCMPDS_6:88
.=Exec(ii7,t01).a2 by SCMPDS_5:45
.=s.a2 by A75,A89,SCMPDS_2:58;
A90: a3<>DataLoc(t01.a,5) by A78,SCMP_GCD:4;
thus IExec(IF1,t1).a3=IExec(i7,t1).a3 by A86,SCMPDS_6:88
.=Exec(ii7,t01).a3 by SCMPDS_5:45
.=s.a3 by A76,A90,SCMPDS_2:58;
hereby let i be Nat;
assume A91:i>=8;
then i > 5 by AXIOMS:22;
then A92: intpos i <> DataLoc(t01.a,5) by A78,SCMP_GCD:4;
thus IExec(WB1,s).intpos i=IExec(IF1,t1).intpos i by SCMPDS_5:39
.=IExec(i7,t1).intpos i by A86,SCMPDS_6:88
.=Exec(ii7,t01).intpos i by SCMPDS_5:45
.=t01.intpos i by A92,SCMPDS_2:58
.=t1.intpos i by SCMPDS_5:40
.=s.intpos i by A70,A91;
end;
suppose A93: t1.DataLoc(t1.a,6) > 0;
A94: a<>DataLoc(t5.a,7) by A84,SCMP_GCD:4,def 2;
thus IExec(IF1,t1).a=IExec(i5 ';' i6,t1).a by A93,SCMPDS_6:87
.=Exec(i6,t5).a by SCMPDS_5:47
.=0 by A80,A94,SCMPDS_2:60;
A95: a1<>DataLoc(t5.a,7) by A84,SCMP_GCD:4;
thus IExec(IF1,t1).a1=IExec(i5 ';' i6,t1).a1 by A93,SCMPDS_6:87
.=Exec(i6,t5).a1 by SCMPDS_5:47
.=s.a1 by A81,A95,SCMPDS_2:60;
A96: a2<>DataLoc(t5.a,7) by A84,SCMP_GCD:4;
thus IExec(IF1,t1).a2=IExec(i5 ';' i6,t1).a2 by A93,SCMPDS_6:87
.=Exec(i6,t5).a2 by SCMPDS_5:47
.=s.a2 by A82,A96,SCMPDS_2:60;
A97: a3<>DataLoc(t5.a,7) by A84,SCMP_GCD:4;
thus IExec(IF1,t1).a3=IExec(i5 ';' i6,t1).a3 by A93,SCMPDS_6:87
.=Exec(i6,t5).a3 by SCMPDS_5:47
.=s.a3 by A83,A97,SCMPDS_2:60;
hereby let i be Nat;
assume A98:i>=8;
then i > 7 by AXIOMS:22;
then A99: intpos i <> DataLoc(t5.a,7) by A84,SCMP_GCD:4;
i > 4 by A98,AXIOMS:22;
then A100: intpos i<>DataLoc(t01.a,4) by A79,SCMP_GCD:4;
thus IExec(WB1,s).intpos i=IExec(IF1,t1).intpos i by SCMPDS_5:39
.=IExec(i5 ';' i6,t1).intpos i by A93,SCMPDS_6:87
.=Exec(i6,t5).intpos i by SCMPDS_5:47
.=t5.intpos i by A99,SCMPDS_2:60
.=t01.intpos i by A100,SCMPDS_2:60
.=t1.intpos i by SCMPDS_5:40
.=s.intpos i by A70,A98;
end;
end;
hence IExec(WB1,s).a=0 & IExec(WB1,s).a1=s.a1 &
IExec(WB1,s).a2=s.a2 & IExec(WB1,s).a3=s.a3 by SCMPDS_5:39;
thus for i be Nat st i >= 8 holds IExec(WB1,s).intpos i=s.intpos i by A85;
A101: t1.DataLoc(t1.a,6)=t1.intpos (0+6) by A56,SCMP_GCD:5
.=s.intpos me - s.intpos md by A67;
A102: t01.a4=s.a4 by A1,A64,SCMPDS_5:40;
A103: t01.a5=s.a5-1 by A66,SCMPDS_5:40;
hereby
assume s.intpos md < s.intpos me;
then A104: t1.DataLoc(t1.a,6) > 0 by A101,SQUARE_1:11;
A105: a5<>DataLoc(t01.a,4) by A79,SCMP_GCD:4;
A106: a5<>DataLoc(t5.a,7) by A84,SCMP_GCD:4;
thus IExec(WB1,s).a5=IExec(IF1,t1).a5 by SCMPDS_5:39
.=IExec(i5 ';' i6,t1).a5 by A104,SCMPDS_6:87
.=Exec(i6,t5).a5 by SCMPDS_5:47
.=t5.a5 by A106,SCMPDS_2:60
.=s.a5-1 by A103,A105,SCMPDS_2:60;
A107: a4<>DataLoc(t5.a,7) by A84,SCMP_GCD:4;
thus IExec(WB1,s).a4=IExec(IF1,t1).a4 by SCMPDS_5:39
.=IExec(i5 ';' i6,t1).a4 by A104,SCMPDS_6:87
.=Exec(i6,t5).a4 by SCMPDS_5:47
.=t5.a4 by A107,SCMPDS_2:60
.=t01.a4+-1 by A79,SCMPDS_2:60
.=s.a4-1 by A102,XCMPLX_0:def 8;
A108: a7<>DataLoc(t01.a,4) by A79,SCMP_GCD:4;
thus IExec(WB1,s).a7=IExec(IF1,t1).a7 by SCMPDS_5:39
.=IExec(i5 ';' i6,t1).a7 by A104,SCMPDS_6:87
.=Exec(i6,t5).a7 by SCMPDS_5:47
.=t5.a7+ -1 by A84,SCMPDS_2:60
.=t5.a7-1 by XCMPLX_0:def 8
.=s.a5-1 by A77,A108,SCMPDS_2:60;
end;
hereby
assume s.intpos md >= s.intpos me;
then A109: t1.DataLoc(t1.a,6) <= 0 by A101,REAL_2:106;
thus IExec(WB1,s).a5=IExec(IF1,t1).a5 by SCMPDS_5:39
.=IExec(i7,t1).a5 by A109,SCMPDS_6:88
.=Exec(ii7,t01).a5 by SCMPDS_5:45
.=0 by A78,SCMPDS_2:58;
A110: a4<>DataLoc(t01.a,5) by A78,SCMP_GCD:4;
thus IExec(WB1,s).a4=IExec(IF1,t1).a4 by SCMPDS_5:39
.=IExec(i7,t1).a4 by A109,SCMPDS_6:88
.=Exec(ii7,t01).a4 by SCMPDS_5:45
.=s.a4 by A102,A110,SCMPDS_2:58;
A111: a7<>DataLoc(t01.a,5) by A78,SCMP_GCD:4;
thus IExec(WB1,s).a7=IExec(IF1,t1).a7 by SCMPDS_5:39
.=IExec(i7,t1).a7 by A109,SCMPDS_6:88
.=Exec(ii7,t01).a7 by SCMPDS_5:45
.=s.a5 by A77,A111,SCMPDS_2:58;
end;
end;
Lm9:
for s being State of SCMPDS,m4,md be Nat st s.GBP=0 & s.a5 > 0
& s.a4=m4+s.a5 & m4>=8 & s.a2=md & md >= 8 holds IExec(WH1,s).GBP=0 &
IExec(WH1,s).a1=s.a1 & IExec(WH1,s).a5=0 &
IExec(WH1,s).a2=s.a2 & IExec(WH1,s).a3=s.a3 &
(for i be Nat st i >= 8 holds IExec(WH1,s).intpos i=s.intpos i) &
ex mE be Nat st mE=IExec(WH1,s).a7 & IExec(WH1,s).a4=m4+mE &
mE <= s.a5 & (for i be Nat st m4+mE < i & i <=s.a4 holds
IExec(WH1,s).intpos md < IExec(WH1,s).intpos i) &
(mE = 0 or IExec(WH1,s).intpos md >= IExec(WH1,s).intpos(m4+mE))
proof
let s be State of SCMPDS,m4,md be Nat;
assume A1: s.GBP=0 & s.a5 > 0 & s.a4=m4+s.a5 & m4>=8 &
s.a2=md & md >= 8;
set a=GBP;
defpred P[Nat] means
for t being State of SCMPDS st
t.a=0 & t.a5 =$1+1 & t.a4=m4+t.a5 & t.a2=md holds IExec(WH1,t).a=0 &
IExec(WH1,t).a1=t.a1 & IExec(WH1,t).a5=0 &
IExec(WH1,t).a2=t.a2 & IExec(WH1,t).a3=t.a3 &
(for i be Nat st i >= 8 holds IExec(WH1,t).intpos i=t.intpos i) &
ex mE be Nat st mE=IExec(WH1,t).a7 & IExec(WH1,t).a4=m4+mE & mE <= t.a5 &
(for i be Nat st m4+mE < i & i <=t.a4 holds
IExec(WH1,t).intpos md < IExec(WH1,t).intpos i) &
(mE=0 or IExec(WH1,t).intpos md >= IExec(WH1,t).intpos (m4+mE));
now
let t be State of SCMPDS;
set b=DataLoc(t.a,5);
assume A2: t.a=0 & t.a5 =0+1 & t.a4=m4+t.a5 & t.a2=md;
set me=m4+1;
me>=m4 by NAT_1:29;
then A3: me>=8 by A1,AXIOMS:22;
A4: b=intpos (0+5) by A2,SCMP_GCD:5;
A5: now let v be State of SCMPDS;
assume A6: v.a4 >= m4+v.b & v.a2=t.a2 & v.a=t.a & v.b > 0;
then A7: m4+v.b>m4+0 by REAL_1:53;
then A8: v.a4 >=m4 by A6,AXIOMS:22;
v.a4 > 0 by A1,A6,A7,AXIOMS:22;
then reconsider ME=v.a4 as Nat by INT_1:16;
A9: ME >= 8 by A1,A8,AXIOMS:22;
then A10: (v.intpos md < v.intpos ME implies IExec(WB1,v).a5=v.a5-1
&
IExec(WB1,v).a4=v.a4-1 & IExec(WB1,v).a7=v.a5-1) &
(v.intpos md >= v.intpos ME implies IExec(WB1,v).a5=0 &
IExec(WB1,v).a4=v.a4 & IExec(WB1,v).a7=v.a5)
by A1,A2,A4,A6,Lm8;
thus IExec(WB1,v).a=v.a by A1,A2,A4,A6,A9,Lm8;
thus WB1 is_closed_on v & WB1 is_halting_on v by SCMPDS_6:34,35;
hereby
per cases;
suppose A11: v.intpos md < v.intpos ME;
hence IExec(WB1,v).b < v.b by A4,A10,INT_1:26;
m4+v.b-1=m4+IExec(WB1,v).b by A4,A10,A11,XCMPLX_1:29;
hence IExec(WB1,v).a4 >= m4+IExec(WB1,v).b by A6,A10,A11,REAL_1:49
;
suppose A12:v.intpos md >= v.intpos ME;
hence IExec(WB1,v).b < v.b by A1,A2,A4,A6,A9,Lm8;
m4+IExec(WB1,v).b < m4+v.b by A4,A6,A10,A12,REAL_1:53;
hence IExec(WB1,v).a4 >= m4+IExec(WB1,v).b by A6,A10,A12,AXIOMS:
22
;
end;
thus IExec(WB1,v).a2=v.a2 by A1,A2,A4,A6,A9,Lm8;
end;
set It=IExec(WB1,t);
A13: It.a=0 & It.a1=t.a1 & It.a2=t.a2 & It.a3=t.a3 &
(for i be Nat st i >= 8 holds It.intpos i=t.intpos i) &
(t.intpos md < t.intpos me implies It.a5=t.a5-1 &
It.a4=t.a4-1 & It.a7=t.a5-1) &
(t.intpos md >= t.intpos me implies It.a5=0 &
It.a4=t.a4 & It.a7=t.a5) by A1,A2,A3,Lm8;
then A14: It.DataLoc(It.a,5)=It.intpos(0+5) by SCMP_GCD:5
.=0 by A2,A13;
A15: now let x;
thus IExec(WH1,t).x =IExec(WH1,It).x by A2,A4,A5,Lm7,Th5
.=It.x by A14,SCMPDS_8:23;
end;
hence IExec(WH1,t).a=0 by A13;
thus IExec(WH1,t).a1=t.a1 by A13,A15;
thus IExec(WH1,t).a5=0 by A2,A13,A15;
thus IExec(WH1,t).a2=t.a2 by A13,A15;
thus IExec(WH1,t).a3=t.a3 by A13,A15;
A16: now let i be Nat;
assume A17: i >= 8;
thus IExec(WH1,t).intpos i=It.intpos i by A15
.=t.intpos i by A1,A2,A3,A17,Lm8;
end;
hence for i be Nat st i >= 8 holds IExec(WH1,t).intpos i=t.intpos i;
A18: IExec(WH1,t).intpos me=t.intpos me by A3,A16;
hereby
per cases;
suppose A19: t.intpos md < t.intpos me;
take ME=0;
thus IExec(WH1,t).a7=ME by A2,A13,A15,A19;
thus IExec(WH1,t).a4=t.a4-1 by A13,A15,A19
.=m4+ME by A2,XCMPLX_1:26;
thus ME <= t.a5 by A2;
hereby
let i be Nat;
assume A20: m4+ME < i & i <=t.a4;
then m4+1 <= i by INT_1:20;
then i=m4+1 by A2,A20,AXIOMS:21;
hence IExec(WH1,t).intpos md < IExec(WH1,t).intpos i by A1,A16,
A18,A19;
end;
thus
ME=0 or IExec(WH1,t).intpos md >= IExec(WH1,t).intpos (m4+ME);
suppose A21: t.intpos md >= t.intpos me;
take ME=1;
thus IExec(WH1,t).a7=ME by A2,A13,A15,A21;
thus IExec(WH1,t).a4=m4+ME by A2,A13,A15,A21;
thus ME <= t.a5 by A2;
thus for i be Nat st m4+ME < i & i <=t.a4
holds IExec(WH1,t).intpos md < IExec(WH1,t).intpos i by A2;
thus ME=0 or IExec(WH1,t).intpos md >=
IExec(WH1,t).intpos (m4+ME) by A1,A16,A18,A21;
end;
end;
then A22: P[0];
A23: now
let k be Nat;
assume A24:P[k];
now
let t be State of SCMPDS;
set b=DataLoc(t.a,5);
assume A25: t.a=0 & t.a5 =(k+1)+1 & t.a4=m4+t.a5 & t.a2=md;
set me=m4+(k+1+1);
me>=m4 by NAT_1:29;
then A26: me>=8 by A1,AXIOMS:22;
A27: t.a5 >= 1 by A25,NAT_1:29;
then A28: t.a5 > 0 by AXIOMS:22;
A29: b=intpos (0+5) by A25,SCMP_GCD:5;
then A30: t.b > 0 by A27,AXIOMS:22;
A31: now let v be State of SCMPDS;
assume A32: v.a4 >= m4+v.b & v.a2=t.a2 & v.a=t.a & v.b > 0;
then A33: m4+v.b>m4+0 by REAL_1:53;
then A34: v.a4 >=m4 by A32,AXIOMS:22;
v.a4 > 0 by A1,A32,A33,AXIOMS:22;
then reconsider ME=v.a4 as Nat by INT_1:16;
A35: ME >= 8 by A1,A34,AXIOMS:22;
then A36: (v.intpos md < v.intpos ME implies IExec(WB1,v).a5=v.a5-1
&
IExec(WB1,v).a4=v.a4-1 & IExec(WB1,v).a7=v.a5-1) &
(v.intpos md >= v.intpos ME implies IExec(WB1,v).a5=0 &
IExec(WB1,v).a4=v.a4 & IExec(WB1,v).a7=v.a5)
by A1,A25,A29,A32,Lm8;
thus IExec(WB1,v).a=v.a by A1,A25,A29,A32,A35,Lm8;
thus WB1 is_closed_on v & WB1 is_halting_on v by SCMPDS_6:34,35;
hereby
per cases;
suppose A37:v.intpos md < v.intpos ME;
hence IExec(WB1,v).b < v.b by A29,A36,INT_1:26;
m4+v.b-1=m4+IExec(WB1,v).b by A29,A36,A37,XCMPLX_1:29;
hence IExec(WB1,v).a4 >= m4+IExec(WB1,v).b by A32,A36,A37,REAL_1:
49;
suppose A38:v.intpos md >= v.intpos ME;
hence IExec(WB1,v).b < v.b by A1,A25,A29,A32,A35,Lm8;
m4+IExec(WB1,v).b < m4+v.b by A29,A32,A36,A38,REAL_1:53;
hence IExec(WB1,v).a4 >= m4+IExec(WB1,v).b by A32,A36,A38,AXIOMS:
22;
end;
thus IExec(WB1,v).a2=v.a2 by A1,A25,A29,A32,A35,Lm8;
end;
set It=IExec(WB1,t);
A39: It.a=0 & It.a1=t.a1 & It.a2=t.a2 & It.a3=t.a3 &
(for i be Nat st i >= 8 holds It.intpos i=t.intpos i) &
(t.intpos md < t.intpos me implies It.a5=t.a5-1 &
It.a4=t.a4-1 & It.a7=t.a5-1) &
(t.intpos md >= t.intpos me implies It.a5=0 &
It.a4=t.a4 & It.a7=t.a5) by A1,A25,A26,A28,Lm8;
then A40: DataLoc(It.a,5)=intpos(0+5) by SCMP_GCD:5;
per cases;
suppose A41: t.intpos md < t.intpos me;
then A42: It.a5=k+1 by A25,A39,XCMPLX_1:26;
A43: It.a4=t.a4-1 by A1,A25,A26,A28,A41,Lm8;
A44: It.a4=m4+It.a5 by A25,A39,A41,XCMPLX_1:29;
A45: IExec(WH1,t)=IExec(WH1,It) by A25,A28,A29,A31,Lm7,Th5;
hence IExec(WH1,t).a=0 by A24,A25,A39,A42,A44;
thus IExec(WH1,t).a1=t.a1 by A24,A25,A39,A42,A44,A45;
thus IExec(WH1,t).a5=0 by A24,A25,A39,A42,A44,A45;
thus IExec(WH1,t).a2=t.a2 by A24,A25,A39,A42,A44,A45;
thus IExec(WH1,t).a3=t.a3 by A24,A25,A39,A42,A44,A45;
A46: now let i be Nat;
assume A47: i >= 8;
hence IExec(WH1,t).intpos i=It.intpos i by A24,A25,A39,A42,A44,A45
.=t.intpos i by A1,A25,A26,A28,A47,Lm8;
end;
hence for i be Nat st i >= 8 holds IExec(WH1,t).intpos i=t.intpos i;
consider mE be Nat such that
A48: mE=IExec(WH1,It).a7 & IExec(WH1,It).a4=m4+mE & mE <= It.a5 &
(for i be Nat st m4+mE < i & i <=It.a4 holds
IExec(WH1,It).intpos md < IExec(WH1,It).intpos i) &
(mE=0 or IExec(WH1,It).intpos md >= IExec(WH1,It).intpos (m4+mE))
by A24,A25,A39,A42,A44;
take mE;
thus mE=IExec(WH1,t).a7 by A25,A29,A30,A31,A48,Lm7,Th5;
thus IExec(WH1,t).a4=m4+mE by A25,A29,A30,A31,A48,Lm7,Th5;
It.a5 < t.a5 by A39,A41,INT_1:26;
hence mE <= t.a5 by A48,AXIOMS:22;
hereby
let i be Nat;
assume A49: m4+mE < i & i <=t.a4;
per cases;
suppose A50: i=t.a4;
IExec(WH1,t).intpos me =t.intpos me by A26,A46;
hence IExec(WH1,t).intpos md < IExec(WH1,t).intpos i by A1,A25,A41
,A46,A50;
suppose i<>t.a4;
then i < t.a4 by A49,REAL_1:def 5;
then i+1 <= t.a4 by INT_1:20;
then i <= It.a4 by A43,REAL_1:84;
hence IExec(WH1,t).intpos md < IExec(WH1,t).intpos i by A45,A48,
A49;
end;
thus mE=0 or
IExec(WH1,t).intpos md >= IExec(WH1,t).intpos (m4+mE) by A45,A48;
suppose A51: t.intpos md >= t.intpos me;
A52: now let x;
thus IExec(WH1,t).x =IExec(WH1,It).x by A25,A28,A29,A31,Lm7,Th5
.=It.x by A39,A40,A51,SCMPDS_8:23;
end;
hence IExec(WH1,t).a=0 by A39;
thus IExec(WH1,t).a1=t.a1 by A39,A52;
thus IExec(WH1,t).a5=0 by A39,A51,A52;
thus IExec(WH1,t).a2=t.a2 by A39,A52;
thus IExec(WH1,t).a3=t.a3 by A39,A52;
A53: now let i be Nat;
assume A54: i >= 8;
thus IExec(WH1,t).intpos i=It.intpos i by A52
.=t.intpos i by A1,A25,A26,A28,A54,Lm8;
end;
hence for i be Nat st i >= 8 holds IExec(WH1,t).intpos i=t.intpos i;
A55: IExec(WH1,t).intpos me=t.intpos me by A26,A53;
take ME=k+1+1;
thus IExec(WH1,t).a7=ME by A25,A39,A51,A52;
thus IExec(WH1,t).a4=m4+ME by A25,A39,A51,A52;
thus ME <= t.a5 by A25;
thus for i be Nat st m4+ME < i & i <=t.a4 &
not IExec(WH1,t).intpos md < IExec(WH1,t).intpos i
holds contradiction by A25;
thus ME=0 or IExec(WH1,t).intpos md >= IExec(WH1,t).intpos (m4+ME)
by A1,A51,A53,A55;
end;
hence P[k+1];
end;
A56: for k be Nat holds P[k] from Ind(A22,A23);
s.a5 >=1+0 by A1,INT_1:20;
then s.a5-1 >= 0 by SQUARE_1:12;
then reconsider m5=s.a5-1 as Nat by INT_1:16;
s.a5=m5+1 by XCMPLX_1:27;
hence thesis by A1,A56;
end;
Lm10:
for s being State of SCMPDS,m4,md be Nat st s.GBP=0 & s.a5 > 0
& s.a4=m4+s.a5 & m4>=8 & s.a2=md & md >= 8 holds
WH1 is_closed_on s & WH1 is_halting_on s
proof
let s be State of SCMPDS,m4,md be Nat;
assume A1: s.GBP=0 & s.a5 > 0 & s.a4=m4+s.a5 & m4>=8 &
s.a2=md & md >= 8;
set a=GBP;
set b=DataLoc(s.a,5);
A2: b=intpos (0+5) by A1,SCMP_GCD:5;
now let v be State of SCMPDS;
assume A3: v.a4 >= m4+v.b & v.a2=s.a2 & v.a=s.a & v.b > 0;
then A4: m4+v.b>m4+0 by REAL_1:53;
then A5: v.a4 >=m4 by A3,AXIOMS:22;
v.a4 > 0 by A1,A3,A4,AXIOMS:22;
then reconsider ME=v.a4 as Nat by INT_1:16;
A6: ME >= 8 by A1,A5,AXIOMS:22;
then A7: (v.intpos md < v.intpos ME implies IExec(WB1,v).a5=v.a5-1 &
IExec(WB1,v).a4=v.a4-1 & IExec(WB1,v).a7=v.a5-1) &
(v.intpos md >= v.intpos ME implies IExec(WB1,v).a5=0 &
IExec(WB1,v).a4=v.a4 & IExec(WB1,v).a7=v.a5)
by A1,A2,A3,Lm8;
thus IExec(WB1,v).a=v.a by A1,A2,A3,A6,Lm8;
thus WB1 is_closed_on v & WB1 is_halting_on v by SCMPDS_6:34,35;
hereby
per cases;
suppose A8: v.intpos md < v.intpos ME;
hence IExec(WB1,v).b < v.b by A2,A7,INT_1:26;
m4+v.b-1=m4+IExec(WB1,v).b by A2,A7,A8,XCMPLX_1:29;
hence IExec(WB1,v).a4 >= m4+IExec(WB1,v).b by A3,A7,A8,REAL_1:49
;
suppose A9:v.intpos md >= v.intpos ME;
hence IExec(WB1,v).b < v.b by A1,A2,A3,A6,Lm8;
m4+IExec(WB1,v).b < m4+v.b by A2,A3,A7,A9,REAL_1:53;
hence IExec(WB1,v).a4 >= m4+IExec(WB1,v).b by A3,A7,A9,AXIOMS:22
;
end;
thus IExec(WB1,v).a2=v.a2 by A1,A2,A3,A6,Lm8;
end;
hence thesis by A1,A2,Lm7,Th5;
end;
Lm11:
card WH1=11
proof
thus card WH1=9+2 by Lm7,SCMPDS_8:17
.=11;
end;
Lm12:
card WB2=9
proof
thus card WB2= card (j1 ';' j2 ';' j3 ';' j4) + card IF2 by SCMPDS_4:45
.= 4+card IF2 by Th4
.= 4+(card (j5 ';' j6) +card j7+2) by SCMPDS_6:79
.= 4+(2+card j7+2) by SCMP_GCD:9
.= 4+(2+1+2) by SCMPDS_5:6
.= 9;
end;
Lm13:
card WH2=11
proof
thus card WH2= 9+2 by Lm12,SCMPDS_8:17
.=11;
end;
Lm14:
for s being State of SCMPDS,md,me be Nat st s.a2=md & s.a3=me &
md >= 8 & me >= 8 & s.GBP=0 & s.a7 > 0 holds
IExec(WB2,s).GBP=0 & IExec(WB2,s).a1=s.a1 &
IExec(WB2,s).a2=s.a2 & IExec(WB2,s).a4=s.a4 &
(for i be Nat st i >= 8 holds IExec(WB2,s).intpos i=s.intpos i) &
(s.intpos md > s.intpos me implies IExec(WB2,s).a7=s.a7-1 &
IExec(WB2,s).a3=s.a3+1 & IExec(WB2,s).a5=s.a7-1) &
(s.intpos md <= s.intpos me implies IExec(WB2,s).a7=0 &
IExec(WB2,s).a3=s.a3 & IExec(WB2,s).a5=s.a7)
proof
let s be State of SCMPDS,md,me be Nat;
set a=GBP;
assume A1: s.a2=md & s.a3=me & md >= 8 & me >= 8 & s.a=0 & s.a7 > 0;
set t0=Initialized s,
t1=IExec(j1 ';' j2 ';' j3 ';' j4,s),
t2=IExec(j1 ';' j2 ';' j3,s),
t3=IExec(j1 ';' j2,s),
t4=Exec(j1, t0);
A2: t0.a=0 by A1,SCMPDS_5:40;
A3: t0.a1=s.a1 by SCMPDS_5:40;
A4: t0.a2=md by A1,SCMPDS_5:40;
A5: t0.a4=s.a4 by SCMPDS_5:40;
A6: t0.a3=me by A1,SCMPDS_5:40;
A7: t0.a7=s.a7 by SCMPDS_5:40;
A8: DataLoc(t0.a,5)=intpos (0+5) by A2,SCMP_GCD:5;
then a<>DataLoc(t0.a,5) by SCMP_GCD:4,def 2;
then A9: t4.a =0 by A2,SCMPDS_2:59;
a1<>DataLoc(t0.a,5) by A8,SCMP_GCD:4;
then A10: t4.a1 =s.a1 by A3,SCMPDS_2:59;
a2<>DataLoc(t0.a,5) by A8,SCMP_GCD:4;
then A11: t4.a2 =md by A4,SCMPDS_2:59;
a4<>DataLoc(t0.a,5) by A8,SCMP_GCD:4;
then A12: t4.a4 =s.a4 by A5,SCMPDS_2:59;
a3<>DataLoc(t0.a,5) by A8,SCMP_GCD:4;
then A13: t4.a3 =me by A6,SCMPDS_2:59;
a7<>DataLoc(t0.a,5) by A8,SCMP_GCD:4;
then A14: t4.a7 =s.a7 by A7,SCMPDS_2:59;
DataLoc(t0.a,7)=intpos (0+7) by A2,SCMP_GCD:5;
then A15: t4.a5 =s.a7 by A7,A8,SCMPDS_2:59;
A16: now let i be Nat;
assume i>=8;
then i > 5 by AXIOMS:22;
then intpos i <> DataLoc(t0.a,5) by A8,SCMP_GCD:4;
hence t4.intpos i=t0.intpos i by SCMPDS_2:59
.=s.intpos i by SCMPDS_5:40;
end;
A17: DataLoc(t4.a,7)=intpos (0+7) by A9,SCMP_GCD:5;
then A18: a<>DataLoc(t4.a,7) by SCMP_GCD:4,def 2;
A19: t3.a =Exec(j2, t4).a by SCMPDS_5:47
.=0 by A9,A18,SCMPDS_2:60;
A20: a1<>DataLoc(t4.a,7) by A17,SCMP_GCD:4;
A21: t3.a1 =Exec(j2, t4).a1 by SCMPDS_5:47
.=s.a1 by A10,A20,SCMPDS_2:60;
A22: a2<>DataLoc(t4.a,7) by A17,SCMP_GCD:4;
A23: t3.a2 =Exec(j2, t4).a2 by SCMPDS_5:47
.=md by A11,A22,SCMPDS_2:60;
A24: a4<>DataLoc(t4.a,7) by A17,SCMP_GCD:4;
A25: t3.a4 =Exec(j2, t4).a4 by SCMPDS_5:47
.=s.a4 by A12,A24,SCMPDS_2:60;
A26: a3<>DataLoc(t4.a,7) by A17,SCMP_GCD:4;
A27: t3.a3 =Exec(j2, t4).a3 by SCMPDS_5:47
.=me by A13,A26,SCMPDS_2:60;
A28: t3.a7 =Exec(j2, t4).a7 by SCMPDS_5:47
.=t4.a7+ -1 by A17,SCMPDS_2:60
.=s.a7-1 by A14,XCMPLX_0:def 8;
A29: a5<>DataLoc(t4.a,7) by A17,SCMP_GCD:4;
A30: t3.a5 =Exec(j2, t4).a5 by SCMPDS_5:47
.=s.a7 by A15,A29,SCMPDS_2:60;
A31: now let i be Nat;
assume A32:i>=8;
then i > 7 by AXIOMS:22;
then A33: intpos i <> DataLoc(t4.a,7) by A17,SCMP_GCD:4;
thus t3.intpos i =Exec(j2, t4).intpos i by SCMPDS_5:47
.=t4.intpos i by A33,SCMPDS_2:60
.=s.intpos i by A16,A32;
end;
A34: DataLoc(t3.a,6)=intpos (0+6) by A19,SCMP_GCD:5;
then A35: a<>DataLoc(t3.a,6) by SCMP_GCD:4,def 2;
A36: t2.a =Exec(j3, t3).a by SCMPDS_5:46
.=0 by A19,A35,SCMPDS_2:59;
A37: a1<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A38: t2.a1 =Exec(j3, t3).a1 by SCMPDS_5:46
.=s.a1 by A21,A37,SCMPDS_2:59;
A39: a2<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A40: t2.a2 =Exec(j3, t3).a2 by SCMPDS_5:46
.=md by A23,A39,SCMPDS_2:59;
A41: a4<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A42: t2.a4 =Exec(j3, t3).a4 by SCMPDS_5:46
.=s.a4 by A25,A41,SCMPDS_2:59;
A43: a3<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A44: t2.a3 =Exec(j3, t3).a3 by SCMPDS_5:46
.=me by A27,A43,SCMPDS_2:59;
A45: a7<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A46: t2.a7 =Exec(j3, t3).a7 by SCMPDS_5:46
.=s.a7-1 by A28,A45,SCMPDS_2:59;
A47: DataLoc(t3.a2,0)=intpos (md+0) by A23,SCMP_GCD:5;
A48: t2.a6 =Exec(j3, t3).a6 by SCMPDS_5:46
.=t3.intpos md by A34,A47,SCMPDS_2:59
.=s.intpos md by A1,A31;
A49: a5<>DataLoc(t3.a,6) by A34,SCMP_GCD:4;
A50: t2.a5 =Exec(j3, t3).a5 by SCMPDS_5:46
.=s.a7 by A30,A49,SCMPDS_2:59;
A51: now let i be Nat;
assume A52:i>=8;
then i > 6 by AXIOMS:22;
then A53: intpos i <> DataLoc(t3.a,6) by A34,SCMP_GCD:4;
thus t2.intpos i=Exec(j3, t3).intpos i by SCMPDS_5:46
.=t3.intpos i by A53,SCMPDS_2:59
.=s.intpos i by A31,A52;
end;
A54: DataLoc(t2.a,6)=intpos (0+6) by A36,SCMP_GCD:5;
then A55: a<>DataLoc(t2.a,6) by SCMP_GCD:4,def 2;
A56: t1.a =Exec(j4, t2).a by SCMPDS_5:46
.=0 by A36,A55,SCMPDS_2:62;
A57: a1<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A58: t1.a1 =Exec(j4, t2).a1 by SCMPDS_5:46
.=s.a1 by A38,A57,SCMPDS_2:62;
A59: a2<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A60: t1.a2 =Exec(j4, t2).a2 by SCMPDS_5:46
.=md by A40,A59,SCMPDS_2:62;
A61: a4<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A62: t1.a4 =Exec(j4, t2).a4 by SCMPDS_5:46
.=s.a4 by A42,A61,SCMPDS_2:62;
A63: a3<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A64: t1.a3 =Exec(j4, t2).a3 by SCMPDS_5:46
.=me by A44,A63,SCMPDS_2:62;
A65: a7<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A66: t1.a7 =Exec(j4, t2).a7 by SCMPDS_5:46
.=s.a7-1 by A46,A65,SCMPDS_2:62;
A67: t1.a6 =Exec(j4, t2).a6 by SCMPDS_5:46
.=t2.a6-t2.DataLoc(t2.a3,0) by A54,SCMPDS_2:62
.=t2.a6-t2.intpos(me+0) by A44,SCMP_GCD:5
.=s.intpos md - s.intpos me by A1,A48,A51;
A68: a5<>DataLoc(t2.a,6) by A54,SCMP_GCD:4;
A69: t1.a5 =Exec(j4, t2).a5 by SCMPDS_5:46
.=s.a7 by A50,A68,SCMPDS_2:62;
A70: now let i be Nat;
assume A71:i>=8;
then i > 6 by AXIOMS:22;
then A72: intpos i <> DataLoc(t2.a,6) by A54,SCMP_GCD:4;
thus t1.intpos i=Exec(j4, t2).intpos i by SCMPDS_5:46
.=t2.intpos i by A72,SCMPDS_2:62
.=s.intpos i by A51,A71;
end;
set t01=Initialized t1,
jj7= (GBP,7):=0,
t5=Exec(j5,t01);
A73: t01.a=0 by A56,SCMPDS_5:40;
A74: t01.a1=s.a1 by A58,SCMPDS_5:40;
A75: t01.a2=s.a2 by A1,A60,SCMPDS_5:40;
A76: t01.a4=s.a4 by A62,SCMPDS_5:40;
A77: t01.a5=s.a7 by A69,SCMPDS_5:40;
A78: DataLoc(t01.a,7)=intpos(0+7) by A73,SCMP_GCD:5;
A79: DataLoc(t01.a,3)=intpos(0+3) by A73,SCMP_GCD:5;
then a<>DataLoc(t01.a,3) by SCMP_GCD:4,def 2;
then A80: t5.a=0 by A73,SCMPDS_2:60;
a1<>DataLoc(t01.a,3) by A79,SCMP_GCD:4;
then A81: t5.a1=s.a1 by A74,SCMPDS_2:60;
a2<>DataLoc(t01.a,3) by A79,SCMP_GCD:4;
then A82: t5.a2=s.a2 by A75,SCMPDS_2:60;
a4<>DataLoc(t01.a,3) by A79,SCMP_GCD:4;
then A83: t5.a4=s.a4 by A76,SCMPDS_2:60;
A84: DataLoc(t5.a,5)=intpos(0+5) by A80,SCMP_GCD:5;
A85: now
per cases;
suppose A86: t1.DataLoc(t1.a,6) <= 0;
A87: a<>DataLoc(t01.a,7) by A78,SCMP_GCD:4,def 2;
thus IExec(IF2,t1).a=IExec(j7,t1).a by A86,SCMPDS_6:88
.=Exec(jj7,t01).a by SCMPDS_5:45
.=0 by A73,A87,SCMPDS_2:58;
A88: a1<>DataLoc(t01.a,7) by A78,SCMP_GCD:4;
thus IExec(IF2,t1).a1=IExec(j7,t1).a1 by A86,SCMPDS_6:88
.=Exec(jj7,t01).a1 by SCMPDS_5:45
.=s.a1 by A74,A88,SCMPDS_2:58;
A89: a2<>DataLoc(t01.a,7) by A78,SCMP_GCD:4;
thus IExec(IF2,t1).a2=IExec(j7,t1).a2 by A86,SCMPDS_6:88
.=Exec(jj7,t01).a2 by SCMPDS_5:45
.=s.a2 by A75,A89,SCMPDS_2:58;
A90: a4<>DataLoc(t01.a,7) by A78,SCMP_GCD:4;
thus IExec(IF2,t1).a4=IExec(j7,t1).a4 by A86,SCMPDS_6:88
.=Exec(jj7,t01).a4 by SCMPDS_5:45
.=s.a4 by A76,A90,SCMPDS_2:58;
hereby let i be Nat;
assume A91:i>=8;
then i > 7 by AXIOMS:22;
then A92: intpos i <> DataLoc(t01.a,7) by A78,SCMP_GCD:4;
thus IExec(WB2,s).intpos i=IExec(IF2,t1).intpos i by SCMPDS_5:39
.=IExec(j7,t1).intpos i by A86,SCMPDS_6:88
.=Exec(jj7,t01).intpos i by SCMPDS_5:45
.=t01.intpos i by A92,SCMPDS_2:58
.=t1.intpos i by SCMPDS_5:40
.=s.intpos i by A70,A91;
end;
suppose A93: t1.DataLoc(t1.a,6) > 0;
A94: a<>DataLoc(t5.a,5) by A84,SCMP_GCD:4,def 2;
thus IExec(IF2,t1).a=IExec(j5 ';' j6,t1).a by A93,SCMPDS_6:87
.=Exec(j6,t5).a by SCMPDS_5:47
.=0 by A80,A94,SCMPDS_2:60;
A95: a1<>DataLoc(t5.a,5) by A84,SCMP_GCD:4;
thus IExec(IF2,t1).a1=IExec(j5 ';' j6,t1).a1 by A93,SCMPDS_6:87
.=Exec(j6,t5).a1 by SCMPDS_5:47
.=s.a1 by A81,A95,SCMPDS_2:60;
A96: a2<>DataLoc(t5.a,5) by A84,SCMP_GCD:4;
thus IExec(IF2,t1).a2=IExec(j5 ';' j6,t1).a2 by A93,SCMPDS_6:87
.=Exec(j6,t5).a2 by SCMPDS_5:47
.=s.a2 by A82,A96,SCMPDS_2:60;
A97: a4<>DataLoc(t5.a,5) by A84,SCMP_GCD:4;
thus IExec(IF2,t1).a4=IExec(j5 ';' j6,t1).a4 by A93,SCMPDS_6:87
.=Exec(j6,t5).a4 by SCMPDS_5:47
.=s.a4 by A83,A97,SCMPDS_2:60;
hereby let i be Nat;
assume A98:i>=8;
then i > 5 by AXIOMS:22;
then A99: intpos i <> DataLoc(t5.a,5) by A84,SCMP_GCD:4;
i > 3 by A98,AXIOMS:22;
then A100: intpos i<>DataLoc(t01.a,3) by A79,SCMP_GCD:4;
thus IExec(WB2,s).intpos i=IExec(IF2,t1).intpos i by SCMPDS_5:39
.=IExec(j5 ';' j6,t1).intpos i by A93,SCMPDS_6:87
.=Exec(j6,t5).intpos i by SCMPDS_5:47
.=t5.intpos i by A99,SCMPDS_2:60
.=t01.intpos i by A100,SCMPDS_2:60
.=t1.intpos i by SCMPDS_5:40
.=s.intpos i by A70,A98;
end;
end;
hence IExec(WB2,s).a=0 & IExec(WB2,s).a1=s.a1 &
IExec(WB2,s).a2=s.a2 & IExec(WB2,s).a4=s.a4 by SCMPDS_5:39;
thus for i be Nat st i >= 8 holds IExec(WB2,s).intpos i=s.intpos i by A85;
A101: t1.DataLoc(t1.a,6)=t1.intpos (0+6) by A56,SCMP_GCD:5
.=s.intpos md - s.intpos me by A67;
A102: t01.a3=s.a3 by A1,A64,SCMPDS_5:40;
A103: t01.a7=s.a7-1 by A66,SCMPDS_5:40;
hereby
assume s.intpos md > s.intpos me;
then A104: t1.DataLoc(t1.a,6) > 0 by A101,SQUARE_1:11;
A105: a7<>DataLoc(t01.a,3) by A79,SCMP_GCD:4;
A106: a7<>DataLoc(t5.a,5) by A84,SCMP_GCD:4;
thus IExec(WB2,s).a7=IExec(IF2,t1).a7 by SCMPDS_5:39
.=IExec(j5 ';' j6,t1).a7 by A104,SCMPDS_6:87
.=Exec(j6,t5).a7 by SCMPDS_5:47
.=t5.a7 by A106,SCMPDS_2:60
.=s.a7-1 by A103,A105,SCMPDS_2:60;
A107: a3<>DataLoc(t5.a,5) by A84,SCMP_GCD:4;
thus IExec(WB2,s).a3=IExec(IF2,t1).a3 by SCMPDS_5:39
.=IExec(j5 ';' j6,t1).a3 by A104,SCMPDS_6:87
.=Exec(j6,t5).a3 by SCMPDS_5:47
.=t5.a3 by A107,SCMPDS_2:60
.=s.a3+1 by A79,A102,SCMPDS_2:60;
A108: a5<>DataLoc(t01.a,3) by A79,SCMP_GCD:4;
thus IExec(WB2,s).a5=IExec(IF2,t1).a5 by SCMPDS_5:39
.=IExec(j5 ';' j6,t1).a5 by A104,SCMPDS_6:87
.=Exec(j6,t5).a5 by SCMPDS_5:47
.=t5.a5+ -1 by A84,SCMPDS_2:60
.=t5.a5-1 by XCMPLX_0:def 8
.=s.a7-1 by A77,A108,SCMPDS_2:60;
end;
hereby
assume s.intpos md <= s.intpos me;
then A109: t1.DataLoc(t1.a,6) <= 0 by A101,REAL_2:106;
thus IExec(WB2,s).a7=IExec(IF2,t1).a7 by SCMPDS_5:39
.=IExec(j7,t1).a7 by A109,SCMPDS_6:88
.=Exec(jj7,t01).a7 by SCMPDS_5:45
.=0 by A78,SCMPDS_2:58;
A110: a3<>DataLoc(t01.a,7) by A78,SCMP_GCD:4;
thus IExec(WB2,s).a3=IExec(IF2,t1).a3 by SCMPDS_5:39
.=IExec(j7,t1).a3 by A109,SCMPDS_6:88
.=Exec(jj7,t01).a3 by SCMPDS_5:45
.=s.a3 by A102,A110,SCMPDS_2:58;
A111: a5<>DataLoc(t01.a,7) by A78,SCMP_GCD:4;
thus IExec(WB2,s).a5=IExec(IF2,t1).a5 by SCMPDS_5:39
.=IExec(j7,t1).a5 by A109,SCMPDS_6:88
.=Exec(jj7,t01).a5 by SCMPDS_5:45
.=s.a7 by A77,A111,SCMPDS_2:58;
end;
end;
Lm15:
for s being State of SCMPDS,m3,md be Nat st s.GBP=0 & s.a7 > 0
& s.a3+s.a7=m3 & s.a3>=8 & s.a2=md & md >= 8 holds IExec(WH2,s).GBP=0 &
IExec(WH2,s).a1=s.a1 & IExec(WH2,s).a7=0 &
IExec(WH2,s).a2=s.a2 & IExec(WH2,s).a4=s.a4 &
(for i be Nat st i >= 8 holds IExec(WH2,s).intpos i=s.intpos i) &
ex m5,mE3 be Nat st m5=IExec(WH2,s).a5 & IExec(WH2,s).a3=mE3 &
mE3+m5=m3 & m5 <= s.a7 & (for i be Nat st s.a3 <= i & i < mE3 holds
IExec(WH2,s).intpos md > IExec(WH2,s).intpos i) &
(m5 = 0 or IExec(WH2,s).intpos md <= IExec(WH2,s).intpos mE3)
proof
let s be State of SCMPDS,m3,md be Nat;
set a=GBP;
assume A1: s.a=0 & s.a7 > 0 & s.a3+s.a7=m3 & s.a3>=8 & s.a2=md
& md >= 8;
defpred P[Nat] means
for t being State of SCMPDS st t.a=0 & t.a7 =$1+1 & t.a3+t.a7=m3 &
t.a3>=8 & t.a2=md holds IExec(WH2,t).a=0 & IExec(WH2,t).a1=t.a1 &
IExec(WH2,t).a7=0 & IExec(WH2,t).a2=t.a2 & IExec(WH2,t).a4=t.a4 &
(for i be Nat st i >= 8 holds IExec(WH2,t).intpos i=t.intpos i) &
ex m5,mE3 be Nat st m5=IExec(WH2,t).a5 & IExec(WH2,t).a3=mE3 &
mE3+m5=m3 & m5 <= t.a7 & (for i be Nat st t.a3 <= i & i < mE3 holds
IExec(WH2,t).intpos md > IExec(WH2,t).intpos i) &
(m5=0 or IExec(WH2,t).intpos md <= IExec(WH2,t).intpos mE3);
now
let t be State of SCMPDS;
set b=DataLoc(t.a,7);
assume A2: t.a=0 & t.a7 =0+1 & t.a3+t.a7=m3 & t.a3>=8 & t.a2=md;
then t.a3 >= 0 by AXIOMS:22;
then reconsider me=t.a3 as Nat by INT_1:16;
A3: me=t.a3;
A4: b=intpos (0+7) by A2,SCMP_GCD:5;
A5: now let v be State of SCMPDS;
assume A6: v.a3 >= 8 & v.a2=t.a2 & v.a=t.a & v.b > 0;
then v.a3 > 0 by AXIOMS:22;
then reconsider ME=v.a3 as Nat by INT_1:16;
A7: ME=v.a3;
A8: (v.intpos md > v.intpos ME implies IExec(WB2,v).a7=v.a7-1 &
IExec(WB2,v).a3=v.a3+1 & IExec(WB2,v).a5=v.a7-1) &
(v.intpos md <= v.intpos ME implies IExec(WB2,v).a7=0 &
IExec(WB2,v).a3=v.a3 & IExec(WB2,v).a5=v.a7)
by A1,A2,A4,A6,Lm14;
thus IExec(WB2,v).a=v.a by A1,A2,A4,A6,A7,Lm14;
thus WB2 is_closed_on v & WB2 is_halting_on v by SCMPDS_6:34,35;
hereby
per cases;
suppose A9: v.intpos md > v.intpos ME;
hence IExec(WB2,v).b < v.b by A4,A8,INT_1:26;
A10: IExec(WB2,v).a3=v.a3+1 by A1,A2,A4,A6,A9,Lm14;
v.a3 +1 > v.a3 by REAL_1:69;
hence IExec(WB2,v).a3 >= 8 by A6,A10,AXIOMS:22;
suppose A11:v.intpos md <= v.intpos ME;
hence IExec(WB2,v).b < v.b by A1,A2,A4,A6,Lm14;
thus IExec(WB2,v).a3 >= 8 by A1,A2,A4,A6,A11,Lm14;
end;
thus IExec(WB2,v).a2=v.a2 by A1,A2,A4,A6,A7,Lm14;
end;
set It=IExec(WB2,t);
A12: It.a=0 & It.a1=t.a1 & It.a2=t.a2 & It.a4=t.a4 &
(for i be Nat st i >= 8 holds It.intpos i=t.intpos i) &
(t.intpos md > t.intpos me implies It.a7=t.a7-1 &
It.a3=t.a3+1 & It.a5=t.a7-1) &
(t.intpos md <= t.intpos me implies It.a7=0 &
It.a3=t.a3 & It.a5=t.a7) by A1,A2,A3,Lm14;
then A13: It.DataLoc(It.a,7)=It.intpos(0+7) by SCMP_GCD:5
.=0 by A2,A12;
A14: now let x;
thus IExec(WH2,t).x =IExec(WH2,It).x by A2,A4,A5,Lm12,Th6
.=It.x by A13,SCMPDS_8:23;
end;
hence IExec(WH2,t).a=0 by A12;
thus IExec(WH2,t).a1=t.a1 by A12,A14;
thus IExec(WH2,t).a7=0 by A2,A12,A14;
thus IExec(WH2,t).a2=t.a2 by A12,A14;
thus IExec(WH2,t).a4=t.a4 by A12,A14;
A15: now let i be Nat;
assume A16: i >= 8;
thus IExec(WH2,t).intpos i=It.intpos i by A14
.=t.intpos i by A1,A2,A3,A16,Lm14;
end;
hence for i be Nat st i >= 8 holds IExec(WH2,t).intpos i=t.intpos i;
A17: IExec(WH2,t).intpos me=t.intpos me by A2,A15;
hereby
per cases;
suppose A18: t.intpos md > t.intpos me;
take m5=0;
take mE3=m3;
thus IExec(WH2,t).a5=m5 by A2,A12,A14,A18;
thus IExec(WH2,t).a3 =mE3 by A2,A12,A14,A18;
thus mE3+m5=m3;
thus m5 <= t.a7 by A2;
hereby
let i be Nat;
assume A19: t.a3 <= i & i < mE3;
then i <= me by A2,NAT_1:38;
then i=t.a3 by A19,AXIOMS:21;
hence IExec(WH2,t).intpos md > IExec(WH2,t).intpos i by A1,A15,A17
,A18;
end;
thus
m5=0 or IExec(WH2,t).intpos md <= IExec(WH2,t).intpos mE3;
suppose A20: t.intpos md <= t.intpos me;
take m5=1;
take mE3=me;
thus IExec(WH2,t).a5=m5 by A2,A12,A14,A20;
thus IExec(WH2,t).a3=mE3 by A12,A14,A20;
thus mE3+m5=m3 by A2;
thus m5 <= t.a7 by A2;
thus for i be Nat st t.a3 <= i & i < mE3
holds IExec(WH2,t).intpos md > IExec(WH2,t).intpos i;
thus m5=0 or IExec(WH2,t).intpos md <= IExec(WH2,t).intpos mE3
by A1,A15,A17,A20;
end;
end;
then A21: P[0];
A22: now
let k be Nat;
assume A23:P[k];
now
let t be State of SCMPDS;
set b=DataLoc(t.a,7);
assume A24: t.a=0 & t.a7 =(k+1)+1 & t.a3+t.a7=m3 & t.a3>=8 & t.a2=md;
then t.a3 >= 0 by AXIOMS:22;
then reconsider me=t.a3 as Nat by INT_1:16;
A25: me=t.a3;
A26: b=intpos (0+7) by A24,SCMP_GCD:5;
A27: t.a7 >= 1 by A24,NAT_1:29;
then A28: t.a7 > 0 by AXIOMS:22;
A29: t.b > 0 by A26,A27,AXIOMS:22;
A30: now let v be State of SCMPDS;
assume A31: v.a3 >= 8 & v.a2=t.a2 & v.a=t.a & v.b > 0;
then v.a3 > 0 by AXIOMS:22;
then reconsider ME=v.a3 as Nat by INT_1:16;
A32: ME=v.a3;
A33: (v.intpos md > v.intpos ME implies IExec(WB2,v).a7=v.a7-1 &
IExec(WB2,v).a3=v.a3+1 & IExec(WB2,v).a5=v.a7-1) &
(v.intpos md <= v.intpos ME implies IExec(WB2,v).a7=0 &
IExec(WB2,v).a3=v.a3 & IExec(WB2,v).a5=v.a7)
by A1,A24,A26,A31,Lm14;
thus IExec(WB2,v).a=v.a by A1,A24,A26,A31,A32,Lm14;
thus WB2 is_closed_on v & WB2 is_halting_on v by SCMPDS_6:34,35;
hereby
per cases;
suppose A34: v.intpos md > v.intpos ME;
hence IExec(WB2,v).b < v.b by A26,A33,INT_1:26;
A35: IExec(WB2,v).a3=v.a3+1 by A1,A24,A26,A31,A34,Lm14;
v.a3 +1 > v.a3 by REAL_1:69;
hence IExec(WB2,v).a3 >= 8 by A31,A35,AXIOMS:22;
suppose A36:v.intpos md <= v.intpos ME;
hence IExec(WB2,v).b < v.b by A1,A24,A26,A31,Lm14;
thus IExec(WB2,v).a3 >= 8 by A1,A24,A26,A31,A36,Lm14;
end;
thus IExec(WB2,v).a2=v.a2 by A1,A24,A26,A31,A32,Lm14;
end;
set It=IExec(WB2,t);
A37: It.a=0 & It.a1=t.a1 & It.a2=t.a2 & It.a4=t.a4 &
(for i be Nat st i >= 8 holds It.intpos i=t.intpos i) &
(t.intpos md > t.intpos me implies It.a7=t.a7-1 &
It.a3=t.a3+1 & It.a5=t.a7-1) &
(t.intpos md <= t.intpos me implies It.a7=0 &
It.a3=t.a3 & It.a5=t.a7) by A1,A24,A25,A28,Lm14;
then A38: DataLoc(It.a,7)=intpos(0+7) by SCMP_GCD:5;
per cases;
suppose A39: t.intpos md > t.intpos me;
then A40: It.a7=k+1 by A24,A37,XCMPLX_1:26;
A41: It.a3=t.a3+1 by A1,A24,A28,A39,Lm14;
t.a3 < It.a3 by A37,A39,REAL_1:69;
then A42: It.a3 >= 8 by A24,AXIOMS:22;
A43: It.a3+It.a7=m3 by A24,A37,A40,XCMPLX_1:1;
A44: IExec(WH2,t)=IExec(WH2,It) by A24,A26,A28,A30,Lm12,Th6;
hence IExec(WH2,t).a=0 by A23,A24,A37,A40,A42,A43;
thus IExec(WH2,t).a1=t.a1 by A23,A24,A37,A40,A42,A43,A44;
thus IExec(WH2,t).a7=0 by A23,A24,A37,A40,A42,A43,A44;
thus IExec(WH2,t).a2=t.a2 by A23,A24,A37,A40,A42,A43,A44;
thus IExec(WH2,t).a4=t.a4 by A23,A24,A37,A40,A42,A43,A44;
A45: now let i be Nat;
assume A46: i >= 8;
hence IExec(WH2,t).intpos i=It.intpos i by A23,A24,A37,A40,A42,A43
,A44
.=t.intpos i by A1,A24,A25,A28,A46,Lm14;
end;
hence for i be Nat st i >= 8 holds IExec(WH2,t).intpos i=t.intpos i;
consider m5,mE3 be Nat such that
A47: m5=IExec(WH2,It).a5 & IExec(WH2,It).a3=mE3 & mE3+m5=m3 &
m5 <= It.a7 & (for i be Nat st It.a3 <= i & i < mE3 holds
IExec(WH2,It).intpos md > IExec(WH2,It).intpos i) &
(m5=0 or IExec(WH2,It).intpos md <= IExec(WH2,It).intpos mE3)
by A23,A24,A37,A40,A42,A43;
take m5;
take mE3;
thus m5=IExec(WH2,t).a5 by A24,A29,A30,A47,Lm12,Th6;
thus IExec(WH2,t).a3=mE3 by A24,A29,A30,A47,Lm12,Th6;
thus mE3+m5=m3 by A47;
It.a7 < t.a7 by A37,A39,INT_1:26;
hence m5 <= t.a7 by A47,AXIOMS:22;
hereby
let i be Nat;
assume A48: t.a3 <= i & i < mE3;
per cases;
suppose A49: i=t.a3;
IExec(WH2,t).intpos me =t.intpos me by A24,A45;
hence IExec(WH2,t).intpos md > IExec(WH2,t).intpos i by A1,A39,A45
,A49;
suppose i<>t.a3;
then t.a3 < i by A48,REAL_1:def 5;
then It.a3 <= i by A41,INT_1:20;
hence IExec(WH2,t).intpos md > IExec(WH2,t).intpos i by A44,A47,
A48;
end;
thus m5=0 or
IExec(WH2,t).intpos md <= IExec(WH2,t).intpos mE3 by A44,A47;
suppose A50: t.intpos md <= t.intpos me;
A51: now let x;
thus IExec(WH2,t).x =IExec(WH2,It).x by A24,A26,A28,A30,Lm12,Th6
.=It.x by A37,A38,A50,SCMPDS_8:23;
end;
hence IExec(WH2,t).a=0 by A37;
thus IExec(WH2,t).a1=t.a1 by A37,A51;
thus IExec(WH2,t).a7=0 by A37,A50,A51;
thus IExec(WH2,t).a2=t.a2 by A37,A51;
thus IExec(WH2,t).a4=t.a4 by A37,A51;
A52: now let i be Nat;
assume A53: i >= 8;
thus IExec(WH2,t).intpos i=It.intpos i by A51
.=t.intpos i by A1,A24,A25,A28,A53,Lm14;
end;
hence for i be Nat st i >= 8 holds IExec(WH2,t).intpos i=t.intpos i;
A54: IExec(WH2,t).intpos me=t.intpos me by A24,A52;
take m5=k+1+1;
take mE3=me;
thus IExec(WH2,t).a5=m5 by A24,A37,A50,A51;
thus IExec(WH2,t).a3=mE3 by A37,A50,A51;
thus mE3+m5=m3 by A24;
thus m5 <= t.a7 by A24;
thus for i be Nat st t.a3 <= i & i < mE3
holds IExec(WH2,t).intpos md > IExec(WH2,t).intpos i;
thus m5=0 or IExec(WH2,t).intpos md <= IExec(WH2,t).intpos mE3
by A1,A50,A52,A54;
end;
hence P[k+1];
end;
A55: for k be Nat holds P[k] from Ind(A21,A22);
s.a7 >=1+0 by A1,INT_1:20;
then s.a7-1 >= 0 by SQUARE_1:12;
then reconsider m7=s.a7-1 as Nat by INT_1:16;
s.a7=m7+1 by XCMPLX_1:27;
hence thesis by A1,A55;
end;
Lm16:
for s being State of SCMPDS,md be Nat st s.GBP=0 & s.a7 > 0 &
s.a3>=8 & s.a2=md & md >= 8 holds
WH2 is_closed_on s & WH2 is_halting_on s
proof
let s be State of SCMPDS,md be Nat;
set a=GBP;
set b=DataLoc(s.a,7);
assume A1: s.a=0 & s.a7 > 0 & s.a3>=8 & s.a2=md & md >= 8;
then A2: b=intpos (0+7) by SCMP_GCD:5;
now let v be State of SCMPDS;
assume A3: v.a3 >= 8 & v.a2=s.a2 & v.a=s.a & v.b > 0;
then v.a3 > 0 by AXIOMS:22;
then reconsider ME=v.a3 as Nat by INT_1:16;
A4: ME=v.a3;
A5: (v.intpos md > v.intpos ME implies IExec(WB2,v).a7=v.a7-1 &
IExec(WB2,v).a3=v.a3+1 & IExec(WB2,v).a5=v.a7-1) &
(v.intpos md <= v.intpos ME implies IExec(WB2,v).a7=0 &
IExec(WB2,v).a3=v.a3 & IExec(WB2,v).a5=v.a7)
by A1,A2,A3,Lm14;
thus IExec(WB2,v).a=v.a by A1,A2,A3,A4,Lm14;
thus WB2 is_closed_on v & WB2 is_halting_on v by SCMPDS_6:34,35;
hereby
per cases;
suppose A6: v.intpos md > v.intpos ME;
hence IExec(WB2,v).b < v.b by A2,A5,INT_1:26;
A7: IExec(WB2,v).a3=v.a3+1 by A1,A2,A3,A6,Lm14;
v.a3 +1 > v.a3 by REAL_1:69;
hence IExec(WB2,v).a3 >= 8 by A3,A7,AXIOMS:22;
suppose A8:v.intpos md <= v.intpos ME;
hence IExec(WB2,v).b < v.b by A1,A2,A3,Lm14;
thus IExec(WB2,v).a3 >= 8 by A1,A2,A3,A8,Lm14;
end;
thus IExec(WB2,v).a2=v.a2 by A1,A2,A3,A4,Lm14;
end;
hence thesis by A1,Lm12,Th6;
end;
Lm17:
card WB3=29
proof
thus card WB3=card (WH1 ';' WH2 )+card IF3 by SCMPDS_4:45
.=11+ 11+card IF3 by Lm11,Lm13,SCMPDS_4:45
.=22+(card (k5 ';' k6 ';' k7 ';' k8 ';' k9 ';' k0)+1) by SCMPDS_6:89
.=22+(card (k5 ';' k6 ';' k7 ';' k8 ';' k9)+1+1) by SCMP_GCD:8
.=22+(card (k5 ';' k6 ';' k7 ';' k8)+1+1+1) by SCMP_GCD:8
.=22+(card (k5 ';' k6 ';' k7)+1+1+1+1) by SCMP_GCD:8
.=22+(card (k5 ';' k6)+1+1+1+1+1) by SCMP_GCD:8
.=22+(2+1+1+1+1+1) by SCMP_GCD:9
.=29;
end;
Lm18:
card WH3=31
proof
thus card WH3=29+2 by Lm17,SCMPDS_8:17
.=31;
end;
begin :: The Basic Property of Partition Program
theorem Th12:
card Partition=38
proof
thus card Partition=card (K4 ';' WH3 ';' j8 ';' j9)+1 by Def1,SCMP_GCD:8
.=card (K4 ';' WH3 ';' j8)+1+1 by SCMP_GCD:8
.=card (K4 ';' WH3)+1+1+1 by SCMP_GCD:8
.=card K4+card WH3+1+1+1 by SCMPDS_4:45
.=4+31+1+1+1 by Lm18,Th4
.=38;
end;
Lm19:
for s be State of SCMPDS,m3,m4 be Nat st s.GBP=0 & s.a5 > 0 &
s.a3=m3 & s.a4=m4 & m3>6 & m4 > 6 holds
IExec(IF3,s).GBP=0 & IExec(IF3,s).a1=s.a1 & IExec(IF3,s).a2=s.a2 &
IExec(IF3,s).intpos m3=s.intpos m4 &
IExec(IF3,s).intpos m4=s.intpos m3 & IExec(IF3,s).a3=s.a3+1 &
IExec(IF3,s).a4=s.a4-1 & IExec(IF3,s).a5=s.a5-2 &
for i be Nat st i >= 8 & i <> m3 & i <> m4 holds
IExec(IF3,s).intpos i=s.intpos i
proof
let s be State of SCMPDS,m3,m4 be Nat;
set a=GBP;
assume A1: s.a=0 & s.a5 > 0 & s.a3=m3 & s.a4=m4 & m3 > 6 & m4 > 6;
then A2: DataLoc(s.a,5)=intpos(0+5) by SCMP_GCD:5;
set x=intpos m3,
y=intpos m4,
t0=Initialized s,
t1=IExec(k5 ';' k6 ';' k7 ';' k8 ';' k9 ';' k0,s),
t2=IExec(k5 ';' k6 ';' k7 ';' k8 ';' k9,s),
t3=IExec(k5 ';' k6 ';' k7 ';' k8,s),
t4=IExec(k5 ';' k6 ';' k7,s),
t5=IExec(k5 ';' k6,s),
t6=Exec(k5,t0);
A3: m4 > 0 by A1,AXIOMS:22;
A4: m3 > 0 by A1,AXIOMS:22;
A5: m4 > 3 by A1,AXIOMS:22;
A6: m4 > 5 by A1,AXIOMS:22;
A7: m3 > 5 by A1,AXIOMS:22;
A8: m3 > 3 by A1,AXIOMS:22;
A9: m3 > 4 by A1,AXIOMS:22;
A10: m4 > 4 by A1,AXIOMS:22;
A11: t0.a=0 by A1,SCMPDS_5:40;
A12: t0.a1=s.a1 by SCMPDS_5:40;
A13: t0.a2=s.a2 by SCMPDS_5:40;
A14: t0.a3=m3 by A1,SCMPDS_5:40;
A15: t0.a4=m4 by A1,SCMPDS_5:40;
A16: t0.a5=s.a5 by SCMPDS_5:40;
A17: t0.x=s.x by SCMPDS_5:40;
A18: DataLoc(t0.a,6)=intpos (0+6) by A11,SCMP_GCD:5;
then a<>DataLoc(t0.a,6) by SCMP_GCD:4,def 2;
then A19: t6.a =0 by A11,SCMPDS_2:59;
a1<>DataLoc(t0.a,6) by A18,SCMP_GCD:4;
then A20: t6.a1 =s.a1 by A12,SCMPDS_2:59;
a2<>DataLoc(t0.a,6) by A18,SCMP_GCD:4;
then A21: t6.a2 =s.a2 by A13,SCMPDS_2:59;
a3<>DataLoc(t0.a,6) by A18,SCMP_GCD:4;
then A22: t6.a3 =m3 by A14,SCMPDS_2:59;
a4<>DataLoc(t0.a,6) by A18,SCMP_GCD:4;
then A23: t6.a4 =m4 by A15,SCMPDS_2:59;
a5<>DataLoc(t0.a,6) by A18,SCMP_GCD:4;
then A24: t6.a5 =s.a5 by A16,SCMPDS_2:59;
A25: t6.a6 =t0.DataLoc(t0.a4,0) by A18,SCMPDS_2:59
.=t0.intpos(m4+0) by A15,SCMP_GCD:5
.=s.y by SCMPDS_5:40;
A26: x<>DataLoc(t0.a,6) by A1,A18,SCMP_GCD:4;
A27: now
let i be Nat;
assume i >= 8 & i <> m3 & i <> m4;
then i > 6 by AXIOMS:22;
then intpos i<>DataLoc(t0.a,6) by A18,SCMP_GCD:4;
hence t6.intpos i =t0.intpos i by SCMPDS_2:59
.=s.intpos i by SCMPDS_5:40;
end;
A28: DataLoc(t6.a4,0)=intpos (m4+0) by A23,SCMP_GCD:5;
then A29: a<>DataLoc(t6.a4,0) by A3,SCMP_GCD:4,def 2;
A30: t5.a =Exec(k6, t6).a by SCMPDS_5:47
.=0 by A19,A29,SCMPDS_2:59;
m4 > 1 by A1,AXIOMS:22;
then A31: a1<>DataLoc(t6.a4,0) by A28,SCMP_GCD:4;
A32: t5.a1 =Exec(k6, t6).a1 by SCMPDS_5:47
.=s.a1 by A20,A31,SCMPDS_2:59;
m4 > 2 by A1,AXIOMS:22;
then A33: a2<>DataLoc(t6.a4,0) by A28,SCMP_GCD:4;
A34: t5.a2 =Exec(k6, t6).a2 by SCMPDS_5:47
.=s.a2 by A21,A33,SCMPDS_2:59;
A35: a3<>DataLoc(t6.a4,0) by A5,A28,SCMP_GCD:4;
A36: t5.a3 =Exec(k6, t6).a3 by SCMPDS_5:47
.=m3 by A22,A35,SCMPDS_2:59;
A37: a4<>DataLoc(t6.a4,0) by A10,A28,SCMP_GCD:4;
A38: t5.a4 =Exec(k6, t6).a4 by SCMPDS_5:47
.=m4 by A23,A37,SCMPDS_2:59;
A39: a5<>DataLoc(t6.a4,0) by A6,A28,SCMP_GCD:4;
A40: t5.a5 =Exec(k6, t6).a5 by SCMPDS_5:47
.=s.a5 by A24,A39,SCMPDS_2:59;
A41: a6<>DataLoc(t6.a4,0) by A1,A28,SCMP_GCD:4;
A42: t5.a6 =Exec(k6, t6).a6 by SCMPDS_5:47
.=s.y by A25,A41,SCMPDS_2:59;
A43: t5.y=Exec(k6, t6).y by SCMPDS_5:47
.=t6.DataLoc(t6.a3,0) by A28,SCMPDS_2:59
.=t6.intpos(m3+0) by A22,SCMP_GCD:5
.=s.x by A17,A26,SCMPDS_2:59;
A44: now
let i be Nat;
assume A45: i >= 8 & i <> m3 & i <> m4;
then A46: intpos i <> DataLoc(t6.a4,0) by A28,SCMP_GCD:4;
thus t5.intpos i =Exec(k6, t6).intpos i by SCMPDS_5:47
.=t6.intpos i by A46,SCMPDS_2:59
.=s.intpos i by A27,A45;
end;
A47: DataLoc(t5.a3,0)=intpos (m3+0) by A36,SCMP_GCD:5;
then A48: a<>DataLoc(t5.a3,0) by A4,SCMP_GCD:4,def 2;
A49: t4.a =Exec(k7, t5).a by SCMPDS_5:46
.=0 by A30,A48,SCMPDS_2:59;
m3 > 1 by A1,AXIOMS:22;
then A50: a1<>DataLoc(t5.a3,0) by A47,SCMP_GCD:4;
A51: t4.a1 =Exec(k7, t5).a1 by SCMPDS_5:46
.=s.a1 by A32,A50,SCMPDS_2:59;
m3 > 2 by A1,AXIOMS:22;
then A52: a2<>DataLoc(t5.a3,0) by A47,SCMP_GCD:4;
A53: t4.a2 =Exec(k7, t5).a2 by SCMPDS_5:46
.=s.a2 by A34,A52,SCMPDS_2:59;
A54: a3<>DataLoc(t5.a3,0) by A8,A47,SCMP_GCD:4;
A55: t4.a3 =Exec(k7, t5).a3 by SCMPDS_5:46
.=m3 by A36,A54,SCMPDS_2:59;
A56: a4<>DataLoc(t5.a3,0) by A9,A47,SCMP_GCD:4;
A57: t4.a4 =Exec(k7, t5).a4 by SCMPDS_5:46
.=m4 by A38,A56,SCMPDS_2:59;
A58: a5<>DataLoc(t5.a3,0) by A7,A47,SCMP_GCD:4;
A59: t4.a5 =Exec(k7, t5).a5 by SCMPDS_5:46
.=s.a5 by A40,A58,SCMPDS_2:59;
A60: t5.DataLoc(t5.a,6)=t5.intpos(0+6) by A30,SCMP_GCD:5
.=s.y by A42;
A61: t4.x=Exec(k7, t5).x by SCMPDS_5:46
.=s.y by A47,A60,SCMPDS_2:59;
A62: now
per cases;
suppose A63: y<>DataLoc(t5.a3,0);
thus t4.y =Exec(k7, t5).y by SCMPDS_5:46
.=s.x by A43,A63,SCMPDS_2:59;
suppose A64: y=DataLoc(t5.a3,0);
thus t4.y =Exec(k7, t5).y by SCMPDS_5:46
.=s.x by A47,A60,A64,SCMPDS_2:59;
end;
A65: now
let i be Nat;
assume A66: i >= 8 & i <> m3 & i <> m4;
then A67: intpos i <> DataLoc(t5.a3,0) by A47,SCMP_GCD:4;
thus t4.intpos i =Exec(k7, t5).intpos i by SCMPDS_5:46
.=t5.intpos i by A67,SCMPDS_2:59
.=s.intpos i by A44,A66;
end;
A68: DataLoc(t4.a,5)=intpos (0+5) by A49,SCMP_GCD:5;
then A69: a<>DataLoc(t4.a,5) by SCMP_GCD:4,def 2;
A70: t3.a =Exec(k8, t4).a by SCMPDS_5:46
.=0 by A49,A69,SCMPDS_2:60;
A71: a1<>DataLoc(t4.a,5) by A68,SCMP_GCD:4;
A72: t3.a1 =Exec(k8, t4).a1 by SCMPDS_5:46
.=s.a1 by A51,A71,SCMPDS_2:60;
A73: a2<>DataLoc(t4.a,5) by A68,SCMP_GCD:4;
A74: t3.a2 =Exec(k8, t4).a2 by SCMPDS_5:46
.=s.a2 by A53,A73,SCMPDS_2:60;
A75: a3<>DataLoc(t4.a,5) by A68,SCMP_GCD:4;
A76: t3.a3 =Exec(k8, t4).a3 by SCMPDS_5:46
.=m3 by A55,A75,SCMPDS_2:60;
A77: a4<>DataLoc(t4.a,5) by A68,SCMP_GCD:4;
A78: t3.a4 =Exec(k8, t4).a4 by SCMPDS_5:46
.=m4 by A57,A77,SCMPDS_2:60;
A79: t3.a5 =Exec(k8, t4).a5 by SCMPDS_5:46
.=t4.a5+-2 by A68,SCMPDS_2:60
.=s.a5-2 by A59,XCMPLX_0:def 8;
A80: x<>DataLoc(t4.a,5) by A7,A68,SCMP_GCD:4;
A81: t3.x =Exec(k8, t4).x by SCMPDS_5:46
.=s.y by A61,A80,SCMPDS_2:60;
A82: y<>DataLoc(t4.a,5) by A6,A68,SCMP_GCD:4;
A83: t3.y =Exec(k8, t4).y by SCMPDS_5:46
.=s.x by A62,A82,SCMPDS_2:60;
A84: now
let i be Nat;
assume A85: i >= 8 & i <> m3 & i <> m4;
then i > 5 by AXIOMS:22;
then A86: intpos i <> DataLoc(t4.a,5) by A68,SCMP_GCD:4;
thus t3.intpos i =Exec(k8, t4).intpos i by SCMPDS_5:46
.=t4.intpos i by A86,SCMPDS_2:60
.=s.intpos i by A65,A85;
end;
A87: DataLoc(t3.a,3)=intpos (0+3) by A70,SCMP_GCD:5;
then A88: a<>DataLoc(t3.a,3) by SCMP_GCD:4,def 2;
A89: t2.a =Exec(k9, t3).a by SCMPDS_5:46
.=0 by A70,A88,SCMPDS_2:60;
A90: a2<>DataLoc(t3.a,3) by A87,SCMP_GCD:4;
A91: t2.a2 =Exec(k9, t3).a2 by SCMPDS_5:46
.=s.a2 by A74,A90,SCMPDS_2:60;
A92: a1<>DataLoc(t3.a,3) by A87,SCMP_GCD:4;
A93: t2.a1 =Exec(k9, t3).a1 by SCMPDS_5:46
.=s.a1 by A72,A92,SCMPDS_2:60;
A94: t2.a3 =Exec(k9, t3).a3 by SCMPDS_5:46
.=m3+1 by A76,A87,SCMPDS_2:60;
A95: a4<>DataLoc(t3.a,3) by A87,SCMP_GCD:4;
A96: t2.a4 =Exec(k9, t3).a4 by SCMPDS_5:46
.=m4 by A78,A95,SCMPDS_2:60;
A97: a5<>DataLoc(t3.a,3) by A87,SCMP_GCD:4;
A98: t2.a5 =Exec(k9, t3).a5 by SCMPDS_5:46
.=s.a5-2 by A79,A97,SCMPDS_2:60;
A99: x<>DataLoc(t3