let s be State of SCM+FSA; for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA 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)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 holds
((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)
let p be Instruction-Sequence of SCM+FSA; for a being Int-Location
for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA 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)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 holds
((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)
let a be Int-Location; for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA 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)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 holds
((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)
let k be Nat; for J being really-closed good MacroInstruction of SCM+FSA 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)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 holds
((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)
let J be really-closed good MacroInstruction of SCM+FSA ; ( ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations) )
set UFLI = FinSeq-Locations ;
set I = J;
set ST = StepTimes (a,J,p,s);
set au = 1 -stRWNotIn ({a} \/ (UsedILoc J));
set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))));
set UILI = UsedILoc 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))
and
A3:
((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0
; ((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)
Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc 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} \/ (UsedILoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J))
by A2, SFMASTR1:3;
then A4:
DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1)) = DataPart (IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)))
by A1, A3, SCMFSA9A:32;
A5:
now for x being Int-Location st x in UsedILoc J holds
((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . xlet x be
Int-Location;
( x in UsedILoc J implies ((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x )A6:
not 1
-stRWNotIn ({a} \/ (UsedILoc J)) in {a} \/ (UsedILoc J)
by SCMFSA_M:25;
assume
x in UsedILoc J
;
((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . xthen A7:
1
-stRWNotIn ({a} \/ (UsedILoc J)) <> x
by A6, XBOOLE_0:def 3;
thus ((StepTimes (a,J,p,s)) . (k + 1)) . x =
(IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x
by A4, SCMFSA_M:2
.=
(Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc 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 A7, SCMFSA_2:65
;
verum end;
now 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))) . xlet x be
FinSeq-Location ;
((StepTimes (a,J,p,s)) . (k + 1)) . x = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . xthus ((StepTimes (a,J,p,s)) . (k + 1)) . x =
(IExec ((J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) . x
by A4, SCMFSA_M:2
.=
(Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc 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
;
verum end;
hence
((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)
by A5, SCMFSA_M:28; verum