:: SFMASTR2 semantic presentation begin set D = Data-Locations ; theorem Th1: :: SFMASTR2:1 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for b being Int-Location for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not b in UsedIntLoc I holds (IExec (I,p,s)) . b = (Initialized s) . b proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for b being Int-Location for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not b in UsedIntLoc I holds (IExec (I,p,s)) . b = (Initialized s) . b let p be Instruction-Sequence of SCM+FSA; ::_thesis: for b being Int-Location for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not b in UsedIntLoc I holds (IExec (I,p,s)) . b = (Initialized s) . b let b be Int-Location; ::_thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not b in UsedIntLoc I holds (IExec (I,p,s)) . b = (Initialized s) . b let I be Program of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not b in UsedIntLoc I implies (IExec (I,p,s)) . b = (Initialized s) . b ) set a = b; assume that A1: I is_closed_on Initialized s,p and A2: I is_halting_on Initialized s,p and A3: not b in UsedIntLoc I ; ::_thesis: (IExec (I,p,s)) . b = (Initialized s) . b set Is = Initialized s; set pI = p +* I; A4: p +* I halts_on Initialize (Initialized s) by A2, SCMFSA7B:def_7; A5: Initialized s = Initialize (Initialized s) by MEMSTR_0:44; for m being Element of NAT st m < LifeSpan ((p +* I),(Initialized s)) holds IC (Comput ((p +* I),(Initialized s),m)) in dom I by A1, A5, SCMFSA7B:def_6; then A6: (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) . b = (Initialized s) . b by A3, FUNCT_4:25, SF_MASTR:61; DataPart (IExec (I,p,s)) = DataPart (Result ((p +* I),(Initialized s))) by SCMFSA6B:def_1 .= DataPart (Result ((p +* I),(Initialized s))) .= DataPart (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) by A5, A4, EXTPRO_1:23 ; hence (IExec (I,p,s)) . b = (Initialized s) . b by A6, SCMFSA_M:2; ::_thesis: verum end; theorem :: SFMASTR2:2 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for f being FinSeq-Location for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not f in UsedInt*Loc I holds (IExec (I,p,s)) . f = (Initialized s) . f proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for f being FinSeq-Location for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not f in UsedInt*Loc I holds (IExec (I,p,s)) . f = (Initialized s) . f let p be Instruction-Sequence of SCM+FSA; ::_thesis: for f being FinSeq-Location for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not f in UsedInt*Loc I holds (IExec (I,p,s)) . f = (Initialized s) . f let f be FinSeq-Location ; ::_thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not f in UsedInt*Loc I holds (IExec (I,p,s)) . f = (Initialized s) . f let I be Program of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not f in UsedInt*Loc I implies (IExec (I,p,s)) . f = (Initialized s) . f ) set a = f; assume that A1: I is_closed_on Initialized s,p and A2: I is_halting_on Initialized s,p and A3: not f in UsedInt*Loc I ; ::_thesis: (IExec (I,p,s)) . f = (Initialized s) . f set Is = Initialized s; set pI = p +* I; A4: p +* I halts_on Initialize (Initialized s) by A2, SCMFSA7B:def_7; A5: Initialized s = Initialize (Initialized s) by MEMSTR_0:44; for m being Element of NAT st m < LifeSpan ((p +* I),(Initialized s)) holds IC (Comput ((p +* I),(Initialized s),m)) in dom I by A1, A5, SCMFSA7B:def_6; then A6: (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) . f = (Initialized s) . f by A3, FUNCT_4:25, SF_MASTR:63; DataPart (IExec (I,p,s)) = DataPart (Result ((p +* I),(Initialized s))) by SCMFSA6B:def_1 .= DataPart (Result ((p +* I),(Initialized s))) .= DataPart (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) by A5, A4, EXTPRO_1:23 ; hence (IExec (I,p,s)) . f = (Initialized s) . f by A6, SCMFSA_M:2; ::_thesis: verum end; theorem Th3: :: SFMASTR2:3 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st ( ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedIntLoc I holds (IExec (I,p,s)) . a = s . a proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st ( ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedIntLoc I holds (IExec (I,p,s)) . a = s . a let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for I being Program of SCM+FSA st ( ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedIntLoc I holds (IExec (I,p,s)) . a = s . a let a be Int-Location; ::_thesis: for I being Program of SCM+FSA st ( ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedIntLoc I holds (IExec (I,p,s)) . a = s . a let I be Program of SCM+FSA; ::_thesis: ( ( ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedIntLoc I implies (IExec (I,p,s)) . a = s . a ) assume that A1: ( ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) or I is parahalting ) and A2: ( s . (intloc 0) = 1 or a is read-write ) and A3: not a in UsedIntLoc I ; ::_thesis: (IExec (I,p,s)) . a = s . a A4: ( a = intloc 0 or a is read-write ) by SCMFSA_M:def_2; ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) by A1, SCMFSA7B:18, SCMFSA7B:19; hence (IExec (I,p,s)) . a = (Initialized s) . a by A3, Th1 .= s . a by A2, A4, SCMFSA_M:9, SCMFSA_M:37 ; ::_thesis: verum end; theorem Th4: :: SFMASTR2:4 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ( I is_closed_on s,p iff I is_closed_on Initialized s,p ) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ( I is_closed_on s,p iff I is_closed_on Initialized s,p ) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ( I is_closed_on s,p iff I is_closed_on Initialized s,p ) let I be Program of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies ( I is_closed_on s,p iff I is_closed_on Initialized s,p ) ) assume s . (intloc 0) = 1 ; ::_thesis: ( I is_closed_on s,p iff I is_closed_on Initialized s,p ) then DataPart (Initialized s) = DataPart s by SCMFSA_M:19; hence ( I is_closed_on s,p iff I is_closed_on Initialized s,p ) by SCMFSA8B:3; ::_thesis: verum end; theorem Th5: :: SFMASTR2:5 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ( I is_closed_on s,p & I is_halting_on s,p iff ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) ) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ( I is_closed_on s,p & I is_halting_on s,p iff ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) ) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ( I is_closed_on s,p & I is_halting_on s,p iff ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) ) let I be Program of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies ( I is_closed_on s,p & I is_halting_on s,p iff ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) ) ) assume s . (intloc 0) = 1 ; ::_thesis: ( I is_closed_on s,p & I is_halting_on s,p iff ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) ) then DataPart (Initialized s) = DataPart s by SCMFSA_M:19; hence ( I is_closed_on s,p & I is_halting_on s,p iff ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) ) by SCMFSA8B:5; ::_thesis: verum end; begin definition let a be Int-Location; let I be Program of SCM+FSA; func times* (a,I) -> Program of SCM+FSA equals :: SFMASTR2:def 1 while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))))); correctness coherence while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))))) is Program of SCM+FSA; ; end; :: deftheorem defines times* SFMASTR2:def_1_:_ for a being Int-Location for I being Program of SCM+FSA holds times* (a,I) = while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))))); definition let a be Int-Location; let I be Program of SCM+FSA; func times (a,I) -> Program of SCM+FSA equals :: SFMASTR2:def 2 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ";" (times* (a,I)); correctness coherence ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ";" (times* (a,I)) is Program of SCM+FSA; ; end; :: deftheorem defines times SFMASTR2:def_2_:_ for a being Int-Location for I being Program of SCM+FSA holds times (a,I) = ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ";" (times* (a,I)); notation let a be Int-Location; let I be Program of SCM+FSA; synonym a times I for times (a,I); end; theorem :: SFMASTR2:6 canceled; theorem :: SFMASTR2:7 canceled; theorem Th8: :: SFMASTR2:8 for b being Int-Location for I being Program of SCM+FSA holds {b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I)) proof let b be Int-Location; ::_thesis: for I being Program of SCM+FSA holds {b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I)) let I be Program of SCM+FSA; ::_thesis: {b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I)) set a = b; set aux = 1 -stRWNotIn ({b} \/ (UsedIntLoc I)); UsedIntLoc (times (b,I)) = (UsedIntLoc ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))) := b)) \/ (UsedIntLoc (while>0 ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))))) by SF_MASTR:29 .= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc (while>0 ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))))) by SF_MASTR:14 .= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ({(1 -stRWNotIn ({b} \/ (UsedIntLoc I)))} \/ (UsedIntLoc (I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))))) by SCMFSA9A:24 .= ({(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ {(1 -stRWNotIn ({b} \/ (UsedIntLoc I)))}) \/ (UsedIntLoc (I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))) by XBOOLE_1:4 .= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc (I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))) by ZFMISC_1:9 .= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ((UsedIntLoc I) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))) by SF_MASTR:30 .= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ((UsedIntLoc I) \/ {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)}) by SF_MASTR:14 .= ({(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I)) \/ {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)} by XBOOLE_1:4 ; then A1: {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I)) by XBOOLE_1:7; UsedIntLoc I c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) by XBOOLE_1:7; then A2: UsedIntLoc I c= UsedIntLoc (times (b,I)) by A1, XBOOLE_1:1; ( {b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} & {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) ) by XBOOLE_1:7, ZFMISC_1:7; then {b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) by XBOOLE_1:1; then {b} c= UsedIntLoc (times (b,I)) by A1, XBOOLE_1:1; hence {b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I)) by A2, XBOOLE_1:8; ::_thesis: verum end; theorem :: SFMASTR2:9 for b being Int-Location for I being Program of SCM+FSA holds UsedInt*Loc (times (b,I)) = UsedInt*Loc I proof let b be Int-Location; ::_thesis: for I being Program of SCM+FSA holds UsedInt*Loc (times (b,I)) = UsedInt*Loc I let I be Program of SCM+FSA; ::_thesis: UsedInt*Loc (times (b,I)) = UsedInt*Loc I set a = b; set aux = 1 -stRWNotIn ({b} \/ (UsedIntLoc I)); thus UsedInt*Loc (times (b,I)) = (UsedInt*Loc ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))) := b)) \/ (UsedInt*Loc (while>0 ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))))) by SF_MASTR:45 .= {} \/ (UsedInt*Loc (while>0 ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))))) by SF_MASTR:32 .= UsedInt*Loc (I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))) by SCMFSA9A:25 .= (UsedInt*Loc I) \/ (UsedInt*Loc (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))) by SF_MASTR:46 .= (UsedInt*Loc I) \/ {} by SF_MASTR:32 .= UsedInt*Loc I ; ::_thesis: verum end; registration let I be good Program of SCM+FSA; let a be Int-Location; cluster times (a,I) -> good ; coherence times (a,I) is good ; end; definition let p be Instruction-Sequence of SCM+FSA; let s be State of SCM+FSA; let I be Program of SCM+FSA; let a be Int-Location; func StepTimes (a,I,p,s) -> Function of NAT,(product (the_Values_of SCM+FSA)) equals :: SFMASTR2:def 3 StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s)))); correctness coherence StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s)))) is Function of NAT,(product (the_Values_of SCM+FSA)); ; end; :: deftheorem defines StepTimes SFMASTR2:def_3_:_ for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA for a being Int-Location holds StepTimes (a,I,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s)))); theorem Th10: :: SFMASTR2:10 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 let J be good Program of SCM+FSA; ::_thesis: ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 set I = J; set ST = StepTimes (a,J,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set Is = Initialized s; thus ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (intloc 0) by SCMFSA_9:def_5 .= (Initialized s) . (intloc 0) by SCMFSA_2:63 .= 1 by SCMFSA_M:9 ; ::_thesis: verum end; theorem Th11: :: SFMASTR2:11 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a let J be good Program of SCM+FSA; ::_thesis: ( ( s . (intloc 0) = 1 or a is read-write ) implies ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a ) set I = J; set ST = StepTimes (a,J,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set Is = Initialized s; assume A1: ( s . (intloc 0) = 1 or a is read-write ) ; ::_thesis: ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a A2: ( a = intloc 0 or a is read-write ) by SCMFSA_M:def_2; thus ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_9:def_5 .= (Initialized s) . a by SCMFSA_2:63 .= s . a by A1, A2, SCMFSA_M:9, SCMFSA_M:37 ; ::_thesis: verum end; theorem Th12: :: SFMASTR2:12 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) holds ( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) ) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) holds ( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) ) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) holds ( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) ) let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) holds ( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) ) let J be good Program of SCM+FSA; ::_thesis: for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) holds ( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) ) let k be Element of NAT ; ::_thesis: ( ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) implies ( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) ) ) set I = J; assume that A1: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 and A2: ( J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) ) ; ::_thesis: ( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) ) set ST = StepTimes (a,J,p,s); A3: ( J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) ) by A1, A2, Th5; set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))); A4: Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:18; Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:19; then A5: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A3, A4, SFMASTR1:3; hereby ::_thesis: ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) percases ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ) ; suppose ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 then DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) = DataPart ((StepTimes (a,J,p,s)) . k) by SCMFSA9A:31; hence ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 by A1, SCMFSA_M:2; ::_thesis: verum end; suppose ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 then DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) = DataPart (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) by A1, A3, A4, A5, SCMFSA9A:32, SFMASTR1:2; hence ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (intloc 0) by SCMFSA_M:2 .= (Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))),(IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))))) . (intloc 0) by A3, SFMASTR1:11 .= (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (intloc 0) by SCMFSA_2:65 .= 1 by A3, SCMFSA8C:67 ; ::_thesis: verum end; end; end; not 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) in {a} \/ (UsedIntLoc J) by SCMFSA_M:25; then A6: not 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) in UsedIntLoc J by XBOOLE_0:def_3; assume ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 then DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) = DataPart (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) by A1, A3, A4, A5, SCMFSA9A:32, SFMASTR1:2; hence ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_M:2 .= (Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))),(IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A3, SFMASTR1:11 .= ((IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - ((IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (intloc 0)) by SCMFSA_2:65 .= ((IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 by A3, SCMFSA8C:67 .= ((Initialized ((StepTimes (a,J,p,s)) . k)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 by A3, A6, Th1 .= (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 by SCMFSA_M:37 ; ::_thesis: verum end; theorem Th13: :: SFMASTR2:13 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,I,p,s)) . 0) . a = s . a proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,I,p,s)) . 0) . a = s . a let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for I being Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,I,p,s)) . 0) . a = s . a let a be Int-Location; ::_thesis: for I being Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,I,p,s)) . 0) . a = s . a let I be Program of SCM+FSA; ::_thesis: ( ( s . (intloc 0) = 1 or a is read-write ) implies ((StepTimes (a,I,p,s)) . 0) . a = s . a ) set ST = StepTimes (a,I,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc I)); set Is = Initialized s; assume A1: ( s . (intloc 0) = 1 or a is read-write ) ; ::_thesis: ((StepTimes (a,I,p,s)) . 0) . a = s . a A2: ( a = intloc 0 or a is read-write ) by SCMFSA_M:def_2; a in {a} by TARSKI:def_1; then a in {a} \/ (UsedIntLoc I) by XBOOLE_0:def_3; then A3: 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) <> a by SCMFSA_M:25; thus ((StepTimes (a,I,p,s)) . 0) . a = (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) . a by SCMFSA_9:def_5 .= (Initialized s) . a by A3, SCMFSA_2:63 .= s . a by A1, A2, SCMFSA_M:9, SCMFSA_M:37 ; ::_thesis: verum end; theorem :: SFMASTR2:14 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for f being FinSeq-Location for I being Program of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for f being FinSeq-Location for I being Program of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for f being FinSeq-Location for I being Program of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f let a be Int-Location; ::_thesis: for f being FinSeq-Location for I being Program of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f let f be FinSeq-Location ; ::_thesis: for I being Program of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f let I be Program of SCM+FSA; ::_thesis: ((StepTimes (a,I,p,s)) . 0) . f = s . f set ST = StepTimes (a,I,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc I)); set Is = Initialized s; thus ((StepTimes (a,I,p,s)) . 0) . f = (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) . f by SCMFSA_9:def_5 .= (Initialized s) . f by SCMFSA_2:63 .= s . f by SCMFSA_M:37 ; ::_thesis: verum end; definition let p be Instruction-Sequence of SCM+FSA; let s be State of SCM+FSA; let a be Int-Location; let I be Program of SCM+FSA; pred ProperTimesBody a,I,s,p means :Def4: :: SFMASTR2:def 4 for k being Element of NAT st k < s . a holds ( I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) ); end; :: deftheorem Def4 defines ProperTimesBody SFMASTR2:def_4_:_ for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for a being Int-Location for I being Program of SCM+FSA holds ( ProperTimesBody a,I,s,p iff for k being Element of NAT st k < s . a holds ( I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) ) ); theorem Th15: :: SFMASTR2:15 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st I is parahalting holds ProperTimesBody a,I,s,p proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st I is parahalting holds ProperTimesBody a,I,s,p let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for I being Program of SCM+FSA st I is parahalting holds ProperTimesBody a,I,s,p let a be Int-Location; ::_thesis: for I being Program of SCM+FSA st I is parahalting holds ProperTimesBody a,I,s,p let I be Program of SCM+FSA; ::_thesis: ( I is parahalting implies ProperTimesBody a,I,s,p ) assume A1: I is parahalting ; ::_thesis: ProperTimesBody a,I,s,p then reconsider I9 = I as parahalting Program of SCM+FSA ; let k be Element of NAT ; :: according to SFMASTR2:def_4 ::_thesis: ( k < s . a implies ( I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) ) ) assume k < s . a ; ::_thesis: ( I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) ) I9 is paraclosed ; hence I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) by SCMFSA7B:18; ::_thesis: I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) thus I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) by A1, SCMFSA7B:19; ::_thesis: verum end; theorem Th16: :: SFMASTR2:16 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p holds for k being Element of NAT st k <= s . a holds ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p holds for k being Element of NAT st k <= s . a holds ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p holds for k being Element of NAT st k <= s . a holds ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p holds for k being Element of NAT st k <= s . a holds ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 let J be good Program of SCM+FSA; ::_thesis: ( ProperTimesBody a,J,s,p implies for k being Element of NAT st k <= s . a holds ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) set I = J; set ST = StepTimes (a,J,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set Is = Initialized s; defpred S1[ Element of NAT ] means ( $1 <= s . a implies ((StepTimes (a,J,p,s)) . $1) . (intloc 0) = 1 ); assume A1: ProperTimesBody a,J,s,p ; ::_thesis: for k being Element of NAT st k <= s . a holds ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that A3: ( k <= s . a implies ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) and A4: k + 1 <= s . a ; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 reconsider sa = s . a as Element of NAT by A4, INT_1:3; A5: k < sa by A4, NAT_1:13; then ( J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) ) by A1, Def4; hence ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 by A3, A5, Th12; ::_thesis: verum end; A6: S1[ 0 ] proof assume 0 <= s . a ; ::_thesis: ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 thus ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (intloc 0) by SCMFSA_9:def_5 .= (Initialized s) . (intloc 0) by SCMFSA_2:63 .= 1 by SCMFSA_M:9 ; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A6, A2); ::_thesis: verum end; theorem Th17: :: SFMASTR2:17 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) & ProperTimesBody a,J,s,p holds for k being Element of NAT st k <= s . a holds (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) & ProperTimesBody a,J,s,p holds for k being Element of NAT st k <= s . a holds (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) & ProperTimesBody a,J,s,p holds for k being Element of NAT st k <= s . a holds (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) & ProperTimesBody a,J,s,p holds for k being Element of NAT st k <= s . a holds (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a let J be good Program of SCM+FSA; ::_thesis: ( ( s . (intloc 0) = 1 or a is read-write ) & ProperTimesBody a,J,s,p implies for k being Element of NAT st k <= s . a holds (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a ) set I = J; assume that A1: ( s . (intloc 0) = 1 or a is read-write ) and A2: ProperTimesBody a,J,s,p ; ::_thesis: for k being Element of NAT st k <= s . a holds (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a set Is = Initialized s; set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set ST = StepTimes (a,J,p,s); set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))); defpred S1[ Nat] means ( $1 <= s . a implies (((StepTimes (a,J,p,s)) . $1) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + $1 = s . a ); A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof not 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) in {a} \/ (UsedIntLoc J) by SCMFSA_M:25; then A4: not 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) in UsedIntLoc J by XBOOLE_0:def_3; let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that A5: ( k <= s . a implies (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a ) and A6: k + 1 <= s . a ; ::_thesis: (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a reconsider sa = s . a as Element of NAT by A6, INT_1:3; A7: k < sa by A6, NAT_1:13; then A8: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A2, Th16; A9: now__::_thesis:_not_((StepWhile>0_((1_-stRWNotIn_({a}_\/_(UsedIntLoc_J))),(J_";"_(SubFrom_((1_-stRWNotIn_({a}_\/_(UsedIntLoc_J))),(intloc_0)))),p,(Exec_(((1_-stRWNotIn_({a}_\/_(UsedIntLoc_J)))_:=_a),(Initialized_s)))))_._k)_._(1_-stRWNotIn_({a}_\/_(UsedIntLoc_J)))_<=_0 assume ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ; ::_thesis: contradiction then (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k < (s . a) + 0 by A7, XREAL_1:8; hence contradiction by A5, A7; ::_thesis: verum end; A10: Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:18; A11: J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A2, A7, Def4; then A12: J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A8, Th4; J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A2, A7, Def4; then A13: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A8, A11, Th5; Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:19; then J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A12, A13, A10, SFMASTR1:3; then DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) = DataPart (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) by A8, A12, A13, A10, A9, SCMFSA9A:32, SFMASTR1:2; then ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_M:2 .= (Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))),(IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A12, A13, SFMASTR1:11 .= ((IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - ((IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (intloc 0)) by SCMFSA_2:65 .= ((IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 by A12, A13, SCMFSA8C:67 .= ((Initialized ((StepTimes (a,J,p,s)) . k)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 by A12, A13, A4, Th1 .= (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 by SCMFSA_M:37 ; hence (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a by A5, A7; ::_thesis: verum end; A14: ( a = intloc 0 or a is read-write ) by SCMFSA_M:def_2; A15: S1[ 0 ] proof assume 0 <= s . a ; ::_thesis: (((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 0 = s . a thus (((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 0 = (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_9:def_5 .= (Initialized s) . a by SCMFSA_2:63 .= s . a by A1, A14, SCMFSA_M:9, SCMFSA_M:37 ; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A3); ::_thesis: verum end; theorem Th18: :: SFMASTR2:18 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or a is read-write ) holds for k being Element of NAT st k >= s . a holds ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or a is read-write ) holds for k being Element of NAT st k >= s . a holds ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or a is read-write ) holds for k being Element of NAT st k >= s . a holds ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or a is read-write ) holds for k being Element of NAT st k >= s . a holds ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) let J be good Program of SCM+FSA; ::_thesis: ( ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or a is read-write ) implies for k being Element of NAT st k >= s . a holds ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) ) set I = J; assume that A1: ProperTimesBody a,J,s,p and A2: 0 <= s . a and A3: ( s . (intloc 0) = 1 or a is read-write ) ; ::_thesis: for k being Element of NAT st k >= s . a holds ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set ST = StepTimes (a,J,p,s); set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))); defpred S1[ Nat] means ( $1 >= s . a implies ( ((StepTimes (a,J,p,s)) . $1) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . $1) . (intloc 0) = 1 ) ); A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof reconsider sa = s . a as Element of NAT by A2, INT_1:3; let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that A5: ( k >= s . a implies ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 ) ) and A6: k + 1 >= s . a ; ::_thesis: ( ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 ) percases ( k + 1 = sa or k + 1 > sa ) by A6, XXREAL_0:1; supposeA7: k + 1 = sa ; ::_thesis: ( ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 ) then (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a by A1, A3, Th17; hence ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 by A7; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 thus ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 by A1, A7, Th16; ::_thesis: verum end; supposeA8: k + 1 > sa ; ::_thesis: ( ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 ) then A9: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) by A5, NAT_1:13, SCMFSA9A:31; hence ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 by A5, A8, NAT_1:13, SCMFSA_M:2; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 thus ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 by A5, A8, A9, NAT_1:13, SCMFSA_M:2; ::_thesis: verum end; end; end; A10: S1[ 0 ] proof assume A11: 0 >= s . a ; ::_thesis: ( ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 ) thus ((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 0 .= 0 by A1, A2, A3, A11, Th17 ; ::_thesis: ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 thus ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1 by A1, A2, Th16; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A10, A4); ::_thesis: verum end; theorem Th19: :: SFMASTR2:19 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ((StepTimes (a,I,p,s)) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ((StepTimes (a,I,p,s)) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ((StepTimes (a,I,p,s)) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) let a be Int-Location; ::_thesis: for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ((StepTimes (a,I,p,s)) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) let I be Program of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies ((StepTimes (a,I,p,s)) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) ) set ST = StepTimes (a,I,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc I)); set Is = Initialized s; set UILI = UsedIntLoc I; assume s . (intloc 0) = 1 ; ::_thesis: ((StepTimes (a,I,p,s)) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) then A1: DataPart (Initialized s) = DataPart s by SCMFSA_M:19; A2: now__::_thesis:_for_x_being_Int-Location_st_x_in_UsedIntLoc_I_holds_ ((StepTimes_(a,I,p,s))_._0)_._x_=_s_._x let x be Int-Location; ::_thesis: ( x in UsedIntLoc I implies ((StepTimes (a,I,p,s)) . 0) . x = s . x ) A3: not 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) in {a} \/ (UsedIntLoc I) by SCMFSA_M:25; assume x in UsedIntLoc I ; ::_thesis: ((StepTimes (a,I,p,s)) . 0) . x = s . x then A4: 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) <> x by A3, XBOOLE_0:def_3; thus ((StepTimes (a,I,p,s)) . 0) . x = (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) . x by SCMFSA_9:def_5 .= (Initialized s) . x by A4, SCMFSA_2:63 .= s . x by A1, SCMFSA_M:2 ; ::_thesis: verum end; now__::_thesis:_for_x_being_FinSeq-Location_holds_((StepTimes_(a,I,p,s))_._0)_._x_=_s_._x let x be FinSeq-Location ; ::_thesis: ((StepTimes (a,I,p,s)) . 0) . x = s . x thus ((StepTimes (a,I,p,s)) . 0) . x = (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) . x by SCMFSA_9:def_5 .= (Initialized s) . x by SCMFSA_2:63 .= s . x by SCMFSA_M:37 ; ::_thesis: verum end; hence ((StepTimes (a,I,p,s)) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) by A2, SCMFSA_M:28; ::_thesis: verum end; theorem Th20: :: SFMASTR2:20 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) let J be good Program of SCM+FSA; ::_thesis: for k being Element of NAT st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) let k be Element of NAT ; ::_thesis: ( ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) ) set UFLI = FinSeq-Locations ; set I = J; set ST = StepTimes (a,J,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))); set UILI = UsedIntLoc J; assume that A1: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 and A2: ( J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) ) and A3: ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) A4: Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:18; Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:19; then J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A2, A4, SFMASTR1:3; then A5: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) = DataPart (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) by A1, A2, A3, A4, SCMFSA9A:32, SFMASTR1:2; A6: now__::_thesis:_for_x_being_Int-Location_st_x_in_UsedIntLoc_J_holds_ ((StepTimes_(a,J,p,s))_._(k_+_1))_._x_=_(IExec_(J,(p_+*_(times*_(a,J))),((StepTimes_(a,J,p,s))_._k)))_._x let x be Int-Location; ::_thesis: ( x in UsedIntLoc J implies ((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x ) A7: not 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) in {a} \/ (UsedIntLoc J) by SCMFSA_M:25; assume x in UsedIntLoc J ; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x then A8: 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) <> x by A7, XBOOLE_0:def_3; thus ((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x by A5, SCMFSA_M:2 .= (Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))),(IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))))) . x by A2, SFMASTR1:11 .= (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x by A8, SCMFSA_2:65 ; ::_thesis: verum end; now__::_thesis:_for_x_being_FinSeq-Location_holds_((StepTimes_(a,J,p,s))_._(k_+_1))_._x_=_(IExec_(J,(p_+*_(times*_(a,J))),((StepTimes_(a,J,p,s))_._k)))_._x let x be FinSeq-Location ; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x thus ((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x by A5, SCMFSA_M:2 .= (Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))),(IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))))) . x by A2, SFMASTR1:12 .= (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x by SCMFSA_2:65 ; ::_thesis: verum end; hence ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) by A6, SCMFSA_M:28; ::_thesis: verum end; theorem Th21: :: SFMASTR2:21 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ( ProperTimesBody a,J,s,p or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ( ProperTimesBody a,J,s,p or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st ( ProperTimesBody a,J,s,p or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA for k being Element of NAT st ( ProperTimesBody a,J,s,p or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) let J be good Program of SCM+FSA; ::_thesis: for k being Element of NAT st ( ProperTimesBody a,J,s,p or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or a is read-write ) holds ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) let k be Element of NAT ; ::_thesis: ( ( ProperTimesBody a,J,s,p or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or a is read-write ) implies ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) ) set UFLI = FinSeq-Locations ; set I = J; assume that A1: ( ProperTimesBody a,J,s,p or J is parahalting ) and A2: k < s . a and A3: ( s . (intloc 0) = 1 or a is read-write ) ; ::_thesis: ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) set ST = StepTimes (a,J,p,s); A4: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A1, A2, Th15, Th16; set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); A5: ProperTimesBody a,J,s,p by A1, Th15; then A6: (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a by A2, A3, Th17; A7: J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A2, A5, Def4; then A8: J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A4, Th4; A9: k - k < (s . a) - k by A2, XREAL_1:9; J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A2, A5, Def4; then J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A4, A7, Th5; hence ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) by A4, A8, A6, A9, Th20; ::_thesis: verum set UILI = UsedIntLoc J; end; theorem :: SFMASTR2:22 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st s . a <= 0 & s . (intloc 0) = 1 holds (IExec ((times (a,I)),p,s)) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for I being Program of SCM+FSA st s . a <= 0 & s . (intloc 0) = 1 holds (IExec ((times (a,I)),p,s)) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for I being Program of SCM+FSA st s . a <= 0 & s . (intloc 0) = 1 holds (IExec ((times (a,I)),p,s)) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) let a be Int-Location; ::_thesis: for I being Program of SCM+FSA st s . a <= 0 & s . (intloc 0) = 1 holds (IExec ((times (a,I)),p,s)) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) let I be Program of SCM+FSA; ::_thesis: ( s . a <= 0 & s . (intloc 0) = 1 implies (IExec ((times (a,I)),p,s)) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) ) set FSL = FinSeq-Locations ; assume that A1: s . a <= 0 and A2: s . (intloc 0) = 1 ; ::_thesis: (IExec ((times (a,I)),p,s)) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) set UILI = UsedIntLoc I; set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc I)); set WH = while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))))); set s1 = Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s)); A3: ( a = intloc 0 or a is read-write ) by SCMFSA_M:def_2; A4: Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a)),p,s) by SCMFSA6C:5; A5: (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc I))) = (Initialized s) . a by SCMFSA_2:63 .= s . a by A2, A3, SCMFSA_M:9, SCMFSA_M:37 ; then A6: ( while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))))) is_closed_on IExec ((Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a)),p,s),p & while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))))) is_halting_on IExec ((Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a)),p,s),p ) by A1, A4, SCMFSA_9:38; (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:63 .= 1 by SCMFSA_M:9 ; then A7: DataPart (IExec ((while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) by A1, A5, SCMFSA9A:35; A8: now__::_thesis:_for_x_being_FinSeq-Location_st_x_in_FinSeq-Locations_holds_ (IExec_((times_(a,I)),p,s))_._x_=_s_._x let x be FinSeq-Location ; ::_thesis: ( x in FinSeq-Locations implies (IExec ((times (a,I)),p,s)) . x = s . x ) assume x in FinSeq-Locations ; ::_thesis: (IExec ((times (a,I)),p,s)) . x = s . x thus (IExec ((times (a,I)),p,s)) . x = (IExec ((while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))))) . x by A4, A6, SFMASTR1:15 .= (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) . x by A7, SCMFSA_M:2 .= (Initialized s) . x by SCMFSA_2:63 .= s . x by SCMFSA_M:37 ; ::_thesis: verum end; A9: DataPart s = DataPart (Initialized s) by A2, SCMFSA_M:19; A10: now__::_thesis:_for_x_being_Int-Location_st_x_in_UsedIntLoc_I_holds_ (IExec_((times_(a,I)),p,s))_._x_=_s_._x let x be Int-Location; ::_thesis: ( x in UsedIntLoc I implies (IExec ((times (a,I)),p,s)) . x = s . x ) A11: not 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) in {a} \/ (UsedIntLoc I) by SCMFSA_M:25; assume x in UsedIntLoc I ; ::_thesis: (IExec ((times (a,I)),p,s)) . x = s . x then A12: 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) <> x by A11, XBOOLE_0:def_3; thus (IExec ((times (a,I)),p,s)) . x = (IExec ((while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))))) . x by A4, A6, SFMASTR1:14 .= (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))) . x by A7, SCMFSA_M:2 .= (Initialized s) . x by A12, SCMFSA_2:63 .= s . x by A9, SCMFSA_M:2 ; ::_thesis: verum end; [#] FinSeq-Locations = FinSeq-Locations ; hence (IExec ((times (a,I)),p,s)) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations) by A10, A8, SCMFSA_M:27; ::_thesis: verum end; theorem Th23: :: SFMASTR2:23 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) let J be good Program of SCM+FSA; ::_thesis: for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) let k be Element of NAT ; ::_thesis: ( s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) implies DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) ) set I = J; assume A1: s . a = k ; ::_thesis: ( ( not ProperTimesBody a,J,s,p & not J is parahalting ) or ( not s . (intloc 0) = 1 & not a is read-write ) or DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) ) set ST = StepTimes (a,J,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set ISu = J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))); set s1 = Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)); set Is1 = Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))); set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))); set ISW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))); (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:63 .= 1 by SCMFSA_M:9 ; then A2: DataPart (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) by SCMFSA_M:19; set WH = while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))); assume A3: ( ProperTimesBody a,J,s,p or J is parahalting ) ; ::_thesis: ( ( not s . (intloc 0) = 1 & not a is read-write ) or DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) ) then A4: ProperTimesBody a,J,s,p by Th15; assume A5: ( s . (intloc 0) = 1 or a is read-write ) ; ::_thesis: DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) A6: StepTimes (a,J,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) ; A7: ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))), Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)),p proof let k be Element of NAT ; :: according to SCMFSA9A:def_4 ::_thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ( J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) ) assume ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; ::_thesis: ( J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) then A8: k < s . a by A1, A4, A5, A6, Th18; then A9: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A3, Th15, Th16; then A10: DataPart ((StepTimes (a,J,p,s)) . k) = DataPart (Initialized ((StepTimes (a,J,p,s)) . k)) by SCMFSA_M:19; A11: J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A4, A8, Def4; then A12: J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A9, Th4; J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A4, A8, Def4; then A13: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A11, A9, Th5; A14: Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:18; then A15: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A12, A13, SFMASTR1:2; hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A10, SCMFSA8B:3; ::_thesis: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:19; then J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A12, A13, A14, SFMASTR1:3; hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A10, A15, SCMFSA8B:5; ::_thesis: verum end; then A16: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) by A2, SCMFSA9A:34; A17: WithVariantWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))), Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))),p proof reconsider sa = s . a as Element of NAT by A1; deffunc H1( State of SCM+FSA) -> Element of NAT = abs ($1 . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))); consider f being Function of (product (the_Values_of SCM+FSA)),NAT such that A18: for x being Element of product (the_Values_of SCM+FSA) holds f . x = H1(x) from FUNCT_2:sch_4(); A19: for x being State of SCM+FSA holds f . x = H1(x) proof let x be State of SCM+FSA; ::_thesis: f . x = H1(x) reconsider x = x as Element of product (the_Values_of SCM+FSA) by CARD_3:107; f . x = H1(x) by A18; hence f . x = H1(x) ; ::_thesis: verum end; take f ; :: according to SCMFSA9A:def_5 ::_thesis: for b1 being Element of NAT holds ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . b1) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (b1 + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . b1) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) let k be Element of NAT ; ::_thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) by A2, A7, SCMFSA9A:34; then A20: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_M:2; DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) by A2, A7, SCMFSA9A:34; then A21: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_M:2; percases ( k < s . a or k >= s . a ) ; supposeA22: k < s . a ; ::_thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) then A23: k - k < (s . a) - k by XREAL_1:9; A24: (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a by A4, A5, A22, Th17; A25: k + 1 <= sa by A22, NAT_1:13; then A26: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9; A27: (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a by A4, A5, A25, Th17; then A28: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 1) + k ; A29: f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) = abs (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) by A19 .= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A21, A27, A26, ABSVALUE:def_1 ; f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) = abs (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) by A19 .= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A20, A24, A23, ABSVALUE:def_1 ; hence ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) by A24, A28, A29, NAT_1:13; ::_thesis: verum end; suppose k >= s . a ; ::_thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) hence ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) by A1, A4, A5, A6, A20, Th18; ::_thesis: verum end; end; end; A30: ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))), Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))),p proof let k be Element of NAT ; :: according to SCMFSA9A:def_4 ::_thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ( J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) ) assume A31: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; ::_thesis: ( J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) A32: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) by A2, A7, SCMFSA9A:34; then A33: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_M:2; then A34: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A7, A31, SCMFSA9A:def_4; hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A32, SCMFSA8B:3; ::_thesis: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A7, A31, A33, SCMFSA9A:def_4; hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A32, A34, SCMFSA8B:5; ::_thesis: verum end; then consider K being Element of NAT such that A35: ExitsAtWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) = K and A36: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . K) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 and A37: for i being Element of NAT st ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . i) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 holds K <= i and DataPart (Comput ((p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))))),(Initialize (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))),(LifeSpan ((p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))))),(Initialize (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))))))) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . K) by A17, SCMFSA9A:def_6; A38: while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_closed_on Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))),p by A30, A17, SCMFSA9A:27; while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_halting_on Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))),p by A30, A17, SCMFSA9A:27; then A39: while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_halting_on Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)),p by A2, A38, SCMFSA8B:5; A40: DataPart (IExec ((while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (ExitsAtWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))))) by A30, A17, SCMFSA9A:36; A41: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . K) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . K) by A2, A7, SCMFSA9A:34; ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 by A1, A4, A5, A6, Th18; then ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 by A16, SCMFSA_M:2; then A42: K <= k by A37; then A43: (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . K) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + K = k by A1, A4, A5, A6, Th17; K - K <= k - K by A42, XREAL_1:9; then A44: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . K) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 by A36, A41, A43, SCMFSA_M:2; A45: (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . K) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + K = k by A41, A43, SCMFSA_M:2; A46: now__::_thesis:_for_x_being_Int-Location_holds_(IExec_((times_(a,J)),p,s))_._x_=_((StepTimes_(a,J,p,s))_._k)_._x let x be Int-Location; ::_thesis: (IExec ((times (a,J)),p,s)) . x = ((StepTimes (a,J,p,s)) . k) . x thus (IExec ((times (a,J)),p,s)) . x = (IExec ((while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . x by A2, A38, A39, SCMFSA8B:3, SFMASTR1:14 .= ((StepTimes (a,J,p,s)) . k) . x by A40, A35, A16, A45, A44, SCMFSA_M:2 ; ::_thesis: verum end; now__::_thesis:_for_x_being_FinSeq-Location_holds_(IExec_((times_(a,J)),p,s))_._x_=_((StepTimes_(a,J,p,s))_._k)_._x let x be FinSeq-Location ; ::_thesis: (IExec ((times (a,J)),p,s)) . x = ((StepTimes (a,J,p,s)) . k) . x thus (IExec ((times (a,J)),p,s)) . x = (IExec ((while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . x by A2, A38, A39, SCMFSA8B:3, SFMASTR1:15 .= ((StepTimes (a,J,p,s)) . k) . x by A40, A35, A16, A45, A44, SCMFSA_M:2 ; ::_thesis: verum end; hence DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) by A46, SCMFSA_M:2; ::_thesis: verum end; theorem Th24: :: SFMASTR2:24 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for a being Int-Location for J being good Program of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for J being good Program of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) let a be Int-Location; ::_thesis: for J being good Program of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) let J be good Program of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) implies ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) ) set I = J; assume A1: s . (intloc 0) = 1 ; ::_thesis: ( ( not ProperTimesBody a,J,s,p & not J is parahalting ) or ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) ) set taI = times (a,J); set ST = StepTimes (a,J,p,s); set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J)); set ISu = J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))); set WH = while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))); set s1 = Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)); set Is1 = Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))); set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))); set ISW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))); A2: StepTimes (a,J,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) ; A3: ( Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a)),p,s) & Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_closed_on Initialized s,p ) by SCMFSA6C:5, SCMFSA7B:18; A4: Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_halting_on Initialized s,p by SCMFSA7B:19; (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:63 .= 1 by SCMFSA_M:9 ; then A5: DataPart (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) by SCMFSA_M:19; assume A6: ( ProperTimesBody a,J,s,p or J is parahalting ) ; ::_thesis: ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) then A7: ProperTimesBody a,J,s,p by Th15; A8: Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_halting_on Initialized s,p by SCMFSA7B:19; percases ( s . a < 0 or 0 <= s . a ) ; supposeA9: s . a < 0 ; ::_thesis: ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) A10: ( a = intloc 0 or a is read-write ) by SCMFSA_M:def_2; A11: (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (Initialized s) . a by SCMFSA_2:63 .= s . a by A1, A10, SCMFSA_M:9, SCMFSA_M:37 ; then A12: while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_closed_on Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)),p by A9, SCMFSA_9:38; then A13: times (a,J) is_closed_on Initialized s,p by A3, A4, SFMASTR1:2; hence times (a,J) is_closed_on s,p by A1, Th4; ::_thesis: times (a,J) is_halting_on s,p while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_halting_on Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)),p by A9, A11, SCMFSA_9:38; then times (a,J) is_halting_on Initialized s,p by A3, A8, A12, SFMASTR1:3; hence times (a,J) is_halting_on s,p by A1, A13, Th5; ::_thesis: verum end; supposeA14: 0 <= s . a ; ::_thesis: ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) A15: ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))), Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)),p proof let k be Element of NAT ; :: according to SCMFSA9A:def_4 ::_thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ( J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) ) assume ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; ::_thesis: ( J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) then A16: k < s . a by A1, A7, A2, A14, Th18; then A17: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A6, Th15, Th16; then A18: DataPart ((StepTimes (a,J,p,s)) . k) = DataPart (Initialized ((StepTimes (a,J,p,s)) . k)) by SCMFSA_M:19; A19: J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A7, A16, Def4; then A20: J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A17, Th4; J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A7, A16, Def4; then A21: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A19, A17, Th5; A22: Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:18; then A23: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A20, A21, SFMASTR1:2; hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A18, SCMFSA8B:3; ::_thesis: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:19; then J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A20, A21, A22, SFMASTR1:3; hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A18, A23, SCMFSA8B:5; ::_thesis: verum end; A24: WithVariantWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))), Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))),p proof reconsider sa = s . a as Element of NAT by A14, INT_1:3; deffunc H1( State of SCM+FSA) -> Element of NAT = abs ($1 . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))); consider f being Function of (product (the_Values_of SCM+FSA)),NAT such that A25: for x being Element of product (the_Values_of SCM+FSA) holds f . x = H1(x) from FUNCT_2:sch_4(); A26: for x being State of SCM+FSA holds f . x = H1(x) proof let x be State of SCM+FSA; ::_thesis: f . x = H1(x) reconsider x = x as Element of product (the_Values_of SCM+FSA) by CARD_3:107; f . x = H1(x) by A25; hence f . x = H1(x) ; ::_thesis: verum end; take f ; :: according to SCMFSA9A:def_5 ::_thesis: for b1 being Element of NAT holds ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . b1) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (b1 + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . b1) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) let k be Element of NAT ; ::_thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) by A5, A15, SCMFSA9A:34; then A27: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_M:2; DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) by A5, A15, SCMFSA9A:34; then A28: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_M:2; percases ( k < s . a or k >= s . a ) ; supposeA29: k < s . a ; ::_thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) then A30: k - k < (s . a) - k by XREAL_1:9; A31: (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a by A1, A7, A29, Th17; A32: k + 1 <= sa by A29, NAT_1:13; then A33: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9; A34: (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a by A1, A7, A32, Th17; then A35: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 1) + k ; A36: f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) = abs (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) by A26 .= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A28, A34, A33, ABSVALUE:def_1 ; f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) = abs (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) by A26 .= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A27, A31, A30, ABSVALUE:def_1 ; hence ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) by A31, A35, A36, NAT_1:13; ::_thesis: verum end; suppose k >= s . a ; ::_thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) hence ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) by A1, A7, A2, A14, A27, Th18; ::_thesis: verum end; end; end; A37: ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))), Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))),p proof let k be Element of NAT ; :: according to SCMFSA9A:def_4 ::_thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ( J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) ) assume A38: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; ::_thesis: ( J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) A39: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) by A5, A15, SCMFSA9A:34; then A40: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA_M:2; then A41: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A15, A38, SCMFSA9A:def_4; hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A39, SCMFSA8B:3; ::_thesis: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A15, A38, A40, SCMFSA9A:def_4; hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A39, A41, SCMFSA8B:5; ::_thesis: verum end; then A42: while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_closed_on Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)),p by A5, A24, SCMFSA8B:3, SCMFSA9A:27; A43: times (a,J) is_closed_on Initialized s,p by A3, A42, A4, SFMASTR1:2; hence times (a,J) is_closed_on s,p by A1, Th4; ::_thesis: times (a,J) is_halting_on s,p ( while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_closed_on Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))),p & while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_halting_on Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))),p ) by A37, A24, SCMFSA9A:27; then while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))) is_halting_on Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)),p by A5, SCMFSA8B:5; then times (a,J) is_halting_on Initialized s,p by A3, A8, A42, SFMASTR1:3; hence times (a,J) is_halting_on s,p by A1, A43, Th5; ::_thesis: verum end; end; end; begin definition let d be read-write Int-Location; func triv-times d -> Program of SCM+FSA equals :: SFMASTR2:def 5 times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))); correctness coherence times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) is Program of SCM+FSA; ; end; :: deftheorem defines triv-times SFMASTR2:def_5_:_ for d being read-write Int-Location holds triv-times d = times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))); theorem :: SFMASTR2:25 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for d being read-write Int-Location st s . d <= 0 holds (IExec ((triv-times d),p,s)) . d = s . d proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for d being read-write Int-Location st s . d <= 0 holds (IExec ((triv-times d),p,s)) . d = s . d let p be Instruction-Sequence of SCM+FSA; ::_thesis: for d being read-write Int-Location st s . d <= 0 holds (IExec ((triv-times d),p,s)) . d = s . d let d be read-write Int-Location; ::_thesis: ( s . d <= 0 implies (IExec ((triv-times d),p,s)) . d = s . d ) set a = d; assume A1: s . d <= 0 ; ::_thesis: (IExec ((triv-times d),p,s)) . d = s . d set I = (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))); set au = 1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))); set WH = while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(intloc 0))))); set s1 = Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s)); A2: (Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = (Initialized s) . d by SCMFSA_2:63 .= s . d by SCMFSA_M:37 ; d in {d} by TARSKI:def_1; then d in {d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) by XBOOLE_0:def_3; then A3: 1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) <> d by SCMFSA_M:25; (Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:63 .= 1 by SCMFSA_M:9 ; then A4: DataPart (IExec ((while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(intloc 0)))))),p,(Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))))) = DataPart (Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) by A1, A2, SCMFSA9A:35; A5: Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d)),p,s) by SCMFSA6C:5; then ( while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(intloc 0))))) is_closed_on IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d)),p,s),p & while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(intloc 0))))) is_halting_on IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d)),p,s),p ) by A1, A2, SCMFSA_9:38; hence (IExec ((triv-times d),p,s)) . d = (IExec ((while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(intloc 0)))))),p,(Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))))) . d by A5, SFMASTR1:14 .= (Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . d by A4, SCMFSA_M:2 .= (Initialized s) . d by A3, SCMFSA_2:63 .= s . d by SCMFSA_M:37 ; ::_thesis: verum end; theorem :: SFMASTR2:26 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for d being read-write Int-Location st 0 <= s . d holds (IExec ((triv-times d),p,s)) . d = 0 proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for d being read-write Int-Location st 0 <= s . d holds (IExec ((triv-times d),p,s)) . d = 0 let p be Instruction-Sequence of SCM+FSA; ::_thesis: for d being read-write Int-Location st 0 <= s . d holds (IExec ((triv-times d),p,s)) . d = 0 let d be read-write Int-Location; ::_thesis: ( 0 <= s . d implies (IExec ((triv-times d),p,s)) . d = 0 ) set a = d; set I1 = while=0 (d,(Macro (d := d))); set i2 = SubFrom (d,(intloc 0)); set I = (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))); set au = 1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))); set ST = StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s); defpred S1[ Nat] means ( ( $1 < s . d implies ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1) . (intloc 0) = 1 ) ) & ( $1 <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1) . d) + $1 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1) . d ) ) ); d in {d,(intloc 0)} by TARSKI:def_2; then d in UsedIntLoc (SubFrom (d,(intloc 0))) by SF_MASTR:14; then d in (UsedIntLoc (while=0 (d,(Macro (d := d))))) \/ (UsedIntLoc (SubFrom (d,(intloc 0)))) by XBOOLE_0:def_3; then A1: d in UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))) by SF_MASTR:30; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that A3: ( k < s . d implies ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (intloc 0) = 1 ) ) and A4: ( k <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) + k = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d ) ) ; ::_thesis: S1[k + 1] A5: now__::_thesis:_(_k_<_s_._d_implies_(_((StepTimes_(d,((while=0_(d,(Macro_(d_:=_d))))_";"_(SubFrom_(d,(intloc_0)))),p,s))_._k)_._(1_-stRWNotIn_({d}_\/_(UsedIntLoc_((while=0_(d,(Macro_(d_:=_d))))_";"_(SubFrom_(d,(intloc_0)))))))_>_0_&_(((StepTimes_(d,((while=0_(d,(Macro_(d_:=_d))))_";"_(SubFrom_(d,(intloc_0)))),p,s))_._(k_+_1))_._d)_+_(k_+_1)_=_s_._d_)_) assume A6: k < s . d ; ::_thesis: ( ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) > 0 & (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d ) then A7: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d <> 0 by A4; then A8: DataPart (IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) = DataPart ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) by A3, A6, SCMFSA9A:22; A9: while=0 (d,(Macro (d := d))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A7, SCMFSA_9:18; then A10: while=0 (d,(Macro (d := d))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A3, A6, Th4; while=0 (d,(Macro (d := d))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A7, SCMFSA_9:18; then A11: while=0 (d,(Macro (d := d))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A3, A6, A9, Th5; A12: k - k < (s . d) - k by A6, XREAL_1:9; hence ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) > 0 by A4, A6; ::_thesis: (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) ) by A3, A6, Th5; then ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) | ((UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) \/ FinSeq-Locations) = (IExec (((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) | ((UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) \/ FinSeq-Locations) by A3, A4, A6, A12, Th20; then ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d = (IExec (((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) . d by A1, SCMFSA_M:28 .= (Exec ((SubFrom (d,(intloc 0))),(IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))))) . d by A10, A11, SFMASTR1:11 .= ((IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) . d) - ((IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) . (intloc 0)) by SCMFSA_2:65 .= (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) - ((IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) . (intloc 0)) by A8, SCMFSA_M:2 .= (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) - 1 by A3, A6, A8, SCMFSA_M:2 ; hence (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d by A4, A6; ::_thesis: verum end; hereby ::_thesis: ( k + 1 <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d ) ) assume A13: k + 1 < s . d ; ::_thesis: ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1 ) then reconsider sa = s . d as Element of NAT by INT_1:3; A14: k < sa by A13, NAT_1:12; then A15: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1 by A3, Th12; A16: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d <> 0 by A5, A13, A14; then A17: while=0 (d,(Macro (d := d))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by SCMFSA_9:18; A18: Macro (SubFrom (d,(intloc 0))) is_closed_on IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1))),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by SCMFSA7B:18; while=0 (d,(Macro (d := d))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A16, SCMFSA_9:18; then A19: while=0 (d,(Macro (d := d))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A15, A17, Th5; A20: while=0 (d,(Macro (d := d))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A15, A17, Th4; then A21: (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A19, A18, SFMASTR1:2; hence (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A15, Th4; ::_thesis: ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1 ) Macro (SubFrom (d,(intloc 0))) is_halting_on IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1))),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by SCMFSA7B:19; then (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A19, A20, A18, SFMASTR1:3; hence (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A15, A21, Th5; ::_thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1 thus ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1 by A3, A14, Th12; ::_thesis: verum end; A22: k < k + 1 by NAT_1:13; assume A23: k + 1 <= s . d ; ::_thesis: ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d ) hence (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d by A5, A22, XXREAL_0:2; ::_thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) - 1 by A3, A4, A5, A23, A22, Th12, XXREAL_0:2; hence ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d by A4, A5, A23, A22, XXREAL_0:2; ::_thesis: verum end; A24: S1[ 0 ] proof hereby ::_thesis: ( 0 <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d) + 0 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d ) ) assume 0 < s . d ; ::_thesis: ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1 ) then A25: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d <> 0 by Th13; then A26: while=0 (d,(Macro (d := d))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by SCMFSA_9:18; A27: Macro (SubFrom (d,(intloc 0))) is_closed_on IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by SCMFSA7B:18; A28: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1 by Th10; while=0 (d,(Macro (d := d))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A25, SCMFSA_9:18; then A29: while=0 (d,(Macro (d := d))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A28, A26, Th5; A30: while=0 (d,(Macro (d := d))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A28, A26, Th4; then A31: (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A29, A27, SFMASTR1:2; hence (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A28, Th4; ::_thesis: ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1 ) Macro (SubFrom (d,(intloc 0))) is_halting_on IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by SCMFSA7B:19; then (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A29, A30, A27, SFMASTR1:3; hence (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) by A28, A31, Th5; ::_thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1 thus ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1 by Th10; ::_thesis: verum end; assume 0 <= s . d ; ::_thesis: ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d) + 0 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d ) thus (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d) + 0 = s . d by Th13; ::_thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d = s . d by Th13; hence ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d by Th11; ::_thesis: verum end; A32: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A24, A2); A33: ProperTimesBody d,(while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))),s,p proof let k be Element of NAT ; :: according to SFMASTR2:def_4 ::_thesis: ( k < s . d implies ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) ) ) thus ( k < s . d implies ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) ) ) by A32; ::_thesis: verum end; assume 0 <= s . d ; ::_thesis: (IExec ((triv-times d),p,s)) . d = 0 then reconsider k = s . d as Element of NAT by INT_1:3; A34: (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) + k = s . d by A32; DataPart (IExec ((times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))),p,s)) = DataPart ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) by A33, Th23; hence (IExec ((triv-times d),p,s)) . d = 0 by A34, SCMFSA_M:2; ::_thesis: verum end; begin definition let N, result be Int-Location; func Fib-macro (N,result) -> Program of SCM+FSA equals :: SFMASTR2:def 6 (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))))); correctness coherence (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))))) is Program of SCM+FSA; ; end; :: deftheorem defines Fib-macro SFMASTR2:def_6_:_ for N, result being Int-Location holds Fib-macro (N,result) = (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))))); theorem :: SFMASTR2:27 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for N, result being read-write Int-Location st N <> result holds for n being Element of NAT st n = s . N holds ( (IExec ((Fib-macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib-macro (N,result)),p,s)) . N = s . N ) proof let s be State of SCM+FSA; ::_thesis: for p being Instruction-Sequence of SCM+FSA for N, result being read-write Int-Location st N <> result holds for n being Element of NAT st n = s . N holds ( (IExec ((Fib-macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib-macro (N,result)),p,s)) . N = s . N ) let p be Instruction-Sequence of SCM+FSA; ::_thesis: for N, result being read-write Int-Location st N <> result holds for n being Element of NAT st n = s . N holds ( (IExec ((Fib-macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib-macro (N,result)),p,s)) . N = s . N ) let N, result be read-write Int-Location; ::_thesis: ( N <> result implies for n being Element of NAT st n = s . N holds ( (IExec ((Fib-macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib-macro (N,result)),p,s)) . N = s . N ) ) assume A1: N <> result ; ::_thesis: for n being Element of NAT st n = s . N holds ( (IExec ((Fib-macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib-macro (N,result)),p,s)) . N = s . N ) let n be Element of NAT ; ::_thesis: ( n = s . N implies ( (IExec ((Fib-macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib-macro (N,result)),p,s)) . N = s . N ) ) set i1 = SubFrom (result,result); set next = 1 -stRWNotIn {N,result}; set Nsave = 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))); set i0 = (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N; set i2 = (1 -stRWNotIn {N,result}) := (intloc 0); set i30 = AddTo (result,(1 -stRWNotIn {N,result})); set I31 = swap (result,(1 -stRWNotIn {N,result})); set I301 = (AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))); set i02 = (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0)); set s1 = IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s); set I3 = times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))); set ST = StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s))); assume A2: n = s . N ; ::_thesis: ( (IExec ((Fib-macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib-macro (N,result)),p,s)) . N = s . N ) A3: not 1 -stRWNotIn {N,result} in {N,result} by SCMFSA_M:25; then A4: 1 -stRWNotIn {N,result} <> N by TARSKI:def_2; A5: {N} \/ (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) c= UsedIntLoc (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))) by Th8; A6: 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))) = 1 -stRWNotIn (UsedIntLoc (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) by SFMASTR1:def_4; then A7: not 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))) in UsedIntLoc (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))) by SCMFSA_M:25; N in {N} by TARSKI:def_1; then N in {N} \/ (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) by XBOOLE_0:def_3; then A8: 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))) <> N by A6, A5, SCMFSA_M:25; A9: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)))) . N by SCMFSA6C:6 .= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)) . N by A4, SCMFSA_2:63 .= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . N by SCMFSA6C:8 .= (Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . N by A1, SCMFSA_2:65 .= (Initialized s) . N by A8, SCMFSA_2:63 .= s . N by SCMFSA_M:37 ; then A10: DataPart (IExec ((times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) = DataPart ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . n) by A2, Th23; defpred S1[ Nat] means ( $1 <= (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N implies ( ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . $1) . result = Fib $1 & ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . $1) . (1 -stRWNotIn {N,result}) = Fib ($1 + 1) ) ); set UIFS = (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations; set i4 = N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))); A11: UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))) = (UsedIntLoc (AddTo (result,(1 -stRWNotIn {N,result})))) \/ (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by SF_MASTR:29 .= {result,(1 -stRWNotIn {N,result})} \/ (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by SF_MASTR:14 ; 1 -stRWNotIn {N,result} in {result,(1 -stRWNotIn {N,result})} by TARSKI:def_2; then A12: 1 -stRWNotIn {N,result} in UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))) by A11, XBOOLE_0:def_3; then 1 -stRWNotIn {N,result} in {N} \/ (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) by XBOOLE_0:def_3; then A13: 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))) <> 1 -stRWNotIn {N,result} by A6, A5, SCMFSA_M:25; result in {result,(1 -stRWNotIn {N,result})} by TARSKI:def_2; then A14: result in UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))) by A11, XBOOLE_0:def_3; then result in {N} \/ (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) by XBOOLE_0:def_3; then A15: 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))) <> result by A6, A5, SCMFSA_M:25; A16: 1 -stRWNotIn {N,result} <> result by A3, TARSKI:def_2; A17: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A18: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof A19: k < k + 1 by NAT_1:13; assume A20: k + 1 <= (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N ; ::_thesis: ( ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . result = Fib (k + 1) & ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . (1 -stRWNotIn {N,result}) = Fib ((k + 1) + 1) ) then k < (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N by A19, XXREAL_0:2; then A21: ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) | ((UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations) = (IExec (((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k))) | ((UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations) by Th21; hence ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . result = (IExec (((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k))) . result by A14, SCMFSA_M:28 .= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)))))) . result by SCMFSA8B:9 .= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:10 .= (Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)) . (1 -stRWNotIn {N,result}) by A16, SCMFSA_2:64 .= Fib (k + 1) by A18, A20, A19, SCMFSA_M:37, XXREAL_0:2 ; ::_thesis: ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . (1 -stRWNotIn {N,result}) = Fib ((k + 1) + 1) thus ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . (1 -stRWNotIn {N,result}) = (IExec (((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k))) . (1 -stRWNotIn {N,result}) by A12, A21, SCMFSA_M:28 .= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)))))) . (1 -stRWNotIn {N,result}) by SCMFSA8B:9 .= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)))) . result by SCMFSA6C:10 .= ((Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)) . result) + ((Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)) . (1 -stRWNotIn {N,result})) by SCMFSA_2:64 .= (((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k) . result) + ((Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)) . (1 -stRWNotIn {N,result})) by SCMFSA_M:37 .= (((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k) . result) + (((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k) . (1 -stRWNotIn {N,result})) by SCMFSA_M:37 .= Fib ((k + 1) + 1) by A18, A20, A19, PRE_FF:1, XXREAL_0:2 ; ::_thesis: verum end; end; A22: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)))) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) by SCMFSA6C:6 .= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) by A13, SCMFSA_2:63 .= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) by SCMFSA6C:8 .= (Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) by A15, SCMFSA_2:65 .= (Initialized s) . N by SCMFSA_2:63 .= s . N by SCMFSA_M:37 ; A23: ( (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0)) is_halting_on Initialized s,p & (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0)) is_closed_on Initialized s,p ) by SCMFSA7B:18, SCMFSA7B:19; reconsider i02 = (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0)) as good Program of SCM+FSA ; A24: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (1 -stRWNotIn {N,result}) = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:6 .= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)) . (intloc 0) by SCMFSA_2:63 .= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . (intloc 0) by SCMFSA6C:8 .= (Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . (intloc 0) by SCMFSA_2:65 .= (Initialized s) . (intloc 0) by SCMFSA_2:63 .= Fib (0 + 1) by PRE_FF:1, SCMFSA_M:9 ; A25: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (intloc 0) = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)))) . (intloc 0) by SCMFSA6C:6 .= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)) . (intloc 0) by SCMFSA_2:63 .= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . (intloc 0) by SCMFSA6C:8 .= (Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . (intloc 0) by SCMFSA_2:65 .= (Initialized s) . (intloc 0) by SCMFSA_2:63 .= 1 by SCMFSA_M:9 ; then A26: times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) is_closed_on IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s),p by Th24; A27: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . result = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)))) . result by SCMFSA6C:6 .= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))),p,s)) . result by A16, SCMFSA_2:63 .= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . result by SCMFSA6C:8 .= ((Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . result) - ((Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . result) by SCMFSA_2:65 .= Fib 0 by PRE_FF:1 ; A28: S1[ 0 ] proof assume 0 <= (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N ; ::_thesis: ( ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . result = Fib 0 & ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . (1 -stRWNotIn {N,result}) = Fib (0 + 1) ) A29: ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) | ((UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations) = (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) | ((UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations) by A25, Th19; hence ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . result = Fib 0 by A14, A27, SCMFSA_M:28; ::_thesis: ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . (1 -stRWNotIn {N,result}) = Fib (0 + 1) thus ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . (1 -stRWNotIn {N,result}) = Fib (0 + 1) by A12, A24, A29, SCMFSA_M:28; ::_thesis: verum end; A30: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A28, A17); A31: times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) is_halting_on IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s),p by A25, Th24; then A32: ( times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) is_closed_on Initialized (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)),p & times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))) is_halting_on Initialized (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)),p ) by A25, A26, Th5; A33: i02 ";" (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))) is_closed_on Initialized s,p by A26, A23, SFMASTR1:2; hence (IExec ((Fib-macro (N,result)),p,s)) . result = (Exec ((N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))))),(IExec ((i02 ";" (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)))) . result by A26, A31, A23, SFMASTR1:3, SFMASTR1:11 .= (IExec ((i02 ";" (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . result by A1, SCMFSA_2:63 .= (IExec ((times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . result by A26, A31, SFMASTR1:7 .= ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . n) . result by A10, SCMFSA_M:2 .= Fib n by A9, A30, A2 ; ::_thesis: (IExec ((Fib-macro (N,result)),p,s)) . N = s . N thus (IExec ((Fib-macro (N,result)),p,s)) . N = (Exec ((N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))))),(IExec ((i02 ";" (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)))) . N by A26, A31, A23, A33, SFMASTR1:3, SFMASTR1:11 .= (IExec ((i02 ";" (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) by SCMFSA_2:63 .= (IExec ((times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result})))))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) by A26, A31, SFMASTR1:7 .= s . N by A7, A22, A32, Th3 ; ::_thesis: verum end;