let s be State 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,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,s)) . k) & J is_closed_on Initialized ((StepTimes (a,J,s)) . k) & ((StepTimes (a,J,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds
((StepTimes (a,J,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,((StepTimes (a,J,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,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,s)) . k) & J is_closed_on Initialized ((StepTimes (a,J,s)) . k) & ((StepTimes (a,J,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds
((StepTimes (a,J,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,((StepTimes (a,J,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,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,s)) . k) & J is_closed_on Initialized ((StepTimes (a,J,s)) . k) & ((StepTimes (a,J,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds
((StepTimes (a,J,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,((StepTimes (a,J,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations)
let k be Element of NAT ; :: thesis: ( ((StepTimes (a,J,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,s)) . k) & J is_closed_on Initialized ((StepTimes (a,J,s)) . k) & ((StepTimes (a,J,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes (a,J,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,((StepTimes (a,J,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) )
set I = J;
set ST = StepTimes (a,J,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)))),(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))));
set UILI = UsedIntLoc J;
assume that
A1: ((StepTimes (a,J,s)) . k) . (intloc 0) = 1 and
A2: ( J is_halting_on Initialized ((StepTimes (a,J,s)) . k) & J is_closed_on Initialized ((StepTimes (a,J,s)) . k) ) and
A3: ((StepTimes (a,J,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; :: thesis: ((StepTimes (a,J,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,((StepTimes (a,J,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations)
A4: Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on IExec (J,((StepTimes (a,J,s)) . k)) by SCMFSA7B:24;
Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on IExec (J,((StepTimes (a,J,s)) . k)) by SCMFSA7B:25;
then J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,s)) . k) by A2, A4, SFMASTR1:4;
then A5: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) = DataPart (IExec ((J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),((StepTimes (a,J,s)) . k))) by A1, A2, A3, A4, SCMFSA9A:38, SFMASTR1:3;

A6: now

let x be Int-Location ; :: thesis: ( x in UsedIntLoc J implies ((StepTimes (a,J,s)) . (k + 1)) . x = (IExec (J,((StepTimes (a,J,s)) . k))) . x )
A7: not 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) in {a} \/ (UsedIntLoc J) by SFMASTR1:21;
assume x in UsedIntLoc J ; :: thesis: ((StepTimes (a,J,s)) . (k + 1)) . x = (IExec (J,((StepTimes (a,J,s)) . k))) . x
then A8: 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) <> x by A7, XBOOLE_0:def 3;
thus ((StepTimes (a,J,s)) . (k + 1)) . x = (IExec ((J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),((StepTimes (a,J,s)) . k))) . x by A5, SCMFSA6A:38
.= (Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))),(IExec (J,((StepTimes (a,J,s)) . k))))) . x by A2, SFMASTR1:12
.= (IExec (J,((StepTimes (a,J,s)) . k))) . x by A8, SCMFSA_2:91 ; :: thesis: verum

end;

now

let x be FinSeq-Location ; :: thesis: ((StepTimes (a,J,s)) . (k + 1)) . x = (IExec (J,((StepTimes (a,J,s)) . k))) . x
thus ((StepTimes (a,J,s)) . (k + 1)) . x = (IExec ((J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),((StepTimes (a,J,s)) . k))) . x by A5, SCMFSA6A:38
.= (Exec ((SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))),(IExec (J,((StepTimes (a,J,s)) . k))))) . x by A2, SFMASTR1:13
.= (IExec (J,((StepTimes (a,J,s)) . k))) . x by SCMFSA_2:91 ; :: thesis: verum

end;

hence ((StepTimes (a,J,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,((StepTimes (a,J,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations) by A6, Th7; :: thesis: verum