:: The { \bf for } (going up) Macro Instruction
:: by Piotr Rudnicki
::
:: Received June 4, 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, FSM_1, SCMFSA_2, SF_MASTR, AMI_1, SCMFSA7B, SUBSET_1,
SCMFSA6C, SCMFSA6B, FUNCT_1, XBOOLE_0, FUNCT_4, CARD_1, AMISTD_2,
RELAT_1, GRAPHSP, AMI_3, PARTFUN1, COMPLEX1, SCMFSA8B, SCMFSA_9, ARYTM_3,
CARD_3, SFMASTR1, ARYTM_1, AMISTD_1, XXREAL_0, SCMFSA6A, TARSKI,
SCMFSA9A, FINSEQ_1, GRAPH_2, AOFA_I00, FUNCT_2, FINSEQ_2, SFMASTR3,
NAT_1, COMPOS_1, MEMSTR_0, EXTPRO_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
CARD_3, INT_2, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCT_7,
PBOOLE, FUNCOP_1, GRAPH_2, FINSEQ_1, FINSEQ_2, MEMSTR_0, COMPOS_0,
COMPOS_1, EXTPRO_1, AMISTD_1, SCMFSA_2, SCMFSA6A, SCMFSA6B, SF_MASTR,
SCMFSA6C, SCMFSA7B, SCMFSA8B, SCMFSA_9, SFMASTR1, SCMFSA9A, XXREAL_0,
NAT_1, SCMFSA_M, SCMFSA_X, FINSEQ_6;
constructors SETWISEO, REAL_1, INT_2, MESFUNC1, SCMFSA6A, SCMFSA6B, SCMFSA6C,
SCMFSA8A, SCMFSA8B, SCMFSA_9, SFMASTR1, SCMFSA9A, RELSET_1, FUNCT_4,
PBOOLE, GRAPH_2, SCMFSA7B, MEMSTR_0, AMISTD_1, FINSEQ_2, SCMFSA_M,
SF_MASTR, FUNCT_7, SCMFSA_X, PRE_POLY, SCMFSA10, COMPOS_2, AMISTD_2,
AMI_3, SCMFSA8C, FINSEQ_6;
registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1,
XREAL_0, NAT_1, INT_1, CARD_3, SCMFSA_2, SF_MASTR, SCMFSA6B, SCMFSA6C,
SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA_9, SFMASTR1, VALUED_0, AFINSQ_1,
COMPOS_1, EXTPRO_1, FUNCT_4, MEMSTR_0, AMI_3, SCMFSA_M, PRE_POLY,
AMISTD_1, SCMFSA6A, SCMFSA8C, SCMFSA10, COMPOS_2, SCMFSA_X;
requirements REAL, NUMERALS, SUBSET, ARITHM;
definitions TARSKI, SCMFSA7B, SCMFSA9A;
equalities SCMFSA6A, COMPOS_1, MEMSTR_0;
expansions SCMFSA7B, SCMFSA9A, FINSEQ_6;
theorems TARSKI, ZFMISC_1, ENUMSET1, ABSVALUE, NAT_1, INT_1, RELAT_1, FUNCT_7,
FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, GRAPH_2, SCMFSA_2, SCMFSA6A,
SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8B, SCMFSA8C, SCMFSA_9,
SFMASTR1, SCMFSA9A, SFMASTR2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0,
PARTFUN1, AFINSQ_1, CARD_3, FINSEQ_6, SCMFSA_M, ORDINAL1;
schemes FUNCT_2, NAT_1;
begin :: SCM+FSA preliminaries
reserve s for State of SCM+FSA,
a, c for read-write Int-Location,
aa, bb, cc,
dd, x for Int-Location,
f for FinSeq-Location,
I, J for MacroInstruction of SCM+FSA,
Ig for good MacroInstruction of SCM+FSA,
i, k for Nat,
p for Instruction-Sequence of SCM+FSA;
::$CT
theorem Th1:
s.intloc 0 = 1 implies DataPart IExec(Stop SCM+FSA,p,s) = DataPart s
proof
assume
A1: s.intloc 0 = 1;
thus DataPart IExec(Stop SCM+FSA,p,s)
= DataPart(Initialized s) by SCMFSA8C:14
.= DataPart s by A1,SCMFSA_M:19;
end;
theorem Th2:
Stop SCM+FSA does not refer aa
proof
A1: rng Stop SCM+FSA = {halt SCM+FSA} by AFINSQ_1:33;
let i be Instruction of SCM+FSA;
assume i in rng Stop SCM+FSA;
then i = halt SCM+FSA by A1,TARSKI:def 1;
hence thesis;
end;
theorem Th3:
aa <> bb implies cc := bb does not refer aa
proof
assume
A1: aa <> bb;
now
let e be Int-Location;
let l be Nat;
let f be FinSeq-Location;
thus e := aa <> cc := bb by A1,SF_MASTR:1;
A2: InsCode (cc := bb) = 1 by SCMFSA_2:18;
hence AddTo(e,aa) <> cc := bb by SCMFSA_2:19;
thus SubFrom(e,aa) <> cc := bb by A2,SCMFSA_2:20;
thus MultBy(e,aa) <> cc := bb by A2,SCMFSA_2:21;
thus Divide(aa,e) <> cc := bb & Divide(e,aa) <> cc := bb by A2,SCMFSA_2:22;
thus aa =0_goto l <> cc := bb;
thus aa >0_goto l <> cc := bb;
thus e :=(f,aa) <> cc := bb by A2,SCMFSA_2:26;
thus (f,e):= aa <> cc := bb & (f,aa):= e <> cc := bb by A2,SCMFSA_2:27;
thus f :=<0,...,0> aa <> cc := bb by A2,SCMFSA_2:29;
end;
hence thesis;
end;
theorem Th4: :: change SCMFSA_2:98
Exec(a := (f, bb), s).a = (s.f)/.|.s.bb.|
proof
ex k being Nat st k = |.s.bb.| & Exec(a:=(f,bb), s).a = (s.f
)/.k by SCMFSA_2:72;
hence thesis;
end;
theorem Th5: :: see SCMFSA_2:99
Exec((f, aa) := bb, s).f = s.f+*(|.s.aa.|, s.bb)
proof
ex k being Nat st k=|.s.aa.| & Exec((f,aa):=bb, s).f = s.f+*
(k,s.bb) by SCMFSA_2:73;
hence thesis;
end;
registration
let a be read-write Int-Location, b be Int-Location,
I, J be good MacroInstruction of
SCM+FSA;
cluster if>0(a, b, I, J) -> good;
coherence
proof
if>0(a, b, I, J) = SubFrom(a,b) ";" if>0(a,I,J) by SCMFSA8B:def 5;
hence thesis;
end;
end;
theorem Th6:
for I,J being MacroInstruction of SCM+FSA holds
UsedILoc if>0(aa, bb, I, J) = {aa, bb} \/ (UsedILoc I) \/ UsedILoc J
proof let I,J be MacroInstruction of SCM+FSA;
set a = aa;
thus UsedILoc if>0(a, bb, I, J) = UsedILoc (SubFrom(a,bb) ";" if>0(a,I,J
)) by SCMFSA8B:def 5
.= (UsedIntLoc SubFrom(a,bb)) \/ UsedILoc if>0(a,I,J) by SF_MASTR:29
.= {a,bb} \/ UsedILoc if>0(a,I,J) by SF_MASTR:14
.= {a,bb} \/ ({a} \/ UsedILoc I \/ UsedILoc J) by SCMFSA9A:9
.= {a,bb} \/ ({a} \/ (UsedILoc I \/ UsedILoc J)) by XBOOLE_1:4
.= {a,bb} \/ {a} \/ ((UsedILoc I \/ UsedILoc J)) by XBOOLE_1:4
.= {a, bb} \/ (UsedILoc I \/ UsedILoc J) by ZFMISC_1:9
.= {a, bb} \/ UsedILoc I \/ UsedILoc J by XBOOLE_1:4;
end;
::$CT
theorem Th7:
for I,J being really-closed MacroInstruction of SCM+FSA holds
cc <> aa & I does not destroy cc & J does not destroy cc implies
if>0(aa, bb, I, J) does not destroy cc
proof let I,J be really-closed MacroInstruction of SCM+FSA;
assume that
A1: cc <> aa and
A2: I does not destroy cc & J does not destroy cc;
if>0(aa, bb, I, J) = SubFrom(aa,bb) ";" if>0(aa,I,J) &
if>0(aa,I,J) does not destroy cc by A2,SCMFSA8B:def 5,SCMFSA8C:88;
hence thesis by A1,SCMFSA7B:8,SCMFSA8C:53;
end;
begin :: The for-up macro instruction
definition let p;
let a, b, c be Int-Location, I be MacroInstruction of SCM+FSA,
s be State of SCM+FSA;
func StepForUp(a, b, c, I, p,s) ->
sequence of product the_Values_of
SCM+FSA equals
StepWhile>0(1-stRWNotIn ({a, b, c} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, b, c} \/ UsedILoc I), intloc 0), p,
s+*(1-stRWNotIn ({a, b, c} \/ UsedILoc I), s.c-s.b+1)+*(a, s.b));
coherence;
end;
theorem Th8:
s.intloc 0 = 1 implies StepForUp(a,bb,cc,I,p,s).0.intloc 0 = 1
proof
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set S = s+*(aux, s.cc-s.bb+1)+*(a, s.bb);
A1: S.intloc 0 = (s+*(aux, s.cc-s.bb+1)).intloc 0 by FUNCT_7:32
.= s.intloc 0 by FUNCT_7:32;
assume s.intloc 0 = 1;
hence thesis by A1,SCMFSA_9:def 5;
end;
theorem Th9:
StepForUp(a,bb,cc,I,p,s).0.a = s.bb
proof
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set S = s+*(aux, s.cc-s.bb+1)+*(a, s.bb);
StepWhile>0(aux, I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0),p,S)
.0 = S & a in dom (s+*(aux, s.cc-s.bb+1)) by SCMFSA_2:42,SCMFSA_9:def 5;
hence thesis by FUNCT_7:31;
end;
theorem Th10:
a <> bb implies StepForUp(a,bb,cc,I,p,s).0.bb = s.bb
proof
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set S = s+*(aux, s.cc-s.bb+1)+*(a, s.bb);
bb in {a, bb, cc} by ENUMSET1:def 1;
then bb in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
then
A1: bb <> aux by SCMFSA_M:25;
assume a <> bb;
then S.bb = (s+*(aux, s.cc-s.bb+1)).bb by FUNCT_7:32
.= s.bb by A1,FUNCT_7:32;
hence thesis by SCMFSA_9:def 5;
end;
theorem Th11:
a <> cc implies StepForUp(a,bb,cc,I,p,s).0.cc = s.cc
proof
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set S = s+*(aux, s.cc-s.bb+1)+*(a, s.bb);
cc in {a, bb, cc} by ENUMSET1:def 1;
then cc in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
then
A1: cc <> aux by SCMFSA_M:25;
assume a <> cc;
then S.cc = (s+*(aux, s.cc-s.bb+1)).cc by FUNCT_7:32
.= s.cc by A1,FUNCT_7:32;
hence thesis by SCMFSA_9:def 5;
end;
theorem Th12:
a <> dd & dd in UsedILoc I implies StepForUp(a,bb,cc,I,p,s).
0.dd = s.dd
proof
assume that
A1: a <> dd and
A2: dd in UsedILoc I;
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
dd in {a, bb, cc} \/ UsedILoc I by A2,XBOOLE_0:def 3;
then
A3: dd <> aux by SCMFSA_M:25;
set S = s+*(aux, s.cc-s.bb+1)+*(a, s.bb);
S.dd = (s+*(aux, s.cc-s.bb+1)).dd by A1,FUNCT_7:32
.= s.dd by A3,FUNCT_7:32;
hence thesis by SCMFSA_9:def 5;
end;
theorem Th13:
StepForUp(a,bb,cc,I,p,s).0.f = s.f
proof
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set S = s+*(aux, s.cc-s.bb+1)+*(a, s.bb);
S.f = (s+*(aux, s.cc-s.bb+1)).f by FUNCT_7:32,SCMFSA_2:58
.= s.f by FUNCT_7:32,SCMFSA_2:58;
hence thesis by SCMFSA_9:def 5;
end;
theorem Th14:
s.intloc 0 = 1 implies for aux being read-write Int-Location st
aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I)
holds DataPart IExec( aux := cc
";" SubFrom(aux, bb) ";" AddTo(aux, intloc 0) ";" (a := bb),p,s)
= DataPart(s+*(aux, s.cc-s.bb+1)+*(a, s.bb))
proof
assume
A1: s.intloc 0 = 1;
cc = intloc 0 or cc is read-write by SCMFSA_M:def 2;
then
A2: (Initialized s).cc = s.cc by A1,SCMFSA_M:9,37;
set i3 = a := bb;
let aux be read-write Int-Location such that
A3: aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
bb in {a, bb, cc} by ENUMSET1:def 1;
then bb in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
then
A4: bb <> aux by A3,SCMFSA_M:25;
set s2 = s+*(aux, s.cc-s.bb+1)+*(a, s.bb);
A5: aux in dom s by SCMFSA_2:42;
a in {a, bb, cc} by ENUMSET1:def 1;
then a in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
then
A6: a <> aux by A3,SCMFSA_M:25;
then
A7: s2.aux = (s+*(aux, s.cc-s.bb+1)).aux by FUNCT_7:32
.= s.cc-s.bb+1 by A5,FUNCT_7:31;
set i2 = AddTo(aux, intloc 0);
set i1 = SubFrom(aux, bb);
set i0 = aux := cc;
set s1 = IExec(i0 ";" i1 ";" i2 ";" i3,p,s);
A8: IExec(i0 ";" i1,p,s).intloc 0
= Exec(i1, Exec(i0, Initialized s)).intloc 0
by SCMFSA6C:8
.= Exec(i0, Initialized s).intloc 0 by SCMFSA_2:65
.= (Initialized s).intloc 0 by SCMFSA_2:63
.= 1 by SCMFSA_M:9;
A9: a in dom (s+*(aux, s.cc-s.bb+1)) by SCMFSA_2:42;
bb = intloc 0 or bb is read-write by SCMFSA_M:def 2;
then
A10: (Initialized s).bb = s.bb by A1,SCMFSA_M:9,37;
A11: s1.a = Exec(i3, IExec(i0 ";" i1 ";" i2,p,s)).a by SCMFSA6C:6
.= IExec(i0 ";" i1 ";" i2,p,s).bb by SCMFSA_2:63
.= Exec(i2, IExec(i0 ";" i1,p,s)).bb by SCMFSA6C:6
.= IExec(i0 ";" i1,p,s).bb by A4,SCMFSA_2:64
.= Exec(i1, Exec(i0, Initialized s)).bb by SCMFSA6C:8
.= Exec(i0, Initialized s).bb by A4,SCMFSA_2:65
.= s.bb by A4,A10,SCMFSA_2:63;
A12: s1.aux = Exec(i3, IExec(i0 ";" i1 ";" i2,p,s)).aux by SCMFSA6C:6
.= IExec(i0 ";" i1 ";" i2,p,s).aux by A6,SCMFSA_2:63
.= Exec(i2, IExec(i0 ";" i1,p,s)).aux by SCMFSA6C:6
.= IExec(i0 ";" i1,p,s).aux + 1 by A8,SCMFSA_2:64
.= Exec(i1, Exec(i0, Initialized s)).aux +1 by SCMFSA6C:8
.= Exec(i0, Initialized s).aux - Exec(i0, Initialized s).bb +1
by SCMFSA_2:65
.= (Initialized s).cc - Exec(i0, Initialized s).bb +1 by SCMFSA_2:63
.= s.cc-s.bb+1 by A4,A2,A10,SCMFSA_2:63;
now
hereby
let x be Int-Location;
per cases;
suppose
x = a;
hence s1.x = s2.x by A11,A9,FUNCT_7:31;
end;
suppose
x = aux;
hence s1.x = s2.x by A12,A7;
end;
suppose
A13: x <> aux & x <> a;
then
A14: s2.x = (s+*(aux, s.cc-s.bb+1)).x by FUNCT_7:32
.= s.x by A13,FUNCT_7:32;
A15: x = intloc 0 or x is read-write by SCMFSA_M:def 2;
s1.x = Exec(i3, IExec(i0 ";" i1 ";" i2,p,s)).x by SCMFSA6C:6
.= IExec(i0 ";" i1 ";" i2,p,s).x by A13,SCMFSA_2:63
.= Exec(i2, IExec(i0 ";" i1,p,s)).x by SCMFSA6C:6
.= IExec(i0 ";" i1,p,s).x by A13,SCMFSA_2:64
.= Exec(i1, Exec(i0, Initialized s)).x by SCMFSA6C:8
.= Exec(i0, Initialized s).x by A13,SCMFSA_2:65
.= (Initialized s).x by A13,SCMFSA_2:63
.= s.x by A1,A15,SCMFSA_M:9,37;
hence s1.x = s2.x by A14;
end;
end;
let x be FinSeq-Location;
thus s1.x = Exec(i3, IExec(i0 ";" i1 ";" i2,p,s)).x by SCMFSA6C:7
.= IExec(i0 ";" i1 ";" i2,p,s).x by SCMFSA_2:63
.= Exec(i2, IExec(i0 ";" i1,p,s)).x by SCMFSA6C:7
.= IExec(i0 ";" i1,p,s).x by SCMFSA_2:64
.= Exec(i1, Exec(i0, Initialized s)).x by SCMFSA6C:9
.= Exec(i0, Initialized s).x by SCMFSA_2:65
.= (Initialized s).x by SCMFSA_2:63
.= s.x by SCMFSA_M:37
.= (s+*(aux, s.cc-s.bb+1)).x by FUNCT_7:32,SCMFSA_2:58
.= s2.x by FUNCT_7:32,SCMFSA_2:58;
end;
hence thesis by SCMFSA_M:2;
end;
definition let p;
let a, b, c be Int-Location, I be MacroInstruction of SCM+FSA,
s be State of SCM+FSA;
pred ProperForUpBody a, b, c, I, s, p means
for i being Nat
st i < s.c-s.b+1 holds
I is_halting_on StepForUp(a, b, c, I,p,s).i,
p +* while>0(1-stRWNotIn ({a, b, c} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, b, c} \/ UsedILoc I), intloc 0));
end;
theorem Th15:
for I being parahalting MacroInstruction of SCM+FSA
holds ProperForUpBody aa, bb, cc, I, s, p by SCMFSA7B:19;
theorem Th16:
for Ig being good really-closed MacroInstruction of SCM+FSA holds
StepForUp(a,bb,cc,Ig,p,s).k.intloc 0 = 1 &
Ig is_halting_on StepForUp(a,bb,cc,Ig,p,s).k,
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc Ig),
Ig ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc Ig), intloc 0))
implies StepForUp(a,bb,cc,Ig,p,s).(k+1).intloc 0 = 1
proof let Ig be good really-closed MacroInstruction of SCM+FSA;
set I = Ig;
assume that
A1: StepForUp(a,bb,cc,I,p,s).k.intloc 0 = 1 and
A2:
I is_halting_on
StepForUp(a,bb,cc,I,p,s).k,
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I), intloc 0));
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
::: as MacroInstruction of SCM+FSA;
set SW2 = StepWhile>0(aux,IB,p,s+*(aux,s.cc-s.bb+1)+*(a, s.bb));
A3: IB = I ";"(AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0)) by SCMFSA6A:28;
per cases;
suppose
SW2.k.aux <= 0;
then DataPart SW2.(k+1) = DataPart SW2.k by SCMFSA9A:31;
hence thesis by A1,SCMFSA_M:2;
end;
suppose
A4: SW2.k.aux > 0;
A5: I is_halting_on Initialized SW2.k,p+*while>0(aux,IB) by A1,A2,SCMFSA8B:42;
AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0)
is_halting_on IExec(I,p+*while>0(aux,IB),SW2.k),p+*while>0(aux,IB)
by SCMFSA7B:19;
then
A6: DataPart SW2.(k+1) = DataPart IExec(IB,p+*while>0(aux,IB),SW2.k)
by A1,A3,A4,A5,SCMFSA9A:32,SFMASTR1:3;
IExec(IB,p+*while>0(aux,IB),SW2.k).intloc 0
= IExec(AddTo(a, intloc 0) ";" SubFrom(aux,intloc 0),p+*while>0(aux,IB),
IExec(I,p+*while>0(aux,IB),
SW2.k)).intloc 0 by A3,A5,SFMASTR1:7
.= Exec(SubFrom(aux, intloc 0), Exec(AddTo(a, intloc 0), Initialized
IExec(I,p+*while>0(aux,IB),SW2.k))).intloc 0 by SCMFSA6C:8
.= Exec(AddTo(a, intloc 0),
Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).intloc 0 by SCMFSA_2:65
.= (Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).intloc 0
by SCMFSA_2:64
.= 1 by SCMFSA_M:9;
hence thesis by A6,SCMFSA_M:2;
end;
end;
theorem Th17:
for Ig being good really-closed MacroInstruction of SCM+FSA holds
s.intloc 0 = 1 & ProperForUpBody a,bb,cc,Ig,s,p implies for k
st k <= s.cc-s.bb+1 holds StepForUp(a,bb,cc,Ig,p,s).k.intloc 0 = 1 & (Ig
does not destroy a implies StepForUp(a,bb,cc,Ig,p,s).k.a = k+s.bb &
StepForUp(a, bb, cc, Ig,p, s).k.a <= s.cc+1) &
StepForUp(a,bb,cc,Ig,p,s).k.(1-stRWNotIn
({a, bb, cc} \/ UsedILoc Ig)) + k = s.cc-s.bb+1
proof let Ig be good really-closed MacroInstruction of SCM+FSA;
set I = Ig;
assume that
A1: s.intloc 0 = 1 and
A2: ProperForUpBody a,bb,cc,I,s,p;
set scb1 = s.cc-s.bb+1;
set aux = (1-stRWNotIn ({a, bb, cc} \/ UsedILoc I));
set SF = StepForUp(a,bb,cc,I,p,s);
set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
set s2 = s+*(aux, s.cc-s.bb+1)+*(a, s.bb),
p2 = p;
set SW2 = StepWhile>0(aux,IB,p2,s2);
A3: IB = I ";"(AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0)) by SCMFSA6A:28;
defpred P[Nat] means $1 <= scb1 implies SF.$1.intloc 0 = 1 & (I
does not destroy a implies SF.$1.a = $1+s.bb & SF.$1.a <= s.cc+1) & SF.$1.aux +
$1 = scb1;
a in {a, bb, cc} by ENUMSET1:def 1;
then a in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
then
A4: aux <> a by SCMFSA_M:25;
A5: for k st P[k] holds P[k+1]
proof
let k such that
A6: P[k];
thus P[k+1]
proof
A7: not aux in UsedILoc I
proof
assume not thesis;
then aux in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
hence contradiction by SCMFSA_M:25;
end;
set k1 = k+1;
assume
A8: k+1 <= scb1;
A9: k < k+1 by XREAL_1:29;
then
A10: SW2.k.aux > 0 by A6,A8,XREAL_1:8,XXREAL_0:2;
A11: k < scb1 by A8,A9,XXREAL_0:2;
A12: I is_halting_on SF.k,
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I), intloc 0))
by A2,A11;
then
A13: I is_halting_on Initialized SW2.k, p+*while>0(aux,IB)
by A6,A8,A9,SCMFSA8B:42,XXREAL_0:2;
thus SF.k1.intloc 0 = 1 by A6,A8,A9,A12,Th16,XXREAL_0:2;
AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0) is_halting_on
IExec(I,p+*while>0(aux,IB),SW2.k), p+*while>0(aux,IB) by SCMFSA7B:19;
then IB is_halting_on Initialized SW2.k, p+*while>0(aux,IB)
by A3,A13,SFMASTR1:3;
then
A14: DataPart SW2.(k+1) = DataPart IExec(IB,p+*while>0(aux,IB),SW2.k)
by A6,A8,A9,A10,SCMFSA9A:32,XXREAL_0:2;
hereby
assume
A15: I does not destroy a;
A16: IExec(IB,p+*while>0(aux,IB),SW2.k).a
= IExec(AddTo(a, intloc 0) ";" SubFrom(aux,intloc 0),
p+*while>0(aux,IB),IExec(I,p+*while>0(aux,IB),SW2.k)).a
by A3,A13,SFMASTR1:7
.= Exec(SubFrom(aux, intloc 0), Exec(AddTo(a, intloc 0),
Initialized IExec(I,p+*while>0(aux,IB),SW2.k))).a by SCMFSA6C:8
.= Exec(AddTo(a, intloc 0),
Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).a by A4,SCMFSA_2:65
.= (Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).a +
(Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).
intloc 0 by SCMFSA_2:64
.= (Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).a +1
by SCMFSA_M:9
.= IExec(I,p+*while>0(aux,IB),SW2.k).a +1 by SCMFSA_M:37
.= (Initialized SW2.k).a +1 by A13,A15,SCMFSA8C:95
.= SW2.k.a +1 by SCMFSA_M:37;
hence SF.k1.a = k1+s.bb by A6,A8,A9,A14,A15,SCMFSA_M:2,XXREAL_0:2;
k1+s.bb <= s.cc+1-s.bb+s.bb by A8,XREAL_1:6;
hence SF.k1.a <= s.cc+1 by A6,A8,A9,A14,A15,A16,SCMFSA_M:2,XXREAL_0:2;
end;
IExec(IB,p+*while>0(aux,IB),SW2.k).aux
= IExec(AddTo(a, intloc 0) ";" SubFrom(aux,
intloc 0), p+*while>0(aux,IB),IExec(I,p+*while>0(aux,IB),SW2.k)).aux
by A3,A13,SFMASTR1:7
.= Exec(SubFrom(aux, intloc 0), Exec(AddTo(a, intloc 0), Initialized
IExec(I,p+*while>0(aux,IB),SW2.k))).aux by SCMFSA6C:8
.= Exec(AddTo(a, intloc 0),
Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).aux - Exec(
AddTo(a, intloc 0),
Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).intloc 0 by SCMFSA_2:65
.= Exec(AddTo(a, intloc 0),
Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).aux - (
Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).intloc 0 by SCMFSA_2:64
.= Exec(AddTo(a, intloc 0),
Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).aux - 1 by SCMFSA_M:9
.= (Initialized IExec(I,p+*while>0(aux,IB),SW2.k)).aux -1
by A4,SCMFSA_2:64
.= IExec(I,p+*while>0(aux,IB),SW2.k).aux -1 by SCMFSA_M:37
.= (Initialized SW2.k).aux -1 by A13,A7,SCMFSA8C:95,SFMASTR1:1
.= SW2.k.aux -1 by SCMFSA_M:37;
hence SF.k1.aux + k1 = SW2.k.aux-1+k1 by A14,SCMFSA_M:2
.= scb1 by A6,A8,A9,XXREAL_0:2;
end;
end;
A17: a in dom (s+*(aux, s.cc-s.bb+1)) by SCMFSA_2:42;
A18: aux in dom s by SCMFSA_2:42;
A19: P[0]
proof
assume
A20: 0 <= scb1;
A21: SW2.0 = s2 by SCMFSA_9:def 5;
hence SF.0.intloc 0 = (s+*(aux, s.cc-s.bb+1)).intloc 0 by FUNCT_7:32
.= 1 by A1,FUNCT_7:32;
hereby
assume I does not destroy a;
thus SF.0.a = 0+s.bb by A17,A21,FUNCT_7:31;
0+s.bb <= s.cc+1-s.bb+s.bb by A20,XREAL_1:6;
hence SF.0.a <= s.cc+1 by A17,A21,FUNCT_7:31;
end;
thus SF.0.aux + 0 = (s+*(aux, s.cc-s.bb+1)).aux by A4,A21,FUNCT_7:32
.= scb1 by A18,FUNCT_7:31;
end;
thus for k holds P[k] from NAT_1:sch 2(A19, A5);
end;
theorem Th18:
for Ig being good really-closed MacroInstruction of SCM+FSA holds
s.intloc 0 = 1 & ProperForUpBody a,bb,cc,Ig,s,p implies for k
holds StepForUp(a,bb,cc,Ig,p,s).k.(1-stRWNotIn({a, bb, cc} \/ UsedILoc Ig))
> 0 iff k < s.cc-s.bb+1
proof let Ig be good really-closed MacroInstruction of SCM+FSA;
set I = Ig;
set SF = StepForUp(a,bb,cc,I,p,s);
set aux = (1-stRWNotIn ({a, bb, cc} \/ UsedILoc I));
set s2 = s+*(aux, s.cc-s.bb+1)+*(a, s.bb),
p2 = p;
set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
set SW2 = StepWhile>0(aux,IB,p2,s2);
set scb1 = s.cc-s.bb+1;
defpred P[Nat] means SF.$1.aux > 0 implies $1 < scb1;
assume
A1: s.intloc 0 = 1 & ProperForUpBody a,bb,cc,I,s,p;
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k] and
A4: SF.(k+1).aux > 0;
A5: SF.k.aux > 0
proof
assume
A6: SF.k.aux <= 0;
then DataPart SF.(k+1) = DataPart SF.k by SCMFSA9A:31;
hence contradiction by A4,A6,SCMFSA_M:2;
end;
then reconsider scb1 as Element of NAT by A3,INT_1:3;
assume k+1 >= s.cc-s.bb+1;
then
A7: SF.(k+1).aux+(k+1) > 0+scb1 by A4,XREAL_1:8;
k+1 <= scb1 by A3,A5,NAT_1:13;
hence contradiction by A1,A7,Th17;
end;
let k;
a in {a, bb, cc} by ENUMSET1:def 1;
then a in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
then
A8: aux <> a by SCMFSA_M:25;
A9: aux in dom s by SCMFSA_2:42;
A10: P[0]
proof
SW2.0 = s2 by SCMFSA_9:def 5;
then
A11: SF.0.aux = (s+*(aux, s.cc-s.bb+1)).aux by A8,FUNCT_7:32
.= scb1 by A9,FUNCT_7:31;
assume SF.0.aux > 0;
hence thesis by A11;
end;
for k holds P[k] from NAT_1:sch 2(A10, A2);
hence P[k];
assume
A12: k < scb1;
then
A13: k-k < scb1-k by XREAL_1:9;
SF.k.aux + k = scb1 by A1,A12,Th17;
hence thesis by A13;
end;
theorem Th19:
for Ig being good really-closed MacroInstruction of SCM+FSA holds
s.intloc 0 = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < s.cc-s.
bb+1 implies
StepForUp(a,bb,cc,Ig,p,s).(k+1) |
({a, bb, cc} \/ UsedILoc Ig \/ FinSeq-Locations)
= IExec(Ig ";" AddTo(a, intloc 0),
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc Ig),
Ig ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc Ig), intloc 0)),
StepForUp(a, bb, cc, Ig, p, s).k) |
({a, bb, cc} \/ UsedILoc Ig \/ FinSeq-Locations)
proof let Ig be good really-closed MacroInstruction of SCM+FSA;
assume that
A1: s.intloc 0 = 1 and
A2: ProperForUpBody a,bb,cc,Ig,s,p and
A3: k < s.cc-s.bb+1;
set FL = FinSeq-Locations;
set I = Ig;
set aux = (1-stRWNotIn ({a, bb, cc} \/ UsedILoc I));
set SF = StepForUp(a,bb,cc,I,p,s);
set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
set s2 = s+*(aux, s.cc-s.bb+1)+*(a, s.bb),
p2 = p;
set SW2 = StepWhile>0(aux,IB,p2,s2);
A4: SW2.k.intloc 0 = 1 by A1,A2,A3,Th17;
set scb1 = s.cc-s.bb+1;
A5: SF.k.aux+k = scb1 by A1,A2,A3,Th17;
A6: SW2.k.aux > 0
proof
assume SW2.k.aux <= 0;
then SW2.k.aux + k < 0+scb1 by A3,XREAL_1:8;
hence contradiction by A5;
end;
set S2 = IExec(IB,p+*while>0(aux,IB),SW2.k);
set IB1 = I ";" AddTo(a, intloc 0);
set Iloc = {a, bb, cc} \/ UsedILoc I;
set S1 = IExec(IB1,p+*while>0(aux,IB), SW2.k);
I is_halting_on SF.k,
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I), intloc 0))
by A2,A3;
then
A7: I is_halting_on Initialized SW2.k,p+*while>0(aux,IB) by A4,SCMFSA8B:42;
Macro AddTo(a, intloc 0) is_halting_on
IExec(I,p+*while>0(aux,IB),SW2.k),p+*while>0(aux,IB)
by SCMFSA7B:19;
then
A8: IB1 is_halting_on Initialized SW2.k,p+*while>0(aux,IB) by A7,SFMASTR1:3;
now
hereby
let x be Int-Location;
assume x in Iloc;
then
A9: x <> aux by SCMFSA_M:25;
S2.x = Exec(SubFrom(aux, intloc 0), S1).x by A8,SFMASTR1:11
.= S1.x by A9,SCMFSA_2:65;
hence S1.x = S2.x;
end;
let x be FinSeq-Location;
S2.x = Exec(SubFrom(aux, intloc 0), S1).x by A8,SFMASTR1:12
.= S1.x by SCMFSA_2:65;
hence S1.x = S2.x;
end;
then
A10: S1 | (Iloc \/ FL) = IExec(IB,p+*while>0(aux,IB),SW2.k) | (Iloc \/ FL)
by SCMFSA_M:28;
A11: IB = I ";"(AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0))
by SCMFSA6A:28;
AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0)
is_halting_on IExec(I,p+*while>0(aux,IB),SW2.k),p+*while>0(aux,IB)
by SCMFSA7B:19;
then DataPart SW2.(k+1) = DataPart IExec(IB,p+*while>0(aux,IB),SW2.k)
by A4,A6,A7,A11,SCMFSA9A:32,SFMASTR1:3;
hence thesis by A10,RELAT_1:153,SCMFSA_2:100,XBOOLE_1:9;
end;
definition
let a, b, c be Int-Location, I be MacroInstruction of SCM+FSA;
func for-up(a, b, c, I) -> MacroInstruction of SCM+FSA equals
(1-stRWNotIn ({a, b, c}
\/ UsedILoc I)) := c ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedILoc I), b)
";" AddTo(1-stRWNotIn ({a, b, c} \/ UsedILoc I), intloc 0) ";" (a := b) ";"
while>0( 1-stRWNotIn ({a, b, c} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, b, c} \/ UsedILoc I), intloc 0));
coherence;
end;
registration
let a, b, c be Int-Location, I be really-closed MacroInstruction of SCM+FSA;
cluster for-up(a, b, c, I) -> really-closed;
coherence;
end;
reserve I for MacroInstruction of SCM+FSA;
theorem Th20:
{aa, bb, cc} \/ UsedILoc I c= UsedILoc for-up(aa, bb, cc, I)
proof
set aux = 1-stRWNotIn ({aa, bb, cc} \/ UsedILoc I);
set i0 = aux := cc;
set i1 = SubFrom(aux, bb);
set i2 = AddTo(aux, intloc 0);
set i3 = aa := bb;
set I4 = while>0( aux, I ";" AddTo(aa, intloc 0) ";" SubFrom(aux, intloc 0));
A1: UsedILoc (i0 ";" i1 ";" i2 ";" i3) = UsedILoc (i0 ";" i1 ";" i2) \/
UsedIntLoc i3 by SF_MASTR:30
.= UsedILoc (i0 ";" i1) \/ (UsedIntLoc i2) \/ UsedIntLoc i3 by SF_MASTR:30
.= (UsedIntLoc i0) \/ (UsedIntLoc i1) \/ (UsedIntLoc i2) \/ UsedIntLoc
i3 by SF_MASTR:31
.= {aux, cc} \/ (UsedIntLoc i1) \/ (UsedIntLoc i2) \/ UsedIntLoc i3 by
SF_MASTR:14
.= {aux, cc} \/ {aux, bb} \/ (UsedIntLoc i2) \/ UsedIntLoc i3 by
SF_MASTR:14
.= {aux, cc} \/ {aux, bb} \/ {aux, intloc 0} \/ UsedIntLoc i3 by
SF_MASTR:14
.= {aux, cc} \/ {aux, bb} \/ {aux, intloc 0} \/ {aa, bb} by SF_MASTR:14;
let x be object;
A2: UsedILoc I4 = {aux} \/ UsedILoc (I ";" AddTo(aa, intloc 0) ";"
SubFrom(aux, intloc 0)) by SCMFSA9A:24
.= {aux} \/ (UsedILoc (I ";" AddTo(aa, intloc 0)) \/ UsedIntLoc
SubFrom(aux, intloc 0)) by SF_MASTR:30
.= {aux} \/ (((UsedILoc I) \/ UsedIntLoc AddTo(aa, intloc 0)) \/
UsedIntLoc SubFrom(aux, intloc 0)) by SF_MASTR:30
.= {aux} \/ ((UsedILoc I) \/ ((UsedIntLoc AddTo(aa, intloc 0)) \/
UsedIntLoc SubFrom(aux, intloc 0))) by XBOOLE_1:4
.= (UsedILoc I) \/ ({aux} \/ (UsedIntLoc AddTo(aa, intloc 0) \/
UsedIntLoc SubFrom(aux, intloc 0))) by XBOOLE_1:4;
assume x in {aa, bb, cc} \/ UsedILoc I;
then
A3: x in {aa, bb, cc} or x in UsedILoc I by XBOOLE_0:def 3;
A4: UsedILoc for-up(aa, bb, cc, I) = (UsedILoc (i0 ";" i1 ";" i2 ";" i3)
) \/ UsedILoc I4 by SF_MASTR:27;
per cases by A3,ENUMSET1:def 1;
suppose
x = aa;
then x in {aa, bb} by TARSKI:def 2;
then x in UsedILoc (i0 ";" i1 ";" i2 ";" i3) by A1,XBOOLE_0:def 3;
hence thesis by A4,XBOOLE_0:def 3;
end;
suppose
x = bb;
then x in {aa, bb} by TARSKI:def 2;
then x in UsedILoc (i0 ";" i1 ";" i2 ";" i3) by A1,XBOOLE_0:def 3;
hence thesis by A4,XBOOLE_0:def 3;
end;
suppose
x = cc;
then x in {aux, cc} by TARSKI:def 2;
then x in {aux, cc} \/ {aux, bb} by XBOOLE_0:def 3;
then x in {aux, cc} \/ {aux, bb} \/ {aux, intloc 0} by XBOOLE_0:def 3;
then x in {aux, cc} \/ {aux, bb} \/ {aux, intloc 0} \/ {aa, bb}by
XBOOLE_0:def 3;
hence thesis by A1,A4,XBOOLE_0:def 3;
end;
suppose
x in UsedILoc I;
then x in UsedILoc I4 by A2,XBOOLE_0:def 3;
hence thesis by A4,XBOOLE_0:def 3;
end;
end;
registration
let a be read-write Int-Location, b, c be Int-Location,
I be good MacroInstruction of SCM+FSA;
cluster for-up(a, b, c, I) -> good;
coherence;
end;
theorem Th21:
a <> aa & aa <> 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I) & I
does not destroy aa implies for-up(a, bb, cc, I) does not destroy aa
proof
assume that
A1: a <> aa and
A2: aa <> 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I) and
A3: I does not destroy aa;
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set i2 = AddTo(aux, intloc 0);
A4: i2 does not destroy aa by A2,SCMFSA7B:7;
set i3 = a := bb;
set i1 = SubFrom(aux, bb);
set i0 = aux := cc;
set I03 = i0 ";" i1 ";" i2 ";" i3;
i0 does not destroy aa & i1 does not destroy aa by A2,SCMFSA7B:6,8;
then i0 ";" i1 ";" i2 does not destroy aa by A4,SCMFSA8C:54,55;
then
A5: I03 does not destroy aa by A1,SCMFSA7B:6,SCMFSA8C:54;
set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
set I4 = while>0( aux, IB);
I ";" AddTo(a, intloc 0) does not destroy aa by A1,A3,SCMFSA7B:7,SCMFSA8C:54;
then IB does not destroy aa by A2,SCMFSA7B:8,SCMFSA8C:54;
then I4 does not destroy aa by SCMFSA8C:92;
hence thesis by A5,SCMFSA8C:52;
end;
theorem Th22:
for I being really-closed MacroInstruction of SCM+FSA holds
s.intloc 0 = 1 & s.bb > s.cc implies (for x st x <> a & x in {bb
, cc} \/ UsedILoc I holds IExec(for-up(a, bb, cc, I),p,s).x = s.x) &
for f
holds IExec(for-up(a, bb, cc, I),p,s).f = s.f
proof let I be really-closed MacroInstruction of SCM+FSA;
assume that
A1: s.intloc 0 = 1 and
A2: s.bb > s.cc;
cc = intloc 0 or cc is read-write by SCMFSA_M:def 2;
then
A3: (Initialized s).cc = s.cc by A1,SCMFSA_M:9,37;
set MI = for-up(a, bb, cc, I);
set i3 = a := bb;
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set i0 = aux := cc;
set i1 = SubFrom(aux, bb);
set i2 = AddTo(aux, intloc 0);
set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
set I4 = while>0( aux, IB);
set I03 = i0 ";" i1 ";" i2 ";" i3;
set s1 = IExec(I03,p,s),
p1 = p;
set s2 = s+*(aux, s.cc-s.bb+1)+*(a, s.bb);
A4: IExec(i0 ";" i1,p,s).intloc 0 = Exec(i1, Exec(i0, Initialized s)).intloc 0
by SCMFSA6C:8
.= Exec(i0, Initialized s).intloc 0 by SCMFSA_2:65
.= (Initialized s).intloc 0 by SCMFSA_2:63
.= 1 by SCMFSA_M:9;
bb = intloc 0 or bb is read-write by SCMFSA_M:def 2;
then
A5: (Initialized s).bb = s.bb by A1,SCMFSA_M:9,37;
A6: s1.intloc 0 = Exec(i3, IExec(i0 ";" i1 ";" i2,p,s)).intloc 0 by SCMFSA6C:6
.= IExec(i0 ";" i1 ";" i2,p,s).intloc 0 by SCMFSA_2:63
.= Exec(i2, IExec(i0 ";" i1,p,s)).intloc 0 by SCMFSA6C:6
.= 1 by A4,SCMFSA_2:64;
s.bb -s.bb > s.cc-s.bb by A2,XREAL_1:9;
then s.cc-s.bb <= -1 by INT_1:8;
then
A7: s.cc-s.bb+1 <= -1+1 by XREAL_1:6;
set s3 = IExec(MI,p,s);
a in {a, bb, cc} by ENUMSET1:def 1;
then a in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
then
A8: a <> aux by SCMFSA_M:25;
bb in {a, bb, cc} by ENUMSET1:def 1;
then bb in {a, bb, cc} \/ UsedILoc I by XBOOLE_0:def 3;
then
A9: bb <> aux by SCMFSA_M:25;
A10: s1.aux = Exec(i3, IExec(i0 ";" i1 ";" i2,p,s)).aux by SCMFSA6C:6
.= IExec(i0 ";" i1 ";" i2,p,s).aux by A8,SCMFSA_2:63
.= Exec(i2, IExec(i0 ";" i1,p,s)).aux by SCMFSA6C:6
.= IExec(i0 ";" i1,p,s).aux + 1 by A4,SCMFSA_2:64
.= Exec(i1, Exec(i0, Initialized s)).aux +1 by SCMFSA6C:8
.= Exec(i0, Initialized s).aux - Exec(i0, Initialized s).bb +1
by SCMFSA_2:65
.= (Initialized s).cc - Exec(i0, Initialized s).bb +1 by SCMFSA_2:63
.= s.cc-s.bb+1 by A9,A3,A5,SCMFSA_2:63;
then I4 is_halting_on s1,p1 by A7,SCMFSA_9:38;
then
A11: DataPart IExec(MI,p,s) = DataPart IExec(I4,p1,s1) by SFMASTR1:9
.= DataPart s1 by A10,A7,A6,SCMFSA9A:35
.= DataPart s2 by A1,Th14;
hereby
let x be Int-Location such that
A12: x <> a and
A13: x in {bb, cc} \/ UsedILoc I;
x in {a, bb, cc} \/ UsedILoc I
proof
per cases by A13,XBOOLE_0:def 3;
suppose
x in {bb, cc};
then x = bb or x = cc by TARSKI:def 2;
then x in {a, bb, cc} by ENUMSET1:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in UsedILoc I;
hence thesis by XBOOLE_0:def 3;
end;
end;
then
A14: x <> aux by SCMFSA_M:25;
thus s3.x = s2.x by A11,SCMFSA_M:2
.= (s+*(aux, s.cc-s.bb+1)).x by A12,FUNCT_7:32
.= s.x by A14,FUNCT_7:32;
end;
let x be FinSeq-Location;
thus s3.x = s2.x by A11,SCMFSA_M:2
.= (s+*(aux, s.cc-s.bb+1)).x by FUNCT_7:32,SCMFSA_2:58
.= s.x by FUNCT_7:32,SCMFSA_2:58;
end;
Lm1: now
let s, a, bb, cc, p;
let I be good really-closed MacroInstruction of SCM+FSA such that
A1: s.intloc 0 = 1 and
A2: ProperForUpBody a,bb,cc,I,s,p or I is parahalting;
A3: ProperForUpBody a,bb,cc,I,s,p by A2,Th15;
set scb1 = s.cc-s.bb+1;
set SF = StepForUp(a,bb,cc,I,p,s);
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
set s2 = s+*(aux, s.cc-s.bb+1)+*(a, s.bb),
p2 = p;
set IB2 = AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
set SW2 = StepWhile>0(aux,IB,p2,s2);
A4: IB = I ";" (AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0)) by SCMFSA6A:28;
A5: ProperBodyWhile>0 aux, IB, s2, p2
proof
let k be Nat;
assume StepWhile>0(aux,IB,p2,s2).k.aux > 0;
then
A6: k < scb1 by A1,A3,Th18;
A7: SF.k.intloc 0 = 1 by A1,A3,A6,Th17;
I is_halting_on SF.k,
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I), intloc 0))
by A3,A6;
then
A8: I is_halting_on Initialized SF.k,
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I), intloc 0))
by A7,SCMFSA8B:42;
IB2 is_halting_on IExec(I,
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I), intloc 0))
, SF.k),
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I), intloc 0))
by SCMFSA7B:19;
then IB is_halting_on Initialized SF.k,
p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I),
I ";" AddTo(a, intloc 0) ";"
SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc I), intloc 0))
by A4,A8,SFMASTR1:3;
hence thesis by A7,SCMFSA8B:42;
end;
set i3 = a := bb;
set i2 = AddTo(aux, intloc 0);
set i1 = SubFrom(aux, bb);
set i0 = aux := cc;
set s1 = IExec(i0 ";" i1 ";" i2 ";" i3,p,s),
p1 = p;
set SW1 = StepWhile>0(aux,IB,p1,s1);
deffunc U(State of SCM+FSA) = |.$1.aux.|;
consider f being Function of product the_Values_of SCM+FSA,NAT such
that
A9: for x being Element of product the_Values_of SCM+FSA holds f.x
= U(x) from FUNCT_2:sch 4;
A10: for x being State of SCM+FSA holds f.x = U(x)
proof let x be State of SCM+FSA;
reconsider x as Element of product the_Values_of SCM+FSA by CARD_3:107;
f.x = U(x) by A9;
hence thesis;
end;
A11: DataPart s1 = DataPart s2 by A1,Th14;
thus ProperBodyWhile>0 aux, IB, s1,p1
proof
let k be Nat;
assume
A12: StepWhile>0(aux,IB,p1,s1).k.aux > 0;
A13: DataPart SW2.k = DataPart SW1.k by A11,A5,SCMFSA9A:34;
then
A14: SW1.k.aux = SW2.k.aux by SCMFSA_M:2;
IB is_halting_on SW2.k, p2+*while>0(aux,IB) by A5,A12,A14;
hence thesis by A13,SCMFSA8B:5;
end;
A15: for k being Nat holds ( f.(SW1.(k+1)) < f.(SW1.k) or SW1.k.aux <= 0 )
proof
let k be Nat;
A16: DataPart SW1.k = DataPart SW2.k by A11,A5,SCMFSA9A:34;
then
A17: SW1.k.aux = SW2.k.aux by SCMFSA_M:2;
DataPart SW2.(k+1) = DataPart SW1.(k+1) by A11,A5,SCMFSA9A:34;
then
A18: SW1.(k+1).aux = SW2.(k+1).aux by SCMFSA_M:2;
now
assume
A19: SW1.k.aux > 0;
then
A20: k < scb1 by A1,A3,A17,Th18;
k < scb1 by A1,A3,A17,A19,Th18;
then
A21: SW2.k.aux+k = s.cc-s.bb+1 by A1,A3,Th17;
reconsider scb1 as Element of NAT by A20,INT_1:3;
A22: k+1 <= scb1 by A20,NAT_1:13;
then
A23: SW2.(k+1).aux+(k+1) = s.cc-s.bb+1 by A1,A3,Th17;
A24: f.(SW1.k) = |. SW1.k.aux .| by A10
.= SW2.k.aux by A17,A19,ABSVALUE:def 1;
per cases;
suppose
A25: SW1.(k+1).aux > 0;
f.(SW1.(k+1)) = |. SW1.(k+1).aux .| by A10
.= scb1-k-1 by A18,A23,A25,ABSVALUE:def 1;
hence f.(SW1.(k+1)) < f.(SW1.k) by A24,A21,XREAL_1:146;
end;
suppose
A26: SW1.(k+1).aux <= 0;
SW2.(k+1).aux = scb1 - (k+1) by A23;
then
A27: SW1.(k+1).aux = 0 by A18,A22,A26,XREAL_1:48;
f.(SW1.(k+1)) = |. SW1.(k+1).aux .| by A10
.= 0 by A27,ABSVALUE:def 1;
hence f.(SW1.(k+1)) < f.(SW1.k) by A16,A19,A24,SCMFSA_M:2;
end;
end;
hence thesis;
end;
thus WithVariantWhile>0 aux, IB, s1, p1
by A15;
end;
theorem Th23:
for Ig being good really-closed MacroInstruction of SCM+FSA holds
s.intloc 0 = 1 & k = s.cc-s.bb+1 & (ProperForUpBody a, bb, cc,
Ig, s,p or Ig is parahalting)
implies DataPart IExec(for-up(a, bb, cc, Ig),p, s) =
DataPart StepForUp(a,bb,cc,Ig,p,s).k
proof let Ig be good really-closed MacroInstruction of SCM+FSA;
set I = Ig;
assume that
A1: s.intloc 0 = 1 and
A2: k = s.cc-s.bb+1 and
A3: ProperForUpBody a,bb,cc,I,s,p or I is parahalting;
set scb1 = s.cc-s.bb+1;
set SF = StepForUp(a,bb,cc,I,p,s);
A4: ProperForUpBody a,bb,cc,I,s,p by A3,Th15;
set i3 = a := bb;
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set i0 = aux := cc;
set i1 = SubFrom(aux, bb);
set i2 = AddTo(aux, intloc 0);
reconsider IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0)
as really-closed MacroInstruction of SCM+FSA;
set I03 = i0 ";" i1 ";" i2 ";" i3;
set s1 = IExec(I03,p,s),
p1 = p;
A5: s1.intloc 0 = Exec(i3, IExec(i0 ";" i1 ";" i2,p,s)).intloc 0 by SCMFSA6C:6
.= IExec(i0 ";" i1 ";" i2,p,s).intloc 0 by SCMFSA_2:63
.= Exec(i2, IExec(i0 ";" i1,p,s)).intloc 0 by SCMFSA6C:6
.= IExec(i0 ";" i1,p,s).intloc 0 by SCMFSA_2:64
.= Exec(i1, Exec(i0, Initialized s)).intloc 0 by SCMFSA6C:8
.= Exec(i0, Initialized s).intloc 0 by SCMFSA_2:65
.= (Initialized s).intloc 0 by SCMFSA_2:63
.= 1 by SCMFSA_M:9;
then
A6: DataPart Initialized s1 = DataPart s1 by SCMFSA_M:19;
set Ex1 = ExitsAtWhile>0(aux, IB,p1, Initialized s1);
set SW1 = StepWhile>0(aux, IB,p1, Initialized s1);
A7: ProperBodyWhile>0 aux, IB, s1,p1 by A1,A3,Lm1;
then
A8: ProperBodyWhile>0 aux, IB, Initialized s1,p1 by A6,SCMFSA9A:38;
set s2 = s+*(aux, s.cc-s.bb+1)+*(a, s.bb),
p2 = p;
set SW2 = StepWhile>0(aux,IB,p2,s2);
A9: DataPart s1 = DataPart s2 by A1,Th14;
then DataPart SW1.k = DataPart SW2.k by A6,A8,SCMFSA9A:34;
then
A10: SW1.k.aux = SW2.k.aux by SCMFSA_M:2;
A11: WithVariantWhile>0 aux, IB, s1,p1 by A1,A3,Lm1;
then
A12: WithVariantWhile>0 aux, IB, Initialized s1,p1 by A5,A6,A7,SCMFSA9A:41;
consider K being Nat such that
A13: ExitsAtWhile>0(aux, IB, p1, Initialized s1) = K and
A14: (StepWhile>0(aux,IB,p1,Initialized s1).K).aux <= 0 and
A15: (for i being Nat
st (StepWhile>0(aux,IB,p1,Initialized s1).i).aux <= 0
holds K <= i) &
DataPart Comput(p1 +* while>0(aux, IB),
Initialize Initialized s1,
(LifeSpan(p1 +* while>0(aux, IB),Initialize Initialized s1)))
= DataPart StepWhile>0(aux,IB,p1,Initialized s1).K
by A12,A8,SCMFSA9A:def 6;
DataPart SW1.K = DataPart SW2.K by A6,A8,A9,SCMFSA9A:34;
then
A16: SW1.K.aux = SW2.K.aux by SCMFSA_M:2;
A17: now
assume
A18: K < scb1;
then SF.K.aux + K < 0+scb1 by A14,A16,XREAL_1:8;
hence contradiction by A1,A4,A18,Th17;
end;
SF.k.aux+k = scb1 by A1,A2,A4,Th17;
then K <= k by A2,A15,A10;
then
A19: Ex1 = k by A2,A13,A17,XXREAL_0:1;
set MI = for-up(a, bb, cc, I);
set I4 = while>0( aux, IB);
I4 is_halting_on s1,p1 by A7,A11,SCMFSA9A:27;
hence DataPart IExec(MI,p,s) = DataPart IExec(I4,p1,s1) by SFMASTR1:9
.= DataPart SW1.Ex1 by A8,A12,SCMFSA9A:36
.= DataPart StepForUp(a,bb,cc,I,p,s).k by A6,A8,A9,A19,SCMFSA9A:34;
end;
theorem Th24:
for Ig being good really-closed MacroInstruction of SCM+FSA holds
s.intloc 0 = 1 & (ProperForUpBody a,bb,cc,Ig,s,p or Ig is
parahalting) implies for-up(a, bb, cc, Ig) is_halting_on s,p
proof let Ig be good really-closed MacroInstruction of SCM+FSA;
set I = Ig;
assume that
A1: s.intloc 0 = 1 and
A2: ProperForUpBody a,bb,cc,I,s,p or I is parahalting;
set i3 = a := bb;
set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I);
set i0 = aux := cc;
set i1 = SubFrom(aux, bb);
set i2 = AddTo(aux, intloc 0);
set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0);
set I4 = while>0( aux, IB);
set I03 = i0 ";" i1 ";" i2 ";" i3;
set s1 = IExec(I03,p,s),
p1 = p;
A3: ProperBodyWhile>0 aux,IB,s1,p1 &
WithVariantWhile>0 aux,IB,s1,p1 by A1,A2,Lm1;
reconsider I03 as parahalting Program of SCM+FSA;
set MI = for-up(a, bb, cc, I);
A4: I03 is_halting_on Initialized s,p by SCMFSA7B:19;
I4 is_halting_on s1,p1 by A3,SCMFSA9A:27;
then MI is_halting_on Initialized s,p by A4,SFMASTR1:3;
hence thesis by A1,SCMFSA8B:42;
end;
begin :: Finding minimum in a section of an array
definition
let start, finish, minpos be Int-Location, f be FinSeq-Location;
func FinSeqMin(f, start, finish, minpos) -> MacroInstruction of SCM+FSA
equals
minpos := start ";"
for-up
(3-rdRWNotIn {start, finish, minpos}, start, finish,
(1-stRWNotIn {start, finish, minpos})
:= (f, 3-rdRWNotIn {start, finish, minpos}) ";"
((2-ndRWNotIn {start, finish, minpos}) := (f, minpos)) ";"
if>0((2-ndRWNotIn {start, finish, minpos}),
(1-stRWNotIn {start, finish, minpos}),
Macro (minpos := (3-rdRWNotIn {start, finish, minpos})),
Stop SCM+FSA
)
);
coherence;
end;
:: set aux1 = 1-stRWNotIn {start, finish, min_pos};
:: set aux2 = 2-ndRWNotIn {start, finish, min_pos};
:: set cv = 3-rdRWNotIn {start, finish, min_pos};
registration
let start, finish be Int-Location, minpos be read-write Int-Location, f be
FinSeq-Location;
cluster FinSeqMin(f, start, finish, minpos) -> good really-closed;
coherence;
end;
theorem Th25:
c <> aa implies FinSeqMin(f, aa, bb, c) does not destroy aa
proof
set a = aa, b = bb;
set aux1 = 1-stRWNotIn {a, b, c};
set aux2 = 2-ndRWNotIn {a, b, c};
set cv = 3-rdRWNotIn {a, b, c};
set i10 = aux1 := (f, cv);
set i11 = aux2 := (f, c);
reconsider I12 = if>0(aux2, aux1, Macro (c := cv), Stop SCM+FSA)
as really-closed MacroInstruction of SCM+FSA;
set I1B = i10 ";" i11 ";" I12;
set I1 = for-up ( cv, a, b, I1B);
A1: Stop SCM+FSA does not destroy a by SCMFSA8C:56;
A2: a in {a, b, c} by ENUMSET1:def 1;
then aux1 <> a by SCMFSA_M:25;
then
A3: i10 does not destroy a by SCMFSA7B:14;
A4: aux2 <> a by A2,SCMFSA_M:25;
then i11 does not destroy a by SCMFSA7B:14;
then
A5: i10 ";" i11 does not destroy a by A3,SCMFSA8C:55;
assume
A6: c <> aa;
then Macro (c := cv) does not destroy a by SCMFSA7B:6,SCMFSA8C:48;
then I12 does not destroy a by A4,A1,Th7;
then
A7: I1B does not destroy a by A5,SCMFSA8C:52;
a in {cv, a, b} by ENUMSET1:def 1;
then a in {cv, a, b} \/ UsedILoc I1B by XBOOLE_0:def 3;
then
A8: a <> 1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B) by SCMFSA_M:25;
cv <> a by A2,SCMFSA_M:25;
then I1 does not destroy a by A7,A8,Th21;
hence thesis by A6,SCMFSA7B:6,SCMFSA8C:53;
end;
theorem Th26:
{aa, bb, c} c= UsedILoc FinSeqMin(f, aa, bb, c)
proof
set a = aa, b = bb;
set aux1 = 1-stRWNotIn {a, b, c};
set aux2 = 2-ndRWNotIn {a, b, c};
set cv = 3-rdRWNotIn {a, b, c};
set i0 = c := a;
set i10 = aux1 := (f, cv);
set i11 = aux2 := (f, c);
set I12 = if>0(aux2, aux1, Macro (c := cv), Stop SCM+FSA);
set I1B = i10 ";" i11 ";" I12;
set I1 = for-up ( cv, a, b, I1B);
A1: UsedILoc (i0 ";" I1) = (UsedIntLoc i0) \/ UsedILoc I1 by SF_MASTR:29;
A2: {cv, a, b} \/ UsedILoc I1B c= UsedILoc I1 by Th20;
let x be object;
A3: UsedIntLoc i0 = {c,a} by SF_MASTR:14;
assume
A4: x in {a, b, c};
per cases by A4,ENUMSET1:def 1;
suppose
x = a;
then x in {c, a} by TARSKI:def 2;
hence thesis by A1,A3,XBOOLE_0:def 3;
end;
suppose
x = b;
then x in {cv, a, b} by ENUMSET1:def 1;
then x in {cv, a, b} \/ UsedILoc I1B by XBOOLE_0:def 3;
hence thesis by A1,A2,XBOOLE_0:def 3;
end;
suppose
x = c;
then x in {c, a} by TARSKI:def 2;
hence thesis by A1,A3,XBOOLE_0:def 3;
end;
end;
theorem Th27:
s.intloc 0 = 1 implies FinSeqMin(f, aa, bb, c) is_halting_on s,p
proof
assume
A1: s.intloc 0 = 1;
set a = aa, b = bb;
set aux1 = 1-stRWNotIn {a, b, c};
set aux2 = 2-ndRWNotIn {a, b, c};
set cv = 3-rdRWNotIn {a, b, c};
set i0 = c := a;
set i10 = aux1 := (f, cv);
set i11 = aux2 := (f, c);
set I12 = if>0(aux2, aux1, Macro (c := cv), Stop SCM+FSA);
set I1B = i10 ";" i11 ";" I12;
set I1 = for-up ( cv, a, b, I1B);
set s1 = IExec(Macro i0,p,s),
p1 = p;
A2: s1.intloc 0 = Exec(i0, Initialized s).intloc 0 by SCMFSA6C:5
.= (Initialized s). intloc 0 by SCMFSA_2:63
.= 1 by SCMFSA_M:9;
A3: Macro i0 is_halting_on Initialized s,p by SCMFSA7B:19;
I1 is_halting_on s1,p1 by A2,Th24;
then FinSeqMin(f, aa, bb, c) is_halting_on Initialized s,p by A3,SFMASTR1:3;
hence thesis by A1,SCMFSA8B:42;
end;
theorem Th28:
aa <> c & bb <> c & s.intloc 0 = 1 implies
IExec(FinSeqMin(f, aa, bb, c),p, s).f = s.f &
IExec(FinSeqMin(f, aa, bb, c),p, s).aa = s.aa &
IExec(FinSeqMin(f, aa, bb, c),p, s).bb = s.bb
proof
assume that
A1: aa <> c and
A2: bb <> c and
A3: s.intloc 0 = 1;
set a = aa, b = bb;
set i0 = c := a;
set s1 = Exec(i0, Initialized s),
p1 = p;
A4: a = intloc 0 or a is read-write by SCMFSA_M:def 2;
A5: b = intloc 0 or b is read-write by SCMFSA_M:def 2;
A6: s1.b = (Initialized s).b by A2,SCMFSA_2:63
.= s.b by A3,A5,SCMFSA_M:9,37;
set cv = 3-rdRWNotIn {a, b, c};
set aux2 = 2-ndRWNotIn {a, b, c};
set aux1 = 1-stRWNotIn {a, b, c};
set i10 = aux1 := (f, cv);
set i11 = aux2 := (f, c);
set I12 = if>0(aux2, aux1, Macro (c := cv), Stop SCM+FSA);
set I1B = i10 ";" i11 ";" I12;
set I1 = for-up ( cv, a, b, I1B);
A7: aux2 <> cv by SCMFSA_M:26;
cv in {cv, a, b} by ENUMSET1:def 1;
then
A8: cv in {cv, a, b} \/ UsedILoc I1B by XBOOLE_0:def 3;
A9: aux1 <> cv by SCMFSA_M:26;
A10: b in {a, b, c} by ENUMSET1:def 1;
then
A11: cv <> b by SCMFSA_M:25;
A12: aux1 <> b by A10,SCMFSA_M:25;
A13: aux2 <> b by A10,SCMFSA_M:25;
A14: s1.a = (Initialized s).a by A1,SCMFSA_2:63
.= s.a by A3,A4,SCMFSA_M:9,37;
b in {cv, a, b} by ENUMSET1:def 1;
then
A15: b in {cv, a, b} \/ UsedILoc I1B by XBOOLE_0:def 3;
A16: a in {a, b, c} by ENUMSET1:def 1;
then
A17: cv <> a by SCMFSA_M:25;
A18: aux1 <> a by A16,SCMFSA_M:25;
A19: aux2 <> a by A16,SCMFSA_M:25;
A20: s1.f = (Initialized s).f by SCMFSA_2:63
.= s.f by SCMFSA_M:37;
a in {cv, a, b} by ENUMSET1:def 1;
then
A21: a in {cv, a, b} \/ UsedILoc I1B by XBOOLE_0:def 3;
c in {a, b, c} by ENUMSET1:def 1;
then
A22: cv <> c by SCMFSA_M:25;
A23: s1.intloc 0 = (Initialized s). intloc 0 by SCMFSA_2:63
.= 1 by SCMFSA_M:9;
then
A24: I1 is_halting_on s1,p1 by Th24;
per cases;
suppose
A25: s.aa > s.bb;
thus IExec(FinSeqMin(f, aa, bb, c),p,s).f = IExec(I1,p1,s1).f by A24,
SFMASTR1:15
.= s.f by A23,A14,A6,A20,A25,Th22;
a in {a, b} by TARSKI:def 2;
then
A26: a in {a, b} \/ UsedILoc I1B by XBOOLE_0:def 3;
thus IExec(FinSeqMin(f, aa, bb, c),p,s).aa = IExec(I1,p1,s1).aa by A24,
SFMASTR1:14
.= s.aa by A17,A23,A14,A6,A25,A26,Th22;
b in {a, b} by TARSKI:def 2;
then
A27: b in {a, b} \/ UsedILoc I1B by XBOOLE_0:def 3;
thus IExec(FinSeqMin(f, aa, bb, c),p,s).bb = IExec(I1,p1,s1).bb by A24,
SFMASTR1:14
.= s.bb by A11,A23,A14,A6,A25,A27,Th22;
end;
suppose
A28: s.aa <= s.bb;
set SF = StepForUp(cv, a, b, I1B,p1, s1);
A29: s.a-s.a <= s.b-s.a by A28,XREAL_1:9;
then reconsider k = s.b - s.a +1 as Element of NAT by INT_1:3;
defpred P[Nat] means 0 < $1 & $1 <= k implies SF.$1.intloc 0 =
1 & SF.$1.cv = $1+s1.a & SF.$1.f = s1.f & SF.$1.a = s1.a & SF.$1.b = s1.b;
A30: ProperForUpBody cv, a, b, I1B, s1,p1 by Th15;
A31: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A32: P[n] and
0 < n+1 and
A33: n+1 <= k;
A34: SF.n.intloc 0 = 1 & SF.n.cv = n+s1.a & SF.n.cv <= s1.b
proof
per cases;
suppose
A35: 0 = n;
hence SF.n.intloc 0 = 1 by A23,Th8;
thus SF.n.cv = n+s1.a by A35,Th9;
thus thesis by A14,A6,A28,A35,Th9;
end;
suppose
A36: 0 < n;
hence SF.n.intloc 0 = 1 by A32,A33,NAT_1:13;
thus SF.n.cv = n+s1.a by A32,A33,A36,NAT_1:13;
n+1-1 <= s.b-s.a+1-1 by A33,XREAL_1:9;
hence thesis by A14,A6,A32,A33,A36,NAT_1:13,XREAL_1:19;
end;
end;
n < n+1 by XREAL_1:29;
then n < k by A33,XXREAL_0:2;
then
A37: SF.(n+1) | (({cv, a, b} \/ UsedILoc I1B) \/ FinSeq-Locations) =
IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n) |
(({cv, a, b} \/ UsedILoc I1B) \/
FinSeq-Locations) by A23,A14,A6,A30,Th19;
then
A38: SF.(n+1).f = IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).f
by SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0),
IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).f
by SFMASTR1:12
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).f
by SCMFSA_2:64
.= IExec(I12,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).f
by SFMASTR1:8;
A39: SF.(n+1).b = IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).b
by A15,A37,SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0), IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).b
by SFMASTR1:11
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).b
by A11,SCMFSA_2:64
.= IExec(I12,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).b
by SFMASTR1:7;
A40: SF.(n+1).a = IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).a by A21,A37,SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0), IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).a
by SFMASTR1:11
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).a
by A17,SCMFSA_2:64
.= IExec(I12,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).a
by SFMASTR1:7;
A41: SF.(n+1).cv = IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).cv
by A8,A37,SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0), IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).cv
by SFMASTR1:11
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/
UsedILoc I1B), intloc 0)), SF.n).cv+IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).intloc 0 by SCMFSA_2:64
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv+1 by SCMFSA6B:11
.= IExec(I12,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv+1 by SFMASTR1:7;
set ss = IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n);
set S0 = Initialized (SF.n);
set S1 = Exec(i10, S0);
set S2 = Exec(i11, Exec(i10, S0));
A42: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).f = S2.f by SCMFSA6C:9
.= S1.f by SCMFSA_2:72
.= S0.f by SCMFSA_2:72;
A43: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).intloc 0 = S2.intloc 0 by SCMFSA6C:8
.= S1.intloc 0 by SCMFSA_2:72
.= S0.intloc 0 by SCMFSA_2:72
.= 1 by SCMFSA_M:9;
then
A44: DataPart IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)) = DataPart
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
by Th1;
A45: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).b
= S2.b by SCMFSA6C:8
.= S1.b by A13,SCMFSA_2:72
.= S0.b by A12,SCMFSA_2:72;
A46: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).a
= S2.a by SCMFSA6C:8
.= S1.a by A19,SCMFSA_2:72
.= S0.a by A18,SCMFSA_2:72;
A47: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv = S2.cv by SCMFSA6C:8
.= S1.cv by A7,SCMFSA_2:72
.= S0.cv by A9,SCMFSA_2:72;
A48: Macro (c := cv) does not refer aux2 & Stop SCM+FSA does not refer
aux2 by A7,Th2,Th3,SCMFSA8C:51;
per cases;
suppose
A49: 0 = n;
thus thesis
proof
thus SF.(n+1).intloc 0 = 1 by A23,A14,A6,A30,A33,Th17;
A50: S0.f = SF.0.f by A49,SCMFSA_M:37
.= s.f by A20,Th13;
A51: S0.cv = SF.0.cv by A49,SCMFSA_M:37
.= s.a by A14,Th9;
A52: S0.b = SF.0.b by A5,A34,A49,SCMFSA_M:9,37
.= s1.b by A11,Th11;
A53: S0.a = SF.0.a by A4,A34,A49,SCMFSA_M:9,37
.= s1.a by A17,Th10;
thus thesis
proof
per cases;
suppose
A54: ss.aux2 <= ss.aux1;
hence
SF.(n+1).cv = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n))
.cv+1 by A7,A48,A41,SCMFSA8B:40
.= (n+1)+s1.a by A14,A44,A47,A49,A51,SCMFSA_M:2;
thus SF.(n+1).f = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).
f by A48,A38,A54,SCMFSA8B:40
.= s1.f by A20,A44,A42,A50,SCMFSA_M:2;
thus SF.(n+1).a = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).
a by A19,A48,A40,A54,SCMFSA8B:40
.= s1.a by A44,A46,A53,SCMFSA_M:2;
thus SF.(n+1).b = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).
b by A13,A48,A39,A54,SCMFSA8B:40
.= s1.b by A44,A45,A52,SCMFSA_M:2;
end;
suppose
A55: ss.aux2 > ss.aux1;
A56: IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.
n)).cv
= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n))).cv
by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv by A22,SCMFSA_2:63;
thus SF.(n+1).cv
= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv+1 by A56,A7,A48,A41,A55,SCMFSA8B:40
.= (n+1)+s1.a by A14,A47,A49,A51,SCMFSA_M:37;
thus SF.(n+1).f = IExec(Macro(c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
).f by A48,A38,A55,SCMFSA8B:40
.= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n))).f by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).f by SCMFSA_2:63
.= s1.f by A20,A42,A50,SCMFSA_M:37;
thus SF.(n+1).a = IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n
)).a by A19,A48,A40,A55,SCMFSA8B:40
.= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n))).a by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).a by A1,SCMFSA_2:63
.= s1.a by A4,A43,A46,A53,SCMFSA_M:9,37;
thus SF.(n+1).b = IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n
)).b by A13,A48,A39,A55,SCMFSA8B:40
.= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
)).b
by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).b
by A2,SCMFSA_2:63
.= s1.b by A5,A43,A45,A52,SCMFSA_M:9,37;
end;
end;
end;
end;
suppose
A57: 0 < n;
thus thesis
proof
thus SF.(n+1).intloc 0 = 1 by A23,A14,A6,A30,A33,Th17;
A58: S0.cv = SF.n.cv by SCMFSA_M:37;
A59: S0.a = s1.a by A4,A32,A33,A57,NAT_1:13,SCMFSA_M:9,37;
A60: S0.b = s1.b by A5,A32,A33,A57,NAT_1:13,SCMFSA_M:9,37;
A61: S0.f = s.f by A20,A32,A33,A57,NAT_1:13,SCMFSA_M:37;
thus thesis
proof
per cases;
suppose
A62: ss.aux2 <= ss.aux1;
hence
SF.(n+1).cv = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n))
.cv+1 by A7,A48,A41,SCMFSA8B:40
.= IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv+1 by A44,SCMFSA_M:2
.= (n+1)+s1.a by A34,A47,A58;
thus SF.(n+1).f = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).
f by A48,A38,A62,SCMFSA8B:40
.= s1.f by A20,A44,A42,A61,SCMFSA_M:2;
thus SF.(n+1).a = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).
a by A19,A48,A40,A62,SCMFSA8B:40
.= s1.a by A44,A46,A59,SCMFSA_M:2;
thus SF.(n+1).b = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).
b by A13,A48,A39,A62,SCMFSA8B:40
.= s1.b by A44,A45,A60,SCMFSA_M:2;
end;
suppose
A63: ss.aux2 > ss.aux1;
A64: IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.
n)).cv
= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n))).cv
by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv by A22,SCMFSA_2:63
.= IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv by SCMFSA_M:37;
thus
SF.(n+1).cv = IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.
n)).cv+1 by A7,A48,A41,A63,SCMFSA8B:40
.= (n+1)+s1.a by A34,A47,A58,A64;
thus SF.(n+1).f
= IExec(Macro(c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
).f by A48,A38,A63,SCMFSA8B:40
.= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n))).f by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).f by SCMFSA_2:63
.= s1.f by A20,A42,A61,SCMFSA_M:37;
thus SF.(n+1).a
= IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n
)).a by A19,A48,A40,A63,SCMFSA8B:40
.= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
)).a by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).a
by A1,SCMFSA_2:63
.= s1.a by A4,A43,A46,A59,SCMFSA_M:9,37;
thus SF.(n+1).b
= IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n
)).b by A13,A48,A39,A63,SCMFSA8B:40
.= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
)).b by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).b
by A2,SCMFSA_2:63
.= s1.b by A5,A43,A45,A60,SCMFSA_M:9,37;
end;
end;
end;
end;
end;
A65: P[0];
A66: for n being Nat holds P[n] from NAT_1:sch 2(A65, A31);
A67: DataPart IExec(I1,p1,s1) = DataPart SF.k by A23,A14,A6,Th23;
thus IExec(FinSeqMin(f, aa, bb, c),p,s).f = IExec(I1,p1,s1).f by A24,
SFMASTR1:15
.= SF.k.f by A67,SCMFSA_M:2
.= s.f by A20,A29,A66;
thus IExec(FinSeqMin(f, aa, bb, c),p,s).aa = IExec(I1,p1,s1).a by A24,
SFMASTR1:14
.= SF.k.a by A67,SCMFSA_M:2
.= s.aa by A14,A29,A66;
thus IExec(FinSeqMin(f, aa, bb, c),p,s).bb = IExec(I1,p1,s1).b by A24,
SFMASTR1:14
.= SF.k.b by A67,SCMFSA_M:2
.= s.bb by A6,A29,A66;
end;
end;
theorem Th29:
1 <= s.aa & s.aa <= s.bb & s.bb <= len (s.f) & aa <> c & bb <> c
& s.intloc 0 = 1 implies IExec(FinSeqMin(f, aa, bb, c),p,s).c
= min_at(s.f, |.s.aa.|, |.s.bb.|)
proof
set a = aa, b = bb;
assume that
A1: 1 <= s.a and
A2: s.a <= s.b and
A3: s.b <= len (s.f) and
A4: a <> c and
A5: b <> c and
A6: s.intloc 0 = 1;
A7: b = intloc 0 or b is read-write by SCMFSA_M:def 2;
set i0 = c := a;
set s1 = Exec(i0, Initialized s),
p1 = p;
A8: a = intloc 0 or a is read-write by SCMFSA_M:def 2;
reconsider sa = |.s.a.| as Element of NAT;
A9: s.a = sa by A1,ABSVALUE:def 1;
s.a-s.a <= s.b-s.a by A2,XREAL_1:9;
then reconsider sba = s.b-s.a as Element of NAT by INT_1:3;
A10: s1.f = (Initialized s).f by SCMFSA_2:63
.= s.f by SCMFSA_M:37;
set k = sba+1;
set cv = 3-rdRWNotIn {a, b, c};
set aux2 = 2-ndRWNotIn {a, b, c};
set aux1 = 1-stRWNotIn {a, b, c};
A11: aux1 <> aux2 by SCMFSA_M:26;
set I12 = if>0(aux2, aux1, Macro (c := cv), Stop SCM+FSA);
set i10 = aux1 := (f, cv);
A12: aux2 <> cv by SCMFSA_M:26;
set i11 = aux2 := (f, c);
A13: aux1 <> cv by SCMFSA_M:26;
A14: c in {a, b, c} by ENUMSET1:def 1;
then
A15: cv <> c by SCMFSA_M:25;
set I1B = i10 ";" i11 ";" I12;
set I1 = for-up ( cv, a, b, I1B);
set SF = StepForUp(cv, a, b, I1B, p1, s1);
defpred P[Nat] means 0 < $1 & $1 <= k implies SF.$1.intloc 0 = 1
& SF.$1.cv = $1+s1.a & SF.$1.f = s1.f & ex sa1 being Element of NAT st sa1 = $1
+sa-1 & SF.$1.c = min_at(s.f, sa, sa1);
cv in {cv, a, b} by ENUMSET1:def 1;
then
A16: cv in {cv, a, b} \/ (UsedILoc I1B) by XBOOLE_0:def 3;
A17: ProperForUpBody cv, a, b, I1B, s1, p1 by Th15;
A18: aux1 <> c by A14,SCMFSA_M:25;
A19: aux2 <> c by A14,SCMFSA_M:25;
A20: s1.c = (Initialized s).a by SCMFSA_2:63
.= s.a by A6,A8,SCMFSA_M:9,37;
A21: s1.a = (Initialized s).a by A4,SCMFSA_2:63
.= s.a by A6,A8,SCMFSA_M:9,37;
A22: s.a <= len (s.f) by A2,A3,XXREAL_0:2;
then
A23: sa in dom (s.f) by A1,A9,FINSEQ_3:25;
A24: s1.b = (Initialized s).b by A5,SCMFSA_2:63
.= s.b by A6,A7,SCMFSA_M:9,37;
A25: s1.intloc 0 = (Initialized s). intloc 0 by SCMFSA_2:63
.= 1 by SCMFSA_M:9;
then
A26: DataPart IExec(I1,p1,s1) = DataPart SF.k by A21,A24,Th23;
c in {c, cv} by TARSKI:def 2;
then c in UsedIntLoc (c := cv) by SF_MASTR:14;
then c in UsedILoc Macro (c := cv) by SF_MASTR:28;
then c in {aux2, aux1} \/ (UsedILoc Macro (c := cv)) by XBOOLE_0:def 3;
then c in {aux2, aux1} \/ (UsedILoc Macro (c := cv)) \/ UsedILoc Stop
SCM+FSA by XBOOLE_0:def 3;
then c in UsedILoc I12 by Th6;
then c in (UsedILoc (i10 ";" i11)) \/ UsedILoc I12 by XBOOLE_0:def 3;
then
A27: c in UsedILoc I1B by SF_MASTR:27;
then
A28: c in {cv, a, b} \/ (UsedILoc I1B) by XBOOLE_0:def 3;
A29: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A30: P[n] and
0 < n+1 and
A31: n+1 <= k;
A32: SF.n.intloc 0 = 1 & SF.n.cv = n+s1.a & SF.n.cv <= s1.b
proof
per cases;
suppose
A33: 0 = n;
hence SF.n.intloc 0 = 1 by A25,Th8;
thus SF.n.cv = n+s1.a by A33,Th9;
thus thesis by A2,A21,A24,A33,Th9;
end;
suppose
A34: 0 < n;
hence SF.n.intloc 0 = 1 by A30,A31,NAT_1:13;
thus SF.n.cv = n+s1.a by A30,A31,A34,NAT_1:13;
n+1-1 <= s.b-s.a+1-1 by A31,XREAL_1:9;
hence thesis by A21,A24,A30,A34,NAT_1:13,XREAL_1:19;
end;
end;
set S0 = Initialized (SF.n);
set S1 = Exec(i10, S0);
set S2 = Exec(i11, Exec(i10, S0));
A35: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).f
= S2.f by SCMFSA6C:9
.= S1.f by SCMFSA_2:72
.= S0.f by SCMFSA_2:72;
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).intloc 0 = S2.intloc 0 by SCMFSA6C:8
.= S1.intloc 0 by SCMFSA_2:72
.= S0.intloc 0 by SCMFSA_2:72
.= 1 by SCMFSA_M:9;
then
A36: DataPart IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n))
= DataPart
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
by Th1;
n < n+1 by XREAL_1:29;
then n < k by A31,XXREAL_0:2;
then
A37: SF.(n+1) | ({cv, a, b} \/ (UsedILoc I1B) \/ FinSeq-Locations) =
IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n) |
({cv, a, b} \/ (UsedILoc I1B) \/
FinSeq-Locations) by A25,A21,A24,A17,Th19;
then
A38: SF.(n+1).f = IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).f
by SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0), IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).f
by SFMASTR1:12
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).f
by SCMFSA_2:64
.= IExec(I12,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).f
by SFMASTR1:8;
A39: SF.(n+1).c = IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).c
by A28,A37,SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0), IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).c
by SFMASTR1:11
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).c
by A15,SCMFSA_2:64
.= IExec(I12,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).c
by SFMASTR1:7;
A40: SF.(n+1).cv = IExec(I1B ";" AddTo(cv, intloc 0),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv by A16,A37,SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0), IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv by SFMASTR1:11
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv+IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).intloc 0 by SCMFSA_2:64
.= IExec(I1B,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv+1 by SCMFSA6B:11
.= IExec(I12,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv+1 by SFMASTR1:7;
A41: Macro (c := cv) does not refer aux2 & Stop SCM+FSA does not refer
aux2 by A12,Th2,Th3,SCMFSA8C:51;
A42: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).c = S2.c by SCMFSA6C:8
.= S1.c by A19,SCMFSA_2:72
.= S0.c by A18,SCMFSA_2:72
.= SF.n.c by SCMFSA_M:37;
A43: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n).cv
= S2.cv by SCMFSA6C:8
.= S1.cv by A12,SCMFSA_2:72
.= S0.cv by A13,SCMFSA_2:72;
per cases;
suppose
A44: 0 = n;
thus thesis
proof
reconsider sa1 = (n+1)+sa-1 as Element of NAT by A44;
A45: SF.0.c = s1.c by A15,A27,Th12;
A46: S1.c = S0.c by A18,SCMFSA_2:72
.= s.a by A20,A44,A45,SCMFSA_M:37;
thus SF.(n+1).intloc 0 = 1 by A25,A21,A24,A17,A31,Th17;
A47: S0.f = SF.0.f by A44,SCMFSA_M:37
.= s.f by A10,Th13;
then
A48: S1.f = s.f by SCMFSA_2:72;
A49: S0.cv = SF.0.cv by A44,SCMFSA_M:37
.= s.a by A21,Th9;
then reconsider S0cv = S0.cv as Element of NAT by A1,INT_1:3;
A50: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).aux1 = S2.aux1 by SCMFSA6C:8
.= S1.aux1 by A11,SCMFSA_2:72
.= (S0.f)/.|.S0.cv.| by Th4
.= s.f.S0cv by A9,A23,A47,A49,PARTFUN1:def 6;
A51: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).aux2 = S2.aux2 by SCMFSA6C:8
.= (S1.f)/.|.S1.c.| by Th4
.= s.f.S0cv by A9,A23,A49,A48,A46,PARTFUN1:def 6;
hence SF.(n+1).cv = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv+1
by A12,A41,A40,A50,SCMFSA8B:40
.= (n+1)+s1.a by A21,A36,A43,A44,A49,SCMFSA_M:2;
thus SF.(n+1).f = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).f
by A41,A38,A50,A51,SCMFSA8B:40
.= s1.f by A10,A36,A35,A47,SCMFSA_M:2;
take sa1;
thus sa1 = (n+1)+sa-1;
SF.(n+1).c = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).c
by A19,A41,A39,A50,A51,SCMFSA8B:40
.= s.a by A20,A36,A42,A44,A45,SCMFSA_M:2;
hence thesis by A1,A22,A9,A44,FINSEQ_6:162;
end;
end;
suppose
A52: 0 < n;
thus thesis
proof
A53: S0.cv = SF.n.cv by SCMFSA_M:37;
then reconsider S0cv = S0.cv as Element of NAT by A1,A21,A32,INT_1:3;
1 <= S0cv & S0cv <= len (s.f) by A1,A3,A9,A21,A24,A32,A53,NAT_1:12
,XXREAL_0:2;
then
A54: S0cv in dom (s.f) by FINSEQ_3:25;
A55: S0.f = s.f by A10,A30,A31,A52,NAT_1:13,SCMFSA_M:37;
then
A56: S1.f = s.f by SCMFSA_2:72;
A57: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).aux1 = S2.aux1 by SCMFSA6C:8
.= S1.aux1 by A11,SCMFSA_2:72
.= (S0.f)/.|.S0.cv.| by Th4
.= (S0.f)/.S0cv by ABSVALUE:def 1
.= s.f.S0cv by A55,A54,PARTFUN1:def 6;
n+s.a <= len (s.f) by A3,A21,A24,A32,XXREAL_0:2;
then n+s.a-1 <= len (s.f)-1 by XREAL_1:9;
then
A58: n+s.a-1+0 <= len (s.f)-1+1 by XREAL_1:7;
thus SF.(n+1).intloc 0 = 1 by A25,A21,A24,A17,A31,Th17;
consider sa1 being Nat such that
A59: sa1 = n+sa-1 and
A60: SF.n.c = min_at(s.f, sa, sa1) by A30,A31,A52,NAT_1:13;
reconsider SFnc = SF.n.c as Element of NAT
by A60,ORDINAL1:def 12;
0+1 <= n by A52,NAT_1:13;
then 1-1 <= n-1 by XREAL_1:9;
then
A61: 0+s.a <= n-1+s.a by XREAL_1:6;
then
A62: sa <= SFnc by A1,A9,A59,A60,A58,FINSEQ_6:161;
then
A63: 1 <= SFnc by A1,A9,XXREAL_0:2;
A64: SFnc <= sa1 by A1,A9,A59,A60,A61,A58,FINSEQ_6:161;
then SFnc <= len (s.f) by A9,A59,A58,XXREAL_0:2;
then
A65: SFnc in dom (s.f) by A63,FINSEQ_3:25;
A66: IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).aux2
= S2.aux2 by SCMFSA6C:8
.= (S1.f)/.|.S1.c.| by Th4
.= (S1.f)/.|.S0.c.| by A18,SCMFSA_2:72
.= (S1.f)/.|.SF.n.c.| by SCMFSA_M:37
.= (S1.f)/.SFnc by ABSVALUE:def 1
.= s.f.SFnc by A56,A65,PARTFUN1:def 6;
A67: for i st sa <= i & i < SF.n.c holds s.f.i > s.f.(SFnc) by A1,A9,A59,A60
,A61,A58,FINSEQ_6:161;
thus thesis
proof
A68: (n+1)+s.a-1 <= len (s.f) by A3,A21,A24,A32,XXREAL_0:2;
A69: (n+1)+s.a-1 = n+s.a+1-1
.= n+sa by A1,ABSVALUE:def 1;
then
A70: s.a <= (n+1)+s.a-1 by NAT_1:12;
per cases;
suppose
A71: s.f.S0cv < s.f.SFnc;
A72: IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
).cv
= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n))).cv by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv by A15,SCMFSA_2:63;
thus SF.(n+1).cv
= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).cv+1 by A72,A12,A41,A40,A57,A66,A71,SCMFSA8B:40
.= IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv+1 by SCMFSA_M:37
.= (n+1)+s1.a by A32,A43,A53;
thus SF.(n+1).f
= IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n))
.f by A41,A38,A57,A66,A71,SCMFSA8B:40
.= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n))).f by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n)).f by SCMFSA_2:63
.= s1.f by A10,A35,A55,SCMFSA_M:37;
reconsider sa11 = (n+1)+sa-1 as Element of NAT by A69;
take sa11;
thus sa11 = (n+1)+sa-1;
A73: for i st s.a <= i & i <= (n+1)+s.a-1 holds s.f.S0cv <= s.f.i
proof
let i such that
A74: s.a <= i and
A75: i <= (n+1)+s.a-1;
per cases by A75,XXREAL_0:1;
suppose
i < (n+1)+s.a-1;
then i+1 <= n+s.a by A69,NAT_1:13;
then i+1-1 <= n+s.a-1 by XREAL_1:9;
then s.f.(SFnc) <= s.f.i by A1,A9,A59,A60,A61,A58,A74,
FINSEQ_6:161;
hence thesis by A71,XXREAL_0:2;
end;
suppose
i = (n+1)+s.a-1;
hence thesis by A21,A32,SCMFSA_M:37;
end;
end;
A76: for i st s.a <= i & i < S0cv holds s.f.i > s.f.S0cv
proof
let i;
assume that
A77: s.a <= i and
A78: i < S0cv;
i+1 <= S0cv by A78,NAT_1:13;
then i+1-1 <= S0cv-1 by XREAL_1:9;
then s.f.SFnc <= s.f.i by A1,A9,A21,A32,A53,A59,A60,A61,A58,A77,
FINSEQ_6:161;
hence thesis by A71,XXREAL_0:2;
end;
SF.(n+1).c
= IExec(Macro (c := cv),
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n))
.c by A19,A41,A39,A57,A66,A71,SCMFSA8B:40
.= ( Exec(c := cv, Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)
)).c
by SCMFSA6C:5
.= (Initialized IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).cv
by SCMFSA_2:63
.= S0cv by A43,SCMFSA_M:37;
hence thesis by A1,A9,A21,A32,A53,A70,A68,A73,A76,FINSEQ_6:161;
end;
suppose
A79: s.f.SFnc <= s.f.S0cv;
thus thesis
proof
A80: for i st s.a <= i & i <= (n+1)+s.a-1 holds s.f.(SFnc) <= s
.f.i
proof
let i such that
A81: s.a <= i and
A82: i <= (n+1)+s.a-1;
per cases by A82,XXREAL_0:1;
suppose
i < (n+1)+s.a-1;
then i+1 <= n+s.a by A69,NAT_1:13;
then i+1-1 <= n+s.a-1 by XREAL_1:9;
hence thesis by A1,A9,A59,A60,A61,A58,A81,FINSEQ_6:161;
end;
suppose
i = (n+1)+s.a-1;
hence thesis by A21,A32,A79,SCMFSA_M:37;
end;
end;
thus SF.(n+1).cv = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n))
.cv+1 by A12,A41,A40,A57,A66,A79,SCMFSA8B:40
.= IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
SF.n).cv+1 by A36,SCMFSA_M:2
.= (n+1)+s1.a by A32,A43,A53;
thus SF.(n+1).f = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n)).
f by A41,A38,A57,A66,A79,SCMFSA8B:40
.= s1.f by A10,A36,A35,A55,SCMFSA_M:2;
reconsider sa11 = (n+1)+sa-1 as Element of NAT by A69;
take sa11;
thus sa11 = (n+1)+sa-1;
n+s.a-1 <= n+s.a-1+1 by XREAL_1:29;
then
A83: SFnc <= (n+1)+s.a-1 by A9,A59,A64,XXREAL_0:2;
SF.(n+1).c = IExec(Stop SCM+FSA,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)),
IExec(i10 ";" i11,
p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B),
I1B ";" AddTo(cv, intloc 0) ";"
SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedILoc I1B), intloc 0)), SF.n))
.c by A19,A41,A39,A57,A66,A79,SCMFSA8B:40
.= SF.n.c by A36,A42,SCMFSA_M:2;
hence thesis by A1,A9,A62,A67,A70,A68,A83,A80,FINSEQ_6:161;
end;
end;
end;
end;
end;
end;
reconsider sb = |.s.b.| as Element of NAT;
A84: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A84, A29);
then consider sab being Element of NAT such that
A85: sab = k+sa-1 and
A86: SF.k.c = min_at(s.f, sa, sab);
A87: sab = sb by A9,A85,ABSVALUE:def 1;
I1 is_halting_on s1,p1 by A25,Th24;
hence IExec(FinSeqMin(f, a, b, c),p, s).c = IExec(I1,p1,s1).c by SFMASTR1:14
.= min_at(s.f, |.s.a.|, |.s.b.|) by A26,A86,A87,SCMFSA_M:2;
end;
begin :: A swap macro instruction
definition
let f be FinSeq-Location, a, b be Int-Location;
func swap(f, a, b) -> MacroInstruction of SCM+FSA equals
1-stRWNotIn {a, b} := (f,a)
";" (2-ndRWNotIn {a, b} := (f,b)) ";" ((f,a) := (2-ndRWNotIn {a, b})) ";" ((f,b
) := (1-stRWNotIn {a, b}));
coherence;
end;
registration
let f be FinSeq-Location, a, b be Int-Location;
cluster swap(f, a, b) -> good parahalting;
coherence;
end;
theorem Th30:
cc <> 1-stRWNotIn {aa, bb} & cc <> 2-ndRWNotIn {aa, bb} implies
swap(f, aa, bb) does not destroy cc
proof
set a = aa, b = bb;
set aux1 = 1-stRWNotIn {a, b};
set aux2 = 2-ndRWNotIn {a, b};
assume cc <> 1-stRWNotIn {aa, bb} & cc <> 2-ndRWNotIn {aa, bb};
then
A1: aux1 := (f,a) does not destroy cc & aux2 := (f,b) does not destroy cc by
SCMFSA7B:14;
(f,a) := aux2 does not destroy cc by SCMFSA7B:15;
then aux1 := (f,a) ";" (aux2 := (f,b)) ";" ((f,a) := aux2) does not destroy
cc by A1,SCMFSA8C:54,55;
hence thesis by SCMFSA7B:15,SCMFSA8C:54;
end;
theorem Th31:
1 <= s.aa & s.aa <= len (s.f) & 1 <= s.bb & s.bb <= len (s.f) &
s.intloc 0 = 1
implies IExec(swap(f,aa,bb),p,s).f = s.f+*(s.aa, s.f.(s.bb))+*(
s.bb, s.f.(s.aa))
proof
set a = aa, b = bb;
assume that
A1: 1 <= s.a and
A2: s.a <= len (s.f) and
A3: 1 <= s.b and
A4: s.b <= len (s.f) and
A5: s.intloc 0 = 1;
set aux1 = 1-stRWNotIn {a, b}, aux2 = 2-ndRWNotIn {a, b};
set i0 = aux1 := (f,a), i1 = aux2 := (f,b), i2 = (f,a) := aux2;
set s0 = Initialized s, s1 = Exec(i0, s0), s2 = IExec(i0 ";" i1,p,s);
A6: b = intloc 0 or b is read-write by SCMFSA_M:def 2;
reconsider sa = s.a as Element of NAT by A1,INT_1:3;
set s0a = |.s0.a.|, s2a = |.s2.a.|;
A7: a = intloc 0 or a is read-write by SCMFSA_M:def 2;
A8: sa = |.s.a.| by ABSVALUE:def 1;
then
A9: s0.f = s.f & sa = s0a by A5,A7,SCMFSA_M:9,37;
reconsider sb = s.b as Element of NAT by A3,INT_1:3;
A10: sb = |.s.b.| by ABSVALUE:def 1;
set s3 = IExec(i0 ";" i1 ";" i2,p,s);
A11: aux1 <> aux2 by SCMFSA_M:26;
A12: s3.aux1 = Exec(i2, s2).aux1 by SCMFSA6C:6
.= s2.aux1 by SCMFSA_2:73
.= Exec(i1, s1).aux1 by SCMFSA6C:8
.= s1.aux1 by A11,SCMFSA_2:72
.= (s0.f)/.s0a by Th4
.= s.f.sa by A1,A2,A9,FINSEQ_4:15;
set i3 = (f,b) := aux1;
A13: s2.f = Exec(i1, s1).f by SCMFSA6C:9
.= s1.f by SCMFSA_2:72;
A14: s3.f = Exec(i2, s2).f by SCMFSA6C:7
.= s2.f+*(s2a, s2.aux2) by Th5;
A15: b in {a, b} by TARSKI:def 2;
then
A16: b <> aux2 by SCMFSA_M:25;
b <> aux1 by A15,SCMFSA_M:25;
then
A17: s1.b = s0.b by SCMFSA_2:72
.= s.b by A5,A6,SCMFSA_M:9,37;
A18: a in {a, b} by TARSKI:def 2;
then
A19: a <> aux2 by SCMFSA_M:25;
A20: a <> aux1 by A18,SCMFSA_M:25;
s2.a = Exec(i1, s1).a by SCMFSA6C:8
.= s1.a by A19,SCMFSA_2:72
.= s0.a by A20,SCMFSA_2:72;
then
A21: sa = s2a by A5,A8,A7,SCMFSA_M:9,37;
set s1b = |.s1.b.|;
A22: s1.f = s0.f by SCMFSA_2:72
.= s.f by SCMFSA_M:37;
A23: s3.b = Exec(i2, s2).b by SCMFSA6C:6
.= s2.b by SCMFSA_2:73
.= Exec(i1, s1).b by SCMFSA6C:8
.= s1.b by A16,SCMFSA_2:72;
A24: s2.aux2 = Exec(i1, s1).aux2 by SCMFSA6C:8
.= (s1.f)/.s1b by Th4
.= s.f.sb by A3,A4,A10,A22,A17,FINSEQ_4:15;
thus IExec(swap(f,a,b),p,s).f = Exec(i3, s3).f by SCMFSA6C:7
.= s.f+*(s.a, s.f.(s.b))+*(s.b, s.f.(s.a)) by A10,A22,A13,A14,A21,A17,A23
,A24,A12,Th5;
end;
theorem
1 <= s.aa & s.aa <= len (s.f) & 1 <= s.bb & s.bb <= len (s.f) & s.
intloc 0 = 1 implies IExec(swap(f,aa,bb),p,s).f.(s.aa) = s.f.(s.bb) &
IExec(swap(f,aa,bb),p,s).f.(s.bb) = s.f.(s.aa)
proof
set a = aa, b = bb;
assume that
A1: 1 <= s.a and
A2: s.a <= len (s.f) and
A3: 1 <= s.b and
A4: s.b <= len (s.f) and
A5: s.intloc 0 = 1;
A6: IExec(swap(f,a,b),p,s).f = (s.f+*(s.a, s.f.(s.b))+*(s.b, s.f.(s.a))) by A1
,A2,A3,A4,A5,Th31;
reconsider sa = s.a as Element of NAT by A1,INT_1:3;
A7: sa in dom (s.f) by A1,A2,FINSEQ_3:25;
A8: dom (s.f+*(s.a, s.f.(s.b))) = dom (s.f) by FUNCT_7:30;
reconsider sb = s.b as Element of NAT by A3,INT_1:3;
A9: sb in dom (s.f) by A3,A4,FINSEQ_3:25;
per cases;
suppose
sa <> sb;
hence
IExec(swap(f,a,b),p,s).f.(s.a) = (s.f+*(s.a, s.f.(s.b))).(s.a) by A6,
FUNCT_7:32
.= s.f.(s.b) by A7,FUNCT_7:31;
thus thesis by A9,A6,A8,FUNCT_7:31;
end;
suppose
sa = sb;
hence IExec(swap(f,a,b),p,s).f.(s.a) = s.f.(s.b) by A7,A6,A8,FUNCT_7:31;
thus thesis by A9,A6,A8,FUNCT_7:31;
end;
end;
theorem Th33:
{aa, bb} c= UsedILoc swap(f, aa, bb)
proof
set a = aa, b = bb;
set aux1 = 1-stRWNotIn {a, b}, aux2 = 2-ndRWNotIn {a, b};
set i0 = aux1 := (f,a), i1 = aux2 := (f,b), i2 = (f,a) := aux2;
set i3 = (f,b) := aux1;
A1: UsedILoc swap(f, a, b) = UsedILoc (i0 ";" i1 ";" i2) \/ UsedIntLoc
i3 by SF_MASTR:30
.= UsedILoc (i0 ";" i1) \/ (UsedIntLoc i2) \/ UsedIntLoc i3 by SF_MASTR:30
.= (UsedIntLoc i0) \/ (UsedIntLoc i1) \/ (UsedIntLoc i2) \/ UsedIntLoc
i3 by SF_MASTR:31
.= {aux1, a} \/ (UsedIntLoc i1) \/ (UsedIntLoc i2) \/ UsedIntLoc i3 by
SF_MASTR:17
.= {aux1, a} \/ {aux2, b} \/ (UsedIntLoc i2) \/ UsedIntLoc i3 by
SF_MASTR:17
.= {aux1, a} \/ {aux2, b} \/ {aux2, a} \/ UsedIntLoc i3 by SF_MASTR:17
.= {aux1, a} \/ {aux2, b} \/ {aux2, a} \/ {aux1, b} by SF_MASTR:17;
let x be object;
assume
A2: x in {a, b};
per cases by A2,TARSKI:def 2;
suppose
x = a;
then x in {aux2, a} by TARSKI:def 2;
then x in {aux1, a} \/ {aux2, b} \/ {aux2, a} by XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
suppose
x = b;
then x in {aux1, b} by TARSKI:def 2;
hence thesis by A1,XBOOLE_0:def 3;
end;
end;
theorem
UsedI*Loc swap(f, aa, bb) = {f}
proof
set a = aa, b = bb;
set aux1 = 1-stRWNotIn {a, b};
set aux2 = 2-ndRWNotIn {a, b};
thus UsedI*Loc swap(f, a, b) = UsedI*Loc (aux1 := (f,a) ";" (aux2 := (f,
b)) ";" ((f,a) := aux2)) \/ UsedInt*Loc ((f,b) := aux1) by SF_MASTR:46
.= UsedI*Loc (aux1 := (f,a) ";" (aux2 := (f,b)) ";" ((f,a) := aux2))
\/ {f} by SF_MASTR:33
.= UsedI*Loc (aux1 := (f,a) ";" (aux2 := (f,b))) \/ (UsedInt*Loc ((f,a
) := aux2)) \/ {f} by SF_MASTR:46
.= UsedI*Loc (aux1 := (f,a) ";" (aux2 := (f,b))) \/ {f} \/ {f} by
SF_MASTR:33
.= (UsedInt*Loc (aux1 := (f,a)) \/ (UsedInt*Loc (aux2 := (f,b)))) \/ {f}
\/ {f} by SF_MASTR:47
.= {f} \/ (UsedInt*Loc (aux2 := (f,b))) \/ {f} \/ {f} by SF_MASTR:33
.= {f} \/ {f} \/ {f} by SF_MASTR:33
.= {f};
end;
begin :: Selection sort
definition
let f be FinSeq-Location;
func Selection-sort f -> Program of SCM+FSA equals
(1-stNotUsed swap(f, 1
-stRWNotIn {} Int-Locations, 2-ndRWNotIn {} Int-Locations)) :=len f ";" for-up
( 1-stRWNotIn {} Int-Locations, intloc 0, (1-stNotUsed swap(f, 1-stRWNotIn {}
Int-Locations, 2-ndRWNotIn {} Int-Locations)), FinSeqMin(f, 1-stRWNotIn {}
Int-Locations, (1-stNotUsed swap(f, 1-stRWNotIn {} Int-Locations, 2-ndRWNotIn
{} Int-Locations)), 2-ndRWNotIn {} Int-Locations) ";" swap(f, 1-stRWNotIn {}
Int-Locations, 2-ndRWNotIn {} Int-Locations) );
coherence;
end;
theorem
for S being State of SCM+FSA st S = IExec(Selection-sort f,p,s)
holds S.f is_non_decreasing_on 1, len (S.f) &
ex p being Permutation of dom(s.f) st S.f = (s.f) * p
proof
set minpos = 2-ndRWNotIn {} Int-Locations;
set cv = 1-stRWNotIn {} Int-Locations;
let S be State of SCM+FSA such that
A1: S = IExec(Selection-sort f,p,s);
set I22 = swap(f, cv, minpos);
set finish = 1-stNotUsed swap(f, cv, minpos);
set i1 = finish :=len f;
set I21 = FinSeqMin(f, cv, finish, minpos);
set I2B = I21 ";" I22;
set I2 = for-up ( cv, intloc 0, finish, I2B );
set s1 = Exec(i1, Initialized s),
p1 = p;
A2: s1.intloc 0 = (Initialized s).intloc 0 by SCMFSA_2:74
.= 1 by SCMFSA_M:9;
cv in {cv, minpos} by TARSKI:def 2;
then cv <> 1-stRWNotIn {cv, minpos} & cv <> 2-ndRWNotIn{cv, minpos} by
SCMFSA_M:25;
then
A3: swap(f, cv, minpos) does not destroy cv by Th30;
set SF = StepForUp(cv, intloc 0, finish, I2B, p1, s1);
A4: s1.finish = len ((Initialized s).f) by SCMFSA_2:74
.= len (s.f) by SCMFSA_M:37;
then reconsider n = s1.finish-s1.intloc 0 +1 as Element of NAT by A2;
defpred P[Nat] means
$1 <= n implies SF.$1.cv = $1+s1.intloc 0 &
SF.$1.finish = s1.finish & SF.$1.f is_split_at $1 & SF.$1.f
is_non_decreasing_on 1, $1 & ex p being Permutation of dom(s.f) st SF.$1.f = (s
.f) * p;
defpred Q[Nat] means $1 < n implies SF.$1.intloc 0 = 1 &
I2B is_halting_on SF.$1,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0));
A5: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat such that
A6: Q[k];
assume k+1 < n;
hence
A7: SF.(k+1).intloc 0 = 1 by A6,Th16,NAT_1:13;
(Initialized SF.(k+1)).intloc 0 = 1 by SCMFSA_M:9;
then
A8: I21 is_halting_on Initialized
SF.(k+1),
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by Th27;
I22 is_halting_on IExec(I21,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.(k+1)),
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by SCMFSA7B:19;
then I2B is_halting_on Initialized SF.(k+1),
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by SFMASTR1:3,A8;
hence thesis by A7,SCMFSA8B:42;
end;
A9: Q[0]
proof
(Initialized SF.0).intloc 0 = 1 by SCMFSA_M:9;
then
A10: I21 is_halting_on Initialized SF.0,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by Th27;
assume 0 < n;
thus
A11: SF.0.intloc 0 = 1 by A2,Th8;
I22 is_halting_on IExec(I21,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.0),
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by SCMFSA7B:19;
then I2B is_halting_on Initialized SF.0,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by SFMASTR1:3,A10;
hence thesis by A11,SCMFSA8B:42;
end;
A12: for k being Nat holds Q[k] from NAT_1:sch 2(A9, A5);
A13: ProperForUpBody cv, intloc 0, finish, I2B, s1, p1
by A12;
then
A14: DataPart IExec(I2,p1,s1) = DataPart SF.n by A2,Th23;
I2 is_halting_on s1,p1 by A2,A13,Th24;
then
A15: S.f = IExec(I2,p1,s1).f by A1,SFMASTR1:15
.= SF.n.f by A14,SCMFSA_M:2;
FinSeqMin(f, cv, finish, minpos) does not destroy cv by Th25,SCMFSA_M:26;
then
A16: I2B does not destroy cv by A3,SCMFSA8C:52;
A17: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A18: P[k];
A19: now
assume
A20: k < n;
hence
A21: SF.k.intloc 0 = 1 by A12;
I2B is_halting_on SF.k,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by A12,A20;
hence I2B is_halting_on Initialized SF.k,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by A21,SCMFSA8B:42;
thus SF.k.cv = k+s1.intloc 0 by A18,A20;
thus SF.k.finish = s1.finish by A18,A20;
thus SF.k.cv <= s1.finish by A2,A18,A20,NAT_1:13;
thus SF.(k+1) | ({cv, intloc 0, finish} \/ (UsedILoc I2B) \/
FinSeq-Locations) = IExec(I2B ";" AddTo(cv,intloc 0),
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k) |
({cv, intloc 0,
finish} \/ (UsedILoc I2B) \/ FinSeq-Locations) by A2,A13,A20,Th19;
end;
set F = SF.k.f, F1 = SF.(k+1).f;
assume
A22: k+1 <= n;
then consider pp being Permutation of dom(s.f) such that
A23: F = (s.f) * pp by A18,NAT_1:13;
thus SF.(k+1).cv = (k+1)+s1.intloc 0 by A16,A2,A13,A22,Th17;
A24: I22 is_halting_on
Initialized IExec(I21,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k),
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by SCMFSA7B:19;
A25: finish = 1-stRWNotIn UsedILoc I22 by SFMASTR1:def 4;
set ma = min_at(F, k+1, len F);
A26: dom(s.f) = Seg len(s.f) by FINSEQ_1:def 3;
then
A27: len F = len (s.f) by A23,FINSEQ_2:43;
A28: 1 <= k+1 by NAT_1:12;
then
A29: k+1 <= ma by A2,A4,A22,A27,FINSEQ_6:161;
then
A30: 1 <= ma by A28,XXREAL_0:2;
ma <= len F by A2,A4,A22,A27,A28,FINSEQ_6:161;
then
A31: ma in dom F by A30,FINSEQ_3:25;
A32: {cv, minpos} c= UsedILoc I22 by Th33;
minpos in {cv, minpos} by TARSKI:def 2;
then
A33: finish <> minpos by A25,A32,SCMFSA_M:25;
cv in {cv, minpos} by TARSKI:def 2;
then
A34: cv <> finish by A25,A32,SCMFSA_M:25;
A35: cv <> minpos by SCMFSA_M:26;
(Initialized SF.k).intloc 0 = 1 by SCMFSA_M:9;
then
A36: I21 is_halting_on Initialized SF.k,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0))
by Th27;
A37: F1 = F+*(k+1, F.ma)+*(ma, F.(k+1))
proof
set S2 = IExec(I21,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k);
A38: len F = |.len F.| by ABSVALUE:def 1;
SF.k.finish = len F & k+1 = |.k+1.| by A4,A19,A22,A23,A26,ABSVALUE:def 1
,FINSEQ_2:43,NAT_1:13;
then
A39: S2.minpos = ma by A2,A19,A22,A33,A35,A28,A38,Th29,NAT_1:13;
then
A40: 1 <= S2.minpos by A28,A29,XXREAL_0:2;
A41: S2.f = F by A19,A22,A33,A35,Th28,NAT_1:13;
then
A42: S2.minpos <= len (S2.f) by A2,A4,A22,A27,A28,A39,FINSEQ_6:161;
A43: S2.cv = k+1 & S2.intloc 0 = 1 by A2,A19,A22,A36,A33,A35,Th28,NAT_1:13
,SCMFSA8C:67;
thus F1 = IExec(I2B ";" AddTo(cv, intloc 0),
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k).f
by A19,A22,NAT_1:13,SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0), IExec(I2B,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k)).f
by A19,A22,NAT_1:13,SFMASTR1:12
.= IExec(I2B,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k).f
by SCMFSA_2:64
.= IExec(I22,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
IExec(I21,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
intloc 0)), SF.k)).f by A36,SFMASTR1:8
.= F+*(k+1, F.ma)+*(ma, F.(k+1)) by A2,A4,A22,A27,A28,A41,A39,A40,A42
,A43,Th31;
end;
k+1 in dom F by A2,A4,A22,A27,A28,FINSEQ_3:25;
then consider p1 being Permutation of dom F such that
A44: F1 = F*p1 by A31,A37,FUNCT_7:111;
{cv, finish, minpos} c= UsedILoc I21 & finish in {cv, finish,
minpos} by Th26,ENUMSET1:def 1;
then finish in (UsedILoc I21) \/ UsedILoc I22 by XBOOLE_0:def 3;
then finish in UsedILoc I2B by SF_MASTR:27;
then finish in {cv, intloc 0, finish} \/ UsedILoc I2B by XBOOLE_0:def 3;
hence SF.(k+1).finish = IExec(I2B ";" AddTo(cv,intloc 0),
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k).finish by A19,A22,NAT_1:13,SCMFSA_M:28
.= Exec(AddTo(cv, intloc 0), IExec(I2B,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k)).finish by A19,A22,NAT_1:13,SFMASTR1:11
.= IExec(I2B,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k).finish by A34,SCMFSA_2:64
.= IExec(I22,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
IExec(I21,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
intloc 0)), SF.k)).finish by A36,SFMASTR1:7
.= (Initialized IExec(I21,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k)).finish
by A25,A24,SCMFSA_M:25,SFMASTR2:1
.= IExec(I21,
p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B),
I2B ";" AddTo(cv,intloc 0) ";"
SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedILoc I2B), intloc 0)),
SF.k).finish by SCMFSA_M:37
.= s1.finish by A19,A22,A33,A35,Th28,NAT_1:13;
thus SF.(k+1).f is_split_at (k+1) by A2,A4,A18,A22,A27,A37,FINSEQ_6:164
,NAT_1:13;
thus SF.(k+1).f is_non_decreasing_on 1, (k+1) by A2,A4,A18,A22,A27,A37,
FINSEQ_6:163,NAT_1:13;
dom F = dom(s.f) by A27,FINSEQ_3:29;
then reconsider p1 as Permutation of dom(s.f);
reconsider ppp = pp*p1 as Permutation of dom(s.f);
take ppp;
thus thesis by A23,A44,RELAT_1:36;
end;
A45: dom(s.f) = Seg len(s.f) by FINSEQ_1:def 3;
A46: cv in {cv, minpos} by TARSKI:def 2;
finish = 1-stRWNotIn UsedILoc I22 & {cv, minpos} c= UsedILoc I22 by Th33,
SFMASTR1:def 4;
then
A47: cv <> finish by A46,SCMFSA_M:25;
A48: P[0]
proof
assume 0 <= n;
thus SF.0.cv = 0+s1.intloc 0 by Th9;
thus SF.0.finish = s1.finish by A47,Th11;
thus SF.0.f is_split_at 0;
thus SF.0.f is_non_decreasing_on 1, 0;
dom(s.f) = Seg len(s.f) by FINSEQ_1:def 3;
then reconsider p = idseq len (s.f) as Permutation of dom(s.f) by
FINSEQ_2:55;
take p;
SF.0.f = s1.f by Th13
.= (Initialized s).f by SCMFSA_2:74
.= s.f by SCMFSA_M:37;
hence thesis by FINSEQ_2:54;
end;
A49: for k being Nat holds P[k] from NAT_1:sch 2(A48, A17);
then ex p being Permutation of dom(s.f) st SF.n.f = (s.f) * p;
then len (S.f) = n by A2,A4,A15,A45,FINSEQ_2:43;
hence S.f is_non_decreasing_on 1, len (S.f) by A49,A15;
thus thesis by A49,A15;
end;