:: Justifying the Correctness of Fibonacci Sequence and Euclid's
:: Algorithm by Loop Invariant
:: by JingChao Chen
::
:: Received June 14, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, AMI_1, SCMPDS_2, TURING_1, FUNCT_1, CARD_1,
SCMFSA_7, RELAT_1, ARYTM_3, CARD_3, FSM_1, XXREAL_0, COMPLEX1, ARYTM_1,
AMI_2, SCMPDS_5, SCMPDS_4, INT_1, SCMFSA6B, SCMFSA_9, UNIALG_2, SCMFSA7B,
SCMP_GCD, SEMI_AF1, GRAPHSP, AMI_3, FINSEQ_1, SCPISORT, NAT_1, ORDINAL4,
SFMASTR2, PRE_FF, FUNCT_4, CIRCUIT2, TARSKI, MSUALG_1, STRUCT_0,
VALUED_1, SCMFSA8B, INT_2, SCPINVAR, PARTFUN1, EXTPRO_1, SCMFSA6C,
COMPOS_1, MEMSTR_0;
notations XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
PARTFUN1, VALUED_1, XCMPLX_0, RECDEF_1, FUNCT_4, INT_1, INT_2, NAT_1,
STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, SCMPDS_2,
SCMPDS_4, SCMPDS_6, SCMP_GCD, SCMPDS_5, SCMPDS_8, FUNCT_2, CARD_3,
DOMAIN_1, FINSEQ_1, GR_CY_1, PRE_FF, SCPISORT, XXREAL_0;
constructors DOMAIN_1, REAL_1, NAT_D, RECDEF_1, PRE_FF, MESFUNC1, GR_CY_1,
SCM_1, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMP_GCD, SCMPDS_8, SCPISORT,
BINOP_2, AMI_2, MEMSTR_0, RELSET_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, CARD_3,
STRUCT_0, SCMPDS_2, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMPDS_8, FINSEQ_1,
CARD_1, VALUED_0, MEMSTR_0, COMPOS_1, AFINSQ_1, EXTPRO_1, FUNCT_4,
COMPOS_0;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions SCPISORT;
equalities FUNCOP_1, COMPOS_1, EXTPRO_1, AMI_3, SCMPDS_2, SCMP_GCD, MEMSTR_0;
expansions SCPISORT;
theorems AMI_3, NAT_1, TARSKI, FUNCT_4, INT_1, SCMPDS_2, ABSVALUE, GRFUNC_1,
SCMPDS_4, SCMPDS_5, SCMPDS_6, ENUMSET1, INT_2, SCMPDS_8, SCMP_GCD,
SCMPDS_7, FUNCT_1, FINSEQ_1, RVSUM_1, FINSEQ_2, MEMSTR_0, PRE_FF,
SCPISORT, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, PREPOWER, ORDINAL1,
FUNCOP_1, NAT_D, FINSEQ_3, PBOOLE, PARTFUN1, AFINSQ_1, COMPOS_1,
EXTPRO_1, CARD_3, XTUPLE_0;
schemes NAT_1, SCMPDS_8, FUNCT_2;
begin :: Preliminaries
reserve m,n for Element of NAT,
i,j for Instruction of SCMPDS,
I for Program
of SCMPDS,
a for Int_position;
theorem Th1:
(i ';' j ';' I). 0=i & (i ';' j ';' I). 1=j
proof
set jI=j ';' I;
A1: i ';' j ';' I =i ';' jI by SCMPDS_4:16
.=Load i ';' jI by SCMPDS_4:def 2;
0 in dom Load i by COMPOS_1:50;
hence (i ';' j ';' I). 0 =(Load i). 0 by A1,AFINSQ_1:def 3
.=i;
A2: 0 in dom Load j by COMPOS_1:50;
0 < card jI;
then
A3: card Load i=1 & 0 in dom jI by AFINSQ_1:66,COMPOS_1:54;
thus (i ';' j ';' I). 1 =(Load i ';' jI). (0+1) by A1
.=jI. 0 by A3,AFINSQ_1:def 3
.=(Load j ';' I). 0 by SCMPDS_4:def 2
.=(Load j). 0 by A2,AFINSQ_1:def 3
.=j;
end;
theorem Th2:
for a,b be Int_position holds
ex f be Function of product the_Values_of SCMPDS,NAT
st for s being State of SCMPDS holds (s.a = s.b
implies f.s =0) & (s.a <> s.b implies f.s=max(|.s.a.|,|.s.b.|))
proof
let a,b be Int_position;
defpred P[set,set] means ex t be State of SCMPDS st t=$1 & (t.a = t.b
implies $2 =0) & (t.a <> t.b implies $2=max(|.t.a.|,|.t.b.|));
A1: now
let s be Element of product the_Values_of SCMPDS;
per cases;
suppose
A2: s.a = s.b;
reconsider y=0 as Element of NAT;
take y;
thus P[s,y] by A2;
end;
suppose
A3: s.a <> s.b;
set mm=max(|.s.a.|,|.s.b.|);
reconsider y=mm as Element of NAT by XXREAL_0:16;
take y;
thus P[s,y] by A3;
end;
end;
consider f be Function of product the_Values_of SCMPDS, NAT such that
A4: for s be Element of product the_Values_of SCMPDS holds P[s,f.s]
from FUNCT_2:sch 3(A1);
A5: for s being State of SCMPDS holds P[s,f.s]
proof
let s be State of SCMPDS;
reconsider s as Element of product the_Values_of SCMPDS by CARD_3:107;
P[s,f.s] by A4;
hence thesis;
end;
take f;
hereby
let s be State of SCMPDS;
P[s,f.s] by A5;
hence
(s.a = s.b implies f.s =0) & (s.a <> s.b implies f.s=max(|.s.a.|,
|.s.b.|));
end;
end;
theorem Th3:
ex f be Function of product the_Values_of SCMPDS,NAT
st for s being State of SCMPDS holds (s.a >= 0 implies f.s =0) &
(s.a < 0 implies f.s= -s.a)
proof
defpred P[set,set] means ex t be State of SCMPDS st t=$1 & (t.a >= 0 implies
$2 =0) & (t.a < 0 implies $2=-t.a);
A1: now
let s be Element of product the_Values_of SCMPDS;
per cases;
suppose
A2: s.a >= 0;
reconsider y=0 as Element of NAT;
take y;
thus P[s,y] by A2;
end;
suppose
A3: s.a < 0;
then -s.a > 0 by XREAL_1:58;
then reconsider y=-s.a as Element of NAT by INT_1:3;
take y;
thus P[s,y] by A3;
end;
end;
consider f be Function of product the_Values_of SCMPDS,NAT such that
A4: for s be Element of product the_Values_of SCMPDS holds P[s,f.s]
from FUNCT_2:sch 3(A1);
A5: for s being State of SCMPDS holds P[s,f.s]
proof
let s be State of SCMPDS;
reconsider s as Element of product the_Values_of SCMPDS by CARD_3:107;
P[s,f.s] by A4;
hence thesis;
end;
take f;
hereby
let s be State of SCMPDS;
P[s,f.s] by A5;
hence (s.a >= 0 implies f.s =0) & (s.a < 0 implies f.s=-s.a);
end;
end;
set A = NAT, D = SCM-Data-Loc;
begin :: Computing directly the result of "while<0" program by loop-invariant
reserve Q,U,P for Instruction-Sequence of SCMPDS;
scheme
WhileLEnd { F(State of SCMPDS)-> Element of NAT,
s() -> 0-started State of SCMPDS,
P() -> Instruction-Sequence of SCMPDS,
I() -> halt-free shiftable Program of SCMPDS,
a() -> Int_position,i() -> Integer,
P[set]}: F(Initialize IExec(while<0(a(),i(),I()),P(),s()))=0
& P[Initialize IExec(while<0(a(),i(),I()),P(),s())]
provided
A1: for t be 0-started State of SCMPDS st P[t] holds F(t)=0
iff t.DataLoc(s().a(),i()) >= 0 and
A2: P[s()] and
A3: for t be 0-started State of SCMPDS,Q st P[t] & t.a()=s().a() &
t.DataLoc(s().a(),i()) < 0
holds IExec(I(),Q,t).a()=t.a() & I() is_closed_on t,Q & I()
is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))]
proof
set b=DataLoc(s().a(),i()), WHL=while<0(a(),i(),I());
defpred Q[Nat] means
for t be 0-started State of SCMPDS, Q st F(t) <= $1 & t.a()=s().a() & P[t]
holds F(Initialize IExec(WHL,Q,t))=0 & P[Initialize IExec(WHL,Q,t)];
A4: Q[0]
proof
let t be 0-started State of SCMPDS, Q;
A5: Initialize t = t by MEMSTR_0:44;
assume that
A6: F(t) <= 0 and
A7: t.a()=s().a() and
A8: P[t];
A9: F(t)=0 by A6;
then t.DataLoc(s().a(),i()) >= 0 by A1,A8;
then for b be Int_position
holds IExec(WHL,Q,t).b = t.b by A7,SCMPDS_8:12;
hence thesis by A8,A9,A5,SCPISORT:4;
end;
A10: now
let k be Nat;
assume
A11: Q[k];
now
let u be 0-started State of SCMPDS;
let U;
assume that
A12: F(u) <= k+1 and
A13: u.a()=s().a() and
A14: P[u];
per cases;
suppose
F(u)=0;
hence F(Initialize IExec(WHL,U,u))=0 &
P[Initialize IExec(WHL,U,u)]
by A4,A13,A14;
end;
suppose
A15: F(u) <> 0;
set Iu=IExec(I(),U,u);
A16: u.b < 0 by A1,A14,A15;
then
A17: Iu.a()=s().a() & P[Initialize Iu] by A3,A13,A14;
deffunc F(State of SCMPDS) = F($1);
A18: P[u] by A14;
A19: for t be 0-started State of SCMPDS st P[t] & F(t)=0
holds t.DataLoc(u.a(),i()) >= 0 by A1,A13;
F(Initialize Iu) < F(u) by A3,A13,A14,A16;
then F(Initialize Iu)+1 <= F(u) by INT_1:7;
then F(Initialize Iu)+1 <= k+1 by A12,XXREAL_0:2;
then
A20: F(Initialize Iu) <= k by XREAL_1:6;
A21: for t being 0-started State of SCMPDS,Q
st P[t] & t.a()=u.a() & t.DataLoc(u.a(),i()) < 0
holds IExec(I(),Q,t).a()=t.a() &
I() is_closed_on t,Q & I() is_halting_on t,Q &
F(Initialize IExec(I(),Q,t)) < F(t) & P[Initialize(IExec(I(),Q,t))]
by A3,A13;
A22: u.DataLoc(u.a(),i()) < 0 by A1,A13,A14,A15;
A23: IExec(WHL,U,u) = IExec(WHL,U,Initialize Iu)
from SCMPDS_8:sch 2 (A22,A19,A18,A21);
(Initialize Iu).a() = Iu.a() by SCMPDS_5:15;
hence F(Initialize IExec(WHL,U,u))=0 &
P[Initialize IExec(WHL,U,u)] by A11,A20,A17,A23;
end;
end;
hence Q[k+1];
end;
for k being Nat holds Q[k] from NAT_1:sch 2(A4,A10);
then Q[F(s())];
hence thesis by A2;
end;
set a1=intpos 1, a2=intpos 2, a3=intpos 3;
begin :: An Example : Summing directly n integers by loop-invariant
:: sum=Sum=x1+x2+...+xn
definition
let n, p0 be Element of NAT;
func sum(n,p0) -> Program of SCMPDS equals
(GBP:=0) ';' (intpos 1:=0) ';' (
intpos 2:=-n) ';' (intpos 3:=(p0+1)) ';' while<0(GBP,2,AddTo(GBP,1,intpos 3,0)
';' AddTo(GBP,2,1) ';' AddTo(GBP,3,1));
coherence;
end;
theorem Th4:
for s being 0-started State of SCMPDS,
I being halt-free shiftable Program
of SCMPDS, a,b,c being Int_position,n,i,p0 be Element of NAT,f be FinSequence
of INT st f is_FinSequence_on s,p0 & len f=n & s.b=0 & s.a=0 & s.
intpos i=-n & s.c = p0+1 &
(for t be 0-started State of SCMPDS, Q
st (ex g be FinSequence of
INT st g is_FinSequence_on s,p0 & len g=t.intpos i+n & t.b=Sum g & t.c = p0+1+
len g) & t.a=0 & t.intpos i < 0 & for i be Element of NAT st i > p0 holds t.
intpos i=s.intpos i holds IExec(I,Q,t).a=0 & I is_closed_on t,Q
& I is_halting_on t,Q
& IExec(I,Q,t).intpos i=t.intpos i+1 &
(ex g be FinSequence of INT st g
is_FinSequence_on s,p0 & len g=t.intpos i+n+1 &
IExec(I,Q,t).c = p0+1+len g &
IExec(I,Q,t).b=Sum g) & for i be Element of NAT st i > p0
holds IExec(I,Q,t).intpos
i=s.intpos i)
holds IExec(while<0(a,i,I),P,s).b=Sum f &
while<0(a,i,I) is_closed_on s,P & while<0(a,i,I) is_halting_on s,P
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, a,b,c
be Int_position,n,i,p0 be Element of NAT,f be FinSequence of INT;
set Iw=IExec(while<0(a,i,I),P,s), Dw=Initialize Iw;
set da=DataLoc(s.a,i);
defpred P[State of SCMPDS] means (for i be Element of NAT st i > p0 holds $1
.intpos i=s.intpos i) & (ex g be FinSequence of INT st g is_FinSequence_on s,p0
& len g=$1.intpos i+n & $1.b=Sum g & $1.intpos i <= 0 & $1.c = p0+1+len g);
assume that
A1: f is_FinSequence_on s,p0 and
A2: len f=n and
A3: s.b=0 and
A4: s.a=0 and
A5: s.intpos i=-n and
A6: s.c = p0+1;
consider ff be Function of product the_Values_of SCMPDS,NAT such that
A7: for t be State of SCMPDS holds (t.da >= 0 implies ff.t =0) & (t.da <
0 implies ff.t=-t.da) by Th3;
deffunc F(State of SCMPDS) = ff.$1;
assume
A8: for t be 0-started State of SCMPDS,Q
st (ex g be FinSequence of INT st g
is_FinSequence_on s,p0 & len g=t.intpos i+n & t.b=Sum g & t.c = p0+1+len g) & t
.a=0 & t.intpos i < 0 & for i be Element of NAT st i > p0 holds t.intpos i=s.
intpos i holds IExec(I,Q,t).a=0 & I is_closed_on t,Q
& I is_halting_on t,Q & IExec(I,Q,t).intpos i=t.intpos i+1
& (ex g be FinSequence of INT st g is_FinSequence_on s
,p0 & len g=t.intpos i+n+1 & IExec(I,Q,t).c = p0+1+len g
& IExec(I,Q,t).b=Sum g) &
for i be Element of NAT st i > p0
holds IExec(I,Q,t).intpos i=s.intpos i;
A9:
for t being 0-started State of SCMPDS st P[t] holds
(F(t) = 0 & t.da < 0 implies contradiction) &
(t.da >= 0 implies F(t)=0)
proof
let t be 0-started State of SCMPDS;
assume P[t];
hereby
assume
A10: F(t)=0;
assume
A11: t.da < 0;
then t.da < 0;
then F(t)=-t.da by A7;
hence contradiction by A10,A11;
end;
assume t.da >= 0;
then t.da >= 0;
hence F(t)=0 by A7;
end;
A12: now
let t be 0-started State of SCMPDS, Q;
assume that
A13: P[t] and
A14: t.a=s.a and
A15: t.DataLoc(s.a,i) < 0;
consider h be FinSequence of INT such that
A16: h is_FinSequence_on s,p0 and
A17: len h=t.intpos i+n & t.b=Sum h and
A18: t.c = p0+1+len h by A13;
A19: t.c = p0+1+len h by A18;
set It=IExec(I,Q,t);
set Dit=Initialize It;
A20: for i being Element of NAT st i > p0 holds t.intpos i = s.intpos i by A13;
A21: intpos (0+i)=da by A4,SCMP_GCD:1;
A22: len h=t.intpos i+n & t.b=Sum h by A17;
hence IExec(I,Q,t).a=t.a by A4,A8,A14,A15,A20,A16,A19,A21;
consider g be FinSequence of INT such that
A23: g is_FinSequence_on s,p0 and
A24: len g=t.intpos i+n+1 and
A25: IExec(I,Q,t).c = p0+1+len g and
A26: IExec(I,Q,t).b=Sum g by A4,A8,A14,A15,A20,A16,A22,A19,A21;
thus I is_closed_on t,Q & I is_halting_on t,Q
by A4,A8,A14,A15,A20,A16,A22,A19,A21;
A27: It.intpos i=t.intpos i+1 by A4,A8,A14,A15,A20,A16,A22,A19,A21;
hereby
per cases;
suppose
It.intpos i >= 0;
then Dit.da >= 0 by A21,SCMPDS_5:15;
then
A28: F(Dit)=0 by A7;
F(t) <> 0 by A9,A13,A15;
hence F(Dit) < F(t) by A28;
end;
suppose
A29: It.intpos i < 0;
t.da < 0 by A15;
then
A30: F(t)=-t.da by A7
.=-t.intpos i by A21;
Dit.da < 0 by A21,A29,SCMPDS_5:15;
then F(Dit)=-Dit.da by A7
.=-(t.intpos i+1) by A21,A27,SCMPDS_5:15
.=-t.intpos i-1;
hence F(Dit) < F(t) by A30,XREAL_1:146;
end;
end;
thus P[Initialize IExec(I,Q,t)]
proof
hereby
let i be Element of NAT;
assume
A31: i > p0;
thus Dit.intpos i=It.intpos i by SCMPDS_5:15
.=s.intpos i by A4,A8,A14,A15,A20,A16,A22,A19,A21,A31;
end;
take g;
thus g is_FinSequence_on s,p0 by A23;
thus len g=IExec(I,Q,t).intpos i+n by A27,A24
.=Dit.intpos i+n by SCMPDS_5:15;
thus Dit.b=Sum g by A26,SCMPDS_5:15;
Dit.intpos i=t.intpos i+1 by A27,SCMPDS_5:15;
hence Dit.intpos i <= 0 by A15,A21,INT_1:7;
thus thesis by A25,SCMPDS_5:15;
end;
end;
A32: P[s]
proof
thus for i be Element of NAT st i > p0 holds s.intpos i=s.intpos i;
consider h be FinSequence of INT such that
A33: len h=0 and
A34: h is_FinSequence_on s,p0 by SCPISORT:2;
take h;
thus h is_FinSequence_on s,p0 by A34;
thus len h=s.intpos i+n by A5,A33
.=s.intpos i+n;
h=<*> REAL by A33;
hence s.b=Sum h by A3,RVSUM_1:72;
thus s.intpos i <= 0 by A5;
thus thesis by A6,A33;
end;
A35: F(Dw)=0 & P[Dw] from WhileLEnd(A9,A32,A12);
then consider g be FinSequence of INT such that
A36: g is_FinSequence_on s,p0 and
A37: len g=Dw.intpos i+n and
A38: Dw.b=Sum g and
A39: Dw.intpos i <= 0;
A40: Dw.intpos i=Iw.intpos(0+i) by SCMPDS_5:15
.=Iw.da by A4,SCMP_GCD:1;
Iw.da = Dw.da by SCMPDS_5:15;
then Dw.intpos i >= 0 by A9,A35,A40;
then
A41: Dw.intpos i=0 by A39;
now
let i be Nat;
reconsider a = i as Element of NAT by ORDINAL1:def 12;
assume i in dom f;
then
A42: 1 <= i & i <= n by A2,FINSEQ_3:25;
hence f.i = s.intpos(p0+a) by A1,A2
.=g.i by A36,A37,A41,A42;
end;
then f = g by A2,A37,A41,FINSEQ_2:9;
hence Iw.b=Sum f by A38,SCMPDS_5:15;
A43: for t be 0-started State of SCMPDS st P[t] & F(t)=0
holds t.da >= 0 by A9;
while<0(a,i,I) is_closed_on s,P & while<0(a,i,I)
is_halting_on s,P from SCMPDS_8:sch 1(A43,A32,A12);
hence thesis;
end;
set j1= AddTo(GBP,1,a3,0), j2= AddTo(GBP,2,1), j3= AddTo(GBP,3,1), WB= j1 ';'
j2 ';' j3, WH= while<0(GBP,2,WB);
Lm1: for s being 0-started State of SCMPDS,
m be Element of NAT st s.GBP=0 & s.a3=m holds
IExec(WB,P,Initialize s).GBP=0 & IExec(WB,P,Initialize s).a1=s.a1+s.intpos m
& IExec(WB,P,Initialize s).a2=s.a2+1 &
IExec(WB,P,Initialize s).a3=m+1 & for i be Element of NAT st i >3
holds IExec(WB,P,Initialize s).intpos i =s.intpos i
proof
set a=GBP;
let s be 0-started State of SCMPDS,m be Element of NAT;
assume that
A1: s.a=0 and
A2: s.a3=m;
set t0=Initialize s, t1=IExec(WB,P,Initialize s),
t2=IExec(j1 ';' j2,P,Initialize s), t3=Exec(j1, t0);
A3: t0.a3=m by A2,SCMPDS_5:15;
A4: t0.a=0 by A1,SCMPDS_5:15;
then 0 <> |.t0.GBP+1.| by ABSVALUE:def 1;
then a <> DataLoc(t0.GBP,1) by XTUPLE_0:1;
then
A5: t3.a=0 by A4,SCMPDS_2:49;
then 0 <> |.t3.GBP+2.| by ABSVALUE:def 1;
then
A6: a <> DataLoc(t3.GBP,2) by XTUPLE_0:1;
3 <> |.t0.GBP+1.| by A4,ABSVALUE:def 1;
then a3 <> DataLoc(t0.GBP,1) by XTUPLE_0:1;
then
A7: t3.a3=m by A3,SCMPDS_2:49;
3 <> |.t3.GBP+2.| by A5,ABSVALUE:def 1;
then
A8: a3 <> DataLoc(t3.GBP,2) by XTUPLE_0:1;
A9: t2.a3=Exec(j2,t3).a3 by SCMPDS_5:42
.=m by A7,A8,SCMPDS_2:48;
A10: t0.a1=s.a1 by SCMPDS_5:15;
A11: DataLoc(t0.a,1)=intpos (0+1) by A4,SCMP_GCD:1;
then
A12: t3.a1=t0.a1+t0.DataLoc(t0.a3,0) by SCMPDS_2:49
.=t0.a1+t0.intpos(m+0) by A3,SCMP_GCD:1
.=s.a1+s.intpos m by A10,SCMPDS_5:15;
1 <> |.t3.GBP+2.| by A5,ABSVALUE:def 1;
then
A13: a1 <> DataLoc(t3.GBP,2) by XTUPLE_0:1;
A14: DataLoc(t3.a,2)=intpos (0+2) by A5,SCMP_GCD:1;
then
A15: |.t3.a+2.|=0+2 by XTUPLE_0:1;
2 <> |.t0.GBP+1.| by A4,ABSVALUE:def 1;
then a2 <> DataLoc(t0.GBP,1) by XTUPLE_0:1;
then
A16: t3.a2=t0.a2 by SCMPDS_2:49
.=s.a2 by SCMPDS_5:15;
A17: t2.a=Exec(j2,t3).a by SCMPDS_5:42
.=0 by A5,A6,SCMPDS_2:48;
then
A18: DataLoc(t2.a,3)=intpos (0+3) by SCMP_GCD:1;
A19: t2.a2=Exec(j2,t3).a2 by SCMPDS_5:42
.=s.a2+1 by A16,A14,SCMPDS_2:48;
A20: t2.a1=Exec(j2,t3).a1 by SCMPDS_5:42
.=s.a1+s.intpos m by A12,A13,SCMPDS_2:48;
0 <> |.t2.GBP+3.| by A17,ABSVALUE:def 1;
then
A21: a <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
thus t1.a=Exec(j3,t2).a by SCMPDS_5:41
.=0 by A17,A21,SCMPDS_2:48;
1 <> |.t2.GBP+3.| by A17,ABSVALUE:def 1;
then
A22: a1 <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
thus t1.a1=Exec(j3,t2).a1 by SCMPDS_5:41
.=s.a1+s.intpos m by A20,A22,SCMPDS_2:48;
2 <> |.t2.GBP+3.| by A17,ABSVALUE:def 1;
then
A23: a2 <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
thus t1.a2=Exec(j3,t2).a2 by SCMPDS_5:41
.=s.a2+1 by A19,A23,SCMPDS_2:48;
thus t1.a3=Exec(j3,t2).a3 by SCMPDS_5:41
.=m+1 by A9,A18,SCMPDS_2:48;
A24: |.t0.a+1.|=0+1 by A11,XTUPLE_0:1;
hereby
let i be Element of NAT;
assume
A25: i >3;
then
A26: intpos i <> DataLoc(t2.a,3) by A18,XTUPLE_0:1;
i <> |.t0.a+1.| by A24,A25;
then
A27: intpos i <> DataLoc(t0.a,1) by XTUPLE_0:1;
i <> |.t3.a+2.| by A15,A25;
then
A28: intpos i <> DataLoc(t3.a,2) by XTUPLE_0:1;
thus t1.intpos i=Exec(j3,t2).intpos i by SCMPDS_5:41
.=t2.intpos i by A26,SCMPDS_2:48
.=Exec(j2,t3).intpos i by SCMPDS_5:42
.=t3.intpos i by A28,SCMPDS_2:48
.=t0.intpos i by A27,SCMPDS_2:49
.=s.intpos i by SCMPDS_5:15;
end;
end;
Lm2: for s being 0-started State of SCMPDS,
n,p0 be Element of NAT,f be FinSequence of
INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f=n & s.a1=0 & s.GBP=0 & s.a2=-
n & s.a3=p0+1 holds IExec(WH,P,Initialize s).a1=Sum f
& WH is_closed_on s,P & WH is_halting_on s ,P
proof
let s be 0-started State of SCMPDS,
n,p0 be Element of NAT,f be FinSequence of INT;
set a=GBP;
A1: Initialize s = s by MEMSTR_0:44;
assume that
A2: p0 >= 3 and
A3: f is_FinSequence_on s,p0 & len f=n & s.a1=0 & s.a=0 & s.a2=-n & s.a3
= p0+1;
now
let t be 0-started State of SCMPDS;
let Q;
A4: Initialize t = t by MEMSTR_0:44;
given g be FinSequence of INT such that
A5: g is_FinSequence_on s,p0 and
A6: len g=t.a2+n and
A7: t.a1=Sum g and
A8: t.a3 = p0+1+len g;
assume that
A9: t.a=0 and
t.a2 < 0;
assume
A10: for i be Element of NAT st i > p0 holds t.intpos i=s.intpos i;
thus IExec(WB,Q,t).a=0 by A8,A9,Lm1,A4;
thus WB is_closed_on t,Q & WB is_halting_on t,Q by SCMPDS_6:20,21;
thus IExec(WB,Q,t).a2=t.a2+1 by A8,A9,Lm1,A4;
thus ex g be FinSequence of INT st g is_FinSequence_on s,p0 &
len g=t.a2+n+1 & IExec(WB,Q,t).a3 = p0+1+len g &
IExec(WB,Q,t).a1=Sum g
proof
consider h be FinSequence of INT such that
A11: len h=len g+1 and
A12: h is_FinSequence_on s,p0 by SCPISORT:2;
take h;
thus h is_FinSequence_on s,p0 by A12;
thus len h=t.a2+n+1 by A6,A11;
thus IExec(WB,Q,t).a3 =p0+1+len g+1 by A8,A9,Lm1,A4
.=p0+1+len h by A11;
A13: p0+1 > p0 by XREAL_1:29;
set m=len h;
A14: m >= 1 by A11,NAT_1:11;
then p0+m >= p0+1 by XREAL_1:6;
then
A15: p0+m > p0 by A13,XXREAL_0:2;
reconsider q = h.m as Element of INT by INT_1:def 2;
A16: now
let i be Nat;
assume that
A17: 1 <= i and
A18: i <= len h;
per cases;
suppose
i=len h;
hence h.i=(g^<*q*>).i by A11,FINSEQ_1:42;
end;
suppose
i<>len h;
then i < len h by A18,XXREAL_0:1;
then
A19: i <= len g by A11,INT_1:7;
then i in Seg (len g) by A17,FINSEQ_1:1;
then
A20: i in dom g by FINSEQ_1:def 3;
thus h.i = s.intpos(p0+i) by A12,A17,A18
.= g.i by A5,A17,A19
.= (g^<*q*>).i by A20,FINSEQ_1:def 7;
end;
end;
len (g^<*q*>)=len h by A11,FINSEQ_2:16;
then
A21: g^<*q*>=h by A16,FINSEQ_1:14;
h.m=s.intpos(p0+m) by A12,A14
.=t.intpos(p0+1+len g) by A10,A11,A15;
hence IExec(WB,Q,t).a1=t.a1+h.m by A8,A9,Lm1,A4
.=Sum h by A7,A21,RVSUM_1:74;
end;
hereby
let i be Element of NAT;
assume
A22: i > p0;
then i > 3 by A2,XXREAL_0:2;
hence IExec(WB,Q,t).intpos i=t.intpos i
by A8,A9,Lm1,A4
.=s.intpos i by A10,A22;
end;
end;
hence thesis by A3,Th4,A1;
end;
Lm3: for s being 0-started State of SCMPDS,
n,p0 be Element of NAT,f be FinSequence of
INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f=n
holds IExec(sum(n,p0),P,s).a1
=Sum f & sum(n,p0) is_halting_on s,P
proof
let s be 0-started State of SCMPDS,
n,p0 be Element of NAT,f be FinSequence of INT;
A1: Initialize s = s by MEMSTR_0:44;
assume that
A2: p0 >= 3 and
A3: f is_FinSequence_on s,p0 and
A4: len f=n;
set a=GBP, i1=a:=0, i2=a1:=0, i3=a2:=-n, i4=a3:=(p0+1), t0=Initialize s,
I4 =i1 ';' i2 ';' i3 ';' i4, t1=IExec(I4,P,Initialize s), Q1 = P,
t2=IExec(i1 ';' i2 ';' i3,P,Initialize s),
t3= IExec(i1 ';' i2,P,Initialize s), t4=Exec(i1, t0);
now
let i be Nat;
assume that
A5: 1 <= i and
A6: i <= len f;
A7: p0+1 >= 3+1 by A2,XREAL_1:6;
A8: p0+i >= p0+ 1 by A5,XREAL_1:6;
then p0+i <> 3 by A7,XXREAL_0:2;
then
A9: intpos (p0+i) <> a3 by XTUPLE_0:1;
p0+i <> 0 by A8;
then
A10: intpos (p0+i) <> a by XTUPLE_0:1;
p0+i <> 1 by A7,A8,XXREAL_0:2;
then
A11: intpos (p0+i) <> a1 by XTUPLE_0:1;
p0+i <> 2 by A7,A8,XXREAL_0:2;
then
A12: intpos (p0+i) <> a2 by XTUPLE_0:1;
thus t1.intpos (p0+i)=Exec(i4, t2).intpos (p0+i) by SCMPDS_5:41
.=t2.intpos (p0+i) by A9,SCMPDS_2:45
.=Exec(i3, t3).intpos (p0+i) by SCMPDS_5:41
.=t3.intpos (p0+i) by A12,SCMPDS_2:45
.=Exec(i2, t4).intpos (p0+i) by SCMPDS_5:42
.=t4.intpos (p0+i) by A11,SCMPDS_2:45
.=t0.intpos (p0+i) by A10,SCMPDS_2:45
.=s.intpos (p0+i) by SCMPDS_5:15
.=f.i by A3,A5,A6;
end;
then
A13: f is_FinSequence_on t1,p0;
A14: f is_FinSequence_on Initialize t1,p0
proof let i be Nat;
assume 1 <= i & i <= len f;
then f.i=t1.intpos(p0+i) by A13;
hence thesis by SCMPDS_5:15;
end;
A15: t4.a=0 by SCMPDS_2:45;
A16: t3.a=Exec(i2, t4).a by SCMPDS_5:42
.=0 by A15,AMI_3:10,SCMPDS_2:45;
A17: t2.a=Exec(i3, t3).a by SCMPDS_5:41
.=0 by A16,AMI_3:10,SCMPDS_2:45;
A18: t1.a3=Exec(i4, t2).a3 by SCMPDS_5:41
.=p0+1 by SCMPDS_2:45;
A19: (Initialize t1).a3 = t1.a3 by SCMPDS_5:15;
A20: t3.a1=Exec(i2, t4).a1 by SCMPDS_5:42
.=0 by SCMPDS_2:45;
A21: t2.a1=Exec(i3, t3).a1 by SCMPDS_5:41
.=0 by A20,AMI_3:10,SCMPDS_2:45;
A22: (Initialize t1).a1 = t1.a1 by SCMPDS_5:15;
A23: t1.a1=Exec(i4, t2).a1 by SCMPDS_5:41
.=0 by A21,AMI_3:10,SCMPDS_2:45;
A24: t2.a2=Exec(i3, t3).a2 by SCMPDS_5:41
.=-n by SCMPDS_2:45;
A25: (Initialize t1).a2 = t1.a2 by SCMPDS_5:15;
A26: (Initialize t1).a = t1.a by SCMPDS_5:15;
A27: t1.a2=Exec(i4, t2).a2 by SCMPDS_5:41
.=-n by A24,AMI_3:10,SCMPDS_2:45;
A28: t1.a=Exec(i4, t2).a by SCMPDS_5:41
.=0 by A17,AMI_3:10,SCMPDS_2:45;
then WH is_closed_on Initialize t1,Q1 & WH is_halting_on Initialize t1,Q1
by A2,A4,A23,A27,A18,Lm2,A14,A19,A22,A25,A26;
then
A29: WH is_closed_on t1,Q1 & WH is_halting_on t1,Q1 by SCMPDS_6:125,126;
IExec(WH,Q1,Initialize t1) = IExec(WH,Q1,Initialize Initialize t1);
then IExec(WH,Q1,Initialize t1).a1=Sum f
by A2,A4,A28,A23,A27,A18,Lm2,A14,A19,A22,A25,A26;
hence IExec(sum(n,p0),P,s).a1=Sum f by A29,A1,SCPISORT:7;
thus thesis by A29,SCPISORT:9;
end;
theorem
for s being 0-started State of SCMPDS,n,
p0 be Element of NAT, f be FinSequence
of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f=n
holds IExec(sum(n,p0),P,s).intpos 1=Sum f & sum(n,p0) is parahalting
proof
let s be 0-started State of SCMPDS,
n,p0 be Element of NAT,f be FinSequence of INT;
assume that
A1: p0 >= 3 and
A2: f is_FinSequence_on s,p0 & len f=n;
thus IExec(sum(n,p0),P,s).a1=Sum f by A1,A2,Lm3;
now
let t be State of SCMPDS, Q;
consider g being FinSequence of INT such that
A3: len g=n & g is_FinSequence_on t,p0 by SCPISORT:2;
g is_FinSequence_on Initialize t,p0
proof let i be Nat;
assume 1 <= i & i <= len g;
then g.i=t.intpos(p0+i) by A3;
hence thesis by SCMPDS_5:15;
end;
then sum(n,p0) is_halting_on Initialize t,Q by A1,Lm3,A3;
hence sum(n,p0) is_halting_on t,Q by SCMPDS_6:126;
end;
hence thesis by SCMPDS_6:21;
end;
begin :: Computing directly the result of "while>0" program by loop-invariant
scheme
WhileGEnd { F(State of SCMPDS)-> Element of NAT,
s() -> 0-started State of SCMPDS,
P() -> Instruction-Sequence of SCMPDS,
I() -> halt-free shiftable Program of SCMPDS,
a() -> Int_position,i() -> Integer, P[set]}:
F(Initialize IExec(while>0(a(),i(),I()),P(),s()))=0
& P[Initialize IExec(while>0(a(),i(),I()),P(),s())]
provided
A1: for t be 0-started State of SCMPDS st P[t]
holds F(t)=0 iff t.DataLoc(s().a(),i()) <= 0 and
A2: P[s()] and
A3: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=s().a() & t.DataLoc(
s().a(),i()) > 0 holds IExec(I(),Q,t).a()=t.a() &
I() is_closed_on t,Q & I()
is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))]
proof
set b=DataLoc(s().a(),i()), WHL=while>0(a(),i(),I());
defpred Q[Nat] means
for t be 0-started State of SCMPDS,Q st F(t) <=
$1 & t.a()=s().a() & P[t]
holds F(Initialize IExec(WHL,Q,t))=0 & P[Initialize IExec(WHL,Q,t)];
A4: Q[0]
proof
let t be 0-started State of SCMPDS, Q;
A5: Initialize t = t by MEMSTR_0:44;
assume that
A6: F(t) <= 0 and
A7: t.a()=s().a() and
A8: P[t];
A9: F(t)=0 by A6;
then t.DataLoc(s().a(),i()) <= 0 by A1,A8;
then for b be Int_position holds IExec(WHL,Q,t).b = t.b
by A7,SCMPDS_8:23;
hence thesis by A8,A9,A5,SCPISORT:4;
end;
A10: now
let k be Nat;
assume
A11: Q[k];
now
let u be 0-started State of SCMPDS;
let U;
assume that
A12: F(u) <= k+1 and
A13: u.a()=s().a() and
A14: P[u];
per cases;
suppose
F(u)=0;
hence F(Initialize IExec(WHL,U,u))=0 &
P[Initialize IExec(WHL,U,u)]
by A4,A13,A14;
end;
suppose
A15: F(u) <> 0;
set Iu=IExec(I(),U,u);
A16: u.b > 0 by A1,A14,A15;
then
A17: Iu.a()=s().a() & P[Initialize Iu] by A3,A13,A14;
deffunc F(State of SCMPDS) = F($1);
A18: P[u] by A14;
A19: for t be 0-started State of SCMPDS st P[t] & F(t)=0
holds t.DataLoc(u.a(),i()) <= 0 by A1,A13;
F(Initialize Iu) < F(u) by A3,A13,A14,A16;
then F(Initialize Iu)+1 <= F(u) by INT_1:7;
then F(Initialize Iu)+1 <= k+1 by A12,XXREAL_0:2;
then
A20: F(Initialize Iu) <= k by XREAL_1:6;
A21: for t being 0-started State of SCMPDS,Q st
P[t] & t.a()=u.a() & t.
DataLoc(u.a(),i()) > 0 holds IExec(I(),Q,t).a()=t.a()
& I() is_closed_on t,Q & I()
is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))
] by A3,A13;
A22: u.DataLoc(u.a(),i()) > 0 by A1,A13,A14,A15;
A23: IExec(WHL,U,u) = IExec(WHL,U,Initialize Iu) from SCMPDS_8:
sch 4 (A22,A19,A18,A21);
(Initialize Iu).a() = Iu.a() by SCMPDS_5:15;
hence F(Initialize IExec(WHL,U,u))=0 &
P[Initialize IExec(WHL,U,u)] by A11,A20,A17,A23;
end;
end;
hence Q[k+1];
end;
for k being Nat holds Q[k] from NAT_1:sch 2(A4,A10);
then Q[F(s())];
hence thesis by A2;
end;
begin :: An Example : Computing directly Fibonacci sequence by loop-invariant
definition
let n be Element of NAT;
func Fib-macro(n) -> Program of SCMPDS equals
(GBP:=0) ';' (intpos 1:=0) ';'
(intpos 2:=1) ';' (intpos 3:=n) ';' while>0(GBP,3,((GBP,4):=(GBP,2)) ';' AddTo(
GBP,2,GBP,1) ';' ((GBP,1):=(GBP,4)) ';' AddTo(GBP,3,-1));
coherence;
end;
theorem Th6:
for s being 0-started State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a,f0,f1 being Int_position,n,i be Element of NAT
st s.a=0 & s.f0=0 & s.f1=1 & s.intpos i=n &
(for t be 0-started State of SCMPDS,Q
for k be
Element of NAT st n=t.intpos i+k & t.f0=Fib k & t.f1 = Fib (k+1) & t.a=0 & t.
intpos i > 0 holds IExec(I,Q,t).a=0 & I is_closed_on t,Q
& I is_halting_on t,Q &
IExec(I,Q,t).intpos i=t.intpos i-1
& IExec(I,Q,t).f0=Fib (k+1) &
IExec(I,Q,t).f1 = Fib (k+1+1))
holds IExec(while>0(a,i,I),P,s).f0=Fib n
& IExec(while>0(a,i,I),P,s).
f1=Fib (n+1) & while>0(a,i,I) is_closed_on s,P
& while>0(a,i,I) is_halting_on s,P
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, a,f0,
f1 be Int_position,n,i be Element of NAT;
set Iw=IExec(while>0(a,i,I),P,s), Dw=Initialize Iw;
set da=DataLoc(s.a,i);
defpred P[State of SCMPDS] means $1.intpos i >= 0 & ex k be Element of NAT
st n=$1.intpos i+k & $1.f0=Fib k & $1.f1=Fib (k+1);
assume that
A1: s.a=0 and
A2: s.f0=0 and
A3: s.f1=1 and
A4: s.intpos i=n;
consider ff be Function of product the_Values_of SCMPDS,NAT such that
A5: for t be State of SCMPDS holds
(t.da <= 0 implies ff.t =0) & (t.da > 0 implies ff.t=t.da) by SCMPDS_8:5;
A6: for t be 0-started State of SCMPDS holds
(t.da <= 0 implies ff.t =0) & (t.da > 0 implies ff.t=t.da) by A5;
deffunc F(State of SCMPDS) = ff.$1;
A7: for t being 0-started State of SCMPDS st P[t] holds
not(F(t)=0 & t.da > 0) & (t.da <= 0 implies F(t)=0) by A6;
assume
A8: for t be 0-started State of SCMPDS,Q
for k be Element of NAT st n=t.intpos i+k & t.
f0=Fib k & t.f1 = Fib (k+1) & t.a=0 & t.intpos i > 0
holds IExec(I,Q,t).a=0 & I is_closed_on t,Q & I is_halting_on t,Q
& IExec(I,Q,t).intpos i=t.intpos i-1 & IExec(I,Q,t).f0=Fib (k+1)
& IExec(I,Q,t).f1 = Fib (k+1+1);
A9: now
let t be 0-started State of SCMPDS, Q;
assume that
A10: P[t] and
A11: t.a=s.a and
A12: t.DataLoc(s.a,i) > 0;
set It=IExec(I,Q,t);
set Dit=Initialize It;
consider k be Element of NAT such that
A13: n=t.intpos i+k and
A14: t.f0=Fib k and
A15: t.f1=Fib (k+1) by A10;
A16: t.f1=Fib (k+1) by A15;
A17: intpos (0+i)=da by A1,SCMP_GCD:1;
A18: n=t.intpos i+k & t.f0=Fib k by A13,A14;
hence IExec(I,Q,t).a=t.a by A1,A8,A11,A12,A16,A17;
thus I is_closed_on t,Q & I is_halting_on t,Q by A1,A8,A11,A12,A18,A16,A17;
A19: It.intpos i=t.intpos i-1 by A1,A8,A11,A12,A18,A16,A17;
hereby
per cases;
suppose
It.intpos i <= 0;
then Dit.da <= 0 by A17,SCMPDS_5:15;
then
A20: F(Dit)=0 by A6;
F(t) <> 0 by A7,A10,A12;
hence F(Dit) < F(t) by A20;
end;
suppose
A21: It.intpos i > 0;
t.da > 0 by A12;
then
A22: F(t)=t.da by A6
.=t.intpos i by A17;
Dit.da > 0 by A17,A21,SCMPDS_5:15;
then F(Dit)=Dit.da by A6
.=t.intpos i-1 by A17,A19,SCMPDS_5:15;
hence F(Dit) < F(t) by A22,XREAL_1:146;
end;
end;
thus P[Dit]
proof
t.intpos i >= 1+0 by A12,A17,INT_1:7;
then t.intpos i-1 >= 0 by XREAL_1:48;
hence Dit.intpos i >= 0 by A19,SCMPDS_5:15;
take m=k+1;
thus n=t.intpos i-1+1+k by A13
.=Dit.intpos i+1+k by A19,SCMPDS_5:15
.=Dit.intpos i+m;
It.f0=Fib m & It.f1=Fib (k+1+1) by A1,A8,A11,A12,A18,A16,A17;
hence thesis by SCMPDS_5:15;
end;
end;
A23: P[s]
proof
s.intpos i =n by A4;
hence s.intpos i >= 0;
take k=0;
thus n=s.intpos i+k by A4;
thus s.f0=Fib k by A2,PRE_FF:1;
thus thesis by A3,PRE_FF:1;
end;
A24: F(Dw)=0 & P[Dw] from WhileGEnd(A7,A23,A9);
A25: Dw.da = Iw.da by SCMPDS_5:15;
Dw.intpos i=Iw.intpos(0+i) by SCMPDS_5:15
.=Iw.da by A1,SCMP_GCD:1;
then Dw.intpos i <= 0 by A7,A24,A25;
then Dw.intpos i=0 by A24;
hence Iw.f0=Fib n & Iw.f1=Fib (n+1) by A24,SCMPDS_5:15;
A26: for t be 0-started State of SCMPDS st P[t] & F(t)=0
holds t.da <= 0 by A7;
while>0(a,i,I) is_closed_on s,P & while>0(a,i,I)
is_halting_on s,P from SCMPDS_8:sch 3(A26,A23,A9);
hence thesis;
end;
set j1= (GBP,4):=(GBP,2), j2= AddTo(GBP,2,GBP,1), j3= (GBP,1):=(GBP,4), j4=
AddTo(GBP,3,-1), WB= j1 ';' j2 ';' j3 ';' j4, WH= while>0(GBP,3,WB);
Lm4: for s being 0-started State of SCMPDS st s.GBP=0
holds IExec(WB,P,s).GBP=0 & IExec(WB,P
,s).a1=s.a2 & IExec(WB,P,s).a2=s.a1+s.a2 &
IExec(WB,P,s).a3=s.a3-1
proof
set a=GBP;
let s be 0-started State of SCMPDS;
set t0=s, t1=IExec(WB,P,s),
t2=IExec(j1 ';' j2 ';' j3,P,s),
Q0 = P,
t3=IExec(j1 ';' j2,P,s), t4=Exec(j1, t0), a4=intpos 4;
assume s.a=0;
then
A1: t0.a=0;
then DataLoc(t0.a,4)=intpos (0+4) by SCMP_GCD:1;
then
A2: t4.a4=t0.DataLoc(t0.a,2) by SCMPDS_2:47
.=t0.intpos(0+2) by A1,SCMP_GCD:1
.=s.a2;
0 <> |.t0.GBP+4.| by A1,ABSVALUE:def 1;
then a <> DataLoc(t0.GBP,4) by XTUPLE_0:1;
then
A3: t4.a=0 by A1,SCMPDS_2:47;
then
A4: DataLoc(t4.a,2)=intpos (0+2) by SCMP_GCD:1;
0 <> |.t4.GBP+2.| by A3,ABSVALUE:def 1;
then
A5: a <> DataLoc(t4.GBP,2) by XTUPLE_0:1;
A6: t3.a=Exec(j2,t4).a by SCMPDS_5:42
.=0 by A3,A5,SCMPDS_2:49;
then
A7: DataLoc(t3.a,1)=intpos (0+1) by SCMP_GCD:1;
4 <> |.t4.GBP+2.| by A3,ABSVALUE:def 1;
then
A8: a4 <> DataLoc(t4.GBP,2) by XTUPLE_0:1;
A9: t3.a4=Exec(j2,t4).a4 by SCMPDS_5:42
.=s.a2 by A2,A8,SCMPDS_2:49;
A10: t2.a1=Exec(j3,t3).a1 by SCMPDS_5:41
.=t3.DataLoc(t3.a,4) by A7,SCMPDS_2:47
.=s.a2 by A6,A9,SCMP_GCD:1;
3 <> |.t4.GBP+2.| by A3,ABSVALUE:def 1;
then
A11: a3 <> DataLoc(t4.GBP,2) by XTUPLE_0:1;
2 <> |.t0.GBP+4.| by A1,ABSVALUE:def 1;
then a2 <> DataLoc(t0.GBP,4) by XTUPLE_0:1;
then
A12: t4.a2=t0.a2 by SCMPDS_2:47
.=s.a2;
1 <> |.t0.GBP+4.| by A1,ABSVALUE:def 1;
then a1 <> DataLoc(t0.GBP,4) by XTUPLE_0:1;
then
A13: t4.a1=t0.a1 by SCMPDS_2:47
.=s.a1;
3 <> |.t0.GBP+4.| by A1,ABSVALUE:def 1;
then a3 <> DataLoc(t0.GBP,4) by XTUPLE_0:1;
then
A14: t4.a3=t0.a3 by SCMPDS_2:47
.=s.a3;
0 <> |.t3.GBP+1.| by A6,ABSVALUE:def 1;
then
A15: a <> DataLoc(t3.GBP,1) by XTUPLE_0:1;
A16: t2.a=Exec(j3,t3).a by SCMPDS_5:41
.=0 by A6,A15,SCMPDS_2:47;
then
A17: DataLoc(t2.a,3)=intpos (0+3) by SCMP_GCD:1;
2 <> |.t3.GBP+1.| by A6,ABSVALUE:def 1;
then
A18: a2 <> DataLoc(t3.GBP,1) by XTUPLE_0:1;
A19: t3.a2=Exec(j2,t4).a2 by SCMPDS_5:42
.=t4.a2+t4.DataLoc(t4.a,1) by A4,SCMPDS_2:49
.=s.a2+s.a1 by A3,A13,A12,SCMP_GCD:1;
A20: t2.a2=Exec(j3,t3).a2 by SCMPDS_5:41
.=s.a2+s.a1 by A19,A18,SCMPDS_2:47;
3 <> |.t3.GBP+1.| by A6,ABSVALUE:def 1;
then
A21: a3 <> DataLoc(t3.GBP,1) by XTUPLE_0:1;
0 <> |.t2.GBP+3.| by A16,ABSVALUE:def 1;
then
A22: a <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
thus t1.a=Exec(j4,t2).a by SCMPDS_5:41
.=0 by A16,A22,SCMPDS_2:48;
1 <> |.t2.GBP+3.| by A16,ABSVALUE:def 1;
then
A23: a1 <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
thus t1.a1=Exec(j4,t2).a1 by SCMPDS_5:41
.=s.a2 by A10,A23,SCMPDS_2:48;
2 <> |.t2.GBP+3.| by A16,ABSVALUE:def 1;
then
A24: a2 <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
A25: t3.a3=Exec(j2,t4).a3 by SCMPDS_5:42
.=s.a3 by A14,A11,SCMPDS_2:49;
A26: t2.a3=Exec(j3,t3).a3 by SCMPDS_5:41
.=s.a3 by A25,A21,SCMPDS_2:47;
thus t1.a2=Exec(j4,t2).a2 by SCMPDS_5:41
.=s.a1+s.a2 by A20,A24,SCMPDS_2:48;
thus t1.a3=Exec(j4,t2).a3 by SCMPDS_5:41
.=t2.a3+-1 by A17,SCMPDS_2:48
.=s.a3-1 by A26;
end;
Lm5: for s being 0-started State of SCMPDS,n be Element of NAT
st s.GBP=0 & s.a1=0 & s.
a2=1 & s.a3=n holds IExec(WH,P,s).a1=Fib n &
IExec(WH,P,s).a2=Fib (n+1) & WH
is_closed_on s,P & WH is_halting_on s,P
proof
let s be 0-started State of SCMPDS,n be Element of NAT;
set a=GBP;
A1: now
let t be 0-started State of SCMPDS,Q;
let k be Element of NAT;
assume that
n=t.a3+k and
A2: t.a1=Fib k and
A3: t.a2 = Fib (k+1) and
A4: t.a=0 and
t.a3 > 0;
thus IExec(WB,Q,t).a=0 by A4,Lm4;
thus WB is_closed_on t,Q & WB is_halting_on t,Q by SCMPDS_6:20,21;
thus IExec(WB,Q,t).a3=t.a3-1 by A4,Lm4;
thus IExec(WB,Q,t).a1=Fib (k+1) by A3,A4,Lm4;
thus IExec(WB,Q,t).a2 =t.a1+t.a2 by A4,Lm4
.=Fib (k+1+1) by A2,A3,PRE_FF:1;
end;
assume s.GBP=0 & s.a1=0 & s.a2=1 & s.a3=n;
hence thesis by A1,Th6;
end;
Lm6: for s being 0-started State of SCMPDS,
n be Element of NAT holds IExec(Fib-macro(n),P,s).a1=Fib n &
IExec(Fib-macro(n),P,s).a2=Fib (n+1)
& Fib-macro(n) is_halting_on s,P
proof
let s be 0-started State of SCMPDS,n be Element of NAT;
set a=GBP, i1=a:=0, i2=a1:=0, i3=a2:=1, i4=a3:=n,
I4=i1 ';' i2 ';' i3 ';' i4, t1=IExec(I4,P,s),
t2=IExec(i1 ';' i2 ';' i3,P,s),
t3=IExec(i1 ';' i2,P,s), t4=Exec(i1, s);
A1: Initialize s = s by MEMSTR_0:44;
A2: t4.a=0 by SCMPDS_2:45;
A3: t3.a=Exec(i2, t4).a by SCMPDS_5:42
.=0 by A2,AMI_3:10,SCMPDS_2:45;
A4: t2.a=Exec(i3, t3).a by SCMPDS_5:41
.=0 by A3,AMI_3:10,SCMPDS_2:45;
A5: t3.a1=Exec(i2, t4).a1 by SCMPDS_5:42
.=0 by SCMPDS_2:45;
A6: t2.a1=Exec(i3, t3).a1 by SCMPDS_5:41
.=0 by A5,AMI_3:10,SCMPDS_2:45;
A7: t1.a1=Exec(i4, t2).a1 by SCMPDS_5:41
.=0 by A6,AMI_3:10,SCMPDS_2:45;
A8: t2.a2=Exec(i3, t3).a2 by SCMPDS_5:41
.=1 by SCMPDS_2:45;
A9: t1.a2=Exec(i4, t2).a2 by SCMPDS_5:41
.=1 by A8,AMI_3:10,SCMPDS_2:45;
A10: t1.a3=Exec(i4, t2).a3 by SCMPDS_5:41
.=n by SCMPDS_2:45;
A11: t1.a=Exec(i4, t2).a by SCMPDS_5:41
.=0 by A4,AMI_3:10,SCMPDS_2:45;
A12: (Initialize t1).GBP = t1.GBP by SCMPDS_5:15;
A13: (Initialize t1).a1 = t1.a1 by SCMPDS_5:15;
A14: (Initialize t1).a2 = t1.a2 by SCMPDS_5:15;
A15: (Initialize t1).a3 = t1.a3 by SCMPDS_5:15;
A16: WH is_closed_on Initialize t1,P &
WH is_halting_on Initialize t1,P by A7,A9,A10,Lm5,A11,A12,A13,A14,A15;
A17: WH is_closed_on t1,P
proof
for k being Nat holds
IC Comput(P+*stop WH,Initialize Initialize t1,k) in dom stop WH
by A16,SCMPDS_6:def 2;
hence thesis by SCMPDS_6:def 2;
end;
A18: WH is_halting_on t1,P
proof
P+*stop WH halts_on Initialize Initialize t1 by A16,SCMPDS_6:def 3;
hence thesis by SCMPDS_6:def 3;
end;
IExec(WH,P,Initialize t1).a1=Fib n by A11,A7,A9,A10,Lm5,A12,A13,A14,A15;
hence IExec(Fib-macro(n),P,s).a1=Fib n by A17,A18,SCPISORT:7;
IExec(WH,P,Initialize t1).a2=Fib (n+1) by A11,A7,A9,A10,Lm5,A12,A13,A14,A15;
hence IExec(Fib-macro(n),P,s).a2=Fib (n+1) by A17,A18,SCPISORT:7;
thus thesis by A17,A18,A1,SCPISORT:9;
end;
theorem
for s being 0-started State of SCMPDS,
n be Element of NAT
holds IExec(Fib-macro(n),P,s).intpos 1=Fib n &
IExec(Fib-macro(n),P,s).intpos 2=Fib (n+1) & Fib-macro(n)
is parahalting
proof
let s be 0-started State of SCMPDS,n be Element of NAT;
thus IExec(Fib-macro(n),P,s).a1=Fib n &
IExec(Fib-macro(n),P,s).a2=Fib (n+1) by Lm6;
for t be State of SCMPDS,Q holds Fib-macro(n) is_halting_on t,Q
proof let t be State of SCMPDS, Q;
Fib-macro(n) is_halting_on Initialize t,Q by Lm6;
hence thesis by SCMPDS_6:126;
end;
hence thesis by SCMPDS_6:21;
end;
begin :: The construction of while<>0 loop program
:: while (a,i)<>0 do I
definition
let a be Int_position, i be Integer;
let I be Program of SCMPDS;
func while<>0(a,i,I) -> Program of SCMPDS equals
(a,i)<>0_goto 2 ';' goto (
card I+2) ';' I ';' goto -(card I+2);
coherence;
end;
begin :: The basic property of "while<>0" program
theorem Th8:
for a be Int_position,i be Integer,I be Program of SCMPDS holds
card while<>0(a,i,I)= card I +3
proof
let a be Int_position,i be Integer, I be Program of SCMPDS;
set i1=(a,i)<>0_goto 2, i2=goto (card I+2);
set I4=i1 ';' i2 ';' I;
thus card while<>0(a,i,I) =card I4+1 by SCMP_GCD:4
.=card (i1 ';' i2)+ card I+1 by AFINSQ_1:17
.=2+card I +1 by SCMP_GCD:5
.=card I + 3;
end;
Lm7: for a be Int_position,i be Integer,I be Program of SCMPDS holds card stop
while<>0(a,i,I)= card I+4
proof
let a be Int_position,i be Integer,I be Program of SCMPDS;
thus card stop while<>0(a,i,I)= card while<>0(a,i,I) +1 by COMPOS_1:55
.= card I +3+1 by Th8
.= card I + 4;
end;
theorem Th9:
for a be Int_position,i be Integer,m be Element of NAT,I be
Program of SCMPDS holds m < card I+3 iff m in dom while<>0(a,i,I)
proof
let a be Int_position,i be Integer,m be Element of NAT, I be Program of
SCMPDS;
card while<>0(a,i,I)=card I + 3 by Th8;
hence thesis by AFINSQ_1:66;
end;
theorem Th10:
for a be Int_position,i be Integer,I be Program of SCMPDS holds
0 in dom while<>0(a,i,I) & 1 in dom while<>0(a,i,I)
proof
let a be Int_position,i be Integer,I be Program of SCMPDS;
3 <= card I+3 by NAT_1:11;
then 0 < card I+3 & 1 < card I+3 by XXREAL_0:2;
hence thesis by Th9;
end;
theorem Th11:
for a be Int_position,i be Integer,I be Program of SCMPDS holds
while<>0(a,i,I). 0=(a,i)<>0_goto 2 & while<>0(a,i,I). 1= goto (card
I +2) & while<>0(a,i,I). (card I+2)=goto -(card I+2)
proof
let a be Int_position,i be Integer,I be Program of SCMPDS;
set i1=(a,i)<>0_goto 2, i2=goto (card I+2), i3=goto -(card I+2);
set I4=i1 ';' i2 ';' I;
set WHL=while<>0(a,i,I);
A1: WHL=i1 ';' i2 ';' (I ';' i3) by SCMPDS_4:11;
hence WHL. 0=i1 by Th1;
thus WHL. 1=i2 by A1,Th1;
card I4=card (i1 ';' i2)+ card I by AFINSQ_1:17
.=card I +2 by SCMP_GCD:5;
hence thesis by SCMP_GCD:6;
end;
Lm8: for a be Int_position,i be Integer,I be Program of SCMPDS holds while<>0
(a,i,I)= ((a,i)<>0_goto 2) ';' (goto (card I+2) ';' I ';' goto -(card I+2))
proof
let a be Int_position,i be Integer,I be Program of SCMPDS;
set i1=(a,i)<>0_goto 2, i2=goto (card I+2), i3=goto -(card I+2);
thus while<>0(a,i,I) = i1 ';' (i2 ';' I) ';' i3 by SCMPDS_4:16
.= i1 ';' (i2 ';' I ';' i3) by SCMPDS_4:15;
end;
theorem Th12:
for s being State of SCMPDS,I being Program of SCMPDS,a being
Int_position, i being Integer st s.DataLoc(s.a,i) = 0 holds while<>0(a,i,I)
is_closed_on s,P & while<>0(a,i,I) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS,a be Int_position, i be
Integer;
set b=DataLoc(s.a,i);
assume
A1: s.b = 0;
set WHL=while<>0(a,i,I), pWH=stop WHL, iWH=pWH,
s3 = Initialize s, P3 = P +* pWH,
s4 = Comput(P3,s3,1), s5 = Comput(P3,s3,2), P4 = P3, P5 = P3;
A2: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A3: s3.DataLoc(s3.a,i)=s3.b by FUNCT_4:11
.= 0 by A1,A2,FUNCT_4:11;
set i1=(a,i)<>0_goto 2, i2=goto (card I+2), i3=goto -(card I+2);
A4: IC s3 = 0 by MEMSTR_0:47;
A5: WHL = i1 ';' (i2 ';' I ';' i3 ) by Lm8;
Comput(P3,s3,0+1) = Following(P3,
Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3)
.= Exec(i1,s3) by A5,SCMPDS_6:11;
then
A6: IC s4 = IC s3 + 1 by A3,SCMPDS_2:55
.= (0+1) by A4;
A7: iWH c= P3 by FUNCT_4:25;
then
A8: pWH c= P4;
A9: 1 in dom WHL by Th10;
then 1 in dom pWH by COMPOS_1:62;
then
A10: P4. 1 = pWH. 1 by A8,GRFUNC_1:2
.=WHL. 1 by A9,COMPOS_1:63
.=i2 by Th11;
A11: card WHL=card I+3 by Th8;
then
A12: (card I+3) in dom pWH by COMPOS_1:64;
A13: P4/.IC s4 = P4.IC s4 by PBOOLE:143;
Comput(P3,s3,1+1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(i2,s4) by A6,A10,A13;
then
A14: IC s5 = ICplusConst(s4,card I+2) by SCMPDS_2:54
.= (card I+2+1) by A6,SCMPDS_6:12
.= (card I+(2+1));
A15: P5/.IC s5 = P5.IC s5 by PBOOLE:143;
pWH c= P5 by A7;
then P5.(card I+3) = pWH.(card I+3) by A12,GRFUNC_1:2
.=halt SCMPDS by A11,COMPOS_1:64;
then
A16: CurInstr(P5,s5) = halt SCMPDS by A14,A15;
now
let k be Nat;
k = 0 or 0 < k;
then
A17: k = 0 or 0 + 1 <= k by INT_1:7;
per cases by A17,XXREAL_0:1;
suppose
k = 0;
then Comput(P3,s3,k) = s3;
hence IC Comput(P3,s3,k) in dom pWH by A4,COMPOS_1:36;
end;
suppose
k = 1;
hence IC Comput(P3,s3,k) in dom pWH by A9,A6,COMPOS_1:62;
end;
suppose
1 < k;
then 1+1 <= k by INT_1:7;
hence IC Comput(P3,s3,k) in dom pWH
by A12,A14,A16,EXTPRO_1:5;
end;
end;
hence WHL is_closed_on s,P by SCMPDS_6:def 2;
P3 halts_on s3 by A16,EXTPRO_1:29;
hence thesis by SCMPDS_6:def 3;
end;
theorem Th13:
for s being State of SCMPDS,I being Program of SCMPDS,a,c being
Int_position, i being Integer st s.DataLoc(s.a,i) = 0
holds IExec(while<>0(a,i,I),P,Initialize s) = s +* Start-At((card I+3),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS, a,c be Int_position, i be
Integer;
set b=DataLoc(s.a,i);
assume
A1: s.b = 0;
set i1=(a,i)<>0_goto 2, i2=goto (card I+2), i3=goto -(card I+2);
set WHL=while<>0(a,i,I), pWH=stop WHL, iWH=pWH,
s3 = Initialize s, P3 = P +* pWH,
s4 = Comput(P3,s3,1), s5 = Comput(P3,s3,2), P4 = P3, P5 = P3;
A2: IC s3 = 0 by MEMSTR_0:47;
A3: iWH c= P3 by FUNCT_4:25;
then
A4: pWH c= P4;
A5: pWH c= P5 by A3;
A6: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
A7: WHL = i1 ';' (i2 ';' I ';' i3 ) by Lm8;
A8: Comput(P3,s3,0+1) = Following(P3,
Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3)
.= Exec(i1,s3) by A7,SCMPDS_6:11;
A9: 1 in dom WHL by Th10;
then 1 in dom pWH by COMPOS_1:62;
then
A10: P4. 1 = pWH. 1 by A4,GRFUNC_1:2
.=WHL. 1 by A9,COMPOS_1:63
.=i2 by Th11;
set SAl=Start-At((card I+3),SCMPDS);
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then s3.DataLoc(s3.a,i)=s3.b by FUNCT_4:11
.= 0 by A1,A6,FUNCT_4:11;
then
A11: IC s4 = IC s3 + 1 by A8,SCMPDS_2:55
.= (0+1) by A2;
A12: P3/.IC s4 = P4.IC s4 by PBOOLE:143;
A13: Comput(P3,s3,1+1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(i2,s4) by A11,A10,A12;
then
A14: IC s5 = ICplusConst(s4,card I+2) by SCMPDS_2:54
.= (card I+2+1) by A11,SCMPDS_6:12
.= (card I+(2+1));
A15: P3/.IC s5 = P5.IC s5 by PBOOLE:143;
A16: card WHL=card I+3 by Th8;
then (card I+3) in dom pWH by COMPOS_1:64;
then P5.(card I+3) = pWH.(card I+3) by A5,GRFUNC_1:2
.=halt SCMPDS by A16,COMPOS_1:64;
then
A17: CurInstr(P3,s5) = halt SCMPDS by A14,A15;
then P3 halts_on s3 by EXTPRO_1:29;
then
A18: s5 = Result(P3,s3) by A17,EXTPRO_1:def 9;
A19: IExec(WHL,P,Initialize s) = Result(P3,s3) by SCMPDS_4:def 5;
A20: now
let x be object;
A21: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A22: x in dom IExec(WHL,P,Initialize s);
per cases by A22,SCMPDS_4:6;
suppose
A23: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A24: not x in dom SAl by A21,TARSKI:def 1;
A25: not x in dom Start-At(0,SCMPDS) by A23,SCMPDS_4:18;
thus IExec(WHL,P,Initialize s).x = s5.x by A18,A19
.= s4.x by A13,A23,SCMPDS_2:54
.= s3.x by A8,A23,SCMPDS_2:55
.= s.x by A25,FUNCT_4:11
.= (s +* SAl).x by A24,FUNCT_4:11;
end;
suppose
A26: x = IC SCMPDS;
hence IExec(WHL,P,Initialize s).x = (card I + 3) by A14,A18,A19
.= (s +* SAl).x by A26,FUNCT_4:113;
end;
end;
dom IExec(WHL,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (s +* SAl) by PARTFUN1:def 2;
hence thesis by A20,FUNCT_1:2;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,a being
Int_position, i being Integer st s.DataLoc(s.a,i) = 0
holds IC IExec(while<>0(a,i,I),P,Initialize s) = (card I + 3)
proof
let s be State of SCMPDS,I be Program of SCMPDS,a be Int_position, i be
Integer;
assume s.DataLoc(s.a,i) = 0;
then IExec(while<>0(a,i,I),P,Initialize s) =s +* Start-At((card I+3),SCMPDS)
by Th13;
hence thesis by FUNCT_4:113;
end;
theorem Th15:
for s being State of SCMPDS,I being Program of SCMPDS,a,b being
Int_position, i being Integer st s.DataLoc(s.a,i) = 0
holds IExec(while<>0(a,i,I),P,Initialize s).b = s.b
proof
let s be State of SCMPDS,I be Program of SCMPDS,a,b be Int_position, i be
Integer;
assume s.DataLoc(s.a,i) = 0;
then
A1: IExec(while<>0(a,i,I),P,Initialize s) = s +* Start-At((card I+3),SCMPDS)
by Th13;
not b in dom Start-At((card I+3),SCMPDS) by SCMPDS_4:18;
hence thesis by A1,FUNCT_4:11;
end;
Lm9: for I being Program of SCMPDS,a being Int_position,i being Integer holds
Shift(I,2) c= while<>0(a,i,I)
proof
let I be Program of SCMPDS,a be Int_position,i be Integer;
set i1=(a,i)<>0_goto 2, i2=goto (card I+2), i3=goto -(card I+2);
card (i1 ';' i2)=2 & while<>0(a,i,I) = i1 ';' i2 ';' I ';' Load i3 by
SCMPDS_4:def 3,SCMP_GCD:5;
hence thesis by SCMPDS_7:3;
end;
registration
let I be shiftable Program of SCMPDS, a be Int_position,i be Integer;
cluster while<>0(a,i,I) -> shiftable;
correctness
proof
set WHL=while<>0(a,i,I), i1=(a,i)<>0_goto 2, i2=goto (card I+2), PF= i1
';' i2 ';' I;
card PF=card (i1 ';' i2)+ card I by AFINSQ_1:17
.=2+card I by SCMP_GCD:5;
then PF=Load i1 ';' Load i2 ';' I & card PF+ -(card I+2) =0 by
SCMPDS_4:def 4;
hence thesis by SCMPDS_4:23;
end;
end;
registration
let I be halt-free Program of SCMPDS, a be Int_position,i be Integer;
cluster while<>0(a,i,I) -> halt-free;
correctness
proof
reconsider i2=goto (card I+2) as No-StopCode Instruction of SCMPDS by
SCMPDS_5:21;
reconsider
i3=goto -(card I+2) as No-StopCode Instruction of SCMPDS by SCMPDS_5:21;
while<>0(a,i,I) =(a,i)<>0_goto 2 ';' i2 ';' I ';' i3;
hence thesis;
end;
end;
begin :: Computing directly the result of "while<>0" program by loop-invariant
scheme
WhileNHalt { F(State of SCMPDS)-> Element of NAT,
s() -> 0-started State of SCMPDS,
P() -> Instruction-Sequence of SCMPDS,
I() -> halt-free shiftable Program of SCMPDS,
a() -> Int_position,i() -> Integer, P[set]}:
while<>0(a(),i(),I()) is_closed_on s(),P() &
while<>0(a(),i(),I()) is_halting_on s(),P()
provided
A1: for t be 0-started State of SCMPDS st P[t] & F(t)=0
holds t.DataLoc(s().a(),i()) = 0 and
A2: P[s()] and
A3: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=s().a() & t.DataLoc(s().a(),i()) <> 0
holds IExec(I(),Q,t).a()=t.a() & I() is_closed_on t,Q &
I() is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))]
proof
A4: Initialize s() = s() by MEMSTR_0:44;
set i1=(a(),i())<>0_goto 2, i2=goto (card I()+2), i3=goto -(card I()+2);
set WHL=while<>0(a(),i(),I()), pWH=stop WHL, pI=stop I();
set b=DataLoc(s().a(),i());
defpred Q[Nat] means
for t be 0-started State of SCMPDS,Q st F(Initialize(t)) <=
$1 & P[Initialize t] & t.a()=s().a()
holds WHL is_closed_on t,Q & WHL is_halting_on t,Q;
A5: for k be Nat st Q[k] holds Q[k + 1]
proof
let k be Nat;
assume
A6: Q[k];
now
let t be 0-started State of SCMPDS;
let Q;
A7: Initialize t = t by MEMSTR_0:44;
assume
A8: F(Initialize t) <= k+1;
assume
A9: P[Initialize t];
assume
A10: t.a()=s().a();
per cases;
suppose
t.b = 0;
hence WHL is_closed_on t,Q & WHL is_halting_on t,Q by A10,Th12;
end;
suppose
A11: t.b <> 0;
A12: IExec(I(),Q,t).a()=t.a() by A3,A9,A10,A11,A7;
A13: 0 in dom pWH by COMPOS_1:36;
A14: WHL = i1 ';' (i2 ';' I() ';' i3) by Lm8;
A15: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
set t2 = Initialize t, Q2 = Q +* pI,
t3 = Initialize t, Q3 = Q +* pWH,
t4 = Comput(Q3,t3,1), Q4 = Q3;
A16: pI c= Q2 by FUNCT_4:25;
set m2=LifeSpan(Q2,t2), t5=Comput(Q4,t4,m2), Q5 = Q4,
l2= (card I() + 2
);
A17: IC t3 = 0 by MEMSTR_0:47;
set m3=m2 +1;
set t6=Comput(Q3,t3,m3), Q6 = Q3;
set t7=Comput(Q3,t3,m3+1), Q7 = Q3;
card I() + 2 < card I() + 3 by XREAL_1:6;
then
A18: l2 in dom WHL by Th9;
A19: pWH c= Q3 by FUNCT_4:25;
WHL c= pWH by AFINSQ_1:74;
then
A20: WHL c= Q3 by A19,XBOOLE_1:1;
Shift(I(),2) c= WHL by Lm9;
then Shift(I(),2) c= Q3 by A20,XBOOLE_1:1;
then
A21: Shift(I(),2) c= Q4;
A22: Comput(Q3,t3,0+1) = Following(Q3,
Comput(Q3,t3,0)) by EXTPRO_1:3
.= Following(Q3,t3)
.= Exec(i1,t3) by A14,SCMPDS_6:11;
for a holds t2.a = t4.a by A22,SCMPDS_2:55;
then
A23: DataPart t2 = DataPart t4 by SCMPDS_4:8;
I() is_halting_on t,Q by A3,A9,A10,A11,A7;
then
A24: Q2 halts_on t2 by SCMPDS_6:def 3;
Q2+*pI halts_on Initialize t2 by A24;
then
A25: I() is_halting_on t2,Q2 by SCMPDS_6:def 3;
A26: IExec(I(),Q,Initialize t) = Result(Q2,t2) by SCMPDS_4:def 5;
A27: P[Initialize(IExec(I(),Q,Initialize t))] by A3,A9,A10,A11,A7;
A28: I() is_closed_on t,Q by A3,A9,A10,A11,A7;
then
A29: I() is_closed_on t2,Q2 by SCMPDS_6:24;
not a() in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then t3.DataLoc(t3.a(),i())= t3.b by A10,FUNCT_4:11
.= t.b by A15,FUNCT_4:11;
then
A30: IC t4 = ICplusConst(t3,2) by A11,A22,SCMPDS_2:55
.= 0+2 by A17,SCMPDS_6:12;
then
A31: IC t5=l2 by A16,A25,A29,A23,A21,SCMPDS_7:18;
A32: Q6/.IC t6 = Q6.IC t6 by PBOOLE:143;
A33: t6=t5 by EXTPRO_1:4;
then
A34: CurInstr(Q6,t6)
=Q5.l2 by A16,A25,A29,A30,A23,A21,A32,SCMPDS_7:18
.=Q4.l2
.=Q3.l2
.=WHL.l2 by A18,A20,GRFUNC_1:2
.=i3 by Th11;
A35: t7 = Following(Q3,t6) by EXTPRO_1:3
.= Exec(i3,t6) by A34;
then IC t7=ICplusConst(t6,0-(card I()+2)) by SCMPDS_2:54
.= 0 by A31,A33,SCMPDS_7:1;
then
A36: Initialize t7 = t7 by MEMSTR_0:46;
A37: Q7 +* pWH=Q7;
A38: DataPart Comput(Q2,t2,m2) = DataPart t5 by A16,A25,A29,A30,A23,A21,
SCMPDS_7:18;
then
A39: DataPart t5 = DataPart(Result(Q2,t2)) by A24,EXTPRO_1:23
.= DataPart(Result(Q2,t2))
.= DataPart IExec(I(),Q,Initialize t) by SCMPDS_4:def 5;
InsCode i3=14 by SCMPDS_2:12;
then InsCode i3 in {0,4,5,6,14} by ENUMSET1:def 3;
then
A40: Initialize(t7)=Initialize(t6) by A35,SCMPDS_8:3
.=Initialize(IExec(I(),Q,Initialize t)) by A39,A33,MEMSTR_0:80;
A41: now
F(Initialize(IExec(I(),Q,Initialize t))) < F(Initialize(t))
by A3,A9,A10,A11,A7;
then
A42: F(Initialize(t7)) < k+1 by A8,A40,XXREAL_0:2;
assume F(Initialize(t7)) > k;
hence contradiction by A42,INT_1:7;
end;
A43: t5.a()=Comput(Q2,t2,m2).a() by A38,SCMPDS_4:8
.=(Result(Q2,t2)).a() by A24,EXTPRO_1:23
.=s().a() by A10,A12,A26,A7;
A44: t7.a()=t6.a() by A35,SCMPDS_2:54
.=s().a() by A43,EXTPRO_1:4;
A45: (Initialize t7).a() = t7.a() by SCMPDS_5:15;
P[Initialize (Initialize t7)] by A27,A40;
then
A46: WHL is_closed_on (Initialize t7),Q7 &
WHL is_halting_on (Initialize t7),Q7 by A6,A41,A44,A45;
A47: WHL is_closed_on t7,Q7
proof
for k being Nat holds
IC Comput(Q7+*stop WHL,Initialize Initialize t7,k) in dom stop WHL
by A46,SCMPDS_6:def 2;
hence thesis by SCMPDS_6:def 2;
end;
now
let k be Nat;
per cases;
suppose
k < m3+1;
then
A48: k <= m3 by INT_1:7;
hereby
per cases by A48,NAT_1:8;
suppose
A49: k <= m2;
hereby
per cases;
suppose
k=0;
hence IC Comput(Q3,t3,k) in dom pWH by A13,A17;
end;
suppose
k<>0;
then consider kn be Nat such that
A50: k=kn+1 by NAT_1:6;
reconsider kn as Element of NAT by ORDINAL1:def 12;
reconsider lm = IC Comput(Q2,t2,kn) as Element
of NAT;
kn < k by A50,XREAL_1:29;
then kn < m2 by A49,XXREAL_0:2;
then IC Comput(Q2,t2,kn) + 2 = IC Comput(
Q4,t4,kn) by A16,A25,A29,A30,A23,A21,SCMPDS_7:16;
then
A51: IC Comput(Q3,t3,k) = (lm+2) by A50,EXTPRO_1:4;
IC Comput(Q2,t2,kn) in dom pI by A28,SCMPDS_6:def 2;
then lm < card pI by AFINSQ_1:66;
then lm < card I()+1 by COMPOS_1:55;
then
A52: lm+2 < card I() +1+2 by XREAL_1:6;
card I() + 3 < card I() + 4 by XREAL_1:6;
then lm+2 < card I() +4 by A52,XXREAL_0:2;
then lm+2 < card pWH by Lm7;
hence IC Comput(Q3,t3,k) in dom pWH by A51,AFINSQ_1:66;
end;
end;
end;
suppose
A53: k=m3;
l2 in dom pWH by A18,COMPOS_1:62;
hence
IC Comput(Q3,t3,k) in dom pWH by A16,A25,A29,A30,A23,A21,A33
,A53,SCMPDS_7:18;
end;
end;
end;
suppose
k >= m3+1;
then consider nn be Nat such that
A54: k=m3+1+nn by NAT_1:10;
reconsider nn as Element of NAT by ORDINAL1:def 12;
Comput(Q3,t3,k)=
Comput(Q7+*pWH,Initialize t7,nn) by A54,A36,EXTPRO_1:4;
hence IC Comput(Q3,t3,k) in dom pWH by A47,SCMPDS_6:def 2;
end;
end;
hence WHL is_closed_on t,Q by SCMPDS_6:def 2;
WHL is_halting_on t7,Q7
proof
Q7+*stop WHL halts_on Initialize Initialize t7 by A46,SCMPDS_6:def 3;
hence thesis by SCMPDS_6:def 3;
end;
then Q7 halts_on t7 by A37,A36,SCMPDS_6:def 3;
then Q3 halts_on t7;
then Q3 halts_on t3 by EXTPRO_1:22;
hence WHL is_halting_on t,Q by SCMPDS_6:def 3;
end;
end;
hence thesis;
end;
set n=F(s());
A55: Q[0]
proof
let t be 0-started State of SCMPDS, Q;
assume that
A56: F(Initialize t) <= 0 & P[Initialize t] and
A57: t.a()=s().a();
(Initialize t).b = t.b by SCMPDS_5:15;
then t.b = 0 by A1,A56,XXREAL_0:1;
hence thesis by A57,Th12;
end;
for k being Nat holds Q[k] from NAT_1:sch 2(A55,A5);
then Q[n];
hence thesis by A2,A4;
end;
scheme
WhileNExec { F(State of SCMPDS)-> Element of NAT,
s() -> 0-started State of SCMPDS,
P() -> Instruction-Sequence of SCMPDS,
I() -> halt-free shiftable Program of SCMPDS,
a() -> Int_position,i() -> Integer,
P[set]}: IExec(while<>0(a(),i(),I()),P(),s())
= IExec(while<>0(a(),i(),I()),P(),Initialize IExec(I(),P(),s()))
provided
A1: s().DataLoc(s().a(),i()) <> 0 and
A2: for t be 0-started State of SCMPDS st P[t] & F(t)=0
holds t.DataLoc(s().a(),i()) = 0 and
A3: P[s()] and
A4: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=s().a() & t.DataLoc(
s().a(),i()) <> 0 holds IExec(I(),Q,t).a()=t.a() &
I() is_closed_on t,Q & I()
is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))]
proof
A5: Initialize s() = s() by MEMSTR_0:44;
set WHL=while<>0(a(),i(),I()),
s1= s(), P1 = P() +* stop WHL;
set sI= s(), PI = P() +* stop I(),
m1=LifeSpan(PI,sI)+2,
s2=Initialize IExec(I(),P(),s()),
m2=LifeSpan(P1,s2);
A6: stop I() c= PI by FUNCT_4:25;
I() is_closed_on s(),P() by A1,A3,A4;
then
A7: I() is_closed_on sI,PI by A5,SCMPDS_6:24;
I() is_halting_on s(),P() by A1,A3,A4;
then
A8: PI halts_on sI by A5,SCMPDS_6:def 3;
PI+*stop I() halts_on Initialize sI by A8,A5;
then
A9: I() is_halting_on sI,PI by SCMPDS_6:def 3;
set s4 = Comput(P1,s1,1), P4 = P1;
set i1=(a(),i())<>0_goto 2, i2=goto (card I()+2), i3=goto -(card I()+2);
set b=DataLoc(s().a(),i());
A10: IC s1 = 0 by A5,MEMSTR_0:47;
set mI=LifeSpan(PI,sI), s5=Comput(P4,s4,mI), P5 = P4,
l2= (
card I() + 2);
A11: WHL = i1 ';' (i2 ';' I() ';' i3) by Lm8;
set m3=mI +1;
set s6=Comput(P1,s1,m3), P6 = P1;
card I() + 2 < card I() + 3 by XREAL_1:6;
then
A12: l2 in dom WHL by Th9;
set s7=Comput(P1,s1,m3+1), P7 = P1;
A13: IExec(I(),P(),s()) = Result(PI,sI) by SCMPDS_4:def 5;
A14: stop WHL c= P1 by FUNCT_4:25;
WHL c= stop WHL by AFINSQ_1:74;
then
A15: WHL c= P1 by A14,XBOOLE_1:1;
deffunc F(State of SCMPDS) = F($1);
A16: for t be 0-started State of SCMPDS st P[t] & F(t)=0
holds t.DataLoc (s().a(),i()) = 0 by A2;
A17: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=s().a() & t.DataLoc(s().
a(),i()) <> 0 holds IExec(I(),Q,t).a()=t.a() &
I() is_closed_on t,Q & I()
is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))] by A4;
A18: Comput(P1,s1,0+1) = Following(P1,
Comput(P1,s1,0)) by EXTPRO_1:3
.= Following(P1,s1)
.= Exec(i1,s1) by A11,A5,SCMPDS_6:11;
Shift(I(),2) c= WHL by Lm9;
then Shift(I(),2) c= P1 by A15,XBOOLE_1:1;
then
A19: Shift(I(),2) c= P4;
for a holds sI.a = s4.a by A18,SCMPDS_2:55;
then
A20: DataPart sI = DataPart s4 by SCMPDS_4:8;
A21: IC s4 = ICplusConst(s1,2) by A1,A18,SCMPDS_2:55
.= (0+2) by A10,SCMPDS_6:12;
then
A22: IC s5=l2 by A6,A9,A7,A20,A19,SCMPDS_7:18;
A23: P6/.IC s6 = P6.IC s6 by PBOOLE:143;
A24: s6=s5 by EXTPRO_1:4;
then
A25: CurInstr(P6,s6)=P5.l2 by A6,A9,A7,A21,A20,A19,A23,SCMPDS_7:18
.=P4.l2
.=P1.l2
.=WHL.l2 by A12,A15,GRFUNC_1:2
.=i3 by Th11;
A26: s7 = Following(P1,s6) by EXTPRO_1:3
.= Exec(i3,s6) by A25;
then IC s7=ICplusConst(s6,0-(card I()+2)) by SCMPDS_2:54
.= 0 by A22,A24,SCMPDS_7:1;
then
A27: IC s2 =IC Comput(P1,s1,m1) by MEMSTR_0:47;
A28: DataPart Comput(PI,sI,mI) = DataPart s5 by A6,A9,A7,A21,A20,A19,
SCMPDS_7:18;
now
let x be Int_position;
A29: not x in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
s5.x=Comput(PI,sI,mI).x by A28,SCMPDS_4:8
.=(Result(PI,sI)).x by A8,EXTPRO_1:23
.=IExec(I(),P(),s()).x by A13;
hence s7.x=IExec(I(),P(),s()).x by A24,A26,SCMPDS_2:54
.=s2.x by A29,FUNCT_4:11;
end;
then
A30: DataPart s7 = DataPart s2 by SCMPDS_4:8;
set m0=LifeSpan(P1,s1);
A31: P[s()] by A3;
WHL is_closed_on s(),P() & WHL is_halting_on s(),P()
from WhileNHalt(A16,A31,A17);
then
A32: P1 halts_on s1 by A5,SCMPDS_6:def 3;
deffunc F(State of SCMPDS) = F($1);
set Es=IExec(I(),P(),s()), bj=DataLoc(Es.a(),i()), EP = P();
A33: IExec(I(),P(),s()).a()=s().a() by A1,A3,A4;
A34: (Initialize Es).a() = Es.a() by SCMPDS_5:15;
A35: for t be 0-started State of SCMPDS
st P[t] & F(t)=0
holds t.DataLoc((Initialize Es).a(),i()) = 0 by A2,A33,A34;
A36: P[Initialize Es] by A1,A3,A4;
A37: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=(Initialize Es).a() &
t.DataLoc((Initialize Es).a(),i()) <> 0
holds IExec(I(),Q,t).a()=t.a() & I() is_closed_on t,Q &
I() is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))] by A4,A33,A34;
A38: WHL is_closed_on Initialize Es,P() &
WHL is_halting_on Initialize Es,P() from WhileNHalt(A35,A36,A37);
WHL is_halting_on Es,P()
proof
P()+*stop WHL halts_on Initialize Initialize Es by A38,SCMPDS_6:def 3;
hence thesis by SCMPDS_6:def 3;
end;
then
A39: P1 halts_on s2 by SCMPDS_6:def 3;
A40: Comput(P1,s1,m1)=s2 by A30,A27,MEMSTR_0:78;
then CurInstr(P1,Comput(P1,s1,m1)) =i1 by A11,SCMPDS_6:11;
then m0 > m1 by A32,EXTPRO_1:36,SCMPDS_6:16;
then consider nn be Nat such that
A41: m0=m1+nn by NAT_1:10;
reconsider nn as Element of NAT by ORDINAL1:def 12;
IC Comput(P1,s1,m1+m2) = IC Comput(P1,s2,m2) by A40,EXTPRO_1:4;
then CurInstr(P1,Comput(P1,s1,m1+m2))
= CurInstr(P1,Comput(P1,s2,m2))
.= halt SCMPDS by A39,EXTPRO_1:def 15;
then m1 + m2 >= m0 by A32,EXTPRO_1:def 15;
then
A42: m2 >= nn by A41,XREAL_1:6;
A43: Comput(P1,s1,m0) = Comput(P1,s2,nn) by A40,A41,EXTPRO_1:4;
then CurInstr(P1,Comput(P1,s2,nn))
=halt SCMPDS by A32,EXTPRO_1:def 15;
then nn >= m2 by A39,EXTPRO_1:def 15;
then nn=m2 by A42,XXREAL_0:1;
then Result(P1,s1) = Comput(P1,s2,m2) by A32,A43,EXTPRO_1:23;
hence IExec(WHL,P(),s()) = Comput(P1,s2,m2) by SCMPDS_4:def 5
.= Result(P1,s2) by A39,EXTPRO_1:23
.= IExec(WHL,P(),Initialize IExec(I(),P(),s()))
by SCMPDS_4:def 5;
end;
scheme
WhileNEnd { F(State of SCMPDS)-> Element of NAT,
s() -> 0-started State of SCMPDS,
P() -> Instruction-Sequence of SCMPDS,
I() -> halt-free shiftable Program of SCMPDS,
a() -> Int_position,i() -> Integer,
P[set]}: F(Initialize IExec(while<>0(a(),i(),I()),P(),s()))=0
& P[Initialize IExec(while<>0(a(),i(),I()),P(),s())]
provided
A1: for t be 0-started State of SCMPDS
st P[t] holds F(t)=0 iff t.
DataLoc(s().a(),i()) = 0 and
A2: P[s()] and
A3: for t be 0-started State of SCMPDS,Q
st P[t] & t.a()=s().a() & t.DataLoc(
s().a(),i()) <> 0 holds IExec(I(),Q,t).a()=t.a() &
I() is_closed_on t,Q & I()
is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))]
proof
set b=DataLoc(s().a(),i()), WHL=while<>0(a(),i(),I());
defpred Q[Nat] means
for t be 0-started State of SCMPDS,Q st F(t) <= $1
& t.a()=s().a() & P[t]
holds F(Initialize IExec(WHL,Q,t))=0 & P[Initialize IExec(WHL,Q,t)];
A4: Q[0]
proof
let t be 0-started State of SCMPDS, Q;
A5: Initialize t = t by MEMSTR_0:44;
assume that
A6: F(t) <= 0 and
A7: t.a()=s().a() and
A8: P[t];
A9: F(t)=0 by A6;
then t.DataLoc(t.a(),i()) = 0 by A1,A7,A8;
then for b be Int_position holds IExec(WHL,Q,t).b = t.b by Th15,A5;
hence thesis by A8,A9,A5,SCPISORT:4;
end;
A10: now
let k be Nat;
assume
A11: Q[k];
now
let u be 0-started State of SCMPDS;
let U;
assume that
A12: F(u) <= k+1 and
A13: u.a()=s().a() and
A14: P[u];
per cases;
suppose
F(u)=0;
hence F(Initialize IExec(WHL,U,u))=0 & P[Initialize IExec(WHL,U,u)]
by A4,A13,A14;
end;
suppose
A15: F(u) <> 0;
set Iu=IExec(I(),U,u);
A16: u.b <> 0 by A1,A14,A15;
then
A17: Iu.a()=s().a() & P[Initialize Iu] by A3,A13,A14;
deffunc F(State of SCMPDS) = F($1);
A18: P[u] by A14;
A19: for t be 0-started State of SCMPDS st P[t] & F(t)=0
holds t.DataLoc(u.a(),i()) = 0 by A1,A13;
F(Initialize Iu) < F(u) by A3,A13,A14,A16;
then F(Initialize Iu)+1 <= F(u) by INT_1:7;
then F(Initialize Iu)+1 <= k+1 by A12,XXREAL_0:2;
then
A20: F(Initialize Iu) <= k by XREAL_1:6;
A21: for t being 0-started State of SCMPDS,Q
st P[t] & t.a()=u.a() & t.DataLoc(u.a(),i()) <> 0
holds IExec(I(),Q,t).a()=t.a()
& I() is_closed_on t,Q &
I() is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t)
& P[Initialize(IExec(I(),Q,t))] by A3,A13;
A22: u.DataLoc(u.a(),i()) <> 0 by A1,A13,A14,A15;
A23: IExec(WHL,U,u) = IExec(WHL,U,Initialize Iu)
from WhileNExec(A22,A19,A18,A21);
(Initialize Iu).a() = Iu.a() by SCMPDS_5:15;
hence F(Initialize IExec(WHL,U,u))=0 &
P[Initialize IExec(WHL,U,u)] by A11,A20,A17,A23;
end;
end;
hence Q[k+1];
end;
for k being Nat holds Q[k] from NAT_1:sch 2(A4,A10);
then Q[F(s())];
hence thesis by A2;
end;
theorem Th16:
for s being 0-started State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a,b,c be Int_position,i,d be Integer st card I > 0 & s.a=d &
s.b > 0 & s.c > 0 & s.DataLoc(d,i)=s.b-s.c &
(for t be 0-started State of SCMPDS,Q st t.b >
0 & t.c > 0 & t.a=d & t.DataLoc(d,i)=t.b-t.c & t.b<>t.c
holds IExec(I,Q,t).a=d &
I is_closed_on t,Q & I is_halting_on t,Q
& (t.b > t.c implies IExec(I,Q,t).b=t.b-t.c
& IExec(I,Q,t).c = t.c) & (t.b <= t.c
implies IExec(I,Q,t).c = t.c-t.b & IExec(I,Q,t)
.b=t.b) & IExec(I,Q,t).DataLoc(d,i)=
IExec(I,Q,t).b-IExec(I,Q,t).c)
holds while<>0(a,i,I) is_closed_on s,P & while<>0(a,i,I) is_halting_on s,P
& (s.DataLoc(s.a,i) <> 0
implies IExec(while<>0(a,i,I),P,s) =
IExec(while<>0(a,i,I),P,Initialize IExec(I,P,s)))
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, a,b,c
be Int_position, i,d be Integer;
set ci=DataLoc(s.a,i);
assume
card I > 0;
consider f be Function of product the_Values_of SCMPDS,NAT such that
A1: for s be State of SCMPDS holds (s.b = s.c implies f.s =0) & (s.b <>
s.c implies f.s=max(|.s.b.|,|.s.c.|)) by Th2;
deffunc F(State of SCMPDS) = f.$1;
defpred P[set] means ex t be State of SCMPDS st t=$1 & t.b > 0 & t.c > 0 & t
.DataLoc(d,i)=t.b-t.c;
assume that
A2: s.a=d and
A3: s.b > 0 and
A4: s.c > 0 and
A5: s.DataLoc(d,i)=s.b-s.c;
assume
A6: for t be 0-started State of SCMPDS,Q
st t.b > 0 & t.c > 0 & t.a=d & t.DataLoc(d,
i)=t.b-t.c & t.b<>t.c holds IExec(I,Q,t).a=d
& I is_closed_on t,Q & I is_halting_on
t,Q & (t.b > t.c implies IExec(I,Q,t).b=t.b-t.c
& IExec(I,Q,t).c = t.c) & (t.b <= t.c
implies IExec(I,Q,t).c = t.c-t.b
& IExec(I,Q,t).b=t.b) & IExec(I,Q,t).DataLoc(d,i)=
IExec(I,Q,t).b-IExec(I,Q,t).c;
A7: now
let t be 0-started State of SCMPDS, Q;
assume that
A8: P[t] and
A9: t.a=s.a and
A10: t.ci <> 0;
set It=IExec(I,Q,t), t2=Initialize It, t1=t;
set x=IExec(I,Q,t).b, y=IExec(I,Q,t).c;
consider v be State of SCMPDS such that
A11: v=t and
A12: v.b > 0 and
A13: v.c > 0 and
A14: v.DataLoc(d,i)=v.b-v.c by A8;
A15: t.b > 0 by A11,A12;
A16: t.c > 0 by A11,A13;
A17: t.DataLoc(d,i)=v.b-v.c by A11,A14
.=t.b-v.c by A11
.=t.b-t.c by A11;
then
A18: t.b<>t.c by A2,A10;
hence IExec(I,Q,t).a=t.a by A2,A6,A9,A15,A16,A17;
thus I is_closed_on t,Q & I is_halting_on t,Q by A2,A6,A9,A15,A16,A17,A18;
A19: now
per cases;
suppose
A20: t.b > t.c;
then t.b-t.c > 0 by XREAL_1:50;
hence x > 0 by A2,A6,A9,A16,A17,A20;
thus y > 0 by A2,A6,A9,A16,A17,A20;
A21: x=t.b-t.c by A2,A6,A9,A16,A17,A20;
hereby
A22: max(t.b,t.c)=t.b by A20,XXREAL_0:def 10;
per cases by XXREAL_0:16;
suppose
max(x,y) = x;
hence max(x,y) < max(t.b,t.c) by A16,A21,A22,XREAL_1:44;
end;
suppose
max(x,y) = y;
hence max(x,y) < max(t.b,t.c) by A2,A6,A9,A16,A17,A20,A22;
end;
end;
end;
suppose
A23: t.b <= t.c;
hence x > 0 by A2,A6,A9,A15,A17,A18;
t.b < t.c by A18,A23,XXREAL_0:1;
then t.c-t.b > 0 by XREAL_1:50;
hence y > 0 by A2,A6,A9,A15,A17,A18,A23;
A24: y=t.c-t.b by A2,A6,A9,A15,A17,A18,A23;
A25: x=t.b by A2,A6,A9,A15,A17,A18,A23;
hereby
A26: max(t.b,t.c)=t.c by A23,XXREAL_0:def 10;
per cases by XXREAL_0:16;
suppose
max(x,y) = y;
hence max(x,y) < max(t.b,t.c) by A15,A24,A26,XREAL_1:44;
end;
suppose
max(x,y) = x;
hence max(x,y) < max(t.b,t.c) by A18,A23,A25,A26,XXREAL_0:1;
end;
end;
end;
end;
thus F(t2) < F(t1)
proof
t1.b <> t.c by A18;
then t1.b <> t1.c;
then
A27: F(t1)=max(|.t1.b.|,|.t1.c.|) by A1
.=max(|.t.b.|,|.t1.c.|)
.=max(|.t.b.|,|.t.c.|)
.=max( t.b,|.t.c.|) by A15,ABSVALUE:def 1
.=max(t.b,t.c) by A16,ABSVALUE:def 1;
then F(t1) >= t.b by XXREAL_0:25;
then
A28: F(t1) > 0 by A15;
per cases;
suppose
t2.b=t2.c;
hence thesis by A1,A28;
end;
suppose
t2.b<>t2.c;
then F(t2)=max(|.t2.b.|,|.t2.c.|) by A1
.=max(|.x.|,|.t2.c.|) by SCMPDS_5:15
.=max(|.x.|,|.y.|) by SCMPDS_5:15
.=max( x,|.y.|) by A19,ABSVALUE:def 1
.=max(x,y) by A19,ABSVALUE:def 1;
hence thesis by A19,A27;
end;
end;
A29: IExec(I,Q,t).DataLoc(d,i)=
IExec(I,Q,t).b-IExec(I,Q,t).c
by A2,A6,A9,A15,A16,A17,A18;
thus P[Initialize It]
proof
take v=Initialize It;
thus v=Initialize It;
thus v.b > 0 & v.c > 0 by A19,SCMPDS_5:15;
thus v.DataLoc(d,i)=x-y by A29,SCMPDS_5:15
.=v.b-y by SCMPDS_5:15
.=v.b-v.c by SCMPDS_5:15;
end;
end;
A30: for t be 0-started State of SCMPDS st P[t] &
F(t)=0 holds t.ci = 0
proof
let t be 0-started State of SCMPDS;
assume that
A31: P[t] and
A32: F(t)=0;
consider v be State of SCMPDS such that
A33: v=t and
A34: v.b > 0 and
v.c > 0 and
A35: v.DataLoc(d,i)=v.b-v.c by A31;
A36: now
assume t.b <> t.c;
then (t).b <> t.c;
then (t).b <> (t).c;
then
A37: F(t)=max(|.t.b.|,|.t.c .|) by A1
.=max(|.t.b.|,|.t.c.|)
.=max(|.t.b.|,|.t.c.|);
t.b > 0 by A33,A34;
then |.t.b.| > 0 by COMPLEX1:47;
hence contradiction by A32,A37,XXREAL_0:25;
end;
thus t.ci=v.b-v.c by A2,A33,A35
.=t.b-v.c by A33
.=t.b-t.c by A33
.=0 by A36;
end;
A38: P[s] by A3,A4,A5;
while<>0(a,i,I) is_closed_on s,P & while<>0(a,i,I) is_halting_on s,P
from WhileNHalt(A30,A38,A7);
hence while<>0(a,i,I) is_closed_on s,P & while<>0(a,i,I) is_halting_on s,P;
assume
A39: s.DataLoc(s.a,i) <> 0;
IExec(while<>0(a,i,I),P,s) =
IExec(while<>0(a,i,I),P,Initialize IExec(I,P,s))
from WhileNExec(A39,A30,A38,A7);
hence thesis;
end;
begin :: An example: computing Greatest Common Divisor (Euclid's algorithm)
:: by loop-invariant
:: gcd(x,y) < x=(GBP,1) y=(GBP,2),(GBP,3)=x-y >
:: while x<>y do
:: if x>y then x=x-y else y=y-x
definition
func GCD-Algorithm -> Program of SCMPDS equals
(GBP:=0) ';' (GBP,3):=(GBP,1)
';' SubFrom(GBP,3,GBP,2) ';' while<>0(GBP,3, if>0(GBP,3,Load SubFrom(GBP,1,GBP,
2), Load SubFrom(GBP,2,GBP,1)) ';' (GBP,3):=(GBP,1) ';' SubFrom(GBP,3,GBP,2) );
coherence;
end;
theorem Th17:
for s being 0-started State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a,b,c be Int_position,i,d be Integer st
s.a=d &
s.b > 0 & s.c > 0 & s.DataLoc(d,i)=s.b-s.c &
(for t be 0-started State of SCMPDS,Q st t.b >
0 & t.c > 0 & t.a=d & t.DataLoc(d,i)=t.b-t.c & t.b<>t.c
holds IExec(I,Q,t).a=d &
I is_closed_on t,Q & I is_halting_on t,Q
& (t.b > t.c implies IExec(I,Q,t).b=t.b-t.c
& IExec(I,Q,t).c = t.c) & (t.b <= t.c
implies IExec(I,Q,t).c = t.c-t.b & IExec(I,Q,t)
.b=t.b) & IExec(I,Q,t).DataLoc(d,i)=
IExec(I,Q,t).b-IExec(I,Q,t).c)
holds IExec(while<>0(a,i,I),P,s).b = s.b gcd s.c
& IExec(while<>0(a,i,I),P,s).c = s.b gcd s.c
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, a,b,c
be Int_position, i,d be Integer;
set ci=DataLoc(s.a,i);
consider f be Function of product the_Values_of SCMPDS,NAT such that
A1: for s be State of SCMPDS holds (s.b = s.c implies f.s =0) & (s.b <>
s.c implies f.s=max(|.s.b.|,|.s.c.|)) by Th2;
deffunc F(State of SCMPDS) = f.$1;
set s1=IExec(while<>0(a,i,I),P,s), ss= s1;
defpred P[set] means
ex t be 0-started State of SCMPDS st t=$1 & t.b > 0 & t.c > 0
& t.b gcd t.c =s.b gcd s.c & t.DataLoc(d,i)=t.b-t.c;
assume that
A2: s.a=d and
A3: s.b > 0 and
A4: s.c > 0 and
A5: s.DataLoc(d,i)=s.b-s.c;
assume
A6: for t be 0-started State of SCMPDS,Q
st t.b > 0 & t.c > 0 & t.a=d & t.DataLoc(d,
i)=t.b-t.c & t.b<>t.c holds IExec(I,Q,t).a=d
& I is_closed_on t,Q & I is_halting_on
t,Q & (t.b > t.c implies IExec(I,Q,t).b=t.b-t.c &
IExec(I,Q,t).c = t.c)
& (t.b <= t.c implies IExec(I,Q,t).c = t.c-t.b & IExec(I,Q,t).b=t.b)
& IExec(I,Q,t).DataLoc(d,i)=IExec(I,Q,t).b-IExec(I,Q,t).c;
A7: now
let t be 0-started State of SCMPDS, Q;
assume that
A8: P[t] and
A9: t.a=s.a and
A10: t.ci <> 0;
set It=IExec(I,Q,t), t2=Initialize It, t1=t;
set x=IExec(I,Q,t).b, y=IExec(I,Q,t).c;
consider v be State of SCMPDS such that
A11: v=t and
A12: v.b > 0 and
A13: v.c > 0 and
A14: v.b gcd v.c =s.b gcd s.c and
A15: v.DataLoc(d,i)=v.b-v.c by A8;
A16: t.b > 0 by A11,A12;
A17: t.c > 0 by A11,A13;
A18: t.DataLoc(d,i)=v.b-v.c by A11,A15
.=t.b-v.c by A11
.=t.b-t.c by A11;
then
A19: t.b > t.c implies IExec(I,Q,t).b=t.b-t.c &
IExec(I,Q,t).c = t.c
by A2,A6,A9,A17;
A20: t.b<>t.c by A2,A10,A18;
hence IExec(I,Q,t).a=t.a by A2,A6,A9,A16,A17,A18;
thus I is_closed_on t,Q & I is_halting_on t,Q by A2,A6,A9,A16,A17,A18,A20;
A21: t.b <= t.c implies IExec(I,Q,t).c =t.c-t.b &
IExec(I,Q,t).b=t.b
by A2,A6,A9,A16,A18,A20;
A22: now
per cases;
suppose
A23: t.b > t.c;
then t.b-t.c > 0 by XREAL_1:50;
hence x > 0 by A2,A6,A9,A17,A18,A23;
thus y > 0 by A2,A6,A9,A17,A18,A23;
thus x gcd y = t.b gcd t.c by A16,A17,A19,A21,PREPOWER:97;
A24: x=t.b-t.c by A2,A6,A9,A17,A18,A23;
hereby
A25: max(t.b,t.c)=t.b by A23,XXREAL_0:def 10;
per cases by XXREAL_0:16;
suppose
max(x,y) = x;
hence max(x,y) < max(t.b,t.c) by A17,A24,A25,XREAL_1:44;
end;
suppose
max(x,y) = y;
hence max(x,y) < max(t.b,t.c) by A2,A6,A9,A17,A18,A23,A25;
end;
end;
end;
suppose
A26: t.b <= t.c;
hence x > 0 by A2,A6,A9,A16,A18,A20;
t.b < t.c by A20,A26,XXREAL_0:1;
then t.c-t.b > 0 by XREAL_1:50;
hence y > 0 by A2,A6,A9,A16,A18,A20,A26;
thus x gcd y =t.b gcd t.c by A16,A17,A19,A21,PREPOWER:97;
A27: y=t.c-t.b by A2,A6,A9,A16,A18,A20,A26;
A28: x=t.b by A2,A6,A9,A16,A18,A20,A26;
hereby
A29: max(t.b,t.c)=t.c by A26,XXREAL_0:def 10;
per cases by XXREAL_0:16;
suppose
max(x,y) = y;
hence max(x,y) < max(t.b,t.c) by A16,A27,A29,XREAL_1:44;
end;
suppose
max(x,y) = x;
hence max(x,y) < max(t.b,t.c) by A20,A26,A28,A29,XXREAL_0:1;
end;
end;
end;
end;
thus F(t2) < F(t1)
proof
t1.b <> t.c by A20;
then t1.b <> t1.c;
then
A30: F(t1)=max(|.t1.b.|,|.t1.c.|) by A1
.=max(|.t.b.|,|.t1.c.|)
.=max(|.t.b.|,|.t.c.|)
.=max( t.b,|.t.c.|) by A16,ABSVALUE:def 1
.=max(t.b,t.c) by A17,ABSVALUE:def 1;
then F(t1) >= t.b by XXREAL_0:25;
then
A31: F(t1) > 0 by A16;
per cases;
suppose
t2.b=t2.c;
hence thesis by A1,A31;
end;
suppose
t2.b<>t2.c;
then F(t2)=max(|.t2.b.|,|.t2.c.|) by A1
.=max(|.x.|,|.t2.c.|) by SCMPDS_5:15
.=max(|.x.|,|.y.|) by SCMPDS_5:15
.=max( x,|.y.|) by A22,ABSVALUE:def 1
.=max(x,y) by A22,ABSVALUE:def 1;
hence thesis by A22,A30;
end;
end;
A32: IExec(I,Q,t).DataLoc(d,i)= IExec(I,Q,t).b-IExec(I,Q,t).c
by A2,A6,A9,A16,A17,A18,A20;
thus P[Initialize It]
proof
take u=Initialize It;
thus u=Initialize It;
thus u.b > 0 & u.c > 0 by A22,SCMPDS_5:15;
thus u.b gcd u.c =It.b gcd u.c by SCMPDS_5:15
.=t.b gcd t.c by A22,SCMPDS_5:15
.=v.b gcd t.c by A11
.=s.b gcd s.c by A11,A14;
thus u.DataLoc(d,i)=x-y by A32,SCMPDS_5:15
.=u.b-y by SCMPDS_5:15
.=u.b-u.c by SCMPDS_5:15;
end;
end;
A33: for t be 0-started State of SCMPDS st P[t] holds
F(t)=0 iff t.ci = 0
proof
let t be 0-started State of SCMPDS;
assume P[t];
then consider v be State of SCMPDS such that
A34: v=t and
A35: v.b > 0 and
v.c > 0 and
v.b gcd v.c =s.b gcd s.c and
A36: v.DataLoc(d,i)=v.b-v.c;
A37: t.ci=v.b-v.c by A2,A34,A36
.=t.b-v.c by A34
.=t.b-t.c by A34;
hereby
assume
A38: F(t)=0;
now
assume t.b <> t.c;
then (t).b <> t.c;
then (t).b <> (t).c;
then
A39: F(t)=max(|.(t).b.|,|.(t).c.|) by A1
.=max(|.t.b.|,|.(t).c.|)
.=max(|.t.b.|,|.t.c.|);
t.b > 0 by A34,A35;
then |.t.b.| > 0 by COMPLEX1:47;
hence contradiction by A38,A39,XXREAL_0:25;
end;
hence t.ci=0 by A37;
end;
thus t.ci=0 implies F(t)=0 by A1,A37;
end;
A40: P[s] by A3,A4,A5;
A41: F(Initialize ss)=0 & P[Initialize ss] from WhileNEnd(A33,A40,A7);
then consider w be 0-started State of SCMPDS such that
A42: w=Initialize ss and
A43: w.b > 0 and
w.c > 0 and
A44: w.b gcd w.c =s.b gcd s.c and
A45: w.DataLoc(d,i)=w.b-w.c;
A46: (Initialize ss).ci = ss.ci by SCMPDS_5:15;
A47: (Initialize ss).b = ss.b by SCMPDS_5:15;
A48: (Initialize ss).c = ss.c by SCMPDS_5:15;
A49: w.b-w.c =s1.ci by A2,A42,A45,SCMPDS_5:15
.=0 by A33,A41,A46;
then
A50: |.w.b.|=|.w.b.| gcd |.w.c.| by NAT_D:32
.=s.b gcd s.c by A44,INT_2:34;
thus IExec(while<>0(a,i,I),P,s).b=ss.b
.=s.b gcd s.c by A42,A43,A50,A47,ABSVALUE:def 1;
thus IExec(while<>0(a,i,I),P,s).c =ss.c
.=s.b gcd s.c by A42,A43,A49,A50,A48,ABSVALUE:def 1;
end;
set i1= GBP:=0, i2= (GBP,3):=(GBP,1), i3= SubFrom(GBP,3,GBP,2), j1= Load
SubFrom(GBP,1,GBP,2), j2= Load SubFrom(GBP,2,GBP,1), IF= if>0(GBP,3,j1,j2), k1=
(GBP,3):=(GBP,1), k2= SubFrom(GBP,3,GBP,2), WB= IF ';' k1 ';' k2, WH= while<>0(
GBP,3,WB);
Lm10: card WB=6
proof
thus card WB=card (IF ';' k1)+1 by SCMP_GCD:4
.=card IF +1+1 by SCMP_GCD:4
.=card j1+card j2 +2+1+1 by SCMPDS_6:65
.= 1+card j2 +2+1+1 by COMPOS_1:54
.= 1+1+2+1+1 by COMPOS_1:54
.=6;
end;
Lm11: card WH=9
proof
thus card WH=6+3 by Lm10,Th8
.=9;
end;
theorem
card GCD-Algorithm=12
proof
thus card GCD-Algorithm=card (i1 ';' i2 ';' i3) + card WH by AFINSQ_1:17
.=card (i1 ';' i2) +1+ card WH by SCMP_GCD:4
.=2+1+ 9 by Lm11,SCMP_GCD:5
.=12;
end;
Lm12: for s being 0-started State of SCMPDS st s.GBP=0 holds
(s.a3 > 0 implies IExec(WB,P,s).a1=s.a1-s.a2 &
IExec(WB,P,s).a2 = s.a2)
& (s.a3 <= 0 implies IExec(WB,P,s).a2=s.a2-s.a1 &
IExec(WB,P,s).a1=s.a1) & IExec(WB,P,s).GBP=0
& IExec(WB,P,s).a3=IExec(WB,P,s).a1-IExec(WB,P,s).a2
proof
let s be 0-started State of SCMPDS;
set s1=IExec(IF,P,s),
s2=IExec(IF ';' k1,P,s), a=GBP, t0 = s,
Q0 = P;
A1: now
assume
A2: s1.GBP=0;
then
A3: DataLoc(s1.a,3)=intpos (0+3) by SCMP_GCD:1;
A4: s2.a3 =Exec(k1, s1).a3 by SCMPDS_5:41
.=s1.DataLoc(s1.a,1) by A3,SCMPDS_2:47
.=s1.intpos (0+1) by A2,SCMP_GCD:1;
1 <> |.s1.GBP+3.| by A2,ABSVALUE:def 1;
then
A5: a1 <> DataLoc(s1.GBP,3) by XTUPLE_0:1;
A6: s2.a1 =Exec(k1, s1).a1 by SCMPDS_5:41
.=s1.a1 by A5,SCMPDS_2:47;
2 <> |.s1.GBP+3.| by A2,ABSVALUE:def 1;
then
A7: a2 <> DataLoc(s1.GBP,3) by XTUPLE_0:1;
A8: s2.a2 =Exec(k1, s1).a2 by SCMPDS_5:41
.=s1.a2 by A7,SCMPDS_2:47;
0 <> |.s1.GBP+3.| by A2,ABSVALUE:def 1;
then
A9: a <> DataLoc(s1.GBP,3) by XTUPLE_0:1;
A10: s2.a =Exec(k1, s1).a by SCMPDS_5:41
.=0 by A2,A9,SCMPDS_2:47;
then
A11: DataLoc(s2.a,3)=intpos (0+3) by SCMP_GCD:1;
0 <> |.s2.GBP+3.| by A10,ABSVALUE:def 1;
then
A12: a <> DataLoc(s2.GBP,3) by XTUPLE_0:1;
thus IExec(WB,P,s).a =Exec(k2, s2).a by SCMPDS_5:41
.=0 by A10,A12,SCMPDS_2:50;
1 <> |.s2.GBP+3.| by A10,ABSVALUE:def 1;
then
A13: a1 <> DataLoc(s2.GBP,3) by XTUPLE_0:1;
thus
A14: IExec(WB,P,s).a1 =Exec(k2, s2).a1 by SCMPDS_5:41
.=s1.a1 by A6,A13,SCMPDS_2:50;
2 <> |.s2.GBP+3.| by A10,ABSVALUE:def 1;
then
A15: a2 <> DataLoc(s2.GBP,3) by XTUPLE_0:1;
thus
A16: IExec(WB,P,s).a2 =Exec(k2, s2).a2 by SCMPDS_5:41
.=s1.a2 by A8,A15,SCMPDS_2:50;
thus IExec(WB,P,s).a3 =Exec(k2, s2).a3 by SCMPDS_5:41
.=s2.a3-s2.DataLoc(s2.a,2) by A11,SCMPDS_2:50
.=IExec(WB,P,s).a1-IExec(WB,P,s).a2
by A10,A8,A4,A14,A16,SCMP_GCD:1;
end;
set s0=s, m1=SubFrom(GBP,1,GBP,2), m2=SubFrom(GBP,2,GBP,1);
assume
A17: s.GBP=0;
then
A18: s0.a=0;
A19: DataLoc(s.a,3)=intpos(0+3) by A17,SCMP_GCD:1;
A20: now
2 <> |.s0.GBP+1.| by A18,ABSVALUE:def 1;
then
A21: a2 <> DataLoc(s0.GBP,1) by XTUPLE_0:1;
0 <> |.s0.GBP+1.| by A18,ABSVALUE:def 1;
then
A22: a <> DataLoc(s0.GBP,1) by XTUPLE_0:1;
assume
A23: s.a3 > 0;
hence s1.a=IExec(j1,P,s).a by A19,SCMPDS_6:73
.=Exec(m1, s0).a by SCMPDS_5:40
.=0 by A18,A22,SCMPDS_2:50;
A24: DataLoc(s0.a,1)=intpos (0+1) by A18,SCMP_GCD:1;
thus s1.a1=IExec(j1,P,s).a1 by A19,A23,SCMPDS_6:73
.=Exec(m1, s0).a1 by SCMPDS_5:40
.=s0.a1-s0.DataLoc(s0.a,2) by A24,SCMPDS_2:50
.=s0.a1-s0.intpos(0+2) by A18,SCMP_GCD:1
.=s.a1-s.a2;
thus s1.a2=IExec(j1,P,s).a2 by A19,A23,SCMPDS_6:73
.=Exec(m1, s0).a2 by SCMPDS_5:40
.=s.a2 by A21,SCMPDS_2:50;
end;
hence
s.a3 > 0 implies IExec(WB,P,s).a1=s.a1-s.a2 &
IExec(WB,P,s).a2 = s.a2 by A1;
A25: now
1 <> |.s0.GBP+2.| by A18,ABSVALUE:def 1;
then
A26: a1 <> DataLoc(s0.GBP,2) by XTUPLE_0:1;
0 <> |.s0.GBP+2.| by A18,ABSVALUE:def 1;
then
A27: a <> DataLoc(s0.GBP,2) by XTUPLE_0:1;
assume
A28: s.a3 <= 0;
hence s1.a=IExec(j2,P,s).a by A19,SCMPDS_6:74
.=Exec(m2, s0).a by SCMPDS_5:40
.=0 by A18,A27,SCMPDS_2:50;
A29: DataLoc(s0.a,2)=intpos (0+2) by A18,SCMP_GCD:1;
thus s1.a2=IExec(j2,P,s).a2 by A19,A28,SCMPDS_6:74
.=Exec(m2, s0).a2 by SCMPDS_5:40
.=s0.a2-s0.DataLoc(s0.a,1) by A29,SCMPDS_2:50
.=s0.a2-s0.intpos(0+1) by A18,SCMP_GCD:1
.=s.a2-s.a1;
thus s1.a1=IExec(j2,P,s).a1 by A19,A28,SCMPDS_6:74
.=Exec(m2, s0).a1 by SCMPDS_5:40
.=s.a1 by A26,SCMPDS_2:50;
end;
hence s.a3 <= 0 implies IExec(WB,P,s).a2=s.a2-s.a1
& IExec(WB,P,s).a1 = s.a1 by A1;
now
per cases;
suppose
s.a3 > 0;
hence s1.a=0 by A20;
end;
suppose
s.a3 <= 0;
hence s1.a=0 by A25;
end;
end;
hence thesis by A1;
end;
Lm13: for s being 0-started State of SCMPDS
st s.GBP=0 & s.a1 > 0 & s.a2 > 0 & s.a3=s.a1
-s.a2 holds IExec(WH,P,s).a1 = s.a1 gcd s.a2
& IExec(WH,P,s).a2 = s.a1 gcd s.a2 &
WH is_closed_on s,P & WH is_halting_on s,P
proof
set a=GBP;
let s be 0-started State of SCMPDS;
A1: DataLoc(0,3)=intpos(0+3) by SCMP_GCD:1;
A2: now
let t be 0-started State of SCMPDS, Q;
assume that
t.a1 > 0 and
t.a2 > 0 and
A3: t.a=0 and
A4: t.DataLoc(0,3)=t.a1-t.a2 and
t.a1<>t.a2;
thus IExec(WB,Q,t).a=0 by A3,Lm12;
thus WB is_closed_on t,Q by SCMPDS_6:20;
thus WB is_halting_on t,Q by SCMPDS_6:21;
hereby
assume t.a1 > t.a2;
then t.a3 > 0 by A1,A4,XREAL_1:50;
hence IExec(WB,Q,t).a1=t.a1-t.a2 &
IExec(WB,Q,t).a2 = t.a2 by A3,Lm12;
end;
hereby
assume t.a1 <= t.a2;
then t.a3 <= 0 by A1,A4,XREAL_1:47;
hence IExec(WB,Q,t).a2=t.a2-t.a1 &
IExec(WB,Q,t).a1 = t.a1 by A3,Lm12;
end;
thus IExec(WB,Q,t).DataLoc(0,3)=
IExec(WB,Q,t).a1-IExec(WB,Q,t).a2
by A1,A3,Lm12;
end;
assume
A5: s.a=0 & s.a1 > 0 & s.a2 > 0 & s.a3=s.a1-s.a2;
hence IExec(WH,P,s).a1 = s.a1 gcd s.a2
& IExec(WH,P,s).a2 = s.a1 gcd s.a2 by A1,A2,Th17;
thus WH is_closed_on s,P & WH is_halting_on s,P
by A5,A1,A2,Lm10,Th16;
end;
set GA=i1 ';' i2 ';' i3 ';' WH;
Lm14: for s being 0-started State of SCMPDS st s.a1 > 0 & s.a2 > 0
holds IExec(GA,P,s).a1
= s.a1 gcd s.a2 & IExec(GA,P,s).a2 = s.a1 gcd s.a2 &
GA is_closed_on s,P & GA is_halting_on s,P
proof
let s be 0-started State of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume
A2: s.a1 > 0 & s.a2 > 0;
set t0=s, Q0 = P,
t1=IExec(i1 ';' i2 ';' i3,P,s),
t2=IExec(i1 ';' i2,P,s),
Q1 = P,
t3=Exec(i1, t0), a=GBP;
A3: t3.a1=t0.a1 by AMI_3:10,SCMPDS_2:45
.=s.a1;
A4: t3.a=0 by SCMPDS_2:45;
then
A5: DataLoc(t3.a,3)=intpos (0+3) by SCMP_GCD:1;
1 <> |.t3.GBP+3.| by A4,ABSVALUE:def 1;
then
A6: a1 <> DataLoc(t3.GBP,3) by XTUPLE_0:1;
A7: t2.a1=Exec(i2,t3).a1 by SCMPDS_5:42
.=s.a1 by A3,A6,SCMPDS_2:47;
A8: t3.a2=t0.a2 by AMI_3:10,SCMPDS_2:45
.=s.a2;
A9: t2.a3=Exec(i2,t3).a3 by SCMPDS_5:42
.=t3.DataLoc(t3.a,1) by A5,SCMPDS_2:47
.=s.a1 by A4,A3,SCMP_GCD:1;
2 <> |.t3.GBP+3.| by A4,ABSVALUE:def 1;
then
A10: a2 <> DataLoc(t3.GBP,3) by XTUPLE_0:1;
A11: t2.a2=Exec(i2,t3).a2 by SCMPDS_5:42
.=s.a2 by A8,A10,SCMPDS_2:47;
0 <> |.t3.GBP+3.| by A4,ABSVALUE:def 1;
then
A12: a <> DataLoc(t3.GBP,3) by XTUPLE_0:1;
A13: t2.a=Exec(i2,t3).a by SCMPDS_5:42
.=0 by A4,A12,SCMPDS_2:47;
then
A14: DataLoc(t2.a,3)=intpos (0+3) by SCMP_GCD:1;
0 <> |.t2.GBP+3.| by A13,ABSVALUE:def 1;
then
A15: a <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
A16: t1.a=Exec(i3,t2).a by SCMPDS_5:41
.=0 by A13,A15,SCMPDS_2:50;
1 <> |.t2.GBP+3.| by A13,ABSVALUE:def 1;
then
A17: a1 <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
A18: t1.a1=Exec(i3,t2).a1 by SCMPDS_5:41
.=s.a1 by A7,A17,SCMPDS_2:50;
2 <> |.t2.GBP+3.| by A13,ABSVALUE:def 1;
then
A19: a2 <> DataLoc(t2.GBP,3) by XTUPLE_0:1;
A20: t1.a2=Exec(i3,t2).a2 by SCMPDS_5:41
.=s.a2 by A11,A19,SCMPDS_2:50;
A21: (Initialize t1).a1 = t1.a1 by SCMPDS_5:15;
A22: (Initialize t1).a2 = t1.a2 by SCMPDS_5:15;
A23: t1.a3=Exec(i3,t2).a3 by SCMPDS_5:41
.=t2.a3-t2.DataLoc(t2.a,2) by A14,SCMPDS_2:50
.=t1.a1-t1.a2 by A13,A11,A9,A18,A20,SCMP_GCD:1;
A24: (Initialize t1).GBP = t1.GBP by SCMPDS_5:15;
A25: (Initialize t1).a3 = t1.a3 by SCMPDS_5:15;
A26: WH is_closed_on Initialize t1,P &
WH is_halting_on Initialize t1,P
by A2,A16,A18,A20,Lm13,A21,A22,A23,A24,A25;
A27: WH is_closed_on t1,Q1
proof
for k being Nat holds
IC Comput(Q1+*stop WH,Initialize Initialize t1,k) in dom stop WH
by A26,SCMPDS_6:def 2;
hence thesis by SCMPDS_6:def 2;
end;
A28: WH is_halting_on t1,Q1
proof
Q1+*stop WH halts_on Initialize Initialize t1 by A26,SCMPDS_6:def 3;
hence thesis by SCMPDS_6:def 3;
end;
IExec(WH,Q1,Initialize t1).a1 = t1.a1 gcd t1.a2
by A2,A16,A18,A20,A23,Lm13,A21,A22,A25,A24;
hence IExec(GA,P,s).a1=s.a1 gcd s.a2 by A18,A20,A27,A28,SCPISORT:7;
IExec(WH,Q1,Initialize t1).a2 = t1.a1 gcd t1. a2
by A2,A16,A18,A20,A23,Lm13,A21,A22,A25,A24;
hence IExec(GA,P,s).a2=s.a1 gcd s.a2 by A18,A20,A27,A28,SCPISORT:7;
thus thesis by A27,A1,A28,SCPISORT:9;
end;
theorem :: SCMP_GCD:18
for s being 0-started State of SCMPDS,x, y being Integer
st s.intpos 1 = x & s.intpos 2 = y & x > 0 & y > 0
holds IExec(GCD-Algorithm,P,s).intpos 1 = x gcd y &
IExec(GCD-Algorithm,P,s).intpos 2 = x gcd y
& GCD-Algorithm is_closed_on s,P &
GCD-Algorithm is_halting_on s,P by Lm14;