:: The { \bf for } (going up) Macro Instruction :: by Piotr Rudnicki :: :: Received June 4, 1998 :: Copyright (c) 1998-2012 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, UNIALG_2, SCMFSA6C, SCMFSA6B, FUNCT_1, XBOOLE_0, FUNCT_4, CARD_1, AMISTD_2, RELAT_1, GRAPHSP, AMI_3, PARTFUN1, COMPLEX1, SCMFSA8B, TURING_1, SCMFSA_9, ARYTM_3, FUNCOP_1, SCMFSA8A, CARD_3, SFMASTR1, ARYTM_1, XXREAL_0, SCMFSA6A, TARSKI, SCMFSA9A, FINSEQ_1, GRAPH_2, AOFA_I00, FUNCT_2, FINSEQ_2, SFMASTR3, NAT_1, PBOOLE, COMPOS_1, MEMSTR_0, EXTPRO_1; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, 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, SCMFSA8A, SCMFSA8B, SCMFSA_9, SFMASTR1, SCMFSA9A, XXREAL_0, ORDINAL1, NAT_1, SCMFSA_M; 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; registrations SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_3, SCMFSA_2, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA_9, SFMASTR1, XBOOLE_0, VALUED_0, AFINSQ_1, FUNCOP_1, COMPOS_1, EXTPRO_1, PBOOLE, FUNCT_4, MEMSTR_0, SCMFSA6A, FINSEQ_1, AMI_3, COMPOS_0, SCMFSA_M, PRE_POLY; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, SCMFSA7B, SCMFSA9A, GRAPH_2, SCMFSA6A, COMPOS_1, EXTPRO_1, MEMSTR_0, SCMFSA_M; 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, MEMSTR_0, SCMFSA6A, SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA8C, SCMFSA_9, SFMASTR1, SCMFSA9A, SFMASTR2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, AFINSQ_1, PBOOLE, EXTPRO_1, CARD_3, SCMFSA_M; 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 Program of SCM+FSA, Ig for good Program of SCM+FSA, i, k for Element of NAT, p for Instruction-Sequence of SCM+FSA; theorem Th1: I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & I does not destroy aa implies IExec(I,p,s).aa = (Initialized s).aa proof set a = aa; A1: DataPart Initialized s = DataPart(Initialize Initialized s) by MEMSTR_0:79; assume I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & I does not destroy a; hence IExec(I,p,s).a = Comput(p+*I, Initialize Initialized s,0).a by SCMFSA8C:60 .= (Initialize Initialized s).a .= (Initialized s).a by A1,SCMFSA_M:2; end; theorem Th2: 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 Th3: 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 by SCMFSA8C:49; end; theorem Th4: aa <> bb implies cc := bb does not refer aa proof assume A1: aa <> bb; now let e be Int-Location; let l be Element of 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 by A2,SCMFSA_2:24; thus aa >0_goto l <> cc := bb by A2,SCMFSA_2:25; 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 by SCMFSA7B:def 1; end; theorem Th5: :: change SCMFSA_2:98 Exec(a := (f, bb), s).a = (s.f)/.abs(s.bb) proof ex k being Element of NAT st k = abs(s.bb) & Exec(a:=(f,bb), s).a = (s.f )/.k by SCMFSA_2:72; hence thesis; end; theorem Th6: :: see SCMFSA_2:99 Exec((f, aa) := bb, s).f = s.f+*(abs(s.aa), s.bb) proof ex k being Element of NAT st k=abs(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 Program 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 Th7: UsedIntLoc if>0(aa, bb, I, J) = {aa, bb} \/ (UsedIntLoc I) \/ UsedIntLoc J proof set a = aa; thus UsedIntLoc if>0(a, bb, I, J) = UsedIntLoc (SubFrom(a,bb) ";" if>0(a,I,J )) by SCMFSA8B:def 5 .= (UsedIntLoc SubFrom(a,bb)) \/ UsedIntLoc if>0(a,I,J) by SF_MASTR:29 .= {a,bb} \/ UsedIntLoc if>0(a,I,J) by SF_MASTR:14 .= {a,bb} \/ ({a} \/ UsedIntLoc I \/ UsedIntLoc J) by SCMFSA9A:9 .= {a,bb} \/ ({a} \/ (UsedIntLoc I \/ UsedIntLoc J)) by XBOOLE_1:4 .= {a,bb} \/ {a} \/ ((UsedIntLoc I \/ UsedIntLoc J)) by XBOOLE_1:4 .= {a, bb} \/ (UsedIntLoc I \/ UsedIntLoc J) by ZFMISC_1:9 .= {a, bb} \/ UsedIntLoc I \/ UsedIntLoc J by XBOOLE_1:4; end; theorem Th8: I does not destroy aa implies while>0(bb, I) does not destroy aa proof set J= (card I +4) .--> goto 0; set F=if>0(bb, I ";" Goto 0, Stop SCM+FSA); A1: Goto 0 does not destroy aa by SCMFSA8C:57; A2: Stop SCM+FSA does not destroy aa by SCMFSA8C:56; assume I does not destroy aa; then I ";" Goto 0 does not destroy aa by A1,SCMFSA8C:52; then A3: F does not destroy aa by A2,SCMFSA8C:88; J does not destroy aa & while>0(bb,I) = F+*J by SCMFSA_9:30,def 2; hence thesis by A3,SCMFSA8A:11; end; theorem Th9: cc <> aa & I does not destroy cc & J does not destroy cc implies if>0(aa, bb, I, J) does not destroy cc proof 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 Program of SCM+FSA, s be State of SCM+FSA; func StepForUp(a, b, c, I, p,s) -> Function of NAT, product the_Values_of SCM+FSA equals StepWhile>0(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0), p, s+*(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), s.c-s.b+1)+*(a, s.b)); coherence; end; theorem Th10: s.intloc 0 = 1 implies StepForUp(a,bb,cc,I,p,s).0.intloc 0 = 1 proof set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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 Th11: StepForUp(a,bb,cc,I,p,s).0.a = s.bb proof set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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 Th12: a <> bb implies StepForUp(a,bb,cc,I,p,s).0.bb = s.bb proof set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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} \/ UsedIntLoc 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 Th13: a <> cc implies StepForUp(a,bb,cc,I,p,s).0.cc = s.cc proof set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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} \/ UsedIntLoc 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 Th14: a <> dd & dd in UsedIntLoc I implies StepForUp(a,bb,cc,I,p,s). 0.dd = s.dd proof assume that A1: a <> dd and A2: dd in UsedIntLoc I; set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I); dd in {a, bb, cc} \/ UsedIntLoc 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 Th15: StepForUp(a,bb,cc,I,p,s).0.f = s.f proof set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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 Th16: s.intloc 0 = 1 implies for aux being read-write Int-Location st aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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} \/ UsedIntLoc I); bb in {a, bb, cc} by ENUMSET1:def 1; then bb in {a, bb, cc} \/ UsedIntLoc 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} \/ UsedIntLoc 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 Program of SCM+FSA, s be State of SCM+FSA; pred ProperForUpBody a, b, c, I, s, p means :Def2: for i being Element of NAT st i < s.c-s.b+1 holds I is_closed_on StepForUp(a, b, c, I,p,s).i, p +* while>0(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0)) & I is_halting_on StepForUp(a, b, c, I,p,s).i, p +* while>0(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0)); end; theorem Th17: for I being parahalting Program of SCM+FSA holds ProperForUpBody aa, bb, cc, I, s, p proof let I be parahalting Program of SCM+FSA; let i be Element of NAT such that i < s.cc-s.bb+1; thus I is_closed_on StepForUp(aa,bb,cc,I,p,s).i, p +* while>0(1-stRWNotIn ({aa, bb, cc} \/ UsedIntLoc I), I ";" AddTo(aa, intloc 0) ";" SubFrom(1-stRWNotIn ({aa, bb, cc} \/ UsedIntLoc I), intloc 0)) by SCMFSA7B:18; thus thesis by SCMFSA7B:19; end; theorem Th18: StepForUp(a,bb,cc,Ig,p,s).k.intloc 0 = 1 & Ig is_closed_on StepForUp(a,bb,cc,Ig,p,s).k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), Ig ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), intloc 0)) & Ig is_halting_on StepForUp(a,bb,cc,Ig,p,s).k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), Ig ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), intloc 0)) implies StepForUp(a,bb,cc,Ig,p,s).(k+1).intloc 0 = 1 proof set I = Ig; assume that A1: StepForUp(a,bb,cc,I,p,s).k.intloc 0 = 1 and A2: I is_closed_on StepForUp(a,bb,cc,I,p,s).k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) & I is_halting_on StepForUp(a,bb,cc,I,p,s).k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)); set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I); set IB = I ";" AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0); 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_closed_on Initialized SW2.k,p+*while>0(aux,IB) & I is_halting_on Initialized SW2.k,p+*while>0(aux,IB) by A1,A2,SFMASTR2:5; A6: AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0) is_closed_on IExec(I,p+*while>0(aux,IB),SW2.k),p+*while>0(aux,IB) by SCMFSA7B:18; then 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) & IB is_closed_on Initialized SW2.k,p+*while>0(aux,IB) by A3,A5,SCMFSA7B:19,SFMASTR1:2; then A7: DataPart SW2.(k+1) = DataPart IExec(IB,p+*while>0(aux,IB),SW2.k) by A1,A3,A4,A5,A6,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 A7,SCMFSA_M:2; end; end; theorem Th19: 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} \/ UsedIntLoc Ig)) + k = s.cc-s.bb+1 proof 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} \/ UsedIntLoc 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} \/ UsedIntLoc 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 UsedIntLoc I proof assume not thesis; then aux in {a, bb, cc} \/ UsedIntLoc 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; then A12: I is_closed_on SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A2,Def2; then A13: I is_closed_on Initialized SW2.k, p+*while>0(aux,IB) by A6,A8,A9,SFMASTR2:4,XXREAL_0:2; A14: I is_halting_on SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A2,A11,Def2; then A15: I is_halting_on Initialized SW2.k, p+*while>0(aux,IB) by A6,A8,A9,A12,SFMASTR2:5,XXREAL_0:2; thus SF.k1.intloc 0 = 1 by A6,A8,A9,A12,A14,Th18,XXREAL_0:2; A16: AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0) is_closed_on IExec(I,p+*while>0(aux,IB),SW2.k), p+*while>0(aux,IB) by SCMFSA7B:18; then A17: IB is_closed_on Initialized SW2.k, p+*while>0(aux,IB) by A3,A13,A15,SFMASTR1: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,A15,A16,SFMASTR1:3; then A18: DataPart SW2.(k+1) = DataPart IExec(IB,p+*while>0(aux,IB),SW2.k) by A6,A8,A9,A10,A17,SCMFSA9A:32,XXREAL_0:2; hereby assume A19: I does not destroy a; A20: 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,A15,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,A19,Th1 .= SW2.k.a +1 by SCMFSA_M:37; hence SF.k1.a = k1+s.bb by A6,A8,A9,A18,A19,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,A18,A19,A20,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,A15,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,A15,A7,Th1,SFMASTR1:1 .= SW2.k.aux -1 by SCMFSA_M:37; hence SF.k1.aux + k1 = SW2.k.aux-1+k1 by A18,SCMFSA_M:2 .= scb1 by A6,A8,A9,XXREAL_0:2; end; end; A21: a in dom (s+*(aux, s.cc-s.bb+1)) by SCMFSA_2:42; A22: aux in dom s by SCMFSA_2:42; A23: P[0] proof assume A24: 0 <= scb1; A25: 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 A21,A25,FUNCT_7:31; 0+s.bb <= s.cc+1-s.bb+s.bb by A24,XREAL_1:6; hence SF.0.a <= s.cc+1 by A21,A25,FUNCT_7:31; end; thus SF.0.aux + 0 = (s+*(aux, s.cc-s.bb+1)).aux by A4,A25,FUNCT_7:32 .= scb1 by A22,FUNCT_7:31; end; thus for k holds P[k] from NAT_1:sch 1(A23, A5); end; theorem Th20: 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} \/ UsedIntLoc Ig)) > 0 iff k < s.cc-s.bb+1 proof set I = Ig; set SF = StepForUp(a,bb,cc,I,p,s); set aux = (1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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,Th19; end; let k; a in {a, bb, cc} by ENUMSET1:def 1; then a in {a, bb, cc} \/ UsedIntLoc 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 1(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,Th19; hence thesis by A13; end; theorem Th21: 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} \/ UsedIntLoc Ig \/ FinSeq-Locations) = IExec(Ig ";" AddTo(a, intloc 0), p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), Ig ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), intloc 0)), StepForUp(a, bb, cc, Ig, p, s).k) | ({a, bb, cc} \/ UsedIntLoc Ig \/ FinSeq-Locations) proof 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} \/ UsedIntLoc 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); SF = SW2; then A4: SW2.k.intloc 0 = 1 by A1,A2,A3,Th19; set scb1 = s.cc-s.bb+1; A5: SF.k.aux+k = scb1 by A1,A2,A3,Th19; 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} \/ UsedIntLoc I; set S1 = IExec(IB1,p+*while>0(aux,IB), SW2.k); A7: Macro AddTo(a, intloc 0) is_closed_on IExec(I,p+*while>0(aux,IB),SW2.k),p+*while>0(aux,IB) by SCMFSA7B:18; A8: I is_closed_on SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A2,A3,Def2; then A9: I is_closed_on Initialized SW2.k,p+*while>0(aux,IB) by A4,SFMASTR2:4; I is_halting_on SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A2,A3,Def2; then A10: I is_halting_on Initialized SW2.k,p+*while>0(aux,IB) by A8,A4,SFMASTR2:5; 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 A11: IB1 is_halting_on Initialized SW2.k,p+*while>0(aux,IB) by A9,A10,A7,SFMASTR1:3; now hereby let x be Int-Location; assume x in Iloc; then A12: x <> aux by SCMFSA_M:25; S2.x = Exec(SubFrom(aux, intloc 0), S1).x by A9,A10,A7,A11,SFMASTR1:2,11 .= S1.x by A12,SCMFSA_2:65; hence S1.x = S2.x; end; let x be FinSeq-Location; S2.x = Exec(SubFrom(aux, intloc 0), S1).x by A9,A10,A7,A11,SFMASTR1:2,12 .= S1.x by SCMFSA_2:65; hence S1.x = S2.x; end; then A13: S1 | (Iloc \/ FL) = IExec(IB,p+*while>0(aux,IB),SW2.k) | (Iloc \/ FL) by SCMFSA_M:28; A14: IB = I ";"(AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0)) & AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0) is_closed_on IExec(I,p+*while>0(aux,IB),SW2.k),p+*while>0(aux,IB) by SCMFSA6A:28,SCMFSA7B:18; then 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) & IB is_closed_on Initialized SW2.k,p+*while>0(aux,IB) by A9,A10,SCMFSA7B:19,SFMASTR1:2; then DataPart SW2.(k+1) = DataPart IExec(IB,p+*while>0(aux,IB),SW2.k) by A4,A6,A9,A10,A14,SCMFSA9A:32,SFMASTR1:3; hence thesis by A13,RELAT_1:153,SCMFSA_2:100,XBOOLE_1:9; end; definition let a, b, c be Int-Location, I be Program of SCM+FSA; func for-up(a, b, c, I) -> Program of SCM+FSA equals (1-stRWNotIn ({a, b, c} \/ UsedIntLoc I)) := c ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), b) ";" AddTo(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0) ";" (a := b) ";" while>0( 1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0) ); coherence; end; theorem Th22: {aa, bb, cc} \/ UsedIntLoc I c= UsedIntLoc for-up(aa, bb, cc, I) proof set aux = 1-stRWNotIn ({aa, bb, cc} \/ UsedIntLoc 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: UsedIntLoc (i0 ";" i1 ";" i2 ";" i3) = UsedIntLoc (i0 ";" i1 ";" i2) \/ UsedIntLoc i3 by SF_MASTR:30 .= UsedIntLoc (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 set; A2: UsedIntLoc I4 = {aux} \/ UsedIntLoc (I ";" AddTo(aa, intloc 0) ";" SubFrom(aux, intloc 0)) by SCMFSA9A:24 .= {aux} \/ (UsedIntLoc (I ";" AddTo(aa, intloc 0)) \/ UsedIntLoc SubFrom(aux, intloc 0)) by SF_MASTR:30 .= {aux} \/ (((UsedIntLoc I) \/ UsedIntLoc AddTo(aa, intloc 0)) \/ UsedIntLoc SubFrom(aux, intloc 0)) by SF_MASTR:30 .= {aux} \/ ((UsedIntLoc I) \/ ((UsedIntLoc AddTo(aa, intloc 0)) \/ UsedIntLoc SubFrom(aux, intloc 0))) by XBOOLE_1:4 .= (UsedIntLoc I) \/ ({aux} \/ (UsedIntLoc AddTo(aa, intloc 0) \/ UsedIntLoc SubFrom(aux, intloc 0))) by XBOOLE_1:4; assume x in {aa, bb, cc} \/ UsedIntLoc I; then A3: x in {aa, bb, cc} or x in UsedIntLoc I by XBOOLE_0:def 3; A4: UsedIntLoc for-up(aa, bb, cc, I) = (UsedIntLoc (i0 ";" i1 ";" i2 ";" i3) ) \/ UsedIntLoc 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 UsedIntLoc (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 UsedIntLoc (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 UsedIntLoc I; then x in UsedIntLoc 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 Program of SCM+FSA; cluster for-up(a, b, c, I) -> good; coherence; end; theorem Th23: a <> aa & aa <> 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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} \/ UsedIntLoc I) and A3: I does not destroy aa; set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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 Th8; hence thesis by A5,SCMFSA8C:52; end; theorem Th24: s.intloc 0 = 1 & s.bb > s.cc implies (for x st x <> a & x in {bb , cc} \/ UsedIntLoc 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 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} \/ UsedIntLoc 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} \/ UsedIntLoc 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} \/ UsedIntLoc 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 & I4 is_closed_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,Th16; hereby let x be Int-Location such that A12: x <> a and A13: x in {bb, cc} \/ UsedIntLoc I; x in {a, bb, cc} \/ UsedIntLoc 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 UsedIntLoc 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 Program 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,Th17; set scb1 = s.cc-s.bb+1; set SF = StepForUp(a,bb,cc,I,p,s); set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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: SF = SW2; A5: IB = I ";" (AddTo(a, intloc 0) ";" SubFrom(aux, intloc 0)) by SCMFSA6A:28; A6: ProperBodyWhile>0 aux, IB, s2, p2 proof let k be Element of NAT; A7: IB2 is_closed_on IExec(I, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) , SF.k), p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by SCMFSA7B:18; assume StepWhile>0(aux,IB,p2,s2).k.aux > 0; then A8: k < scb1 by A1,A3,A4,Th20; then A9: I is_closed_on SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A3,Def2; A10: SF.k.intloc 0 = 1 by A1,A3,A8,Th19; I is_halting_on SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A3,A8,Def2; then A11: I is_halting_on Initialized SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A10,A9,SFMASTR2:5; A12: I is_closed_on Initialized SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A10,A9,SFMASTR2:4; then A13: IB is_closed_on Initialized SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A5,A11,A7,SFMASTR1:2; hence IB is_closed_on SW2.k, p2+*while>0(aux,IB) by A10,SFMASTR2:4; IB2 is_halting_on IExec(I, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) , SF.k), p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by SCMFSA7B:19; then IB is_halting_on Initialized SF.k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I), intloc 0)) by A5,A12,A11,A7,SFMASTR1:3; hence thesis by A10,A13,SFMASTR2:5; 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) = abs($1.aux); consider f being Function of product the_Values_of SCM+FSA,NAT such that A14: for x being Element of product the_Values_of SCM+FSA holds f.x = U(x) from FUNCT_2:sch 4; A15: 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 A14; hence thesis; end; A16: DataPart s1 = DataPart s2 by A1,Th16; thus ProperBodyWhile>0 aux, IB, s1,p1 proof let k be Element of NAT; assume A17: StepWhile>0(aux,IB,p1,s1).k.aux > 0; A18: DataPart SW2.k = DataPart SW1.k by A16,A6,SCMFSA9A:34; then A19: SW1.k.aux = SW2.k.aux by SCMFSA_M:2; then A20: IB is_closed_on SW2.k, p2+*while>0(aux,IB) by A6,A17,SCMFSA9A:def 4; hence IB is_closed_on SW1.k, p2+*while>0(aux,IB) by A18,SCMFSA8B:3; IB is_halting_on SW2.k, p2+*while>0(aux,IB) by A6,A17,A19,SCMFSA9A:def 4; hence thesis by A18,A20,SCMFSA8B:5; end; A21: for k being Element of NAT holds ( f.(SW1.(k+1)) < f.(SW1.k) or SW1.k. aux <= 0 ) proof let k be Element of NAT; A22: DataPart SW1.k = DataPart SW2.k by A16,A6,SCMFSA9A:34; then A23: SW1.k.aux = SW2.k.aux by SCMFSA_M:2; DataPart SW2.(k+1) = DataPart SW1.(k+1) by A16,A6,SCMFSA9A:34; then A24: SW1.(k+1).aux = SW2.(k+1).aux by SCMFSA_M:2; now assume A25: SW1.k.aux > 0; then A26: k < scb1 by A1,A3,A4,A23,Th20; k < scb1 by A1,A3,A4,A23,A25,Th20; then A27: SW2.k.aux+k = s.cc-s.bb+1 by A1,A3,A4,Th19; reconsider scb1 as Element of NAT by A26,INT_1:3; A28: k+1 <= scb1 by A26,NAT_1:13; then A29: SW2.(k+1).aux+(k+1) = s.cc-s.bb+1 by A1,A3,A4,Th19; A30: f.(SW1.k) = abs( SW1.k.aux ) by A15 .= SW2.k.aux by A23,A25,ABSVALUE:def 1; per cases; suppose A31: SW1.(k+1).aux > 0; f.(SW1.(k+1)) = abs( SW1.(k+1).aux ) by A15 .= scb1-k-1 by A24,A29,A31,ABSVALUE:def 1; hence f.(SW1.(k+1)) < f.(SW1.k) by A30,A27,XREAL_1:146; end; suppose A32: SW1.(k+1).aux <= 0; SW2.(k+1).aux = scb1 - (k+1) by A29; then A33: SW1.(k+1).aux = 0 by A24,A28,A32,XREAL_1:48; f.(SW1.(k+1)) = abs( SW1.(k+1).aux ) by A15 .= 0 by A33,ABSVALUE:def 1; hence f.(SW1.(k+1)) < f.(SW1.k) by A22,A25,A30,SCMFSA_M:2; end; end; hence thesis; end; thus WithVariantWhile>0 aux, IB, s1, p1 proof take f; thus thesis by A21; end; end; theorem Th25: 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 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,Th17; set i3 = a := bb; set aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc 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 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,Th16; 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 Element of 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 Element of 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,Th19; end; SF.k.aux+k = scb1 by A1,A2,A4,Th19; 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 & I4 is_closed_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 Th26: s.intloc 0 = 1 & (ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting) implies for-up(a, bb, cc, Ig) is_closed_on s,p & for-up(a, bb, cc, Ig) is_halting_on s,p proof 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} \/ UsedIntLoc 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 ; then A4: I4 is_closed_on s1,p1 by SCMFSA9A:27; reconsider I03 as parahalting Program of SCM+FSA; set MI = for-up(a, bb, cc, I); A5: I03 is_closed_on Initialized s,p & I03 is_halting_on Initialized s,p by SCMFSA7B:18,19; then A6: MI is_closed_on Initialized s,p by A4,SFMASTR1:2; hence MI is_closed_on s,p by A1,SFMASTR2:4; I4 is_halting_on s1,p1 by A3,SCMFSA9A:27; then MI is_halting_on Initialized s,p by A5,A4,SFMASTR1:3; hence thesis by A1,A6,SFMASTR2:5; 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) -> Program 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; coherence; end; theorem Th27: 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); 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: 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,Th9; 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} \/ UsedIntLoc I1B by XBOOLE_0:def 3; then A8: a <> 1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B) by SCMFSA_M:25; cv <> a by A2,SCMFSA_M:25; then I1 does not destroy a by A7,A8,Th23; hence thesis by A6,SCMFSA7B:6,SCMFSA8C:53; end; theorem Th28: {aa, bb, c} c= UsedIntLoc 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: UsedIntLoc (i0 ";" I1) = (UsedIntLoc i0) \/ UsedIntLoc I1 by SF_MASTR:29; A2: {cv, a, b} \/ UsedIntLoc I1B c= UsedIntLoc I1 by Th22; let x be set; 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} \/ UsedIntLoc 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 Th29: s.intloc 0 = 1 implies FinSeqMin(f, aa, bb, c) is_closed_on s,p & 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 = s1.intloc 0 .= (Exec(i0, Initialized s)).intloc 0 by SCMFSA6C:5 .= Exec(i0, Initialized s).intloc 0 .= (Initialized s). intloc 0 by SCMFSA_2:63 .= 1 by SCMFSA_M:9; then A3: I1 is_closed_on s1,p1 by Th26; A4: Macro i0 is_closed_on Initialized s,p & Macro i0 is_halting_on Initialized s,p by SCMFSA7B:18,19; then A5: FinSeqMin(f, aa, bb, c) is_closed_on Initialized s,p by A3,SFMASTR1:2; hence FinSeqMin(f, aa, bb, c) is_closed_on s,p by A1,SFMASTR2:4; I1 is_halting_on s1,p1 by A2,Th26; then FinSeqMin(f, aa, bb, c) is_halting_on Initialized s,p by A3,A4,SFMASTR1:3; hence thesis by A1,A5,SFMASTR2:5; end; theorem Th30: 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} \/ UsedIntLoc 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} \/ UsedIntLoc 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} \/ UsedIntLoc 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_closed_on s1,p1 & I1 is_halting_on s1,p1 by Th26; 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,Th24; a in {a, b} by TARSKI:def 2; then A26: a in {a, b} \/ UsedIntLoc 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,Th24; b in {a, b} by TARSKI:def 2; then A27: b in {a, b} \/ UsedIntLoc 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,Th24; 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 Th17; A31: for n being Element of NAT st P[n] holds P[n+1] proof let n be Element of 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,Th10; thus SF.n.cv = n+s1.a by A35,Th11; thus thesis by A14,A6,A28,A35,Th11; 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} \/ UsedIntLoc I1B) \/ FinSeq-Locations) = IExec(I1B ";" AddTo(cv, intloc 0), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) | (({cv, a, b} \/ UsedIntLoc I1B) \/ FinSeq-Locations) by A23,A14,A6,A30,Th21; then A38: SF.(n+1).f = IExec(I1B ";" AddTo(cv, intloc 0), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).f by SFMASTR1:12 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).f by SCMFSA_2:64 .= IExec(I12, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).b by SFMASTR1:11 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).b by A11,SCMFSA_2:64 .= IExec(I12, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).a by SFMASTR1:11 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).a by A17,SCMFSA_2:64 .= IExec(I12, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv by SFMASTR1:11 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).cv+IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).intloc 0 by SCMFSA_2:64 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).cv+1 by SCMFSA6B:11 .= IExec(I12, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv+1 by SFMASTR1:7; set ss = IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)) = DataPart IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) by Th2; A45: IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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,Th3,Th4,SCMFSA8C:51; per cases; suppose A49: 0 = n; thus thesis proof thus SF.(n+1).intloc 0 = 1 by A23,A14,A6,A30,A33,Th19; A50: S0.f = SF.0.f by A49,SCMFSA_M:37 .= s.f by A20,Th15; A51: S0.cv = SF.0.cv by A49,SCMFSA_M:37 .= s.a by A14,Th11; A52: S0.b = SF.0.b by A5,A34,A49,SCMFSA_M:9,37 .= s1.b by A11,Th13; A53: S0.a = SF.0.a by A4,A34,A49,SCMFSA_M:9,37 .= s1.a by A17,Th12; 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF. n)).cv = ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF. n))).cv .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n))).cv by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv by A22,SCMFSA_2:63; thus SF.(n+1).cv = IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF. n)).cv+1 by A7,A48,A41,A55,SCMFSA8B:40 .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv+1 by A56 .= (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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) ).f by A48,A38,A55,SCMFSA8B:40 .= ( IExec(Macro(c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) )).f .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n))).f by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).f .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n )).a by A19,A48,A40,A55,SCMFSA8B:40 .= ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n ))).a .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n))).a by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).a .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n )).b by A13,A48,A39,A55,SCMFSA8B:40 .= ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n ))).b .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) )).b by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).b .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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,Th19; 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)) .cv+1 by A7,A48,A41,SCMFSA8B:40 .= IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF. n)).cv = ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF. n))).cv .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n))).cv by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv by A22,SCMFSA_2:63 .= IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF. n)).cv+1 by A7,A48,A41,A63,SCMFSA8B:40 .= IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).cv+1 by A64 .= (n+1)+s1.a by A34,A47,A58; thus SF.(n+1).f = IExec(Macro(c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) ).f by A48,A38,A63,SCMFSA8B:40 .= ( IExec(Macro(c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) )).f .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n))).f by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).f .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n )).a by A19,A48,A40,A63,SCMFSA8B:40 .= ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n ))).a .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) )).a by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) ).a .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n )).b by A13,A48,A39,A63,SCMFSA8B:40 .= ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n ))).b .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) )).b by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).b .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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 Element of NAT holds P[n] from NAT_1:sch 1(A65, A31); A67: DataPart IExec(I1,p1,s1) = DataPart SF.k by A23,A14,A6,Th25; 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 Th31: 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, abs(s.aa), abs(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 = abs(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} \/ (UsedIntLoc I1B) by XBOOLE_0:def 3; A17: ProperForUpBody cv, a, b, I1B, s1, p1 by Th17; 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,Th25; c in {c, cv} by TARSKI:def 2; then c in UsedIntLoc (c := cv) by SF_MASTR:14; then c in UsedIntLoc Macro (c := cv) by SF_MASTR:28; then c in {aux2, aux1} \/ (UsedIntLoc Macro (c := cv)) by XBOOLE_0:def 3; then c in {aux2, aux1} \/ (UsedIntLoc Macro (c := cv)) \/ UsedIntLoc Stop SCM+FSA by XBOOLE_0:def 3; then c in UsedIntLoc I12 by Th7; then c in (UsedIntLoc (i10 ";" i11)) \/ UsedIntLoc I12 by XBOOLE_0:def 3; then A27: c in UsedIntLoc I1B by SF_MASTR:27; then A28: c in {cv, a, b} \/ (UsedIntLoc I1B) by XBOOLE_0:def 3; A29: for n being Element of NAT st P[n] holds P[n+1] proof let n be Element of 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,Th10; thus SF.n.cv = n+s1.a by A33,Th11; thus thesis by A2,A21,A24,A33,Th11; 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)) = DataPart IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) by Th2; n < n+1 by XREAL_1:29; then n < k by A31,XXREAL_0:2; then A37: SF.(n+1) | ({cv, a, b} \/ (UsedIntLoc I1B) \/ FinSeq-Locations) = IExec(I1B ";" AddTo(cv, intloc 0), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) | ({cv, a, b} \/ (UsedIntLoc I1B) \/ FinSeq-Locations) by A25,A21,A24,A17,Th21; then A38: SF.(n+1).f = IExec(I1B ";" AddTo(cv, intloc 0), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).f by SFMASTR1:12 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).f by SCMFSA_2:64 .= IExec(I12, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).c by SFMASTR1:11 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).c by A15,SCMFSA_2:64 .= IExec(I12, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv by SFMASTR1:11 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).cv+IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).intloc 0 by SCMFSA_2:64 .= IExec(I1B, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).cv+1 by SCMFSA6B:11 .= IExec(I12, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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,Th3,Th4,SCMFSA8C:51; A42: IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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,Th14; 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,Th19; A47: S0.f = SF.0.f by A44,SCMFSA_M:37 .= s.f by A10,Th15; 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,Th11; 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).aux1 = S2.aux1 by SCMFSA6C:8 .= S1.aux1 by A11,SCMFSA_2:72 .= (S0.f)/.abs(S0.cv) by Th5 .= s.f.S0cv by A9,A23,A47,A49,PARTFUN1:def 6; A51: IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).aux2 = S2.aux2 by SCMFSA6C:8 .= (S1.f)/.abs(S1.c) by Th5 .= 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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,GRAPH_2:60; 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).aux1 = S2.aux1 by SCMFSA6C:8 .= S1.aux1 by A11,SCMFSA_2:72 .= (S0.f)/.abs(S0.cv) by Th5 .= (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,Th19; consider sa1 being Element of 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; 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,GRAPH_2:59; then A63: 1 <= SFnc by A1,A9,XXREAL_0:2; A64: SFnc <= sa1 by A1,A9,A59,A60,A61,A58,GRAPH_2:59; 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n).aux2 = S2.aux2 by SCMFSA6C:8 .= (S1.f)/.abs(S1.c) by Th5 .= (S1.f)/.abs(S0.c) by A18,SCMFSA_2:72 .= (S1.f)/.abs(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,GRAPH_2:59; 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) ).cv = ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) )).cv .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n))).cv by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv by A15,SCMFSA_2:63; thus SF.(n+1).cv = IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) ).cv+1 by A12,A41,A40,A57,A66,A71,SCMFSA8B:40 .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).cv+1 by A72 .= IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)) .f by A41,A38,A57,A66,A71,SCMFSA8B:40 .= ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)) ).f .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n))).f by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).f .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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, GRAPH_2:59; 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, GRAPH_2:59; hence thesis by A71,XXREAL_0:2; end; SF.(n+1).c = IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)) .c by A19,A41,A39,A57,A66,A71,SCMFSA8B:40 .= ( IExec(Macro (c := cv), p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)) ).c .= ( Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n) )).c by SCMFSA6C:5 .= Exec(c := cv, Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), SF.n)).c .= (Initialized IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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,GRAPH_2:59; 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,GRAPH_2:59; 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), intloc 0)), IExec(i10 ";" i11, p1 +* while>0(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc I1B), I1B ";" AddTo(cv, intloc 0) ";" SubFrom(1-stRWNotIn ({cv, a, b} \/ UsedIntLoc 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,GRAPH_2:59; end; end; end; end; end; end; reconsider sb = abs(s.b) as Element of NAT; A84: P[0]; for n being Element of NAT holds P[n] from NAT_1:sch 1(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_closed_on s1,p1 & I1 is_halting_on s1,p1 by A25,Th26; hence IExec(FinSeqMin(f, a, b, c),p, s).c = IExec(I1,p1,s1).c by SFMASTR1:14 .= min_at(s.f, abs(s.a), abs(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) -> Program 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 Th32: 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 Th33: 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 = abs(s0.a), s2a = abs(s2.a); A7: a = intloc 0 or a is read-write by SCMFSA_M:def 2; A8: sa = abs(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 = abs(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 Th5 .= 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 Th6; 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 = abs(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 Th5 .= 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,Th6; 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,Th33; 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 Th35: {aa, bb} c= UsedIntLoc 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: UsedIntLoc swap(f, a, b) = UsedIntLoc (i0 ";" i1 ";" i2) \/ UsedIntLoc i3 by SF_MASTR:30 .= UsedIntLoc (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 set; 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 UsedInt*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 UsedInt*Loc swap(f, a, b) = UsedInt*Loc (aux1 := (f,a) ";" (aux2 := (f, b)) ";" ((f,a) := aux2)) \/ UsedInt*Loc ((f,b) := aux1) by SF_MASTR:46 .= UsedInt*Loc (aux1 := (f,a) ";" (aux2 := (f,b)) ";" ((f,a) := aux2)) \/ {f} by SF_MASTR:33 .= UsedInt*Loc (aux1 := (f,a) ";" (aux2 := (f,b))) \/ (UsedInt*Loc ((f,a ) := aux2)) \/ {f} by SF_MASTR:46 .= UsedInt*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 Th32; 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[Element of 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_closed_on SF.$1, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) & I2B is_halting_on SF.$1, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)); A5: for k being Element of NAT st Q[k] holds Q[k+1] proof let k be Element of NAT such that A6: Q[k]; assume k+1 < n; hence A7: SF.(k+1).intloc 0 = 1 by A6,Th18,NAT_1:13; (Initialized SF.(k+1)).intloc 0 = 1 by SCMFSA_M:9; then A8: I21 is_closed_on Initialized SF.(k+1), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) & I21 is_halting_on Initialized SF.(k+1), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by Th29; A9: I22 is_closed_on IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.(k+1)), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by SCMFSA7B:18; then A10: I2B is_closed_on Initialized SF.(k+1), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A8,SFMASTR1:2; hence I2B is_closed_on SF.(k+1), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A7,SFMASTR2:4; I22 is_halting_on IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.(k+1)), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by SCMFSA7B:19; then I2B is_halting_on Initialized SF.(k+1), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A8,A9,SFMASTR1:3; hence thesis by A7,A10,SFMASTR2:5; end; A11: Q[0] proof (Initialized SF.0).intloc 0 = 1 by SCMFSA_M:9; then A12: I21 is_closed_on Initialized SF.0, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) & I21 is_halting_on Initialized SF.0, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by Th29; assume 0 < n; thus A13: SF.0.intloc 0 = 1 by A2,Th10; A14: I22 is_closed_on IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.0), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by SCMFSA7B:18; then A15: I2B is_closed_on Initialized SF.0, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A12,SFMASTR1:2; hence I2B is_closed_on SF.0, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A13,SFMASTR2:4; I22 is_halting_on IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.0), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by SCMFSA7B:19; then I2B is_halting_on Initialized SF.0, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A12,A14,SFMASTR1:3; hence thesis by A13,A15,SFMASTR2:5; end; A16: for k being Element of NAT holds Q[k] from NAT_1:sch 1(A11, A5); A17: ProperForUpBody cv, intloc 0, finish, I2B, s1, p1 proof let i be Element of NAT; thus thesis by A16; end; then A18: DataPart IExec(I2,p1,s1) = DataPart SF.n by A2,Th25; I2 is_halting_on s1,p1 & I2 is_closed_on s1,p1 by A2,A17,Th26; then A19: S.f = IExec(I2,p1,s1).f by A1,SFMASTR1:15 .= SF.n.f by A18,SCMFSA_M:2; FinSeqMin(f, cv, finish, minpos) does not destroy cv by Th27,SCMFSA_M:26; then A20: I2B does not destroy cv by A3,SCMFSA8C:52; A21: for k being Element of NAT st P[k] holds P[k+1] proof let k be Element of NAT such that A22: P[k]; A23: now assume A24: k < n; hence A25: SF.k.intloc 0 = 1 by A16; A26: I2B is_closed_on SF.k, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A16,A24; hence I2B is_closed_on Initialized SF.k, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A25,SFMASTR2:4; I2B is_halting_on SF.k, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A16,A24; hence I2B is_halting_on Initialized SF.k, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by A25,A26,SFMASTR2:5; thus SF.k.cv = k+s1.intloc 0 by A22,A24; thus SF.k.finish = s1.finish by A22,A24; thus SF.k.cv <= s1.finish by A2,A22,A24,NAT_1:13; thus SF.(k+1) | ({cv, intloc 0, finish} \/ (UsedIntLoc I2B) \/ FinSeq-Locations) = IExec(I2B ";" AddTo(cv,intloc 0), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k) | ({cv, intloc 0, finish} \/ (UsedIntLoc I2B) \/ FinSeq-Locations) by A2,A17,A24,Th21; end; set F = SF.k.f, F1 = SF.(k+1).f; assume A27: k+1 <= n; then consider pp being Permutation of dom(s.f) such that A28: F = (s.f) * pp by A22,NAT_1:13; thus SF.(k+1).cv = (k+1)+s1.intloc 0 by A20,A2,A17,A27,Th19; A29: I22 is_closed_on Initialized IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) & I22 is_halting_on Initialized IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by SCMFSA7B:18,19; A30: finish = 1-stRWNotIn UsedIntLoc I22 by SFMASTR1:def 4; set ma = min_at(F, k+1, len F); A31: dom(s.f) = Seg len(s.f) by FINSEQ_1:def 3; then A32: len F = len (s.f) by A28,FINSEQ_2:43; A33: 1 <= k+1 by NAT_1:12; then A34: k+1 <= ma by A2,A4,A27,A32,GRAPH_2:59; then A35: 1 <= ma by A33,XXREAL_0:2; ma <= len F by A2,A4,A27,A32,A33,GRAPH_2:59; then A36: ma in dom F by A35,FINSEQ_3:25; A37: {cv, minpos} c= UsedIntLoc I22 by Th35; minpos in {cv, minpos} by TARSKI:def 2; then A38: finish <> minpos by A30,A37,SCMFSA_M:25; cv in {cv, minpos} by TARSKI:def 2; then A39: cv <> finish by A30,A37,SCMFSA_M:25; A40: cv <> minpos by SCMFSA_M:26; (Initialized SF.k).intloc 0 = 1 by SCMFSA_M:9; then A41: I21 is_closed_on Initialized SF.k, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) & I21 is_halting_on Initialized SF.k, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)) by Th29; A42: F1 = F+*(k+1, F.ma)+*(ma, F.(k+1)) proof set S2 = IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k); A43: len F = abs(len F) by ABSVALUE:def 1; SF.k.finish = len F & k+1 = abs(k+1) by A4,A23,A27,A28,A31,ABSVALUE:def 1 ,FINSEQ_2:43,NAT_1:13; then A44: S2.minpos = ma by A2,A23,A27,A38,A40,A33,A43,Th31,NAT_1:13; then A45: 1 <= S2.minpos by A33,A34,XXREAL_0:2; A46: S2.f = F by A23,A27,A38,A40,Th30,NAT_1:13; then A47: S2.minpos <= len (S2.f) by A2,A4,A27,A32,A33,A44,GRAPH_2:59; A48: S2.cv = k+1 & S2.intloc 0 = 1 by A2,A23,A27,A41,A38,A40,Th30,NAT_1:13 ,SCMFSA8C:67; thus F1 = IExec(I2B ";" AddTo(cv, intloc 0), p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k).f by A23,A27,NAT_1:13,SCMFSA_M:28 .= Exec(AddTo(cv, intloc 0), IExec(I2B, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k)).f by A23,A27,NAT_1:13,SFMASTR1:12 .= IExec(I2B, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k).f by SCMFSA_2:64 .= IExec(I22, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k)).f by A41,SFMASTR1:8 .= F+*(k+1, F.ma)+*(ma, F.(k+1)) by A2,A4,A27,A32,A33,A46,A44,A45,A47 ,A48,Th33; end; k+1 in dom F by A2,A4,A27,A32,A33,FINSEQ_3:25; then consider p1 being Permutation of dom F such that A49: F1 = F*p1 by A36,A42,FUNCT_7:111; {cv, finish, minpos} c= UsedIntLoc I21 & finish in {cv, finish, minpos} by Th28,ENUMSET1:def 1; then finish in (UsedIntLoc I21) \/ UsedIntLoc I22 by XBOOLE_0:def 3; then finish in UsedIntLoc I2B by SF_MASTR:27; then finish in {cv, intloc 0, finish} \/ UsedIntLoc 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} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k).finish by A23,A27,NAT_1:13,SCMFSA_M:28 .= Exec(AddTo(cv, intloc 0), IExec(I2B, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k)).finish by A23,A27,NAT_1:13,SFMASTR1:11 .= IExec(I2B, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k).finish by A39,SCMFSA_2:64 .= IExec(I22, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k)).finish by A41,SFMASTR1:7 .= (Initialized IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k)).finish by A30,A29,SCMFSA_M:25,SFMASTR2:1 .= IExec(I21, p +* while>0(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), I2B ";" AddTo(cv,intloc 0) ";" SubFrom(1-stRWNotIn ({cv,intloc 0,finish} \/ UsedIntLoc I2B), intloc 0)), SF.k).finish by SCMFSA_M:37 .= s1.finish by A23,A27,A38,A40,Th30,NAT_1:13; thus SF.(k+1).f is_split_at (k+1) by A2,A4,A22,A27,A32,A42,GRAPH_2:62 ,NAT_1:13; thus SF.(k+1).f is_non_decreasing_on 1, (k+1) by A2,A4,A22,A27,A32,A42, GRAPH_2:61,NAT_1:13; dom F = dom(s.f) by A32,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 A28,A49,RELAT_1:36; end; A50: dom(s.f) = Seg len(s.f) by FINSEQ_1:def 3; A51: cv in {cv, minpos} by TARSKI:def 2; finish = 1-stRWNotIn UsedIntLoc I22 & {cv, minpos} c= UsedIntLoc I22 by Th35, SFMASTR1:def 4; then A52: cv <> finish by A51,SCMFSA_M:25; A53: P[0] proof assume 0 <= n; thus SF.0.cv = 0+s1.intloc 0 by Th11; thus SF.0.finish = s1.finish by A52,Th13; thus SF.0.f is_split_at 0 proof let i, j be Element of NAT; assume that A54: 1 <= i & i <= 0 and 0 < j and j <= len (SF.0.f); thus thesis by A54; end; thus SF.0.f is_non_decreasing_on 1, 0 proof let i, j be Element of NAT; assume that 1 <= i and A55: i <= j & j <= 0; thus thesis by A55; end; 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 Th15 .= (Initialized s).f by SCMFSA_2:74 .= s.f by SCMFSA_M:37; hence thesis by FINSEQ_2:54; end; A56: for k being Element of NAT holds P[k] from NAT_1:sch 1(A53, A21); then ex p being Permutation of dom(s.f) st SF.n.f = (s.f) * p; then len (S.f) = n by A2,A4,A19,A50,FINSEQ_2:43; hence S.f is_non_decreasing_on 1, len (S.f) by A56,A19; thus thesis by A56,A19; end;