:: Bubble Sort on SCM+FSA
:: by JingChao Chen and Yatsuka Nakamura
::
:: Received June 17, 1998
:: Copyright (c) 1998-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, EXTPRO_1, SCMFSA_2, AMI_1, SUBSET_1, SCMFSA7B, SCMFSA8C,
AMI_3, CARD_1, AMISTD_2, SCMFSA8B, TURING_1, FSM_1, GRAPHSP, FUNCT_1,
PARTFUN1, COMPLEX1, FUNCT_4, ARYTM_3, SF_MASTR, SCMFSA6C, SCMFSA6B,
FUNCOP_1, RELAT_1, TARSKI, XBOOLE_0, XXREAL_0, AMISTD_1, CIRCUIT2, NAT_1,
STRUCT_0, ARYTM_1, INT_1, FINSEQ_1, FINSEQ_2, SCMFSA6A, CLASSES1,
VALUED_0, MSUALG_1, SCM_HALT, SCMBSORT, COMPOS_1;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, NAT_1, INT_1, RELAT_1, FINSEQ_1, FUNCT_1, COMPLEX1,
FUNCT_2, PBOOLE, FUNCT_4, FINSEQ_2, FUNCT_7, STRUCT_0, MEMSTR_0,
COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, FUNCOP_1,
FINSUB_1, CARD_3, PARTFUN1, SCMFSA6B, SCMFSA6C, SCMFSA6A, SF_MASTR,
SCMFSA8B, SCMFSA8C, CLASSES1, RFINSEQ, SCMFSA7B, NAT_D, SCM_HALT,
XXREAL_0, SCMFSA_M;
constructors SETWISEO, XXREAL_0, REAL_1, AMI_3, SCMFSA6A, SF_MASTR, SCMFSA6B,
SCMFSA6C, SCMFSA8A, SCMFSA8B, SCMFSA8C, SCM_HALT, SCMFSA7B, AMISTD_2,
NAT_D, CLASSES1, RELSET_1, DOMAIN_1, SFMASTR1, AMISTD_1, PBOOLE,
PRE_POLY, SCMFSA_3, SCMFSA_7, SCMFSA_9, SCMFSA_2, XXREAL_2, MEMSTR_0,
SCMFSA_1, SCMFSA_M, FUNCT_7, COMPOS_2, SCMFSA_X, SCMFSA9A;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1,
INT_1, SCMFSA_2, SCMFSA6C, SCMFSA7B, FINSET_1, SCMFSA8A, SCMFSA8B,
SCMFSA_9, SCM_HALT, STRUCT_0, VALUED_0, ORDINAL1, RELAT_1, SCMFSA10,
AMISTD_2, SCMFSA6A, COMPOS_1, SFMASTR1, FUNCT_4, EXTPRO_1, MEMSTR_0,
AMI_3, COMPOS_0, AMISTD_1, SCMFSA_M, SCMFSA8C, SCMFSA9A;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions EXTPRO_1, SCM_HALT;
equalities FUNCOP_1, EXTPRO_1, MEMSTR_0, SCMFSA_2, SCMFSA_M;
expansions EXTPRO_1, MEMSTR_0;
theorems SF_MASTR, FUNCT_1, FUNCT_7, FUNCOP_1, RELAT_1, ZFMISC_1, SCMFSA6A,
FUNCT_4, FINSEQ_3, ENUMSET1, NAT_1, TARSKI, INT_1, PARTFUN1, GRFUNC_1,
RFINSEQ, SCMFSA_2, SCMFSA7B, SCMFSA8B, SCMFSA8A, SCMFSA8C, SCMFSA6C,
SCM_HALT, ABSVALUE, FINSEQ_4, XBOOLE_0, XBOOLE_1, SCMFSA9A, XREAL_1,
XXREAL_0, NAT_D, CLASSES1, PBOOLE, AFINSQ_1, COMPOS_1, EXTPRO_1,
MEMSTR_0, AMI_2, COMPOS_0, SCMFSA_M, AMISTD_1;
schemes NAT_1;
begin :: Preliminaries
reserve p for preProgram of SCM+FSA,
ic for Instruction of SCM+FSA,
i,j,k for Nat,
fa,f for FinSeq-Location,
a,b,da,db for Int-Location,
la,lb for Nat;
reserve p1,p2,q for Instruction-Sequence of SCM+FSA;
set SA0 = Start-At(0,SCM+FSA);
::$CT
theorem Th1:
for s be State of SCM+FSA,f be FinSeq-Location,a,b be Int-Location
holds Exec(b:=(f,a), s).b = (s.f)/.|.s.a.|
proof
let s be State of SCM+FSA,f be FinSeq-Location,a,b be Int-Location;
ex k be Nat st ( k = |.s.a.|)&( Exec(b:=(f,a), s)
.b = (s.f)/.k) by SCMFSA_2:72;
hence thesis;
end;
theorem Th2:
for s be State of SCM+FSA,f be FinSeq-Location,a,b be Int-Location
holds Exec((f,a):=b, s).f = s.f+*(|.s.a.|,s.b)
proof
let s be State of SCM+FSA,f be FinSeq-Location,a,b be Int-Location;
ex k be Nat st ( k = |.s.a.|)&( Exec((f,a):=b, s)
.f = s.f+*(k,s.b)) by SCMFSA_2:73;
hence thesis;
end;
theorem Th3:
for s be State of SCM+FSA,f be FinSeq-Location,m,n be Nat,
a be Int-Location
st m<>n+1 holds Exec(intloc m:=(f,a), Initialized s).intloc (n+1)
=s.intloc (n+1)
proof
let s be State of SCM+FSA,f be FinSeq-Location,m,n be Nat,
a be Int-Location;
assume m<>n+1;
then intloc m<>intloc (n+1) by SCMFSA_2:101;
hence Exec(intloc m:=(f,a), Initialized s).intloc (n+1)
=(Initialized s).intloc (n+1) by SCMFSA_2:72
.=s.intloc (n+1) by SCMFSA_M:37;
end;
theorem Th4:
for s be State of SCM+FSA,m,n be Nat,a be Int-Location
st m<>n+1 holds Exec(intloc m:=a, Initialized s).intloc (n+1) =s.intloc (n+1)
proof
let s be State of SCM+FSA,m,n be Nat,a be Int-Location;
assume m<>n+1;
then intloc m<>intloc (n+1) by SCMFSA_2:101;
hence Exec(intloc m:=a, Initialized s).intloc (n+1)
=(Initialized s).intloc (n+1) by SCMFSA_2:63
.=s.intloc (n+1) by SCMFSA_M:37;
end;
theorem Th5:
for p being Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA, f be FinSeq-Location, a be read-write Int-Location
holds IExec(Stop SCM+FSA,p,s).a =s.a &
IExec(Stop SCM+FSA,p,s).f =s.f
proof
let p being Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA,f be FinSeq-Location,a be read-write Int-Location;
A1: Initialized s
= s +* (((intloc 0) .--> 1) +* Start-At(0,SCM+FSA))
.= Initialize(s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
A2: IExec(Stop SCM+FSA,p,s)
= Initialize (s +* ((intloc 0) .--> 1)) by A1,SCMFSA8C:14
.=Initialized s by A1;
hence IExec(Stop SCM+FSA,p,s).a =s.a by SCMFSA_M:37;
thus thesis by A2,SCMFSA_M:37;
end;
reserve n for Nat;
theorem Th6:
ic in rng p & (ic = a:=b or ic = AddTo(a, b) or ic = SubFrom(a, b) or
ic = MultBy(a, b) or ic = Divide(a, b))
implies a in UsedILoc p & b in UsedILoc p
proof
assume that
A1: ic in rng p and
A2: ic = a:=b or ic = AddTo(a, b) or ic = SubFrom(a, b) or ic = MultBy(
a, b) or ic = Divide(a, b);
A3: UsedIntLoc ic = {a, b} by A2,SF_MASTR:14;
UsedIntLoc ic c= UsedILoc p by A1,SF_MASTR:19;
hence thesis by A3,ZFMISC_1:32;
end;
theorem Th7:
ic in rng p & (ic = a=0_goto la or ic = a>0_goto la)
implies a in UsedILoc p
proof
assume that
A1: ic in rng p and
A2: ic = a=0_goto la or ic = a>0_goto la;
A3: UsedIntLoc ic = {a} by A2,SF_MASTR:16;
UsedIntLoc ic c= UsedILoc p by A1,SF_MASTR:19;
hence thesis by A3,ZFMISC_1:31;
end;
theorem Th8:
ic in rng p & ( ic = b := (fa, a) or ic = (fa, a) := b)
implies a in UsedILoc p & b in UsedILoc p
proof
assume that
A1: ic in rng p and
A2: ic = b := (fa, a) or ic = (fa, a) := b;
A3: UsedIntLoc ic = {a,b} by A2,SF_MASTR:17;
UsedIntLoc ic c= UsedILoc p by A1,SF_MASTR:19;
hence thesis by A3,ZFMISC_1:32;
end;
theorem Th9:
ic in rng p & ( ic = b := (fa, a) or ic = (fa, a) := b)
implies fa in UsedI*Loc p
proof
assume that
A1: ic in rng p and
A2: ic = b := (fa, a) or ic = (fa, a) := b;
A3: UsedInt*Loc ic = {fa} by A2,SF_MASTR:33;
UsedInt*Loc ic c= UsedI*Loc p by A1,SF_MASTR:35;
hence thesis by A3,ZFMISC_1:31;
end;
theorem Th10:
ic in rng p & (ic = a :=len fa or ic = fa :=<0,...,0>a)
implies a in UsedILoc p
proof
assume that
A1: ic in rng p and
A2: ic = a :=len fa or ic = fa :=<0,...,0>a;
A3: UsedIntLoc ic = {a} by A2,SF_MASTR:18;
UsedIntLoc ic c= UsedILoc p by A1,SF_MASTR:19;
hence thesis by A3,ZFMISC_1:31;
end;
theorem Th11:
ic in rng p & (ic = a :=len fa or ic = fa :=<0,...,0>a)
implies fa in UsedI*Loc p
proof
assume that
A1: ic in rng p and
A2: ic = a :=len fa or ic = fa :=<0,...,0>a;
A3: UsedInt*Loc ic = {fa} by A2,SF_MASTR:34;
UsedInt*Loc ic c= UsedI*Loc p by A1,SF_MASTR:35;
hence thesis by A3,ZFMISC_1:31;
end;
theorem Th12:
for t being FinPartState of SCM+FSA,p being Program of SCM+FSA,
x being set st dom t c= Int-Locations \/ FinSeq-Locations &
x in dom t \/ UsedI*Loc p \/ UsedILoc p
holds x is Int-Location or x is FinSeq-Location
proof
let t be FinPartState of SCM+FSA,p be Program of SCM+FSA,x be set;
set D1=UsedI*Loc p;
set D2=UsedILoc p;
assume that
A1: dom t c= Int-Locations \/ FinSeq-Locations and
A2: x in dom t \/ D1 \/ D2;
x in dom t \/ D1 or x in D2 by A2,XBOOLE_0:def 3;
then
A3: x in dom t or x in D1 or x in D2 by XBOOLE_0:def 3;
per cases by A1,A3,XBOOLE_0:def 3;
suppose x in Int-Locations;
hence thesis by AMI_2:def 16;
end;
suppose x in FinSeq-Locations;
hence thesis by SCMFSA_2:def 5;
end;
suppose x in D1;
then x in FinSeq-Locations;
hence thesis by SCMFSA_2:def 5;
end;
suppose x in D2;
then x in Int-Locations;
hence thesis by AMI_2:def 16;
end;
end;
theorem Th13:
for i,k being Nat,t being FinPartState of SCM+FSA,
p being Program of SCM+FSA, s1,s2 being State of SCM+FSA
st k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations &
(for j holds IC Comput(p1,s1,j) in dom p &
IC Comput(p2,s2,j) in dom p) &
Comput(p1,s1,k).IC SCM+FSA = Comput(p2,s2,k).IC SCM+FSA &
Comput(p1,s1,k) |(dom t \/ UsedI*Loc p \/ UsedILoc p) =
Comput(p2,s2,k) |(dom t \/ UsedI*Loc p \/ UsedILoc p) holds
Comput(p1,s1,i).IC SCM+FSA = Comput(p2,s2,i).IC SCM+FSA &
Comput(p1,s1,i) |(dom t \/ UsedI*Loc p \/ UsedILoc p) =
Comput(p2,s2,i) |(dom t \/ UsedI*Loc p \/ UsedILoc p)
proof
let i,k;
let t be FinPartState of SCM+FSA,p be Program of SCM+FSA,
s1,s2 be State of SCM+FSA;
set Dloc=dom t \/ UsedI*Loc p \/ UsedILoc p;
assume that
A1: k <= i and
A2: p c= p1 and
A3: p c= p2 and
A4: dom t c= Int-Locations \/ FinSeq-Locations and
A5: for j holds IC Comput(p1,s1,j) in dom p & IC Comput(
p2,s2,j) in
dom p and
A6: Comput(p1,s1,k).IC SCM+FSA = Comput(p2,s2,k).IC
SCM+FSA and
A7: Comput(p1,s1,k) |Dloc = Comput(p2,s2,k)|Dloc;
consider m being Nat such that
A8: i=k+m by A1,NAT_1:10;
reconsider m as Nat;
A9: i=k+m by A8;
A10: UsedILoc p c= Dloc by XBOOLE_1:7;
Dloc=dom t \/ UsedILoc p \/ UsedI*Loc p by XBOOLE_1:4;
then
A11: UsedI*Loc p c= Dloc by XBOOLE_1:7;
defpred P[Nat] means
Comput(p1, s1,k+$1).IC SCM+FSA = Comput(p2, s2,k+
$1).IC SCM+FSA &
Comput(p1, s1,k+$1) |Dloc = Comput(p2, s2,k+$1)|
Dloc;
A12: P[ 0] by A6,A7;
A13: now
let m be Nat;
assume
A14: P[m];
set sk1= Comput(p1, s1,k+m);
set sk11= Comput(p1, s1,k+(m+1));
set i1=CurInstr(p1,sk1);
set sk2= Comput(p2, s2,k+m);
set sk12= Comput(p2, s2,k+(m+1));
set i2=CurInstr(p2,sk2);
A15: IC sk1 in dom p by A5;
A16: p2/.IC sk2 = p2.IC sk2 by PBOOLE:143;
A17: p1/.IC sk1 = p1.IC sk1 by PBOOLE:143;
i1 =p.IC sk1 by A2,A15,A17,GRFUNC_1:2;
then
A18: i1 in rng p by A15,FUNCT_1:def 3;
A19: i2 =(p2 |dom p).IC sk2 by A16,A5,FUNCT_1:49
.= (p1 |dom p).IC sk1 by A2,A3,A14,GRFUNC_1:33
.=i1 by A17,A5,FUNCT_1:49;
A20: sk11= Comput(p1, s1,k+m+1)
.=Following(p1,sk1) by EXTPRO_1:3
.= Exec(i1,sk1);
A21: sk12= Comput(p2, s2,k+m+1)
.=Following(p2,sk2) by EXTPRO_1:3
.= Exec(i2,sk2);
A22: dom sk11 = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom sk12 by PARTFUN1:def 2;
InsCode i1 = 0 or ... or InsCode i1 = 12 by SCMFSA_2:16;
then per cases;
suppose InsCode i1 = 0;
then
A23: i1=halt SCM+FSA by SCMFSA_2:95;
then sk11=sk1 by A20,EXTPRO_1:def 3;
hence P[m+1] by A14,A19,A21,A23,EXTPRO_1:def 3;
end;
suppose InsCode i1 = 1;
then consider da,db such that
A24: i1 = da:=db by SCMFSA_2:30;
A25: sk11.IC SCM+FSA= IC sk1 + 1 by A20,A24,SCMFSA_2:63
.= sk12.IC SCM+FSA by A14,A19,A21,A24,SCMFSA_2:63;
now
let x be set;
assume
A26: x in Dloc;
per cases by A4,A26,Th12;
suppose
A27: x is Int-Location;
per cases;
suppose
A28: x = da;
then
A29: sk12.x=sk2.db by A19,A21,A24,SCMFSA_2:63;
A30: db in UsedILoc p by A18,A24,Th6;
then sk1.db=(sk2 | Dloc).db by A10,A14,FUNCT_1:49
.=sk2.db by A10,A30,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A24,A28,A29,SCMFSA_2:63;
end;
suppose
A31: x<> da;
then
A32: sk12.x=sk2.x by A19,A21,A24,A27,SCMFSA_2:63;
sk1.x=(sk2 | Dloc).x by A14,A26,FUNCT_1:49
.=sk2.x by A26,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A24,A27,A31,A32,SCMFSA_2:63;
end;
end;
suppose
A33: x is FinSeq-Location;
then
A34: sk12.x=sk2.x by A19,A21,A24,SCMFSA_2:63;
sk1.x=(sk2 | Dloc).x by A14,A26,FUNCT_1:49
.=sk2.x by A26,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A24,A33,A34,SCMFSA_2:63;
end;
end;
hence P[m+1] by A22,A25,FUNCT_1:96;
end;
suppose InsCode i1 = 2;
then consider da,db such that
A35: i1 = AddTo(da,db) by SCMFSA_2:31;
A36: sk11.IC SCM+FSA= IC sk1 + 1 by A20,A35,SCMFSA_2:64
.= sk12.IC SCM+FSA by A14,A19,A21,A35,SCMFSA_2:64;
now
let x be set;
assume
A37: x in Dloc;
per cases by A4,A37,Th12;
suppose
A38: x is Int-Location;
per cases;
suppose
A39: x = da;
then
A40: sk12.x=sk2.da+sk2.db by A19,A21,A35,SCMFSA_2:64;
A41: da in UsedILoc p by A18,A35,Th6;
then
A42: sk1.da=(sk2 | Dloc).da by A10,A14,FUNCT_1:49
.=sk2.da by A10,A41,FUNCT_1:49;
A43: db in UsedILoc p by A18,A35,Th6;
then sk1.db=(sk2 | Dloc).db by A10,A14,FUNCT_1:49
.=sk2.db by A10,A43,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A35,A39,A40,A42,SCMFSA_2:64;
end;
suppose
A44: x<> da;
then
A45: sk12.x=sk2.x by A19,A21,A35,A38,SCMFSA_2:64;
sk1.x=(sk2 | Dloc).x by A14,A37,FUNCT_1:49
.=sk2.x by A37,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A35,A38,A44,A45,SCMFSA_2:64;
end;
end;
suppose
A46: x is FinSeq-Location;
then
A47: sk12.x=sk2.x by A19,A21,A35,SCMFSA_2:64;
sk1.x=(sk2 | Dloc).x by A14,A37,FUNCT_1:49
.=sk2.x by A37,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A35,A46,A47,SCMFSA_2:64;
end;
end;
hence P[m+1] by A22,A36,FUNCT_1:96;
end;
suppose InsCode i1 = 3;
then consider da,db such that
A48: i1 = SubFrom(da,db) by SCMFSA_2:32;
A49: sk11.IC SCM+FSA= IC sk1 + 1 by A20,A48,SCMFSA_2:65
.= sk12.IC SCM+FSA by A14,A19,A21,A48,SCMFSA_2:65;
now
let x be set;
assume
A50: x in Dloc;
per cases by A4,A50,Th12;
suppose
A51: x is Int-Location;
per cases;
suppose
A52: x = da;
then
A53: sk12.x=sk2.da-sk2.db by A19,A21,A48,SCMFSA_2:65;
A54: da in UsedILoc p by A18,A48,Th6;
then
A55: sk1.da=(sk2 | Dloc).da by A10,A14,FUNCT_1:49
.=sk2.da by A10,A54,FUNCT_1:49;
A56: db in UsedILoc p by A18,A48,Th6;
then sk1.db=(sk2 | Dloc).db by A10,A14,FUNCT_1:49
.=sk2.db by A10,A56,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A48,A52,A53,A55,SCMFSA_2:65;
end;
suppose
A57: x<> da;
then
A58: sk12.x=sk2.x by A19,A21,A48,A51,SCMFSA_2:65;
sk1.x=(sk2 | Dloc).x by A14,A50,FUNCT_1:49
.=sk2.x by A50,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A48,A51,A57,A58,SCMFSA_2:65;
end;
end;
suppose
A59: x is FinSeq-Location;
then
A60: sk12.x=sk2.x by A19,A21,A48,SCMFSA_2:65;
sk1.x=(sk2 | Dloc).x by A14,A50,FUNCT_1:49
.=sk2.x by A50,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A48,A59,A60,SCMFSA_2:65;
end;
end;
hence P[m+1] by A22,A49,FUNCT_1:96;
end;
suppose InsCode i1 = 4;
then consider da,db such that
A61: i1 = MultBy(da,db) by SCMFSA_2:33;
A62: sk11.IC SCM+FSA= IC sk1 + 1 by A20,A61,SCMFSA_2:66
.= sk12.IC SCM+FSA by A14,A19,A21,A61,SCMFSA_2:66;
now
let x be set;
assume
A63: x in Dloc;
per cases by A4,A63,Th12;
suppose
A64: x is Int-Location;
per cases;
suppose
A65: x = da;
then
A66: sk12.x=sk2.da*sk2.db by A19,A21,A61,SCMFSA_2:66;
A67: da in UsedILoc p by A18,A61,Th6;
then
A68: sk1.da=(sk2 | Dloc).da by A10,A14,FUNCT_1:49
.=sk2.da by A10,A67,FUNCT_1:49;
A69: db in UsedILoc p by A18,A61,Th6;
then sk1.db=(sk2 | Dloc).db by A10,A14,FUNCT_1:49
.=sk2.db by A10,A69,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A61,A65,A66,A68,SCMFSA_2:66;
end;
suppose
A70: x<> da;
then
A71: sk12.x=sk2.x by A19,A21,A61,A64,SCMFSA_2:66;
sk1.x=(sk2 | Dloc).x by A14,A63,FUNCT_1:49
.=sk2.x by A63,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A61,A64,A70,A71,SCMFSA_2:66;
end;
end;
suppose
A72: x is FinSeq-Location;
then
A73: sk12.x=sk2.x by A19,A21,A61,SCMFSA_2:66;
sk1.x=(sk2 | Dloc).x by A14,A63,FUNCT_1:49
.=sk2.x by A63,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A61,A72,A73,SCMFSA_2:66;
end;
end;
hence P[m+1] by A22,A62,FUNCT_1:96;
end;
suppose InsCode i1 = 5;
then consider da,db such that
A74: i1 = Divide(da,db) by SCMFSA_2:34;
A75: sk11.IC SCM+FSA= IC sk1 + 1 by A20,A74,SCMFSA_2:67
.= sk12.IC SCM+FSA by A14,A19,A21,A74,SCMFSA_2:67;
now
let x be set;
assume
A76: x in Dloc;
per cases by A4,A76,Th12;
suppose
A77: x is Int-Location;
A78: da in UsedILoc p by A18,A74,Th6;
then
A79: sk1.da=(sk2 | Dloc).da by A10,A14,FUNCT_1:49
.=sk2.da by A10,A78,FUNCT_1:49;
A80: db in UsedILoc p by A18,A74,Th6;
then
A81: sk1.db=(sk2 | Dloc).db by A10,A14,FUNCT_1:49
.=sk2.db by A10,A80,FUNCT_1:49;
A82: sk1.x=(sk2 | Dloc).x by A14,A76,FUNCT_1:49
.=sk2.x by A76,FUNCT_1:49;
now
per cases;
suppose
A83: da <> db;
per cases;
suppose
A84: x = da;
then sk11.x=sk1.da div sk1.db by A20,A74,A83,SCMFSA_2:67;
hence sk11.x=sk12.x by A19,A21,A74,A79,A81,A83,A84,
SCMFSA_2:67;
end;
suppose
A85: x = db;
then sk11.x=sk1.da mod sk1.db by A20,A74,SCMFSA_2:67;
hence sk11.x=sk12.x by A19,A21,A74,A79,A81,A85,SCMFSA_2:67;
end;
suppose
A86: x <> da & x <> db;
then sk11.x=sk1.x by A20,A74,A77,SCMFSA_2:67;
hence sk11.x=sk12.x by A19,A21,A74,A77,A82,A86,SCMFSA_2:67;
end;
end;
suppose
A87: da = db;
now
per cases;
case
A88: x = da;
then sk11.x=sk1.da mod sk1.da by A20,A74,A87,SCMFSA_2:68;
hence sk11.x=sk12.x by A19,A21,A74,A79,A87,A88,SCMFSA_2:68;
end;
case
A89: x <> da;
then sk11.x=sk1.x by A20,A74,A77,A87,SCMFSA_2:68;
hence sk11.x=sk12.x by A19,A21,A74,A77,A82,A87,A89,
SCMFSA_2:68;
end;
end;
hence sk11.x=sk12.x;
end;
end;
hence sk11.x=sk12.x;
end;
suppose
A90: x is FinSeq-Location;
then
A91: sk12.x=sk2.x by A19,A21,A74,SCMFSA_2:67;
sk1.x=(sk2 | Dloc).x by A14,A76,FUNCT_1:49
.=sk2.x by A76,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A74,A90,A91,SCMFSA_2:67;
end;
end;
hence P[m+1] by A22,A75,FUNCT_1:96;
end;
suppose InsCode i1 = 6;
then consider lb such that
A92: i1 = goto lb by SCMFSA_2:35;
A93: sk11.IC SCM+FSA=lb by A20,A92,SCMFSA_2:69
.= sk12.IC SCM+FSA by A19,A21,A92,SCMFSA_2:69;
now
let x be set;
assume
A94: x in Dloc;
then
A95: sk1.x=(sk2 | Dloc).x by A14,FUNCT_1:49
.=sk2.x by A94,FUNCT_1:49;
per cases by A4,A94,Th12;
suppose
A96: x is Int-Location;
then sk11.x=sk1.x by A20,A92,SCMFSA_2:69;
hence sk11.x=sk12.x by A19,A21,A92,A95,A96,SCMFSA_2:69;
end;
suppose
A97: x is FinSeq-Location;
then sk11.x=sk1.x by A20,A92,SCMFSA_2:69;
hence sk11.x=sk12.x by A19,A21,A92,A95,A97,SCMFSA_2:69;
end;
end;
hence P[m+1] by A22,A93,FUNCT_1:96;
end;
suppose InsCode i1 = 7;
then consider lb,da such that
A98: i1 = da=0_goto lb by SCMFSA_2:36;
A99: da in UsedILoc p by A18,A98,Th7;
then
A100: sk1.da=(sk2 | Dloc).da by A10,A14,FUNCT_1:49
.=sk2.da by A10,A99,FUNCT_1:49;
A101: now
per cases;
suppose
A102: sk1.da=0;
hence sk11.IC SCM+FSA=lb by A20,A98,SCMFSA_2:70
.= sk12.IC SCM+FSA by A19,A21,A98,A100,A102,SCMFSA_2:70;
end;
suppose
A103: sk1.da<>0;
hence sk11.IC SCM+FSA= IC sk2 + 1 by A14,A20,A98,SCMFSA_2:70
.= sk12.IC SCM+FSA by A19,A21,A98,A100,A103,SCMFSA_2:70;
end;
end;
now
let x be set;
assume
A104: x in Dloc;
then
A105: sk1.x=(sk2 | Dloc).x by A14,FUNCT_1:49
.=sk2.x by A104,FUNCT_1:49;
per cases by A4,A104,Th12;
suppose
A106: x is Int-Location;
then sk11.x=sk1.x by A20,A98,SCMFSA_2:70;
hence sk11.x=sk12.x by A19,A21,A98,A105,A106,SCMFSA_2:70;
end;
suppose
A107: x is FinSeq-Location;
then sk11.x=sk1.x by A20,A98,SCMFSA_2:70;
hence sk11.x=sk12.x by A19,A21,A98,A105,A107,SCMFSA_2:70;
end;
end;
hence P[m+1] by A22,A101,FUNCT_1:96;
end;
suppose InsCode i1 = 8;
then consider lb,da such that
A108: i1 = da>0_goto lb by SCMFSA_2:37;
A109: da in UsedILoc p by A18,A108,Th7;
then
A110: sk1.da=(sk2 | Dloc).da by A10,A14,FUNCT_1:49
.=sk2.da by A10,A109,FUNCT_1:49;
A111: now
per cases;
suppose
A112: sk1.da > 0;
hence sk11.IC SCM+FSA=lb by A20,A108,SCMFSA_2:71
.= sk12.IC SCM+FSA by A19,A21,A108,A110,A112,SCMFSA_2:71;
end;
suppose
A113: sk1.da <= 0;
hence sk11.IC SCM+FSA=IC sk2 + 1 by A14,A20,A108,SCMFSA_2:71
.= sk12.IC SCM+FSA by A19,A21,A108,A110,A113,SCMFSA_2:71;
end;
end;
now
let x be set;
assume
A114: x in Dloc;
then
A115: sk1.x=(sk2 | Dloc).x by A14,FUNCT_1:49
.=sk2.x by A114,FUNCT_1:49;
per cases by A4,A114,Th12;
suppose
A116: x is Int-Location;
then sk11.x=sk1.x by A20,A108,SCMFSA_2:71;
hence sk11.x=sk12.x by A19,A21,A108,A115,A116,SCMFSA_2:71;
end;
suppose
A117: x is FinSeq-Location;
then sk11.x=sk1.x by A20,A108,SCMFSA_2:71;
hence sk11.x=sk12.x by A19,A21,A108,A115,A117,SCMFSA_2:71;
end;
end;
hence P[m+1] by A22,A111,FUNCT_1:96;
end;
suppose InsCode i1 = 9;
then consider a,b,fa such that
A118: i1 = b:=(fa,a) by SCMFSA_2:38;
A119: sk11.IC SCM+FSA= IC sk2 + 1 by A14,A20,A118,SCMFSA_2:72
.= sk12.IC SCM+FSA by A19,A21,A118,SCMFSA_2:72;
now
let x be set;
assume
A120: x in Dloc;
per cases by A4,A120,Th12;
suppose
A121: x is Int-Location;
per cases;
suppose
A122: x = b;
A123: ex k1 being Nat st ( k1=|.sk1.a.|)&( Exec(b:=(fa
,a), sk1).b=(sk1.fa)/.k1) by SCMFSA_2:72;
A124: ex k2 being Nat st ( k2=|.sk2.a.|)&( Exec(b:=(fa
,a), sk2).b=(sk2.fa)/.k2) by SCMFSA_2:72;
A125: a in UsedILoc p by A18,A118,Th8;
then
A126: sk1.a=(sk2 | Dloc).a by A10,A14,FUNCT_1:49
.=sk2.a by A10,A125,FUNCT_1:49;
A127: fa in UsedI*Loc p by A18,A118,Th9;
then sk1.fa=(sk2 | Dloc).fa by A11,A14,FUNCT_1:49
.=sk2.fa by A11,A127,FUNCT_1:49;
hence sk11.x=sk12.x by A19,A20,A21,A118,A122,A123,A124,A126;
end;
suppose
A128: x<> b;
then
A129: sk12.x=sk2.x by A19,A21,A118,A121,SCMFSA_2:72;
sk1.x=(sk2 | Dloc).x by A14,A120,FUNCT_1:49
.=sk2.x by A120,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A118,A121,A128,A129,SCMFSA_2:72;
end;
end;
suppose
A130: x is FinSeq-Location;
then
A131: sk12.x=sk2.x by A19,A21,A118,SCMFSA_2:72;
sk1.x=(sk2 | Dloc).x by A14,A120,FUNCT_1:49
.=sk2.x by A120,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A118,A130,A131,SCMFSA_2:72;
end;
end;
hence P[m+1] by A22,A119,FUNCT_1:96;
end;
suppose InsCode i1 = 10;
then consider a,b,fa such that
A132: i1 = (fa,a):=b by SCMFSA_2:39;
A133: sk11.IC SCM+FSA= IC sk2 + 1 by A14,A20,A132,SCMFSA_2:73
.= sk12.IC SCM+FSA by A19,A21,A132,SCMFSA_2:73;
now
let x be set;
assume
A134: x in Dloc;
per cases by A4,A134,Th12;
suppose
A135: x is FinSeq-Location;
per cases;
suppose
A136: x = fa;
A137: ex k1 being Nat st ( k1=|.sk1.a.|)&( Exec((fa,a)
:=b,sk1).fa=sk1.fa+*(k1,sk1.b)) by SCMFSA_2:73;
A138: ex k2 being Nat st ( k2=|.sk2.a.|)&( Exec((fa,a)
:=b,sk2).fa=sk2.fa+*(k2,sk2.b)) by SCMFSA_2:73;
A139: a in UsedILoc p by A18,A132,Th8;
then
A140: sk1.a=(sk2 | Dloc).a by A10,A14,FUNCT_1:49
.=sk2.a by A10,A139,FUNCT_1:49;
A141: b in UsedILoc p by A18,A132,Th8;
then
A142: sk1.b=(sk2 | Dloc).b by A10,A14,FUNCT_1:49
.=sk2.b by A10,A141,FUNCT_1:49;
A143: fa in UsedI*Loc p by A18,A132,Th9;
then sk1.fa=(sk2 | Dloc).fa by A11,A14,FUNCT_1:49
.=sk2.fa by A11,A143,FUNCT_1:49;
hence sk11.x=sk12.x by A19,A20,A21,A132,A136,A137,A138,A140,A142;
end;
suppose
A144: x<> fa;
then
A145: sk12.x=sk2.x by A19,A21,A132,A135,SCMFSA_2:73;
sk1.x=(sk2 | Dloc).x by A14,A134,FUNCT_1:49
.=sk2.x by A134,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A132,A135,A144,A145,SCMFSA_2:73;
end;
end;
suppose
A146: x is Int-Location;
then
A147: sk12.x=sk2.x by A19,A21,A132,SCMFSA_2:73;
sk1.x=(sk2 | Dloc).x by A14,A134,FUNCT_1:49
.=sk2.x by A134,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A132,A146,A147,SCMFSA_2:73;
end;
end;
hence P[m+1] by A22,A133,FUNCT_1:96;
end;
suppose InsCode i1 = 11;
then consider a,fa such that
A148: i1 = a:=len fa by SCMFSA_2:40;
A149: sk11.IC SCM+FSA= IC sk2 + 1 by A14,A20,A148,SCMFSA_2:74
.= sk12.IC SCM+FSA by A19,A21,A148,SCMFSA_2:74;
now
let x be set;
assume
A150: x in Dloc;
per cases by A4,A150,Th12;
suppose
A151: x is Int-Location;
per cases;
suppose
A152: x = a;
then
A153: sk12.x= len(sk2.fa) by A19,A21,A148,SCMFSA_2:74;
A154: fa in UsedI*Loc p by A18,A148,Th11;
then sk1.fa=(sk2 | Dloc).fa by A11,A14,FUNCT_1:49
.=sk2.fa by A11,A154,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A148,A152,A153,SCMFSA_2:74;
end;
suppose
A155: x<> a;
then
A156: sk12.x=sk2.x by A19,A21,A148,A151,SCMFSA_2:74;
sk1.x=(sk2 | Dloc).x by A14,A150,FUNCT_1:49
.=sk2.x by A150,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A148,A151,A155,A156,SCMFSA_2:74;
end;
end;
suppose
A157: x is FinSeq-Location;
then
A158: sk12.x=sk2.x by A19,A21,A148,SCMFSA_2:74;
sk1.x=(sk2 | Dloc).x by A14,A150,FUNCT_1:49
.=sk2.x by A150,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A148,A157,A158,SCMFSA_2:74;
end;
end;
hence P[m+1] by A22,A149,FUNCT_1:96;
end;
suppose InsCode i1 = 12;
then consider a,fa such that
A159: i1 = fa:=<0,...,0>a by SCMFSA_2:41;
A160: sk11.IC SCM+FSA=IC sk2 + 1 by A14,A20,A159,SCMFSA_2:75
.= sk12.IC SCM+FSA by A19,A21,A159,SCMFSA_2:75;
now
let x be set;
assume
A161: x in Dloc;
per cases by A4,A161,Th12;
suppose
A162: x is FinSeq-Location;
per cases;
suppose
A163: x = fa;
A164: ex k1 being Nat st ( k1 = |.sk1.a.|)&( Exec(fa
:=<0,...,0>a, sk1).fa = k1 |-> 0) by SCMFSA_2:75;
A165: ex k2 being Nat st ( k2 = |.sk2.a.|)&( Exec(fa
:=<0,...,0>a, sk2).fa = k2 |-> 0) by SCMFSA_2:75;
A166: a in UsedILoc p by A18,A159,Th10;
then sk1.a=(sk2 | Dloc).a by A10,A14,FUNCT_1:49
.=sk2.a by A10,A166,FUNCT_1:49;
hence sk11.x=sk12.x by A19,A20,A21,A159,A163,A164,A165;
end;
suppose
A167: x<> fa;
then
A168: sk12.x=sk2.x by A19,A21,A159,A162,SCMFSA_2:75;
sk1.x=(sk2 | Dloc).x by A14,A161,FUNCT_1:49
.=sk2.x by A161,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A159,A162,A167,A168,SCMFSA_2:75;
end;
end;
suppose
A169: x is Int-Location;
then
A170: sk12.x=sk2.x by A19,A21,A159,SCMFSA_2:75;
sk1.x=(sk2 | Dloc).x by A14,A161,FUNCT_1:49
.=sk2.x by A161,FUNCT_1:49;
hence sk11.x=sk12.x by A20,A159,A169,A170,SCMFSA_2:75;
end;
end;
hence P[m+1] by A22,A160,FUNCT_1:96;
end;
end;
for m being Nat holds P[m] from NAT_1:sch 2(A12,A13);
hence thesis by A9;
end;
theorem Th14:
for i,k being Nat,p being Program of SCM+FSA,
s1,s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 &
(for j holds IC Comput(p1,s1,j) in dom p &
IC Comput(p2,s2,j) in dom p) &
Comput(p1,s1,k).IC SCM+FSA = Comput(p2,s2,k).IC
SCM+FSA &
Comput(p1,s1,k) | (UsedI*Loc p \/ UsedILoc p) =
Comput(p2,s2,k) | (UsedI*Loc p \/ UsedILoc p) holds
Comput(p1,s1,i).IC SCM+FSA = Comput(p2,s2,i).IC
SCM+FSA &
Comput(p1,s1,i) |(UsedI*Loc p \/ UsedILoc p) =
Comput(p2,s2,i) |(UsedI*Loc p \/ UsedILoc p)
proof
let i,k be Nat,p be Program of SCM+FSA,s1,s2 be State of SCM+FSA;
set D= UsedI*Loc p \/ UsedILoc p;
assume that
A1: k <= i and
A2: p c= p1 and
A3: p c= p2 and
A4: for j holds IC Comput(p1,s1,j) in dom p & IC Comput(
p2,s2,j) in
dom p and
A5: Comput(p1,s1,k).IC SCM+FSA = Comput(p2,s2,k).IC
SCM+FSA and
A6: Comput(p1,s1,k) | D = Comput(p2,s2,k) | D;
reconsider t={} as PartState of SCM+FSA by FUNCT_1:104,RELAT_1:171;
set D1= dom t \/ UsedI*Loc p \/ UsedILoc p;
A7: dom t c= Int-Locations \/ FinSeq-Locations by RELAT_1:38,XBOOLE_1:2;
A8: D1 = D by RELAT_1:38;
hence Comput(p1,s1,i).IC SCM+FSA = Comput(p2,s2,i).
IC SCM+FSA
by A1,A2,A3,A4,A5,A6,A7,Th13;
thus thesis by A1,A2,A3,A4,A5,A6,A7,A8,Th13;
end;
::$CT 7
theorem Th15:
for i1,i2,i3 be Instruction of SCM+FSA holds card (i1 ";" i2 ";" i3)=6
proof
let i1,i2,i3 be Instruction of SCM+FSA;
thus card (i1 ";" i2 ";" i3) = card (i1 ";" i2) + 2 by SCMFSA6A:34
.= 4 +2 by SCMFSA6A:35
.= 6;
end;
::$CT 2
theorem Th16:
for I,J being Program of SCM+FSA, k being Nat,
i being Instruction of SCM+FSA st k< card J & i = J. k holds
(I ";" J).(card I +k) =IncAddr( i, card I )
proof
let I,J be Program of SCM+FSA, k be Nat,
i be Instruction of SCM+FSA such that
A1: k< card J and
A2: i = J. k;
set m=card I +k;
A3: m < card I + card J by A1,XREAL_1:6;
(m -' card I) = k by NAT_D:34;
hence thesis by A2,A3,NAT_1:11,SCMFSA8C:2;
end;
theorem Th17:
for I,J be Program of SCM+FSA,
i be ins-loc-free Instruction of SCM+FSA st i <> halt SCM+FSA
holds (I ";" i ";" J).card I = i
proof
let I,J be Program of SCM+FSA,
i be ins-loc-free Instruction of SCM+FSA;
assume that
A1: i <> halt SCM+FSA;
set x1= card I;
A2: card (I ";" i) = card I +2 by SCMFSA6A:34;
card I + 0 < card I + 2 by XREAL_1:6;
then
A3: x1 in dom (I ";" i) by A2,AFINSQ_1:66;
A4: (Macro i).( 0) = i by COMPOS_1:58;
A5: card (Macro i) = 2 by COMPOS_1:56;
A6: (I ";" i).x1 = (I ";" Macro i). (card I+0) by SCMFSA6A:def 6
.=IncAddr( i, card I ) by A4,A5,Th16
.=i by COMPOS_0:4;
thus (I ";" i ";" J).x1 = (Directed (I ";" i)).x1 by A3,SCMFSA8A:14
.=i by A1,A3,A6,SCMFSA8A:16;
end;
theorem Th18:
for I,J be Program of SCM+FSA, i be Instruction of SCM+FSA
holds (I ";" i ";" J).(card I+1) = goto(card I+2)
proof
let I,J be Program of SCM+FSA, i be Instruction of SCM+FSA;
set x1= card I;
A1: card (I ";" i) = card I +2 by SCMFSA6A:34;
A2: card (Macro i) = 2 by COMPOS_1:56;
set x2= card I+1;
card I + 1 < card I + 2 by XREAL_1:6;
then
A3: x2 in dom (I ";" i) by A1,AFINSQ_1:66;
(Macro i).1 = halt SCM+FSA by COMPOS_1:59;
then (I ";" Macro i).x2 =IncAddr( halt SCM+FSA, card I ) by A2,Th16;
then
A4: (I ";" i).x2 =IncAddr( halt SCM+FSA, card I ) by SCMFSA6A:def 6
.=halt SCM+FSA by COMPOS_0:4;
thus (I ";" i ";" J).x2 = (Directed (I ";" i)).x2 by A3,SCMFSA8A:14
.= goto (card I+2) by A1,A3,A4,SCMFSA8A:16;
end;
::$CT 3
theorem Th19:
for p being Program of SCM+FSA,s being State of SCM+FSA holds
UsedI*Loc p \/ UsedILoc p c= dom s
proof
let p be Program of SCM+FSA,s be State of SCM+FSA;
Int-Locations c= dom(s) by SCMFSA_2:45;
then
A1: UsedILoc p c= dom(s) by XBOOLE_1:1;
FinSeq-Locations c= dom (s) by SCMFSA_2:46;
then UsedI*Loc p c= dom(s) by XBOOLE_1:1;
hence thesis by A1,XBOOLE_1:8;
end;
theorem Th20:
for p being Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA,I be Program of SCM+FSA,f be FinSeq-Location
holds Result(p +* I,Initialized s).f = IExec(I,p,s).f
proof
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA,I be Program of SCM+FSA,f be FinSeq-Location;
set D= Int-Locations \/ FinSeq-Locations;
f in FinSeq-Locations by SCMFSA_2:def 5;
then
A1: f in D by XBOOLE_0:def 3;
hence Result(p +* I,Initialized s).f
= (DataPart Result(p +* I,Initialized s)).f
by FUNCT_1:49,SCMFSA_2:100
.=(DataPart IExec(I,p,s)).f by SCMFSA8B:32
.= IExec(I,p,s).f by A1,FUNCT_1:49,SCMFSA_2:100;
end;
:: ------ Bubble Sort Algorithm -----------------
set a0 = intloc 0;
set a1 = intloc 1;
set a2 = intloc 2;
set a3 = intloc 3;
set a4 = intloc 4;
set a5 = intloc 5;
set a6 = intloc 6;
Lm1: a0 <> a2 by SCMFSA_2:101;
Lm2: a0 <> a4 by SCMFSA_2:101;
Lm3: a0 <> a5 by SCMFSA_2:101;
Lm4: a0 <> a6 by SCMFSA_2:101;
Lm5: a1 <> a2 by SCMFSA_2:101;
Lm6: a1 <> a3 by SCMFSA_2:101;
Lm7: a1 <> a4 by SCMFSA_2:101;
Lm8: a1 <> a5 by SCMFSA_2:101;
Lm9: a1 <> a6 by SCMFSA_2:101;
Lm10: a2 <> a3 by SCMFSA_2:101;
Lm11: a2 <> a4 by SCMFSA_2:101;
Lm12: a2 <> a5 by SCMFSA_2:101;
Lm13: a2 <> a6 by SCMFSA_2:101;
Lm14: a3 <> a4 by SCMFSA_2:101;
Lm15: a3 <> a5 by SCMFSA_2:101;
Lm16: a3 <> a6 by SCMFSA_2:101;
Lm17: a4 <> a5 by SCMFSA_2:101;
Lm18: a4 <> a6 by SCMFSA_2:101;
Lm19: a5 <> a6 by SCMFSA_2:101;
set initializeWorkMem= (a2:= a0) ";" (a3:= a0) ";"
(a4:= a0) ";" (a5:= a0) ";" (a6:= a0);
:: set a0 = intloc 0;
:: set a1 = intloc 1;
:: set a2 = intloc 2;
:: set a3 = intloc 3;
:: set a4 = intloc 4;
:: set a5 = intloc 5;
:: set a6 = intloc 6;
:: set initializeWorkMem= (a2:= a0) ";" (a3:= a0) ";"
:: (a4:= a0) ";" (a5:= a0) ";" (a6:= a0);
definition
let f be FinSeq-Location;
func bubble-sort f -> Program of SCM+FSA equals
( ((intloc 2):= (intloc 0)) ";" ((intloc 3):= (intloc 0)) ";"
((intloc 4):= (intloc 0)) ";" ((intloc 5):= (intloc 0)) ";"
((intloc 6):= (intloc 0)) ) ";" ((intloc 1):=len f) ";" Times((intloc 1),
(intloc 2) := (intloc 1) ";" SubFrom(intloc 2,intloc 0) ";"
((intloc 3):=len f) ";" Times(intloc 2, (intloc 4):=(intloc 3) ";"
SubFrom(intloc 3,intloc 0) ";" ((intloc 5):=(f,intloc 3)) ";"
((intloc 6):=(f,(intloc 4))) ";" SubFrom(intloc 6,intloc 5) ";"
if>0(intloc 6, ((intloc 6):=(f,intloc 4)) ";"
((f,intloc 3):=(intloc 6)) ";" ((f,intloc 4):=(intloc 5)),Stop SCM+FSA)
) );
correctness;
end;
definition
func Bubble-Sort-Algorithm -> Program of SCM+FSA equals
bubble-sort fsloc 0;
coherence;
end;
set b1=intloc (0+1),b2=intloc (1+1),b3=intloc (2+1),b4=intloc (3+1),
b5=intloc (4+1),b6=intloc (5+1);
set f0=fsloc 0, i1= b4:=b3, i2= SubFrom(b3,a0), i3= b5:=(f0,b3),
i4= b6:=(f0,b4), i5= SubFrom(b6,b5), i6= (f0,b3):=b6, i7= (f0,b4):=b5,
SS= Stop SCM+FSA,
ifc=if>0(b6,i4 ";" i6 ";" i7,SS),
body2= i1 ";" i2 ";" i3 ";" i4 ";" i5 ";" ifc,
T2=Times(b2,body2),
j1= b2 := b1,
j2= SubFrom(b2,a0), j3= b3:=len f0, Sb= j1 ";" j2 ";" j3,
body1= Sb ";" T2,
T1=Times(b1,body1), w2= b2:= a0, w3= b3:= a0, w4= b4:= a0,
w5= b5:= a0, w6= b6:= a0, w7= b1:=len f0;
theorem Th21:
for f being FinSeq-Location holds
UsedILoc (bubble-sort f) = {intloc 0,intloc 1,intloc 2,intloc 3, intloc 4,
intloc 5,intloc 6}
proof
let f be FinSeq-Location;
set i1= a4:=a3, i2= SubFrom(a3,a0), i3= (a5:=(f,a3)), i4= (a6:=(f,a4)),
i5= SubFrom(a6,a5), i6= ((f,a3):=a6), i7= ((f,a4):=a5),
ifc=if>0(a6,i4 ";" i6 ";" i7,Stop SCM+FSA), Sif= UsedILoc ifc,
body2= i1 ";" i2 ";" i3 ";" i4 ";" i5 ";" ifc;
A1: Sif = {a6} \/ UsedILoc (i4 ";" i6 ";" i7) \/ {} by SCMFSA9A:3,43
.= {a6} \/ (UsedILoc (i4 ";" i6) \/ UsedIntLoc i7) by SF_MASTR:30
.= {a6} \/ (UsedILoc (i4 ";" i6) \/ {a4,a5}) by SF_MASTR:17
.= {a6} \/ (UsedIntLoc i4 \/ UsedIntLoc i6 \/ {a4,a5}) by SF_MASTR:31
.= {a6} \/ (UsedIntLoc i4 \/ {a3,a6} \/ {a4,a5}) by SF_MASTR:17
.= {a6} \/ ({a4,a6} \/ {a3,a6} \/ {a4,a5}) by SF_MASTR:17
.= {a6} \/ ({a4,a6,a3,a6} \/ {a4,a5}) by ENUMSET1:5
.= {a6} \/ ({a6,a6,a3,a4} \/ {a4,a5}) by ENUMSET1:75
.= {a6} \/ {a6,a6,a3,a4} \/ {a4,a5} by XBOOLE_1:4
.= {a6,a6,a6,a3,a4} \/ {a4,a5} by ENUMSET1:7
.= {a6,a3,a4} \/ {a4,a5} by ENUMSET1:38
.= {a6,a3} \/ {a4} \/ {a4,a5} by ENUMSET1:3
.= {a6,a3} \/ ({a4} \/ {a4,a5}) by XBOOLE_1:4
.= {a6,a3} \/ {a4,a4,a5} by ENUMSET1:2
.= {a4,a5} \/ {a6,a3} by ENUMSET1:30
.= {a4,a5,a6,a3} by ENUMSET1:5
.= {a4,a3,a6,a5} by ENUMSET1:64;
set ui12=UsedILoc(i1 ";" i2);
A2: UsedILoc body2 = (UsedILoc (i1 ";" i2 ";"i3 ";"i4 ";" i5) )
\/ Sif by SF_MASTR:27
.= (UsedILoc (i1 ";" i2 ";"i3 ";" i4)) \/ (UsedIntLoc i5) \/ Sif
by SF_MASTR:30
.= (UsedILoc (i1 ";" i2 ";"i3 ";" i4)) \/ {a6,a5} \/ Sif
by SF_MASTR:14
.= (UsedILoc (i1 ";" i2 ";"i3 )) \/ (UsedIntLoc i4) \/ {a6,a5} \/ Sif
by SF_MASTR:30
.= (UsedILoc (i1 ";" i2 ";"i3)) \/ {a6,a4} \/ {a6,a5} \/ Sif
by SF_MASTR:17
.= ui12 \/ UsedIntLoc i3 \/ {a6,a4} \/ {a6,a5} \/ Sif by SF_MASTR:30
.= ui12 \/ {a5,a3} \/ {a6,a4} \/ {a6,a5} \/ Sif by SF_MASTR:17
.= ui12 \/ ({a5,a3} \/ {a6,a4}) \/ {a6,a5} \/ Sif by XBOOLE_1:4
.= ui12 \/ {a5,a3,a6,a4} \/ {a6,a5} \/ Sif by ENUMSET1:5
.= ui12 \/ {a4,a3,a6,a5} \/ {a6,a5} \/ Sif by ENUMSET1:75
.= ui12 \/ ({a4,a3} \/ {a6,a5}) \/ {a6,a5} \/ Sif by ENUMSET1:5
.= ui12 \/ {a4,a3} \/ {a6,a5} \/ {a6,a5} \/ Sif by XBOOLE_1:4
.= ui12 \/ {a4,a3} \/ ({a6,a5} \/ {a6,a5}) \/ Sif by XBOOLE_1:4
.= ui12 \/ ({a4,a3} \/ {a6,a5}) \/ Sif by XBOOLE_1:4
.= ui12 \/ {a4,a3,a6,a5} \/ Sif by ENUMSET1:5
.= ui12 \/ ({a4,a3,a6,a5} \/ Sif) by XBOOLE_1:4
.= (UsedIntLoc i1 ) \/ (UsedIntLoc i2) \/ {a4,a3,a6,a5} by A1,SF_MASTR:31
.= (UsedIntLoc i1 ) \/ {a3,a0} \/ {a4,a3,a6,a5} by SF_MASTR:14
.= {a3,a4} \/ {a3,a0} \/ {a4,a3,a6,a5} by SF_MASTR:14
.= {a3,a4,a3,a0} \/ {a4,a3,a6,a5} by ENUMSET1:5
.= {a3,a3,a4,a0} \/ {a4,a3,a6,a5} by ENUMSET1:62
.= {a3,a4,a0} \/ {a4,a3,a6,a5} by ENUMSET1:31
.= {a0,a4,a3} \/ {a4,a3,a6,a5} by ENUMSET1:60
.= {a0} \/ {a4,a3} \/ {a4,a3,a6,a5} by ENUMSET1:2
.= {a0} \/ {a4,a3} \/ ({a4,a3} \/ {a6,a5}) by ENUMSET1:5
.= {a0} \/ {a4,a3} \/ {a4,a3} \/ {a6,a5} by XBOOLE_1:4
.= {a0} \/ ({a4,a3} \/ {a4,a3}) \/ {a6,a5} by XBOOLE_1:4
.= {a0} \/ ({a4,a3} \/ {a6,a5}) by XBOOLE_1:4
.= {a0} \/ {a4,a3,a6,a5} by ENUMSET1:5;
set j1= a2 := a1, j2= SubFrom(a2,a0), j3= (a3:=len f),
Sfor= UsedILoc Times(a2,body2),
body1= j1 ";" j2 ";" j3 ";" Times(a2,body2);
A3: Sfor={a4,a3,a6,a5} \/ {a0} \/ {a2,a0} by A2,SCMFSA9A:44
.={a4,a3,a6,a5} \/ ({a0} \/ {a2,a0}) by XBOOLE_1:4
.={a4,a3,a6,a5} \/ {a0,a0,a2} by ENUMSET1:2
.={a4,a3,a6,a5} \/ {a0,a2} by ENUMSET1:30
.={a4,a5,a6,a3} \/ {a0,a2} by ENUMSET1:64
.={a4,a5,a6} \/ {a3} \/ {a0,a2} by ENUMSET1:6
.={a4,a5,a6} \/ ({a3} \/ {a0,a2}) by XBOOLE_1:4
.={a4,a5,a6} \/ {a0,a2,a3} by ENUMSET1:3;
A4: UsedILoc body1 = UsedILoc (j1 ";" j2 ";"j3) \/ Sfor by SF_MASTR:27
.= UsedILoc (j1 ";" j2) \/ UsedIntLoc j3 \/ Sfor by SF_MASTR:30
.= UsedILoc (j1 ";" j2) \/ {a3} \/ Sfor by SF_MASTR:18
.= UsedIntLoc j1 \/ UsedIntLoc j2 \/ {a3} \/ Sfor by SF_MASTR:31
.= UsedIntLoc j1 \/ {a2,a0} \/ {a3} \/ Sfor by SF_MASTR:14
.= {a2,a1} \/ {a2,a0} \/ {a3} \/ Sfor by SF_MASTR:14
.= {a2,a1} \/ ({a0,a2} \/ {a3}) \/ Sfor by XBOOLE_1:4
.= {a2,a1} \/ {a0,a2,a3} \/ Sfor by ENUMSET1:3
.= {a2,a1} \/ {a0,a2,a3} \/ {a0,a2,a3} \/ {a4,a5,a6} by A3,XBOOLE_1:4
.= {a2,a1} \/ ({a0,a2,a3} \/ {a0,a2,a3}) \/ {a4,a5,a6} by XBOOLE_1:4
.= {a2,a1} \/ ({a0,a2} \/ {a3}) \/ {a4,a5,a6} by ENUMSET1:3
.= {a2,a1} \/ {a0,a2} \/ {a3} \/ {a4,a5,a6} by XBOOLE_1:4
.= {a2,a1,a0,a2} \/ {a3} \/ {a4,a5,a6} by ENUMSET1:5
.= {a2,a2,a0,a1} \/ {a3} \/ {a4,a5,a6} by ENUMSET1:64
.= {a2,a0,a1} \/ {a3} \/ {a4,a5,a6} by ENUMSET1:31
.= {a0,a1,a2} \/ {a3} \/ {a4,a5,a6} by ENUMSET1:59
.= {a0,a1,a2,a3} \/ {a4,a5,a6} by ENUMSET1:6
.= {a0,a1,a2,a3,a4,a5,a6} by ENUMSET1:19;
set k2= a2:= a0, k3= a3:= a0, k4= a4:= a0, k5= a5:= a0;
A5: UsedILoc initializeWorkMem = UsedILoc (k2 ";" k3 ";" k4 ";" k5)
\/ UsedIntLoc (a6:= a0) by SF_MASTR:30
.= UsedILoc (k2 ";" k3 ";" k4 ";" k5) \/ {a6,a0} by SF_MASTR:14
.= UsedILoc (k2 ";" k3 ";" k4 ) \/ UsedIntLoc k5 \/ {a6,a0}
by SF_MASTR:30
.= UsedILoc (k2 ";" k3 ";" k4 ) \/ {a5,a0} \/ {a6,a0} by SF_MASTR:14
.= UsedILoc (k2 ";" k3 ) \/ UsedIntLoc k4 \/ {a5,a0} \/
{a6,a0} by SF_MASTR:30
.= UsedILoc (k2 ";" k3 ) \/ {a4,a0} \/ {a5,a0} \/ {a6,a0} by SF_MASTR:14
.= UsedIntLoc k2 \/ UsedIntLoc k3 \/ {a4,a0} \/ {a5,a0} \/ {a6,a0}
by SF_MASTR:31
.= UsedIntLoc k2 \/ {a3,a0} \/ {a4,a0} \/ {a5,a0} \/
{a6,a0} by SF_MASTR:14
.= {a2,a0} \/ {a3,a0} \/ {a4,a0} \/ {a5,a0} \/ {a6,a0} by SF_MASTR:14
.= {a2,a0} \/ {a3,a0} \/ {a4,a0} \/ ({a5,a0} \/ {a6,a0}) by XBOOLE_1:4
.= {a2,a0} \/ {a3,a0} \/ {a4,a0} \/ {a0,a5,a6} by ENUMSET1:87
.= {a0,a2,a3} \/ {a4,a0} \/ {a0,a5,a6} by ENUMSET1:87
.= {a0,a2,a3} \/ {a4,a0} \/ ({a0} \/ {a5,a6}) by ENUMSET1:2
.= {a0,a2,a3} \/ {a4,a0} \/ {a0} \/ {a5,a6} by XBOOLE_1:4
.= {a0,a2,a3} \/ ({a4,a0} \/ {a0}) \/ {a5,a6} by XBOOLE_1:4
.= {a0,a2,a3} \/ {a4,a0,a0} \/ {a5,a6} by ENUMSET1:3
.= {a0,a2,a3} \/ ({a0,a0} \/ {a4}) \/ {a5,a6} by ENUMSET1:2
.= {a0,a2,a3} \/ {a0,a0} \/ {a4} \/ {a5,a6} by XBOOLE_1:4
.= {a0,a0,a0,a2,a3} \/ {a4} \/ {a5,a6} by ENUMSET1:8
.= {a0,a2,a3} \/ {a4} \/ {a5,a6} by ENUMSET1:38
.= {a0,a2,a3,a4} \/ {a5,a6} by ENUMSET1:6
.= {a0,a2,a3,a4,a5,a6} by ENUMSET1:14
.= {a0} \/ {a2,a3,a4,a5,a6} by ENUMSET1:11;
set k7=(a1:=len f), Ut=UsedILoc Times(a1,body1);
thus UsedILoc (bubble-sort f)
=UsedILoc ( initializeWorkMem ";" k7 ) \/ Ut by SF_MASTR:27
.=UsedILoc initializeWorkMem \/ UsedIntLoc k7 \/ Ut by SF_MASTR:30
.={a0} \/ {a2,a3,a4,a5,a6} \/ {a1} \/ Ut by A5,SF_MASTR:18
.={a0} \/ {a1} \/ {a2,a3,a4,a5,a6} \/ Ut by XBOOLE_1:4
.={a0,a1} \/ {a2,a3,a4,a5,a6} \/ Ut by ENUMSET1:1
.={a0,a1,a2,a3,a4,a5,a6} \/ Ut by ENUMSET1:17
.={a0,a1,a2,a3,a4,a5,a6} \/ ({a1,a0} \/ {a0,a1,a2,a3,a4,a5,a6})
by A4,SCMFSA9A:44
.={a0,a1,a2,a3,a4,a5,a6} \/ {a0,a1,a2,a3,a4,a5,a6} \/ {a1,a0} by XBOOLE_1:4
.={a2,a3,a4,a5,a6} \/ {a0,a1} \/ {a0,a1} by ENUMSET1:17
.={a2,a3,a4,a5,a6} \/ ({a0,a1} \/ {a0,a1}) by XBOOLE_1:4
.={a0,a1,a2,a3,a4,a5,a6} by ENUMSET1:17;
end;
theorem Th22:
for f being FinSeq-Location holds UsedI*Loc (bubble-sort f) = {f}
proof
let f be FinSeq-Location;
set i1= a4:=a3, i2= SubFrom(a3,a0), i3= (a5:=(f,a3)), i4= (a6:=(f,a4)),
i5= SubFrom(a6,a5), i6= ((f,a3):=a6), i7= ((f,a4):=a5),
ifc=if>0(a6,i4 ";" i6 ";" i7,Stop SCM+FSA), Sif= UsedI*Loc ifc,
body2= i1 ";" i2 ";" i3 ";" i4 ";" i5 ";" ifc;
A1: Sif = UsedI*Loc (i4 ";" i6 ";" i7) \/ {} by SCMFSA9A:4,10
.= UsedI*Loc (i4 ";" i6) \/ UsedInt*Loc i7 by SF_MASTR:46
.= UsedI*Loc (i4 ";" i6) \/ {f} by SF_MASTR:33
.= UsedInt*Loc i4 \/ UsedInt*Loc i6 \/ {f} by SF_MASTR:47
.= UsedInt*Loc i4 \/ {f} \/ {f} by SF_MASTR:33
.= {f} \/ {f} \/ {f} by SF_MASTR:33
.= {f};
A2: UsedI*Loc body2 = UsedI*Loc (i1 ";" i2 ";"i3 ";"i4 ";" i5)
\/ Sif by SF_MASTR:43
.= UsedI*Loc (i1 ";" i2 ";"i3 ";" i4) \/ UsedInt*Loc i5 \/ Sif
by SF_MASTR:46
.= UsedI*Loc (i1 ";" i2 ";"i3 ";" i4) \/ {} \/ Sif by SF_MASTR:32
.= UsedI*Loc (i1 ";" i2 ";"i3 ) \/ UsedInt*Loc i4 \/ Sif by SF_MASTR:46
.= UsedI*Loc (i1 ";" i2 ";"i3 ) \/ {f} \/ Sif by SF_MASTR:33
.= UsedI*Loc (i1 ";" i2 ";"i3 ) \/ ({f} \/ {f}) by A1,XBOOLE_1:4
.= UsedI*Loc (i1 ";" i2 ) \/ UsedInt*Loc i3 \/ {f} by SF_MASTR:46
.= UsedI*Loc (i1 ";" i2 ) \/ {f} \/ {f} by SF_MASTR:33
.= UsedInt*Loc i1 \/ UsedInt*Loc i2 \/ {f} \/ {f} by SF_MASTR:47
.= UsedInt*Loc i1 \/ {} \/ {f} \/ {f} by SF_MASTR:32
.= {} \/ {} \/ {f} \/ {f} by SF_MASTR:32
.= {f};
set j1= a2 := a1, j2= SubFrom(a2,a0), j3= (a3:=len f),
Sfor= UsedI*Loc Times(a2,body2),
body1= j1 ";" j2 ";" j3 ";" Times(a2,body2);
A3: Sfor={f} by A2,SCMFSA9A:45;
A4: UsedI*Loc body1 = UsedI*Loc (j1 ";" j2 ";"j3) \/ Sfor by SF_MASTR:43
.= UsedI*Loc (j1 ";" j2) \/ UsedInt*Loc j3 \/ Sfor by SF_MASTR:46
.= UsedI*Loc (j1 ";" j2) \/ {f} \/ Sfor by SF_MASTR:34
.= UsedInt*Loc j1 \/ UsedInt*Loc j2 \/ {f} \/ Sfor by SF_MASTR:47
.= {} \/ UsedInt*Loc j2 \/ {f} \/ Sfor by SF_MASTR:32
.= {} \/ {} \/ {f} \/ Sfor by SF_MASTR:32
.= {f} by A3;
set k2= a2:= a0, k3= a3:= a0, k4= a4:= a0, k5= a5:= a0;
A5: UsedI*Loc initializeWorkMem = UsedI*Loc (k2 ";" k3 ";" k4 ";" k5)
\/ UsedInt*Loc (a6:= a0) by SF_MASTR:46
.= UsedI*Loc (k2 ";" k3 ";" k4 ";" k5) \/ {} by SF_MASTR:32
.= UsedI*Loc (k2 ";" k3 ";" k4) \/ UsedInt*Loc k5 by SF_MASTR:46
.= UsedI*Loc (k2 ";" k3 ";" k4) \/ {} by SF_MASTR:32
.= UsedI*Loc (k2 ";" k3 ) \/ UsedInt*Loc k4 by SF_MASTR:46
.= UsedI*Loc (k2 ";" k3 ) \/ {} by SF_MASTR:32
.= UsedInt*Loc k2 \/ UsedInt*Loc k3 by SF_MASTR:47
.= UsedInt*Loc k2 \/ {} by SF_MASTR:32
.= {} by SF_MASTR:32;
set k7=(a1:=len f) , Ut=UsedI*Loc Times(a1,body1);
thus UsedI*Loc (bubble-sort f)
=UsedI*Loc ( initializeWorkMem ";" k7 ) \/ Ut by SF_MASTR:43
.=UsedI*Loc initializeWorkMem \/ UsedInt*Loc k7 \/ Ut by SF_MASTR:46
.={f} \/ Ut by A5,SF_MASTR:34
.={f} \/ {f} by A4,SCMFSA9A:45
.={f};
end;
::$CT 2
theorem Th23:
for f being FinSeq-Location holds card (bubble-sort f) = 53
proof
let f be FinSeq-Location;
set i1= a4:=a3, i2= SubFrom(a3,a0), i3= (a5:=(f,a3)), i4= (a6:=(f,a4)),
i5= SubFrom(a6,a5), i6= ((f,a3):=a6), i7= ((f,a4):=a5),
ifc=if>0(a6,i4 ";" i6 ";" i7,Stop SCM+FSA), Cif= card ifc,
body2= i1 ";" i2 ";" i3 ";" i4 ";" i5 ";" ifc;
card Stop SCM+FSA = 1 by COMPOS_1:4;
then
A1: Cif=card (i4 ";" i6 ";" i7) + 1 + 4 by SCMFSA8B:12
.=6 + 1 + 4 by Th15
.=11;
A2: card body2 = card (i1 ";" i2 ";" i3 ";" i4 ";" i5) + Cif by SCMFSA6A:21
.= card (i1 ";" i2 ";" i3 ";" (i4 ";" i5))+Cif by SCMFSA6A:28
.= card (i1 ";" i2 ";" i3) + card (i4 ";" i5)+Cif by SCMFSA6A:21
.= 6 + card (i4 ";" i5)+Cif by Th15
.= 6 + 4+ Cif by SCMFSA6A:35
.=21 by A1;
set j1= a2 := a1, j2= SubFrom(a2,a0) , j3= (a3:=len f) ,
body1= j1 ";" j2 ";" j3 ";" Times(a2,body2);
A3: card
body1 = card (j1 ";" j2 ";" j3) + card Times(a2,body2) by SCMFSA6A:21
.= 6 + card Times(a2,body2) by Th15
.= 6 + (21 +7) by A2,SCMFSA8C:94
.= 34;
set k2= a2:= a0, k3= a3:= a0, k4= a4:= a0, k5= a5:= a0, k6= a6:= a0;
A4: card initializeWorkMem
= card (k2 ";" k3 ";" k4 ";" k5)+ 2 by SCMFSA6A:34
.= card (k2 ";" k3 ";" k4 ) + 2+ 2 by SCMFSA6A:34
.= card (k2 ";" k3 ";" k4 ) + 4
.= 6 + 4 by Th15
.= 10;
set k7=(a1:=len f), Ct=card Times(a1,body1);
A5: Ct=34 + 7 by A3,SCMFSA8C:94;
thus card (bubble-sort f)
= card (initializeWorkMem ";" k7)+ Ct by SCMFSA6A:21
.= 10 + 2 + Ct by A4,SCMFSA6A:34
.= 53 by A5;
end;
theorem Th24:
for P being Instruction-Sequence of SCM+FSA
st Bubble-Sort-Algorithm c= P
for f being FinSeq-Location, k being Nat st
k < 53 holds Bubble-Sort-Algorithm.k= P.k
proof
let P be Instruction-Sequence of SCM+FSA such that
A1: Bubble-Sort-Algorithm c= P;
let f be FinSeq-Location, k be Nat;
assume
A2: k < 53;
card (bubble-sort f0) = 53 by Th23;
then k in dom Bubble-Sort-Algorithm by A2,AFINSQ_1:66;
hence Bubble-Sort-Algorithm.k= P.k by A1,GRFUNC_1:2;
end;
Lm20:
for P being Instruction-Sequence of SCM+FSA
st Bubble-Sort-Algorithm c= P holds
P. 0= a2:=a0 & P. 1= goto 2 &
P. 2= a3:=a0 & P. 3= goto 4 &
P. 4= a4:=a0 & P. 5= goto 6 &
P. 6= a5:=a0 & P. 7= goto 8 &
P. 8= a6:=a0 & P. 9= goto 10 &
P. 10= a1:=len fsloc 0 & P. 11= goto 12
proof
set f0=fsloc 0, TT=Times(a1, a2 := a1 ";" SubFrom(a2,a0) ";"
(a3:=len f0) ";" Times(a2, a4:=a3 ";" SubFrom(a3,a0) ";" (a5:=(f0,a3)) ";"
(a6:=(f0,a4)) ";" SubFrom(a6,a5) ";" if>0(a6,(a6:=(f0,a4)) ";"
((f0,a3):=a6) ";"((f0,a4):=a5),Stop SCM+FSA) ) );
set q=Bubble-Sort-Algorithm;
let P be Instruction-Sequence of SCM+FSA
such that
A1: q c= P;
set W2=a2:= a0, W3=a3:= a0, W4=a4:= a0, W5=a5:= a0, W6=a6:= a0,
W7=a1:=len f0, T7=W7 ";" TT, T6=W6 ";" T7, T5=W5 ";" T6, T4=W4 ";" T5,
T3=W3 ";" T4, X3=W2 ";" W3, X4=X3 ";" W4, X5=X4 ";" W5, X6=X5 ";" W6;
A2: q=X5 ";" W6 ";" T7 by SCMFSA6A:27;
then
A3: q=X4 ";" W5 ";" T6 by SCMFSA6A:27;
then
A4: q=X3 ";" W4 ";" T5 by SCMFSA6A:27;
then q=W2 ";" W3 ";" T4 by SCMFSA6A:27;
then q=W2 ";" T3 by SCMFSA6A:31;
then
A5: q= Macro W2 ";" T3 by SCMFSA6A:def 5;
A6: q =Macro W2 ";" W3 ";" T4 by A5,SCMFSA6A:27;
A7: dom Macro W2 = { 0, 1} by COMPOS_1:61;
then
A8: 0 in dom Macro W2 by TARSKI:def 2;
A9: 1 in dom Macro W2 by A7,TARSKI:def 2;
thus P. 0=q. 0 by A1,Th24
.= (Directed Macro W2). 0 by A8,A5,SCMFSA8A:14
.= W2 by SCMFSA7B:1;
thus P. 1=q. 1 by A1,Th24
.= (Directed Macro W2). 1 by A9,A5,SCMFSA8A:14
.= goto 2 by SCMFSA7B:2;
A10: card Macro W2=2 by COMPOS_1:56;
thus P. 2=q. 2 by A1,Th24
.= W3 by A6,A10,Th17;
thus P. 3=q. (2+1) by A1,Th24
.=goto (2+2) by A6,A10,Th18
.=goto 4;
A11: card X3 =4 by SCMFSA6A:35;
thus P. 4=q. 4 by A1,Th24
.= W4 by A4,A11,Th17;
thus P. 5=q. (4+1) by A1,Th24
.=goto (4+2) by A4,A11,Th18
.=goto 6;
A12: card X4=6 by Th15;
thus P. 6=q. 6 by A1,Th24
.= W5 by A3,A12,Th17;
thus P. 7=q. (6+1) by A1,Th24
.=goto (6+2) by A3,A12,Th18
.=goto 8;
A13: card X5 = 6 + 2 by A12,SCMFSA6A:34;
thus P. 8=q. 8 by A1,Th24
.= W6 by A2,A13,Th17;
thus P. 9=q. (8+1) by A1,Th24
.=goto (8+2) by A2,A13,Th18
.=goto 10;
A14: card X6 = 8 + 2 by A13,SCMFSA6A:34;
thus P. 10=q. 10 by A1,Th24
.= W7 by A14,Th17;
thus P. 11=q. (10+1) by A1,Th24
.=goto (10+2) by A14,Th18
.=goto 12;
end;
Lm21: for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st Bubble-Sort-Algorithm c= P
holds Comput(P,s,1).IC SCM+FSA = 1 &
Comput(P, s,1).a0=s.a0 & Comput(P, s,1).fsloc 0=s.fsloc 0 &
Comput(P, s,2).IC SCM+FSA = 2 &
Comput(P, s,2).a0=s.a0 & Comput(P, s,2).fsloc 0=s.fsloc 0 &
Comput(P, s,3).IC SCM+FSA = 3 &
Comput(P, s,3).a0=s.a0 & Comput(P, s,3).fsloc 0=s.fsloc 0 &
Comput(P, s,4).IC SCM+FSA = 4 &
Comput(P, s,4).a0=s.a0 & Comput(P, s,4).fsloc 0=s.fsloc 0 &
Comput(P, s,5).IC SCM+FSA = 5 &
Comput(P, s,5).a0=s.a0 & Comput(P, s,5).fsloc 0=s.fsloc 0 &
Comput(P, s,6).IC SCM+FSA = 6 &
Comput(P, s,6).a0=s.a0 & Comput(P, s,6).fsloc 0=s.fsloc 0 &
Comput(P, s,7).IC SCM+FSA = 7 &
Comput(P, s,7).a0=s.a0 & Comput(P, s,7).fsloc 0=s.fsloc 0 &
Comput(P, s,8).IC SCM+FSA = 8 &
Comput(P, s,8).a0=s.a0 & Comput(P, s,8).fsloc 0=s.fsloc 0 &
Comput(P, s,9).IC SCM+FSA = 9 &
Comput(P, s,9).a0=s.a0 & Comput(P, s,9).fsloc 0=s.fsloc 0 &
Comput(P, s,10).IC SCM+FSA = 10 &
Comput(P, s,10).a0=s.a0 & Comput(P, s,10).fsloc 0=s.fsloc 0 &
Comput(P, s,11).IC SCM+FSA = 11 &
Comput(P, s,11).a0=s.a0 & Comput(P, s,11).fsloc 0=s.fsloc 0 &
Comput(P, s,11).a1=len(s.fsloc 0) &
Comput(P, s,11).a2=s.a0 & Comput(P, s,11).a3=s.a0 &
Comput(P, s,11).a4=s.a0 & Comput(P, s,11).a5=s.a0 &
Comput(P, s,11).a6=s.a0
proof
let s be 0-started State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA such that
A1: Bubble-Sort-Algorithm c= P;
A2: IC Comput(P,s,0) = 0 by MEMSTR_0:def 11;
then
A3: Comput(P,s,0+1) =
Exec((P). 0,Comput(P,s,0)) by EXTPRO_1:6
.= Exec(a2:=a0,Comput(P,s,0)) by A1,Lm20;
hence Comput(P,s,1).IC SCM+FSA = IC Comput(P,s,0)+1 by SCMFSA_2:63
.= 1 by A2;
then
A4: IC Comput(P,s,1)= 1;
A5: Comput(P,s,1).a2 =s.a0 by A3,SCMFSA_2:63;
thus
A6: Comput(P,s,1).a0 =s.a0 by A3,Lm1,SCMFSA_2:63;
thus
A7: Comput(P,s,1).(fsloc 0) =s.(fsloc 0) by A3,SCMFSA_2:63;
A8: Comput(P,s,1+1)
= Exec((P). 1,Comput(P,s,1)) by A4,EXTPRO_1:6
.= Exec(goto 2,Comput(P,s,1)) by A1,Lm20;
hence
A9: Comput(P,s,2).IC SCM+FSA = 2 by SCMFSA_2:69;
A10: IC Comput(P,s,2)= 2 by A8,SCMFSA_2:69;
thus
A11: Comput(P,s,2).a0 =s.a0 by A6,A8,SCMFSA_2:69;
thus
A12: Comput(P,s,2).(fsloc 0) =s.(fsloc 0) by A7,A8,SCMFSA_2:69;
A13: Comput(P,s,2).a2 =s.a0 by A5,A8,SCMFSA_2:69;
A14: Comput(P,s,2+1) =
Exec((P). 2,Comput(P,s,2)) by A10,EXTPRO_1:6
.= Exec(a3:=a0,Comput(P,s,2)) by A1,Lm20;
hence Comput(P,s,3).IC SCM+FSA = IC Comput(P,s,2)+1 by SCMFSA_2:63
.= 3 by A9;
then
A15: IC Comput(P,s,3)= 3;
A16: Comput(P,s,3).a3 =s.a0 by A11,A14,SCMFSA_2:63;
thus
A17: Comput(P,s,3).a0 =s.a0 by A11,A14,SCMFSA_2:63;
thus
A18: Comput(P,s,3).(fsloc 0) =s.(fsloc 0) by A12,A14,SCMFSA_2:63;
A19: Comput(P,s,3).a2 =s.a0 by A13,A14,Lm10,SCMFSA_2:63;
A20: Comput(P,s,3+1) =
Exec((P). 3,Comput(P,s,3)) by A15,EXTPRO_1:6
.= Exec(goto 4,Comput(P,s,3)) by A1,Lm20;
hence
A21: Comput(P,s,4).IC SCM+FSA = 4 by SCMFSA_2:69;
A22: IC Comput(P,s,4)= 4 by A20,SCMFSA_2:69;
thus
A23: Comput(P,s,4).a0 =s.a0 by A17,A20,SCMFSA_2:69;
thus
A24: Comput(P,s,4).(fsloc 0) =s.(fsloc 0) by A18,A20,SCMFSA_2:69;
A25: Comput(P,s,4).a2 =s.a0 by A19,A20,SCMFSA_2:69;
A26: Comput(P,s,4).a3 =s.a0 by A16,A20,SCMFSA_2:69;
A27: Comput(P,s,4+1) =
Exec((P). 4,Comput(P,s,4)) by A22,EXTPRO_1:6
.= Exec(a4:=a0,Comput(P,s,4)) by A1,Lm20;
hence Comput(P,s,5).IC SCM+FSA = IC Comput(P,s,4)+1 by SCMFSA_2:63
.= 5 by A21;
then
A28: IC Comput(P,s,5)= 5;
A29: Comput(P,s,5).a4 =s.a0 by A23,A27,SCMFSA_2:63;
thus
A30: Comput(P,s,5).a0 =s.a0 by A23,A27,Lm2,SCMFSA_2:63;
thus
A31: Comput(P,s,5).(fsloc 0) =s.(fsloc 0) by A24,A27,SCMFSA_2:63;
A32: Comput(P,s,5).a2 =s.a0 by A25,A27,Lm11,SCMFSA_2:63;
A33: Comput(P,s,5).a3 =s.a0 by A26,A27,Lm14,SCMFSA_2:63;
A34: Comput(P,s,5+1)
= Exec((P). 5,Comput(P,s,5)) by A28,EXTPRO_1:6
.= Exec(goto 6,Comput(P,s,5)) by A1,Lm20;
hence
A35: Comput(P,s,6).IC SCM+FSA = 6 by SCMFSA_2:69;
A36: IC Comput(P,s,6)= 6 by A34,SCMFSA_2:69;
thus
A37: Comput(P,s,6).a0 =s.a0 by A30,A34,SCMFSA_2:69;
thus
A38: Comput(P,s,6).(fsloc 0) =s.(fsloc 0) by A31,A34,SCMFSA_2:69;
A39: Comput(P,s,6).a2 =s.a0 by A32,A34,SCMFSA_2:69;
A40: Comput(P,s,6).a3 =s.a0 by A33,A34,SCMFSA_2:69;
A41: Comput(P,s,6).a4 =s.a0 by A29,A34,SCMFSA_2:69;
A42: Comput(P,s,6+1) =
Exec((P). 6,Comput(P,s,6)) by A36,EXTPRO_1:6
.= Exec(a5:=a0,Comput(P,s,6)) by A1,Lm20;
hence Comput(P,s,7).IC SCM+FSA = IC Comput(P,s,6)+1 by SCMFSA_2:63
.= 7 by A35;
then
A43: IC Comput(P,s,7)= 7;
A44: Comput(P,s,7).a5 =s.a0 by A37,A42,SCMFSA_2:63;
thus
A45: Comput(P,s,7).a0 =s.a0 by A37,A42,Lm3,SCMFSA_2:63;
thus
A46: Comput(P,s,7).(fsloc 0) =s.(fsloc 0) by A38,A42,SCMFSA_2:63;
A47: Comput(P,s,7).a2 =s.a0 by A39,A42,Lm12,SCMFSA_2:63;
A48: Comput(P,s,7).a3 =s.a0 by A40,A42,Lm15,SCMFSA_2:63;
A49: Comput(P,s,7).a4 =s.a0 by A41,A42,Lm17,SCMFSA_2:63;
A50: Comput(P,s,7+1) =
Exec((P). 7,Comput(P,s,7)) by A43,EXTPRO_1:6
.= Exec(goto 8,Comput(P,s,7)) by A1,Lm20;
hence
A51: Comput(P,s,8).IC SCM+FSA = 8 by SCMFSA_2:69;
A52: IC Comput(P,s,8)= 8 by A50,SCMFSA_2:69;
thus
A53: Comput(P,s,8).a0 =s.a0 by A45,A50,SCMFSA_2:69;
thus
A54: Comput(P,s,8).(fsloc 0) =s.(fsloc 0) by A46,A50,SCMFSA_2:69;
A55: Comput(P,s,8).a2 =s.a0 by A47,A50,SCMFSA_2:69;
A56: Comput(P,s,8).a3 =s.a0 by A48,A50,SCMFSA_2:69;
A57: Comput(P,s,8).a4 =s.a0 by A49,A50,SCMFSA_2:69;
A58: Comput(P,s,8).a5 =s.a0 by A44,A50,SCMFSA_2:69;
A59: Comput(P,s,8+1) =
Exec((P). 8,Comput(P,s,8)) by A52,EXTPRO_1:6
.= Exec(a6:=a0,Comput(P,s,8)) by A1,Lm20;
hence Comput(P,s,9).IC SCM+FSA = IC Comput(P,s,8)+1 by SCMFSA_2:63
.= 9 by A51;
then
A60: IC Comput(P,s,9)= 9;
A61: Comput(P,s,9).a6 =s.a0 by A53,A59,SCMFSA_2:63;
thus
A62: Comput(P,s,9).a0 =s.a0 by A53,A59,Lm4,SCMFSA_2:63;
thus
A63: Comput(P,s,9).(fsloc 0) =s.(fsloc 0) by A54,A59,SCMFSA_2:63;
A64: Comput(P,s,9).a2 =s.a0 by A55,A59,Lm13,SCMFSA_2:63;
A65: Comput(P,s,9).a3 =s.a0 by A56,A59,Lm16,SCMFSA_2:63;
A66: Comput(P,s,9).a4 =s.a0 by A57,A59,Lm18,SCMFSA_2:63;
A67: Comput(P,s,9).a5 =s.a0 by A58,A59,Lm19,SCMFSA_2:63;
A68: Comput(P,s,9+1) = Exec(P.9,Comput(P,s,9)) by A60,EXTPRO_1:6
.= Exec(goto 10,Comput(P,s,9)) by A1,Lm20;
hence
A69: Comput(P,s,10).IC SCM+FSA = 10 by SCMFSA_2:69;
A70: IC Comput(P,s,10)= 10 by A68,SCMFSA_2:69;
thus
A71: Comput(P,s,10).a0 =s.a0 by A62,A68,SCMFSA_2:69;
thus
A72: Comput(P,s,10).(fsloc 0) =s.(fsloc 0) by A63,A68,SCMFSA_2:69;
A73: Comput(P,s,10).a2 =s.a0 by A64,A68,SCMFSA_2:69;
A74: Comput(P,s,10).a3 =s.a0 by A65,A68,SCMFSA_2:69;
A75: Comput(P,s,10).a4 =s.a0 by A66,A68,SCMFSA_2:69;
A76: Comput(P,s,10).a5 =s.a0 by A67,A68,SCMFSA_2:69;
A77: Comput(P,s,10).a6 =s.a0 by A61,A68,SCMFSA_2:69;
A78: Comput(P,s,10+1) = Exec(P.10,Comput(P,s,10)) by A70,EXTPRO_1:6
.= Exec(a1:=len fsloc 0,Comput(P,s,10)) by A1,Lm20;
hence Comput(P,s,11).IC SCM+FSA = IC Comput(P,s,10)+1 by SCMFSA_2:74
.= 11 by A69;
thus Comput(P,s,11).a0 =s.a0 by A71,A78,SCMFSA_2:74;
thus Comput(P,s,11).(fsloc 0) =s.(fsloc 0) by A72,A78,SCMFSA_2:74;
thus Comput(P,s,11).a1 =len(s.fsloc 0) by A72,A78,SCMFSA_2:74;
thus Comput(P,s,11).a2 =s.a0 by A73,A78,Lm5,SCMFSA_2:74;
thus Comput(P,s,11).a3 =s.a0 by A74,A78,Lm6,SCMFSA_2:74;
thus Comput(P,s,11).a4 =s.a0 by A75,A78,Lm7,SCMFSA_2:74;
thus Comput(P,s,11).a5 =s.a0 by A76,A78,Lm8,SCMFSA_2:74;
thus thesis by A77,A78,Lm9,SCMFSA_2:74;
end;
Lm22: body2 does not destroy b2
proof
A1: i1 does not destroy b2 by SCMFSA7B:6,SCMFSA_2:101;
A2: i2 does not destroy b2 by SCMFSA7B:8,SCMFSA_2:101;
A3: i3 does not destroy b2 by SCMFSA7B:14,SCMFSA_2:101;
A4: i4 does not destroy b2 by SCMFSA7B:14,SCMFSA_2:101;
A5: i6 does not destroy b2 by SCMFSA7B:15;
A6: i7 does not destroy b2 by SCMFSA7B:15;
A7: SS does not destroy b2 by SCMFSA8C:56;
i4 ";" i6 ";" i7 does not destroy b2 by A4,A5,A6,SCMFSA8C:54,55;
then
A8: ifc does not destroy b2 by A7,SCMFSA8C:88;
i1 ";" i2 ";" i3 does not destroy b2 by A1,A2,A3,SCMFSA8C:54,55;
then i1 ";" i2 ";" i3 ";" i4 does not destroy b2 by Lm13,SCMFSA7B:14
,SCMFSA8C:54;
then i1 ";" i2 ";" i3 ";" i4 ";" i5 does not destroy b2
by Lm13,SCMFSA7B:8,SCMFSA8C:54;
hence thesis by A8,SCMFSA8C:52;
end;
Lm23: Times(b2,body2) is good InitHalting
proof
thus Times(b2,body2) is good;
let s be State of SCM+FSA such that
A1: Initialize ((intloc 0) .--> 1) c= s;
let P be Instruction-Sequence of SCM+FSA such that
A2: Times(b2,body2) c= P;
A3: P +* Times(b2,body2) = P by A2,FUNCT_4:98;
A5: dom((intloc 0) .--> 1) misses {IC SCM+FSA} by SCMFSA_2:56,ZFMISC_1:11;
Start-At(0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:25;
then
A6: s = Initialize s by A1,FUNCT_4:98,XBOOLE_1:1;
A7: intloc 0 in dom((intloc 0) .--> 1) by TARSKI:def 1;
dom ((intloc 0) .--> 1) misses dom Start-At(0,SCM+FSA) by A5;
then
((intloc 0) .--> 1) c= Initialize((intloc 0) .--> 1)
by FUNCT_4:32;
then ((intloc 0) .--> 1) c= s by A1,XBOOLE_1:1;
then
A8: s.intloc 0 = ((intloc 0) .--> 1).intloc 0 by A7,GRFUNC_1:2
.= 1 by FUNCOP_1:72;
Times(b2,body2) is_halting_on s,P by Lm22,A8,SCM_HALT:62,A6;
hence P halts_on s by A6,A3,SCMFSA7B:def 7;
end;
Lm24: body2 does not destroy b1
proof
A1: i1 does not destroy b1 by SCMFSA7B:6,SCMFSA_2:101;
A2: i2 does not destroy b1 by SCMFSA7B:8,SCMFSA_2:101;
A3: i3 does not destroy b1 by SCMFSA7B:14,SCMFSA_2:101;
A4: i4 does not destroy b1 by SCMFSA7B:14,SCMFSA_2:101;
A5: i6 does not destroy b1 by SCMFSA7B:15;
A6: i7 does not destroy b1 by SCMFSA7B:15;
A7: SS does not destroy b1 by SCMFSA8C:56;
i4 ";" i6 ";" i7 does not destroy b1 by A4,A5,A6,SCMFSA8C:54,55;
then
A8: ifc does not destroy b1 by A7,SCMFSA8C:88;
i1 ";" i2 ";" i3 does not destroy b1 by A1,A2,A3,SCMFSA8C:54,55;
then i1 ";" i2 ";" i3 ";" i4 does not destroy b1 by Lm9,SCMFSA7B:14
,SCMFSA8C:54;
then i1 ";" i2 ";" i3 ";" i4 ";" i5 does not destroy b1
by Lm9,SCMFSA7B:8,SCMFSA8C:54;
hence thesis by A8,SCMFSA8C:52;
end;
Lm25: body1 does not destroy b1
proof
A1: j1 does not destroy b1 by SCMFSA7B:6,SCMFSA_2:101;
A2: j2 does not destroy b1 by SCMFSA7B:8,SCMFSA_2:101;
A3: j3 does not destroy b1 by SCMFSA7B:16,SCMFSA_2:101;
A4: T2 does not destroy b1 by Lm24,SCMFSA8C:93,SCMFSA_2:101;
j1 ";" j2 ";" j3 does not destroy b1 by A1,A2,A3,SCMFSA8C:54,55;
hence thesis by A4,SCMFSA8C:52;
end;
Lm26: Times(b1,body1) is good InitHalting
proof
thus Times(b1,body1) is good;
let s be State of SCM+FSA such that
A1: Initialize ((intloc 0) .--> 1) c= s;
let P be Instruction-Sequence of SCM+FSA such that
A2: Times(b1,body1) c= P;
A3: P +* Times(b1,body1) = P by A2,FUNCT_4:98;
A5: dom((intloc 0) .--> 1) misses {IC SCM+FSA} by SCMFSA_2:56,ZFMISC_1:11;
Start-At(0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:25;
then
A6: s = Initialize s by A1,FUNCT_4:98,XBOOLE_1:1;
A7: intloc 0 in dom((intloc 0) .--> 1) by TARSKI:def 1;
dom ((intloc 0) .--> 1) misses dom Start-At(0,SCM+FSA) by A5;
then ((intloc 0) .--> 1) c= Initialize((intloc 0) .--> 1) by FUNCT_4:32;
then ((intloc 0) .--> 1) c= s by A1,XBOOLE_1:1;
then
A8: s.intloc 0 = ((intloc 0) .--> 1).intloc 0 by A7,GRFUNC_1:2
.= 1 by FUNCOP_1:72;
reconsider TT=T2 as good InitHalting Program of SCM+FSA by Lm23;
body1= j1 ";" j2 ";" j3 ";" TT;
then Times(b1,body1) is_halting_on s,P by Lm25,A8,SCM_HALT:62,A6;
hence P halts_on s by A6,A3,SCMFSA7B:def 7;
end;
theorem
bubble-sort (fsloc 0) is keepInt0_1 InitHalting by Lm26;
Lm27:
for p be Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA holds (s.b6 > 0 implies
IExec(ifc,p,s).f0 =
s.f0+*(|.s.b3.|,(s.f0)/.|.s.b4.|) +*(|.s.b4.|,s.b5)) &
(s.b6 <= 0 implies IExec(ifc,p,s).f0=s.f0)
proof
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
set s0=Initialized s, s1=Exec(i4, s0), s2=IExec(i4 ";" i6,p,s);
A1: s0.f0=s.f0 by SCMFSA_M:37;
s0.b4=s.b4 by SCMFSA_M:37;
then
A2: s1.b6=(s.f0)/.|.s.b4.| by A1,Th1;
A3: s1.f0=s.f0 by A1,SCMFSA_2:72;
A4: s1.b3=s.b3 by Th3;
A5: s1.b4=s.b4 by Th3;
A6: s1.b5=s.b5 by Th3;
A7: s2.f0 =Exec(i6, s1).f0 by SCMFSA6C:9
.=s.f0+*(|.s.b3.|,(s.f0)/.|.s.b4.|) by A2,A3,A4,Th2;
A8: s2.b4=Exec(i6, s1).b4 by SCMFSA6C:8
.=s.b4 by A5,SCMFSA_2:73;
A9: s2.b5=Exec(i6, s1).b5 by SCMFSA6C:8
.=s.b5 by A6,SCMFSA_2:73;
set I=i4 ";" i6 ";" i7, J=Stop SCM+FSA;
hereby
assume s.b6 >0;
hence IExec(if>0(b6,I,J),p,s).f0 = IExec(I,p,s).f0 by SCM_HALT:44
.=Exec(i7, s2).f0 by SCMFSA6C:7
.=s.f0+*(|.s.b3.|,(s.f0)/.|.s.b4.|) +*(|.s.b4.|,s.b5)
by A7,A8,A9,Th2;
end;
assume s.b6 <= 0;
hence IExec(if>0(b6,I,J),p,s).f0 = IExec(J,p,s).f0 by SCM_HALT:44
.=s.f0 by Th5;
end;
Lm28:
for p be Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA holds IExec(ifc,p,s).b3 = s.b3
proof
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
set s1=Exec(i4, Initialized s), s2=IExec(i4 ";" i6,p,s);
A1: s1.b3=s.b3 by Th3;
A2: s2.b3=Exec(i6, s1).b3 by SCMFSA6C:8
.=s.b3 by A1,SCMFSA_2:73;
per cases;
suppose s.b6 >0;
hence IExec(ifc,p,s).b3 = IExec(i4 ";" i6 ";" i7,p,s).b3 by SCM_HALT:44
.=Exec(i7, s2).b3 by SCMFSA6C:6
.=s.b3 by A2,SCMFSA_2:73;
end;
suppose s.b6 <= 0;
hence IExec(ifc,p,s).b3 = IExec(Stop SCM+FSA,p,s).b3 by SCM_HALT:44
.=s.b3 by Th5;
end;
end;
Lm29:
for p be Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA st s.b3 <= len (s.f0) & s.b3 >= 2 holds
IExec(body2,p,s).b3=s.b3-1 &
s.f0, IExec(body2,p,s).f0 are_fiberwise_equipotent &
( s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3) or
s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3-1)) &
( s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3) or
s.f0.(s.b3-1)=IExec(body2,p,s).f0.(s.b3)) &
( s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3-1) or
s.f0.(s.b3-1)=IExec(body2,p,s).f0.(s.b3-1)) &
(for k be set st k<>(s.b3-1) & k<>s.b3 & k in dom (s.f0) holds
s.f0.k=IExec(body2,p,s).f0.k) &
ex x1,x2 be Integer st x1=IExec(body2,p,s).f0.(s.b3-1) &
x2=IExec(body2,p,s).f0.(s.b3) & x1 >= x2
proof
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
assume that
A1: s.b3 <= len (s.f0) and
A2: s.b3 >= 2;
A3: s.b3-1 >= 2-1 by A2,XREAL_1:9;
then
A4: |.(s.b3-1).|=s.b3-1 by ABSVALUE:def 1;
A5: s.b3-1<=len (s.f0) by A1,XREAL_1:146,XXREAL_0:2;
A6: s.b3>= 1 by A2,XXREAL_0:2;
A7: |.s.b3.|=s.b3 by A2,ABSVALUE:def 1;
reconsider k1=s.b3-1 as Element of NAT by A3,INT_1:3;
reconsider k2=s.b3 as Element of NAT by A2,INT_1:3;
A8: k1 in dom (s.f0) by A3,A5,FINSEQ_3:25;
reconsider n1=s.f0.k1 as Integer;
A9: k2 in dom (s.f0) by A1,A6,FINSEQ_3:25;
reconsider n2=s.f0.k2 as Integer;
set s0=Initialized s, s1=Exec(i1, s0), s2=IExec(i1 ";" i2,p,s),
s3=IExec(i1 ";" i2 ";" i3,p,s), s4=IExec(i1 ";" i2 ";" i3 ";" i4,p,s),
s5=IExec(i1 ";" i2 ";" i3 ";" i4 ";"i5,p,s), s6=IExec(body2,p,s);
A10: s1.b4=s0.b3 by SCMFSA_2:63
.=s.b3 by SCMFSA_M:37;
A11: s1.f0=s0.f0 by SCMFSA_2:63
.=s.f0 by SCMFSA_M:37;
A12: s1.b3=s.b3 by Th4;
A13: s1.a0=s0.a0 by SCMFSA_2:63
.=1 by SCMFSA_M:9;
A14: s2.f0 =Exec(i2, s1).f0 by SCMFSA6C:9
.=s.f0 by A11,SCMFSA_2:65;
A15: s2.b3 =Exec(i2, s1).b3 by SCMFSA6C:8
.=s.b3-1 by A12,A13,SCMFSA_2:65;
A16: s2.b4=Exec(i2, s1).b4 by SCMFSA6C:8
.=s.b3 by A10,Lm14,SCMFSA_2:65;
A17: s3.f0 = Exec(i3, s2).f0 by SCMFSA6C:7
.=s.f0 by A14,SCMFSA_2:72;
A18: (s.f0)/.k1=n1 by A3,A5,FINSEQ_4:15;
A19: s3.b5=Exec(i3, s2).b5 by SCMFSA6C:6
.=n1 by A4,A14,A15,A18,Th1;
A20: s3.b4=Exec(i3, s2).b4 by SCMFSA6C:6
.=s.b3 by A16,Lm17,SCMFSA_2:72;
A21: s3.b3=Exec(i3, s2).b3 by SCMFSA6C:6
.=s.b3-1 by A15,Lm15,SCMFSA_2:72;
A22: s4.f0 = Exec(i4, s3).f0 by SCMFSA6C:7
.=s.f0 by A17,SCMFSA_2:72;
A23: (s.f0)/.k2=n2 by A1,A6,FINSEQ_4:15;
A24: s4.b6=Exec(i4, s3).b6 by SCMFSA6C:6
.=n2 by A7,A17,A20,A23,Th1;
A25: s4.b3=Exec(i4, s3).b3 by SCMFSA6C:6
.=s.b3-1 by A21,Lm16,SCMFSA_2:72;
A26: s4.b4=Exec(i4, s3).b4 by SCMFSA6C:6
.=s.b3 by A20,Lm18,SCMFSA_2:72;
A27: s4.b5=Exec(i4, s3).b5 by SCMFSA6C:6
.=s.f0.(s.b3-1) by A19,Lm19,SCMFSA_2:72;
A28: s5.f0=Exec(i5, s4).f0 by SCMFSA6C:7
.=s.f0 by A22,SCMFSA_2:65;
A29: s5.b3=Exec(i5, s4).b3 by SCMFSA6C:6
.=s.b3-1 by A25,Lm16,SCMFSA_2:65;
A30: s5.b4=Exec(i5, s4).b4 by SCMFSA6C:6
.=s.b3 by A26,Lm18,SCMFSA_2:65;
A31: s5.b5=Exec(i5, s4).b5 by SCMFSA6C:6
.=n1 by A27,Lm19,SCMFSA_2:65;
A32: s5.b6=Exec(i5, s4).b6 by SCMFSA6C:6
.=n2- n1 by A24,A27,SCMFSA_2:65;
A33: s6.f0 = IExec(ifc,p,s5).f0 by SCMFSA6C:2;
thus s6.b3 = IExec(ifc,p,s5).b3 by SCMFSA6C:1
.=s.b3-1 by A29,Lm28;
per cases;
suppose
A34: s5.b6 >0;
then
A35: s6.f0=s.f0+*(k1,n2) +*(k2,n1) by A4,A7,A23,A28,A29,A30,A31,A33,Lm27;
A36: dom (s.f0+*(k1,n2))=dom (s.f0) by FUNCT_7:30;
then
A37: dom (s6.f0)=dom (s.f0) by A35,FUNCT_7:30;
A38: k2 in dom (s.f0+*(k1,n2)) by A1,A6,A36,FINSEQ_3:25;
A39: s6.f0.k2=s.f0.k1 by A9,A35,A36,FUNCT_7:31;
A40: now per cases;
suppose k1=k2;
hence s6.f0.k1=s.f0.k2;
end;
suppose k1<>k2;
hence s6.f0.k1=(s.f0+*(k1,n2)).k1 by A35,FUNCT_7:32
.=s.f0.k2 by A8,FUNCT_7:31;
end;
end;
A41: now
let k be set;
assume that
A42: k<>k1 and
A43: k<>k2
and k in dom (s.f0);
thus s6.f0.k= (s.f0+*(k1,n2)).k by A35,A43,FUNCT_7:32
.= s.f0.k by A42,FUNCT_7:32;
end;
hence s.f0, s6.f0 are_fiberwise_equipotent by A8,A9,A37,A39,A40,RFINSEQ:28;
thus s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3) or
s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3-1) by A40;
thus s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3) or
s.f0.(s.b3-1)=IExec(body2,p,s).f0.(s.b3) by A35,A38,FUNCT_7:31;
thus s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3-1) or
s.f0.(s.b3-1)=IExec(body2,p,s).f0.(s.b3-1) by A40;
thus for k be set st k<>(s.b3-1) & k<>s.b3 & k in dom (s.f0) holds
s.f0.k=s6.f0.k by A41;
A44: n2-n1+n1 > 0+n1 by A32,A34,XREAL_1:6;
take n2,n1;
thus thesis by A9,A35,A36,A40,A44,FUNCT_7:31;
end;
suppose
A45: s5.b6 <=0;
hence s.f0,s6.f0 are_fiberwise_equipotent by A28,A33,Lm27;
thus s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3) or
s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3-1) by A28,A33,A45,Lm27;
thus s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3) or
s.f0.(s.b3-1)=IExec(body2,p,s).f0.(s.b3) by A28,A33,A45,Lm27;
thus s.f0.(s.b3)=IExec(body2,p,s).f0.(s.b3-1) or
s.f0.(s.b3-1)=IExec(body2,p,s).f0.(s.b3-1) by A28,A33,A45,Lm27;
thus for k be set st k<>(s.b3-1) & k<>s.b3 & k in dom (s.f0) holds
s.f0.k=s6.f0.k by A28,A33,A45,Lm27;
A46: n2-n1+n1 <= 0+n1 by A32,A45,XREAL_1:6;
take n1,n2;
thus thesis by A28,A33,A45,A46,Lm27;
end;
end;
Lm30:
for p be Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA st s.b2>=0 & s.b2<s.b3 & s.b3 <= len (s.f0)
holds ex k be Nat st k<=s.b3 & k>=s.b3-s.b2 &
IExec(T2,p,s).f0.k = s.f0.(s.b3)
proof
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
assume that
A1: s.b2>=0 and
A2: s.b2<s.b3 and
A3: s.b3 <= len (s.f0);
defpred P[Nat] means
for t be State of SCM+FSA,q st t.b2=$1 & t.b2<t.b3 & t.b3 <= len (t.f0)
holds (for m be Nat st m>t.b3 & m <= len (t.f0) holds
t.f0.m=IExec(T2,q,t).f0.m) & ex n be Nat st n<=t.b3 &
n>=t.b3-$1 & IExec(T2,q,t).f0.n = t.f0.(t.b3);
A4: P[ 0]
proof
let t be State of SCM+FSA,q;
assume that
A5: t.b2=0 and
A6: t.b2<t.b3
and t.b3 <= len (t.f0);
set If0=IExec(T2,q,t).f0;
thus for m be Nat st m>t.b3 & m <= len (t.f0) holds
t.f0.m=If0.m by A5,SCM_HALT:67;
reconsider n=t.b3 as Element of NAT by A5,A6,INT_1:3;
take n;
thus n<=t.b3;
thus n>=t.b3-0;
thus thesis by A5,SCM_HALT:67;
end;
set sb2=SubFrom(b2,a0);
A7: now
let k be Nat;
assume
A8: P[k];
now
let t be State of SCM+FSA,q;
assume that
A9: t.b2=k+1 and
A10: t.b2<t.b3 and
A11: t.b3 <= len (t.f0);
set t1=IExec(body2 ";"sb2,q,t), IB=IExec(body2,q,t), t2=IExec(T2,q,t1);
A12: t1.b2= Exec(sb2, IB).b2 by SCM_HALT:23
.=IB.b2-IB.a0 by SCMFSA_2:65
.=IB.b2-1 by SCM_HALT:9
.=(Initialized t).b2-1 by Lm22,SCM_HALT:53
.=t.b2-1 by SCMFSA_M:37;
A13: 2 <= k+2 by NAT_1:11;
k+1+1 <= t.b3 by A9,A10,INT_1:7;
then
A14: 2 <= t.b3 by A13,XXREAL_0:2;
A15: t1.b3=Exec(sb2, IB).b3 by SCM_HALT:23
.=IB.b3 by Lm10,SCMFSA_2:65
.=t.b3-1 by A11,A14,Lm29;
A16: t.b2-1 < t.b3-1 by A10,XREAL_1:9;
A17: t1.b2 < t1.b3 by A10,A12,A15,XREAL_1:9;
A18: t1.f0= Exec(sb2, IB).f0 by SCM_HALT:24
.=IB.f0 by SCMFSA_2:65;
A19: t.f0,IB.f0 are_fiberwise_equipotent by A11,A14,Lm29;
then
A20: len (t.f0) = len (t1.f0) by A18,RFINSEQ:3;
then
A21: t1.b3 <= len (t1.f0) by A11,A15,XREAL_1:146,XXREAL_0:2;
A22: IExec(T2,q,t).f0=t2.f0 by A9,Lm22,SCM_HALT:69;
A23: IB.f0 =Exec(sb2, IB).f0 by SCMFSA_2:65
.=t1.f0 by SCM_HALT:24;
thus for m be Nat st m>t.b3 & m <= len (t.f0) holds
t.f0.m=IExec(T2,q,t).f0.m
proof
let m be Nat;
assume that
A24: m>t.b3 and
A25: m <= len (t.f0);
A26: t.b3>t.b3-1 by XREAL_1:146;
A27: m > t1.b3 by A15,A24,XREAL_1:146,XXREAL_0:2;
A28: m <= len (t1.f0) by A18,A19,A25,RFINSEQ:3;
m>=2 by A14,A24,XXREAL_0:2;
then m>=1 by XXREAL_0:2;
then m in dom (t.f0) by A25,FINSEQ_3:25;
hence t.f0.m=t1.f0.m by A11,A14,A23,A24,A26,Lm29
.=IExec(T2,q,t).f0.m by A8,A9,A12,A17,A21,A22,A27,A28;
end;
hereby
reconsider n=t.b3 as Element of NAT by A9,A10,INT_1:3;
reconsider n as Nat;
per cases by A11,A14,Lm29;
suppose
A29: t.f0.(t.b3)=IExec(body2,q,t).f0.(t.b3);
take n;
thus n<=t.b3;
n<=n+(k+1) by NAT_1:11;
hence n>=t.b3-(k+1) by XREAL_1:20;
thus IExec(T2,q,t).f0.n=t.f0.(t.b3)
by A8,A9,A11,A12,A15,A16,A20,A21,A22,A23,A29,XREAL_1:146;
end;
suppose
A30: t.f0.(t.b3)=IExec(body2,q,t).f0.(t.b3-1);
consider m be Nat such that
A31: m<=t1.b3 and
A32: m>=t1.b3-k and
A33: IExec(T2,q,t1).f0.m = t1.f0.(t1.b3) by A8,A9,A12,A17,A21;
take m;
thus m<=t.b3 by A15,A31,XREAL_1:146,XXREAL_0:2;
thus m>=t.b3-(k+1) by A15,A32;
thus IExec(T2,q,t).f0.m =t.f0.(t.b3)
by A9,A15,A23,A30,A33,Lm22,SCM_HALT:69;
end;
end;
end;
hence P[k+1];
end;
A34: for k be Nat holds P[k] from NAT_1:sch 2(A4,A7);
reconsider i=s.b2 as Element of NAT by A1,INT_1:3;
P[i] by A34;
hence thesis by A2,A3;
end;
Lm31: for k be Nat holds
for t be State of SCM+FSA,q st k=t.b2 & k< t.b3 & t.b3 <= len (t.f0) holds
t.f0, IExec(T2,q,t).f0 are_fiberwise_equipotent & (for m be Nat
st m <(t.b3-k) & m>=1 or (m>t.b3 & m in dom (t.f0)) holds
t.f0.m=IExec(T2,q,t).f0.m) &
(for m be Nat st m >= (t.b3-k) & m<=t.b3 holds
(ex x1,x2 be Integer st
x1 =IExec(T2,q,t).f0.(t.b3-k) & x2=IExec(T2,q,t).f0.m & x1 >= x2)) &
for i be Nat st i>=t.b3-k & i<=t.b3 holds
ex n be Nat st n>=t.b3-k & n<=t.b3 & IExec(T2,q,t).f0.i=t.f0.n
proof
defpred P[Nat] means
for t be State of SCM+FSA st $1=t.b2 & $1 < t.b3 & t.b3 <= len (t.f0) holds
(t.f0, IExec(T2,q,t).f0 are_fiberwise_equipotent) & (for m be Nat
st m <(t.b3-$1) & m>=1 or (m>t.b3 & m in dom (t.f0)) holds
t.f0.m=IExec(T2,q,t).f0.m) &
(for m be Nat st m >= (t.b3-$1) & m<=t.b3 holds
(ex x1,x2 be Integer st
x1 =IExec(T2,q,t).f0.(t.b3-$1) & x2=IExec(T2,q,t).f0.m & x1 >= x2)) &
for i be Nat st i>=t.b3-$1 & i<=t.b3 holds
ex n be Nat st n>=t.b3-$1 & n<=t.b3 & IExec(T2,q,t).f0.i=t.f0.n;
now
let t be State of SCM+FSA,q;
assume that
A1: 0=t.b2
and 0 < t.b3
and t.b3 <= len (t.f0);
set If0=IExec(T2,q,t).f0;
thus t.f0, If0 are_fiberwise_equipotent by A1,SCM_HALT:67;
thus for m be Nat
st m < (t.b3-0) & m>=1 or m>t.b3 & m in dom (t.f0)
holds t.f0.m=IExec(T2,q,t).f0.m by A1,SCM_HALT:67;
hereby
let m be Nat;
assume that
A2: m >= (t.b3-0) and
A3: m<=t.b3;
A4: m=t.b3 by A2,A3,XXREAL_0:1;
reconsider n1=t.f0.m as Integer;
take x1=n1,x2=n1;
thus x1=IExec(T2,q,t).f0.(t.b3-0) by A1,A4,SCM_HALT:67;
thus x2=If0.m by A1,SCM_HALT:67;
thus x1 >= x2;
end;
let i be Nat;
assume that
A5: i>=t.b3-0 and
A6: i<=t.b3;
take n=i;
thus n>=t.b3-0 & n<=t.b3 by A5,A6;
thus IExec(T2,q,t).f0.i=t.f0.n by A1,SCM_HALT:67;
end;
then
A7: P[ 0];
set sb2=SubFrom(b2,a0);
A8: now
let k be Nat;
assume
A9: P[k];
now
let t be State of SCM+FSA,q;
set t1=IExec(body2 ";"sb2,q,t), IB=IExec(body2,q,t), t2=IExec(T2,q,t1);
assume that
A10: k+1=t.b2 and
A11: k+1 < t.b3 and
A12: t.b3 <= len (t.f0);
A13: t1.b2= Exec(sb2, IB).b2 by SCM_HALT:23
.=IB.b2-IB.a0 by SCMFSA_2:65
.=IB.b2-1 by SCM_HALT:9
.=(Initialized t).b2-1 by Lm22,SCM_HALT:53
.=k+1-1 by A10,SCMFSA_M:37
.=k;
A14: 2 <= k+2 by NAT_1:11;
k+1+1 <= t.b3 by A11,INT_1:7;
then
A15: 2 <= t.b3 by A14,XXREAL_0:2;
A16: t1.b3=Exec(sb2, IB).b3 by SCM_HALT:23
.=IB.b3 by Lm10,SCMFSA_2:65
.=t.b3-1 by A12,A15,Lm29;
A17: k+1-1 < t.b3-1 by A11,XREAL_1:9;
A18: t1.f0= Exec(sb2, IB).f0 by SCM_HALT:24
.=IB.f0 by SCMFSA_2:65;
A19: t.f0,IB.f0 are_fiberwise_equipotent by A12,A15,Lm29;
then
A20: len (t.f0) = len (t1.f0) by A18,RFINSEQ:3;
A21: t.b3 <= len (t1.f0) by A12,A18,A19,RFINSEQ:3;
A22: t1.b3 <= len (t1.f0) by A12,A16,A20,XREAL_1:146,XXREAL_0:2;
A23: t.b3=t1.b3+1 by A16;
A24: t1.f0, t2.f0 are_fiberwise_equipotent by A9,A13,A16,A17,A22;
A25: IExec(T2,q,t).f0=t2.f0 by A10,Lm22,SCM_HALT:69;
t1.f0, IExec(T2,q,t).f0 are_fiberwise_equipotent by A10,A24,Lm22,
SCM_HALT:69;
hence t.f0,IExec(T2,q,t).f0 are_fiberwise_equipotent
by A18,A19,CLASSES1:76;
A26: t.b3-(k+1)=t1.b3-k by A16;
consider n1,n2 be Integer such that
A27: n1=IB.f0.(t.b3-1) and
A28: n2=IB.f0.(t.b3) and
A29: n1 >= n2 by A12,A15,Lm29;
A30: IB.f0 =Exec(sb2, IB).f0 by SCMFSA_2:65
.=t1.f0 by SCM_HALT:24;
A31: t.b3 in NAT by A11,INT_1:3;
A32: t.b3 >= 1 by A15,XXREAL_0:2;
then
A33: t.b3 in dom (t1.f0) by A12,A20,A31,FINSEQ_3:25;
hereby
let m be Nat;
assume that
A34: m <(t.b3-(k+1)) & m>=1 or m>t.b3 & m in dom (t.f0);
per cases by A34;
suppose
A35: m < (t.b3-(k+1)) & m>=1;
A36: t.b3-(k+1)+(k+1)=t.b3;
A37: m+(k+1) < t.b3-(k+1)+(k+1) by A35,XREAL_1:6;
A38: m+(k+1) < t.b3 by A35,A36,XREAL_1:6;
m<=m+(k+1) by NAT_1:11;
then m<=t.b3 by A37,XXREAL_0:2;
then m<=len(t1.f0) by A12,A20,XXREAL_0:2;
then
A39: m in dom (t.f0) by A20,A35,FINSEQ_3:25;
A40: m<>t.b3 by A35,A36,XREAL_1:29;
m<>t.b3-1
proof
assume
A41: m=t.b3-1;
m+(k+1)=m+1+k;
hence contradiction by A38,A41,NAT_1:11;
end;
hence t.f0.m=t1.f0.m by A12,A15,A30,A39,A40,Lm29
.=IExec(T2,q,t).f0.m by A9,A13,A17,A22,A25,A26,A35;
end;
suppose
A42: m>t.b3 & m in dom (t.f0);
then
A43: m in dom (t1.f0) by A18,A19,RFINSEQ:3;
A44: t.b3>t.b3-1 by XREAL_1:146;
A45: m >t1.b3 by A16,A42,XREAL_1:146,XXREAL_0:2;
thus t.f0.m=t1.f0.m by A12,A15,A30,A42,A44,Lm29
.=IExec(T2,q,t).f0.m by A9,A13,A16,A17,A22,A25,A43,A45;
end;
end;
hereby
let m be Nat;
assume that
A46: m >= (t.b3-(k+1)) and
A47: m<=t.b3;
consider nn be Nat such that
A48: nn<=t1.b3 and
A49: nn>=t1.b3-t1.b2 and
A50: t2.f0.nn = t1.f0.(t1.b3)
by A13,A16,A17,A22,Lm30;
consider y1,y2 be Integer such that
A51: y1 =t2.f0.(t1.b3-k) and
A52: y2=t2.f0.nn and
A53: y1 >= y2 by A9,A13,A16,A17,A22,A48,A49;
per cases;
suppose
A54: m>t1.b3;
then m>=t1.b3+1 by INT_1:7;
then
A55: m=t.b3 by A16,A47,XXREAL_0:1;
take y1,n2;
thus y1=IExec(T2,q,t).f0.(t.b3-(k+1))
by A10,A16,A51,Lm22,SCM_HALT:69;
thus n2=IExec(T2,q,t).f0.m by A9,A13,A16,A17,A22,A25,A28,A30,A33,A54
,A55;
thus y1 >= n2 by A16,A27,A29,A30,A50,A52,A53,XXREAL_0:2;
end;
suppose m<=t1.b3;
then consider y1,y2 be Integer such that
A56: y1 =t2.f0.(t1.b3-k) and
A57: y2=t2.f0.m and
A58: y1 >= y2
by A9,A13,A16,A17,A22,A46;
take y1,y2;
thus y1=IExec(T2,q,t).f0.(t.b3-(k+1))
by A10,A16,A56,Lm22,SCM_HALT:69;
thus y2=IExec(T2,q,t).f0.m by A10,A57,Lm22,SCM_HALT:69;
thus y1>=y2 by A58;
end;
end;
thus for i be Nat st i>=t.b3-(k+1) & i<=t.b3 holds
ex n be Nat st n>=t.b3-(k+1) & n<=t.b3 &
IExec(T2,q,t).f0.i=t.f0.n
proof
let i be Nat;
assume that
A59: i>=t.b3-(k+1) and
A60: i<=t.b3;
per cases;
suppose
A61: i=t.b3;
then
A62: i>t1.b3 by A23,XREAL_1:29;
A63: i in dom (t1.f0) by A21,A32,A61,FINSEQ_3:25;
per cases by A12,A15,Lm29;
suppose
A64: t.f0.(t.b3)=IExec(body2,q,t).f0.(t.b3);
reconsider n=t.b3 as Element of NAT by A11,INT_1:3;
take n;
thus n>=t.b3-(k+1) & n<=t.b3 by A59,A61;
thus IExec(T2,q,t).f0.i=t.f0.n by A9,A13,A16,A17,A22,A25,A30,A61
,A62,A63,A64;
end;
suppose
A65: t.f0.(t.b3-1)=IExec(body2,q,t).f0.(t.b3);
t.b3-1>=1-1 by A32,XREAL_1:9;
then reconsider n=t.b3-1 as Element of NAT by INT_1:3;
take n;
n<=n+k by NAT_1:11;
hence n>=t.b3-(k+1) by A26,XREAL_1:20;
thus n<=t.b3 by XREAL_1:146;
thus IExec(T2,q,t).f0.i=t.f0.n by A9,A13,A16,A17,A22,A25,A30,A61
,A62,A63,A65;
end;
end;
suppose i<>t.b3;
then i < t.b3 by A60,XXREAL_0:1;
then i+1 <= t.b3 by INT_1:7;
then i<=t1.b3 by A16,XREAL_1:19;
then consider n be Nat such that
A66: n>=t1.b3-k and
A67: n<=t1.b3 and
A68: t2.f0.i=t1.f0.n by A9,A13,A16,A17,A22,A59;
thus ex n be Nat st n>=t.b3-(k+1) & n<=t.b3 &
IExec(T2,q,t).f0.i=t.f0.n
proof
per cases;
suppose
A69: n=t1.b3;
per cases by A12,A15,Lm29;
suppose
A70: t.f0.(t.b3)=IExec(body2,q,t).f0.(t.b3-1);
reconsider m=t.b3 as Element of NAT by A11,INT_1:3;
take m;
m <= m +(k+1) by NAT_1:11;
hence m >= t.b3-(k+1) by XREAL_1:20;
thus m <= t.b3;
thus IExec(T2,q,t).f0.i=t.f0.m
by A10,A16,A30,A68,A69,A70,Lm22,SCM_HALT:69;
end;
suppose
A71: t.f0.(t.b3-1)=IExec(body2,q,t).f0.(t.b3-1);
take n;
thus n>=t.b3-(k+1) by A16,A66;
thus n<=t.b3 by A16,A69,XREAL_1:146;
thus IExec(T2,q,t).f0.i=t.f0.n
by A10,A16,A30,A68,A69,A71,Lm22,SCM_HALT:69;
end;
end;
suppose
A72: n<>t1.b3;
A73: t1.b3 < t.b3 by A16,XREAL_1:146;
A74: n<t.b3 by A16,A67,XREAL_1:146,XXREAL_0:2;
k-k < t1.b3-k by A16,A17,XREAL_1:9;
then
A75: n>=0+1 by A66,INT_1:7;
n<= len (t1.f0) by A12,A20,A74,XXREAL_0:2;
then
A76: n in dom (t.f0) by A20,A75,FINSEQ_3:25;
take n;
thus n>=t.b3-(k+1) by A16,A66;
thus n<=t.b3 by A16,A67,XREAL_1:146,XXREAL_0:2;
thus thesis by A12,A15,A16,A25,A30,A67,A68,A72,A73,A76,Lm29;
end;
end;
end;
end;
end;
hence P[k + 1];
end;
for k be Nat holds P[k] from NAT_1:sch 2(A7,A8);
hence thesis;
end;
Lm32:
for p be Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA holds IExec(Sb,p,s).b2=s.b1-1 &
IExec(Sb,p,s).b3=len (s.f0) & IExec(Sb,p,s).f0=s.f0
proof
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
set s0=Initialized s, s1=Exec(j1,s0), s2=IExec(j1 ";"j2,p,s),
s3=IExec(j1 ";" j2 ";" j3,p,s);
A1: s1.b2=s0.b1 by SCMFSA_2:63
.=s.b1 by SCMFSA_M:37;
A2: s1.f0=s0.f0 by SCMFSA_2:63
.=s.f0 by SCMFSA_M:37;
A3: s1.a0=s0.a0 by SCMFSA_2:63
.=1 by SCMFSA_M:9;
A4: s2.f0 =Exec(j2, s1).f0 by SCMFSA6C:9
.=s.f0 by A2,SCMFSA_2:65;
A5: s2.b2 =Exec(j2, s1).b2 by SCMFSA6C:8
.=s.b1-1 by A1,A3,SCMFSA_2:65;
thus s3.b2 = Exec(j3, s2).b2 by SCMFSA6C:6
.=s.b1-1 by A5,Lm10,SCMFSA_2:74;
thus s3.b3 = Exec(j3, s2).b3 by SCMFSA6C:6
.=len(s.f0) by A4,SCMFSA_2:74;
thus s3.f0 = Exec(j3, s2).f0 by SCMFSA6C:7
.=s.f0 by A4,SCMFSA_2:74;
end;
Lm33:
for p be Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA st s.b1=len (s.f0) holds
s.f0, IExec(T1,p,s).f0 are_fiberwise_equipotent &
for i,j be Nat st i>=1 & j<=len (s.f0) & i<j
for x1,x2 be Integer st x1 =IExec(T1,p,s).f0.i &
x2=IExec(T1,p,s).f0.j holds x1 >= x2
proof
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
assume
A1: s.b1=len (s.f0);
per cases;
suppose
A2: len (s.f0)=0;
hence s.f0, IExec(T1,p,s).f0 are_fiberwise_equipotent
by A1,Lm23,SCM_HALT:67;
thus thesis by A2;
end;
suppose
A3: len (s.f0)<>0;
defpred P[Nat] means
for t be State of SCM+FSA,q st t.b1=$1+1 & t.b1<=len (t.f0) holds
(t.f0, IExec(T1,q,t).f0 are_fiberwise_equipotent) &
(for i,j be Nat st i>=len(t.f0)-$1 & j<=len (t.f0) & i<j
for x1,x2 be Integer st x1 =IExec(T1,q,t).f0.i & x2=IExec(T1,q,t).f0.j
holds x1 >= x2) & (for i be Nat st i<len(t.f0)-$1 & i>=1
holds IExec(T1,q,t).f0.i=t.f0.i) &
(for i be Nat st i>=len(t.f0)-$1 & i<=len (t.f0) holds
ex n be Nat st n>=len(t.f0)-$1 & n<=len (t.f0) &
IExec(T1,q,t).f0.i=t.f0.n);
set B11=SubFrom(b1,a0);
A4: P[ 0]
proof
let t be State of SCM+FSA,q;
assume that
A5: t.b1=0+1
and t.b1 <= len (t.f0);
set IB=IExec(body1 ";" B11,q,t);
A6: IB.b1=1-1 by A5,Lm23,Lm25,SCM_HALT:66;
A7: IExec(Sb,q,t).b2=1-1 by A5,Lm32;
A8: IExec(T1,q,t).f0=IExec(T1,q,IB).f0 by A5,Lm23,Lm25,SCM_HALT:69
.=IB.f0 by A6,Lm23,SCM_HALT:67
.=Exec(B11,IExec(body1,q,t)).f0 by Lm23,SCM_HALT:24
.=IExec(body1,q,t).f0 by SCMFSA_2:65
.=IExec(T2,q,IExec(Sb,q,t)).f0 by Lm23,SCM_HALT:21
.=IExec(Sb,q,t).f0 by A7,SCM_HALT:67
.=t.f0 by Lm32;
hence t.f0, IExec(T1,q,t).f0 are_fiberwise_equipotent;
thus
for i,j be Nat st i>=len(t.f0)-0 & j<=len (t.f0) & i<j
for x1,x2 be Integer st x1 =IExec(T1,q,t).f0.i &
x2=IExec(T1,q,t).f0.j holds x1 >= x2 by XXREAL_0:2;
thus for i be Nat st i<len(t.f0)-0 & i>=1 holds
IExec(T1,q,t).f0.i=t.f0.i by A8;
let i be Nat;
assume that
A9: i>=len(t.f0)-0 and
A10: i<=len (t.f0);
take n=i;
thus n>=len(t.f0)-0 & n<=len (t.f0) by A9,A10;
thus thesis by A8;
end;
A11: now
let k be Nat;
assume
A12: P[k];
now
let t be State of SCM+FSA,q;
set t1=IExec(body1 ";"B11,q,t), IB=IExec(body1,q,t), t2=IExec(T1,q,t1);
assume that
A13: t.b1=(k+1)+1 and
A14: t.b1<=len (t.f0);
A15: t1.b1= Exec(B11, IB).b1 by Lm23,SCM_HALT:23
.=IB.b1-IB.a0 by SCMFSA_2:65
.=IB.b1-1 by Lm23,SCM_HALT:9
.=(Initialized t).b1-1 by Lm23,Lm25,SCM_HALT:53
.=(k+1)+1-1 by A13,SCMFSA_M:37
.=k+1;
then t1.b1 < t.b1 by A13,XREAL_1:29;
then
A16: t1.b1 <= len (t.f0) by A14,XXREAL_0:2;
set Ts=IExec(Sb,q,t);
A17: Ts.b2=(k+1)+1-1 by A13,Lm32
.=k+1;
A18: Ts.b3=len (t.f0) by Lm32;
then
A19: Ts.b3=len (Ts.f0) by Lm32;
A20: k+1 < (k+1)+1 by XREAL_1:29;
A21: k+1 < t.b1 by A13,XREAL_1:29;
A22: k+1 < len (t.f0) by A13,A14,A20,XXREAL_0:2;
A23: k+1 < Ts.b3 by A14,A18,A21,XXREAL_0:2;
A24: Ts.f0, IExec(T2,q,Ts).f0 are_fiberwise_equipotent
by A17,A18,A19,A22,Lm31;
A25: Ts.f0=t.f0 by Lm32;
A26: t1.f0= Exec(B11,IB).f0 by Lm23,SCM_HALT:24
.=IB.f0 by SCMFSA_2:65
.=IExec(T2,q,Ts).f0 by Lm23,SCM_HALT:21;
then
A27: t.f0,t1.f0 are_fiberwise_equipotent by A17,A18,A23,A25,Lm31;
A28: len (t.f0) = len (t1.f0) by A24,A25,A26,RFINSEQ:3;
A29: t1.b1 <= len (t1.f0) by A16,A27,RFINSEQ:3;
A30: t1.f0, IExec(T1,q,t1).f0 are_fiberwise_equipotent by A12,A15,A16,A28;
A31: IExec(T1,q,t).f0=t2.f0 by A13,Lm23,Lm25,SCM_HALT:69;
hence t.f0,IExec(T1,q,t).f0 are_fiberwise_equipotent
by A27,A30,CLASSES1:76;
set lk=len(t.f0)-(k+1);
A32: lk+1=len (t1.f0)-k by A28;
thus for i,j be Nat
st i>=len(t.f0)-(k+1) & j<=len (t.f0) & i<j
for x1,x2 be Integer st x1 =IExec(T1,q,t).f0.i &
x2=IExec(T1,q,t).f0.j holds x1 >= x2
proof
let i,j be Nat;
assume that
A33: i>=lk and
A34: j<=len (t.f0) and
A35: i<j;
j > lk by A33,A35,XXREAL_0:2;
then j >= len (t1.f0)-k by A32,INT_1:7;
then consider n be Nat such that
A36: n>=len(t1.f0)-k and
A37: n<=len (t1.f0) and
A38: IExec(T1,q,t1).f0.j=t1.f0.n by A12,A15,A16,A28,A34;
lk < lk +1 by XREAL_1:29;
then
A39: n >= Ts.b3-(k+1) by A18,A28,A36,XXREAL_0:2;
A40: n <= Ts.b3 by A28,A37,Lm32;
hereby
let x1,x2 be Integer;
assume that
A41: x1 =IExec(T1,q,t).f0.i and
A42: x2=IExec(T1,q,t).f0.j;
per cases;
suppose
A43: i=lk;
A44: ex y1,y2 be Integer st ( y1 =IExec(T2,q,Ts).f0.(Ts.b3-(k+1)))
&( y2=IExec(T2,q,Ts).f0.n)&( y1 >= y2)
by A17,A19,A23,A39,A40,Lm31;
A45: i<len(t1.f0)-k by A32,A43,XREAL_1:29;
A46: 1<=i by A13,A14,A43,XREAL_1:19;
i=Ts.b3-(k+1) by A43,Lm32;
hence
x1 >= x2 by A12,A15,A16,A26,A28,A31,A38,A41,A42,A44,A45,A46;
end;
suppose i<>lk;
then i>lk by A33,XXREAL_0:1;
then i>=len (t1.f0)-k by A32,INT_1:7;
hence x1 >= x2 by A12,A15,A16,A28,A31,A34,A35,A41,A42;
end;
end;
end;
thus for i be Nat st i<len(t.f0)-(k+1) & i>=1 holds
IExec(T1,q,t).f0.i=t.f0.i
proof
let i be Nat;
assume that
A47: i<lk and
A48: i>=1;
lk < lk+1 by XREAL_1:29;
then i < len (t1.f0)-k by A28,A47,XXREAL_0:2;
hence IExec(T1,q,t).f0.i=t1.f0.i by A12,A15,A29,A31,A48
.=t.f0.i by A17,A18,A23,A25,A26,A47,A48,Lm31;
end;
thus for i be Nat
st i>=len(t.f0)-(k+1) & i<=len (t.f0) holds
ex n be Nat st n>=len(t.f0)-(k+1) & n<=len (t.f0) &
IExec(T1,q,t).f0.i=t.f0.n
proof
let i be Nat;
assume that
A49: i>=len(t.f0)-(k+1) and
A50: i<=len (t.f0);
per cases;
suppose
A51: i=lk;
then
A52: i < len(t1.f0)-k by A32,XREAL_1:29;
A53: i >= 1 by A13,A14,A51,XREAL_1:19;
consider n be Nat such that
A54: n>=Ts.b3-(k+1) and
A55: n<=Ts.b3 and
A56: IExec(T2,q,Ts).f0.i=Ts.f0.n
by A17,A18,A19,A22,A49,A50,Lm31;
take n;
thus n>=len(t.f0)-(k+1) by A54,Lm32;
thus n<=len(t.f0) by A55,Lm32;
thus thesis by A12,A15,A25,A26,A29,A31,A52,A53,A56;
end;
suppose i<>lk;
then i >lk by A49,XXREAL_0:1;
then i >= len (t1.f0)-k by A32,INT_1:7;
then consider m be Nat such that
A57: m>=len(t1.f0)-k and
A58: m<=len (t1.f0) and
A59: IExec(T1,q,t1).f0.i=t1.f0.m
by A12,A15,A16,A28,A50;
lk+1 > lk by XREAL_1:29;
then m>Ts.b3-(k+1) by A18,A28,A57,XXREAL_0:2;
then consider n be Nat such that
A60: n>=Ts.b3-(k+1) and
A61: n<=Ts.b3 and
A62: IExec(T2,q,Ts).f0.m=Ts.f0.n
by A17,A18,A19,A22,A28,A58,Lm31;
take n;
thus n>=len(t.f0)-(k+1) by A60,Lm32;
thus n<=len(t.f0) by A61,Lm32;
thus thesis by A26,A31,A59,A62,Lm32;
end;
end;
end;
hence P[k+1];
end;
A63: for k be Nat holds P[k] from NAT_1:sch 2(A4,A11);
s.b1>=1+0 by A1,A3,INT_1:7;
then reconsider m=s.b1-1 as Element of NAT by INT_1:5;
A64: m+1=s.b1;
hence s.f0, IExec(T1,p,s).f0 are_fiberwise_equipotent by A1,A63;
len (s.f0)-m=1 by A1;
hence thesis by A63,A64;
end;
end;
theorem Th26:
for p be Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA holds
s.(fsloc 0), IExec(bubble-sort (fsloc 0),p,s).(fsloc 0)
are_fiberwise_equipotent &
for i,j be Nat st i>=1 & j<=len (s.(fsloc 0)) & i<j
for x1,x2 be Integer st x1 =IExec(bubble-sort (fsloc 0),p,s).(fsloc 0).i &
x2=IExec(bubble-sort (fsloc 0),p,s).(fsloc 0).j holds x1 >= x2
proof
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
set W27=w2 ";" w3 ";" w4 ";" w5 ";" w6 ";" w7, s0=Initialized s,
s1=Exec(w2, s0), s2=IExec(w2 ";" w3,p,s), s3=IExec(w2 ";" w3 ";" w4,p,s),
s4=IExec(w2 ";" w3 ";" w4 ";" w5,p,s),
s5=IExec(w2 ";" w3 ";" w4 ";" w5 ";" w6,p,s), s6=IExec(W27,p,s);
A1: s5.f0 =Exec(w6, s4).f0 by SCMFSA6C:7
.=s4.f0 by SCMFSA_2:63
.=Exec(w5, s3).f0 by SCMFSA6C:7
.=s3.f0 by SCMFSA_2:63
.=Exec(w4, s2).f0 by SCMFSA6C:7
.=s2.f0 by SCMFSA_2:63
.=Exec(w3, s1).f0 by SCMFSA6C:9
.=s1.f0 by SCMFSA_2:63
.=s0.f0 by SCMFSA_2:63
.=s.f0 by SCMFSA_M:37;
A2: s6.f0 =Exec(w7, s5).f0 by SCMFSA6C:7
.=s.f0 by A1,SCMFSA_2:74;
A3: s6.b1=Exec(w7, s5).b1 by SCMFSA6C:6
.=len (s6.f0) by A1,A2,SCMFSA_2:74;
A4: IExec(bubble-sort f0,p,s).f0=IExec(T1,p,s6).f0 by Lm26,SCM_HALT:21;
hence s.f0, IExec(bubble-sort f0,p,s).f0 are_fiberwise_equipotent
by A2,A3,Lm33;
let i,j be Nat;
assume that
A5: i>=1 and
A6: j<=len (s.f0) and
A7: i<j;
thus thesis by A2,A3,A4,A5,A6,A7,Lm33;
end;
theorem Th27:
for i being Nat, s being State of SCM+FSA,
P being Instruction-Sequence of SCM+FSA
st Bubble-Sort-Algorithm c= P
for w being FinSequence of INT
st (Initialized ((fsloc 0) .--> w)) c= s
holds IC Comput(P,s,i) in dom Bubble-Sort-Algorithm
proof
set Ba=Bubble-Sort-Algorithm,
Ib=((intloc 0) .--> 1) +* Start-At(0,SCM+FSA);
let i be Nat, s be State of SCM+FSA,
P be Instruction-Sequence of SCM+FSA such that
A1: Bubble-Sort-Algorithm c= P;
let w be FinSequence of INT;
set x = (fsloc 0) .--> w;
assume
A2: (Initialized x) c= s;
set BSA = Bubble-Sort-Algorithm;
Initialize ((intloc 0) .--> 1) c= Initialized x by FUNCT_4:25;
then Initialize ((intloc 0) .--> 1) c= s by A2,XBOOLE_1:1;
then IC s = 0 by MEMSTR_0:47;
then IC s in dom Bubble-Sort-Algorithm by AFINSQ_1:65;
hence thesis by A1,AMISTD_1:21;
end;
theorem Th28:
for p being Instruction-Sequence of SCM+FSA
for s be State of SCM+FSA,t be FinSequence of INT st
Initialize((intloc 0).-->1) +*(fsloc 0 .--> t) c= s &
Bubble-Sort-Algorithm c= p
ex u being FinSequence of REAL
st t,u are_fiberwise_equipotent & u is non-increasing &
u is FinSequence of INT & (Result(p,s)).(fsloc 0) = u
proof
let p being Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA,t be FinSequence of INT;
set Ba=Bubble-Sort-Algorithm, pp=Initialize((intloc 0).-->1),
x=fsloc 0 .--> t,
z=IExec(bubble-sort f0,p,s).f0;
assume that
A1: pp+*x c= s and
A2: Ba c= p;
A3: p +* Ba = p by A2,FUNCT_4:98;
A4: f0 in dom x by TARSKI:def 1;
then f0 in dom (pp+*x) by FUNCT_4:12;
then
A5: s.f0=(pp+*x).f0 by A1,GRFUNC_1:2
.=x.f0 by A4,FUNCT_4:13
.=t by FUNCOP_1:72;
A6: s.f0, z are_fiberwise_equipotent by Th26;
reconsider u=z as FinSequence of REAL by FINSEQ_3:117;
take u;
thus t, u are_fiberwise_equipotent by A5,Th26;
A7: dom (s.f0) = dom u by A6,RFINSEQ:3;
now
let i,j be Nat;
assume that
A8: i in dom u and
A9: j in dom u and
A10: i<j;
A11: i>=1 by A8,FINSEQ_3:25;
A12: j<=len (s.f0) by A7,A9,FINSEQ_3:25;
reconsider y1=z.i as Integer;
reconsider y2=z.j as Integer;
thus u.i>=u.j by A10,A11,A12,Th26;
end;
hence u is non-increasing by RFINSEQ:19;
thus u is FinSequence of INT;
dom pp misses dom x by SCMFSA_M:32;
then pp c=pp+*x by FUNCT_4:32;
then s=s+*pp by A1,FUNCT_4:98,XBOOLE_1:1;
then s= Initialized s;
hence thesis by Th20,A3;
end;
theorem Th29:
for w being FinSequence of INT holds
Initialized ((fsloc 0) .--> w) is Bubble-Sort-Algorithm-autonomic
proof
let w be FinSequence of INT;
set p=Initialized((fsloc 0) .--> w), q=Bubble-Sort-Algorithm;
A1: for P,Q being Instruction-Sequence of SCM+FSA
st q c= P & q c= Q
for s1,s2 being State of SCM+FSA,i st p c= s1 & p c= s2 &
i <= 10 holds
Comput(P,s1,i).intloc 0 = Comput(Q,s2,i).intloc 0
&
Comput(P,s1,i).IC SCM+FSA = Comput(Q,s2,i).IC
SCM+FSA &
Comput(P,s1,i).fsloc 0 = Comput(Q,s2,i).fsloc 0
proof
let P,Q being Instruction-Sequence of SCM+FSA
such that
A2: q c= P & q c= Q;
let s1,s2 be State of SCM+FSA,i;
assume that
A3: p c= s1 and
A4: p c= s2 and
A5: i <= 10;
A6: q c= P by A2;
A7: q c= Q by A2;
A8: s1 is 0-started by A3,MEMSTR_0:17;
A9: s2 is 0-started by A4,MEMSTR_0:17;
A10: s1.intloc 0 =1 by A3,SCMFSA_M:33
.= s2.intloc 0 by A4,SCMFSA_M:33;
A11: s1.fsloc 0 =w by A3,SCMFSA_M:33
.=s2.fsloc 0 by A4,SCMFSA_M:33;
A12: IC s1 = 0 by A8
.= IC s2 by A9;
i = 0 or ... or i = 10 by A5;
then per cases;
suppose
A13: i = 0;
hence Comput(P,s1,i).intloc 0 = Comput(Q,s2,i).intloc 0 by A10;
thus
(Comput(P,s1,i)).IC SCM+FSA = (Comput(Q,s2,i)).IC SCM+FSA by A12,A13;
thus thesis by A11,A13;
end;
suppose
A14: i = 1;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0 by A2,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A14,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 1 by A2,A8,A14,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A7,A9,A14,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0
by A6,A8,A14,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A14,Lm21;
end;
suppose
A15: i = 2;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0
by A6,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A15,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 2 by A2,A8,A15,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A15,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0 by A2,A8,A15,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A15,Lm21;
end;
suppose
A16: i = 3;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0 by A2,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A16,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 3 by A2,A8,A16,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A16,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0
by A6,A8,A16,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A16,Lm21;
end;
suppose
A17: i = 4;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0
by A6,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A17,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 4 by A2,A8,A17,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A17,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0 by A2,A8,A17,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A17,Lm21;
end;
suppose
A18: i = 5;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0
by A6,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A18,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 5 by A2,A8,A18,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A18,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0 by A2,A8,A18,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A18,Lm21;
end;
suppose
A19: i = 6;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0 by A2,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A19,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 6 by A2,A8,A19,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A19,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0 by A2,A8,A19,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A19,Lm21;
end;
suppose
A20: i = 7;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0
by A6,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A20,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 7 by A2,A8,A20,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A20,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0 by A2,A8,A20,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A20,Lm21;
end;
suppose
A21: i = 8;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0 by A2,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A21,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 8 by A2,A8,A21,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A21,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0 by A2,A8,A21,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A21,Lm21;
end;
suppose
A22: i = 9;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0 by A2,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A22,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 9 by A2,A8,A22,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A22,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0 by A2,A8,A22,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A22,Lm21;
end;
suppose
A23: i = 10;
hence Comput(P,s1,i).intloc 0 = s1.intloc 0 by A2,A8,Lm21
.= Comput(Q,s2,i).intloc 0 by A2,A9,A10,A23,Lm21;
thus (Comput(P,s1,i)).IC SCM+FSA = 10 by A2,A8,A23,Lm21
.= (Comput(Q,s2,i)).IC SCM+FSA by A2,A9,A23,Lm21;
thus Comput(P,s1,i).fsloc 0 = s1.fsloc 0 by A2,A8,A23,Lm21
.= Comput(Q,s2,i).fsloc 0 by A2,A9,A11,A23,Lm21;
end;
end;
set UD={fsloc 0,a0,a1,a2,a3,a4,a5,a6}, Us=UsedI*Loc q \/ UsedILoc q;
A24: UsedI*Loc q ={fsloc 0} by Th22;
A25: UsedILoc q ={a0,a1,a2,a3,a4,a5,a6} by Th21;
then
A26: Us = UD by A24,ENUMSET1:22;
A27: for P,Q being Instruction-Sequence of SCM+FSA
st q c= P & q c= Q
for i being Nat,s1,s2 being State of SCM+FSA
st 11 <= i & p c= s1 & p c= s2
holds Comput(P,s1,i) | Us = Comput(Q,s2,i) | Us &
Comput(P,s1,i).IC SCM+FSA = Comput(Q,s2,i).IC SCM+FSA
proof
let P,Q be Instruction-Sequence of SCM+FSA
such that
A28: q c= P & q c= Q;
let i be Nat,s1,s2 be State of SCM+FSA such that
A29: 11 <= i and
A30: p c= s1 and
A31: p c= s2;
set Cs11= Comput(P, s1,11), Cs21= Comput(Q,s2,11);
A32: s1 is 0-started by A30,MEMSTR_0:17;
A33: s2 is 0-started by A31,MEMSTR_0:17;
A34: s1.intloc 0 =1 by A30,SCMFSA_M:33
.= s2.intloc 0 by A31,SCMFSA_M:33;
A35: s1.fsloc 0 =w by A30,SCMFSA_M:33
.=s2.fsloc 0 by A31,SCMFSA_M:33;
A36: Us c= dom(Cs11) by Th19;
A37: Us c= dom(Cs21) by Th19;
now
let x be set;
assume x in Us;
then
A38: x in UD by A24,A25,ENUMSET1:22;
per cases by A38,ENUMSET1:def 6;
suppose
A39: x = fsloc 0;
hence Cs11.x =s1.fsloc 0 by A32,A28,Lm21
.=Cs21.x by A33,A28,A35,A39,Lm21;
end;
suppose
A40: x = a0;
hence Cs11.x =s1.a0 by A32,A28,Lm21
.=Cs21.x by A33,A28,A34,A40,Lm21;
end;
suppose
A41: x = a1;
hence Cs11.x=len(s1.fsloc 0) by A32,A28,Lm21
.=Cs21.x by A33,A28,A35,A41,Lm21;
end;
suppose
A42: x = a2;
hence Cs11.x=s1.a0 by A32,A28,Lm21
.=Cs21.x by A33,A28,A34,A42,Lm21;
end;
suppose
A43: x = a3;
hence Cs11.x=s1.a0 by A32,A28,Lm21
.=Cs21.x by A33,A28,A34,A43,Lm21;
end;
suppose
A44: x = a4;
hence Cs11.x=s1.a0 by A32,A28,Lm21
.=Cs21.x by A33,A28,A34,A44,Lm21;
end;
suppose
A45: x = a5;
hence Cs11.x=s1.a0 by A32,A28,Lm21
.=Cs21.x by A33,A28,A34,A45,Lm21;
end;
suppose
A46: x = a6;
hence Cs11.x=s1.a0 by A32,A28,Lm21
.=Cs21.x by A33,A28,A34,A46,Lm21;
end;
end;
then
A47: Cs11 | Us = Cs21 | Us by A36,A37,FUNCT_1:95;
A48: Cs11.IC SCM+FSA = 11 by A32,A28,Lm21
.=Cs21.IC SCM+FSA by A33,A28,Lm21;
A49: for i holds IC Comput(P,s1,i) in dom q by A30,Th27,A28;
for i holds IC Comput(Q,s2,i) in dom q by A31,Th27,A28;
hence thesis by A29,A47,A48,A49,Th14,A28;
end;
set DD={intloc 0,IC SCM+FSA,fsloc 0};
let P,Q be Instruction-Sequence of SCM+FSA
such that
A50: q c= P & q c= Q;
let s1,s2 be State of SCM+FSA;
assume that
A51: p c= s1 and
A52: p c= s2;
let i be Nat;
reconsider i as Nat;
set Cs1i=Comput(P,s1,i), Cs2i=Comput(Q,s2,i);
A53: dom p = DD by SCMFSA_M:31;
A54: DD c= dom Cs1i by SCMFSA_M:34;
A55: DD c= dom Cs2i by SCMFSA_M:34;
A56: intloc 0 in Us by A26,ENUMSET1:def 6;
A57: fsloc 0 in Us by A26,ENUMSET1:def 6;
A58: Us c= dom(Cs1i) by Th19;
A59: Us c= dom(Cs2i) by Th19;
A60: i>10 implies 10+1 < i+1 by XREAL_1:6;
now
let x be set;
assume
A61: x in DD;
per cases by A61,ENUMSET1:def 1;
suppose
A62: x=intloc 0;
per cases;
suppose i<=10;
hence Cs1i.x=Cs2i.x by A1,A51,A52,A62,A50;
end;
suppose i>10;
then 11 <= i by A60,NAT_1:13;
then Cs1i | Us = Cs2i | Us by A27,A51,A52,A50;
hence Cs1i.x=Cs2i.x by A56,A58,A59,A62,FUNCT_1:95;
end;
end;
suppose
A63: x=IC SCM+FSA;
per cases;
suppose i<=10;
hence Cs1i.x=Cs2i.x by A1,A51,A52,A63,A50;
end;
suppose i>10;
then 11 <= i by A60,NAT_1:13;
hence Cs1i.x=Cs2i.x by A27,A51,A52,A63,A50;
end;
end;
suppose
A64: x=fsloc 0;
per cases;
suppose i<=10;
hence Cs1i.x=Cs2i.x by A1,A51,A52,A64,A50;
end;
suppose i>10;
then 11 <= i by A60,NAT_1:13;
then Cs1i | Us = Cs2i | Us by A27,A51,A52,A50;
hence Cs1i.x=Cs2i.x by A57,A58,A59,A64,FUNCT_1:95;
end;
end;
end;
hence thesis by A53,A54,A55,FUNCT_1:95;
end;
registration
cluster Bubble-Sort-Algorithm -> halt-ending;
coherence;
end;
theorem
Bubble-Sort-Algorithm, Initialize((intloc 0).-->1)
computes Sorting-Function
proof
let x be set;
assume x in dom Sorting-Function;
then consider w being FinSequence of INT such that
A1: x = fsloc 0 .--> w by SCMFSA_M:35;
reconsider d = x as FinPartState of SCM+FSA by A1;
set q = Bubble-Sort-Algorithm,
p = Initialize((intloc 0).-->1);
A2: dom d = { fsloc 0 } by A1;
take d;
thus x = d;
A3: dom d misses {IC SCM+FSA} by A2,SCMFSA_2:57,ZFMISC_1:11;
A4: dom d misses {intloc 0} by A2,SCMFSA_2:58,ZFMISC_1:11;
dom p = dom ((intloc 0).-->1) \/ {IC SCM+FSA} by MEMSTR_0:42
.= {IC SCM+FSA} \/ {intloc 0};
then
A5: dom d misses dom p by A3,A4,XBOOLE_1:70;
A6: d +* p = p +* d by A5,FUNCT_4:35;
Initialized d = d +* p
.= p +* d by A5,FUNCT_4:35
.= (p +* d)
.= p +* d;
then
A7: p +* d is q-autonomic by A1,Th29;
now
let t be State of SCM+FSA;
assume
A8: (p+*d) c= t;
let P be Instruction-Sequence of SCM+FSA
such that
A9: q c= P;
set bf=bubble-sort fsloc 0;
Initialize((intloc 0).-->1) c= (p+*d) by A6,FUNCT_4:25;
then Initialize((intloc 0).-->1) c= t by A8,XBOOLE_1:1;
hence P halts_on t by Lm26,A9,SCM_HALT:def 2;
end;
then
A10: p +* d is q-halted;
thus
A11: p +* d is Autonomy of q by A10,A7,EXTPRO_1:def 12;
consider z being FinSequence of REAL such that
A12: w,z are_fiberwise_equipotent and
A13: z is non-increasing
and z is FinSequence of INT and
A14: Sorting-Function.d = fsloc 0 .--> z by A1,SCMFSA_M:36;
consider t being State of SCM+FSA such that
A15: p +* d c= t by PBOOLE:141;
consider T being Instruction-Sequence of SCM+FSA such that
A16: q c= T by PBOOLE:145;
consider u being FinSequence of REAL such that
A17: w,u are_fiberwise_equipotent and
A18: u is non-increasing
and
u is FinSequence of INT and
A19: (Result(T,t)).(fsloc 0) = u by Th28,A1,A15,A16;
A20: u=z by A12,A13,A17,A18,CLASSES1:76,RFINSEQ:23;
fsloc 0 in the carrier of SCM+FSA;
then
A21: fsloc 0 in dom Result(T,t) by PARTFUN1:def 2;
d c= p +* d by FUNCT_4:25;
then
A22: dom d c= dom(p +* d) by RELAT_1:11;
A23: dom(fsloc 0 .--> z) = { fsloc 0 };
Result(q,p +* d) = (Result(T,t))|dom(p +* d)
by A11,A15,A16,EXTPRO_1:def 13;
hence Sorting-Function.d c= Result(q,p+* d)
by A2,A14,A19,A20,A21,A23,A22,FUNCT_4:85,RELAT_1:151;
end;