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 Initialize ((StepTimes a,J,s) . k) & J is_closed_on Initialize ((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 Initialize ((StepTimes a,J,s) . k) & J is_closed_on Initialize ((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 Initialize ((StepTimes a,J,s) . k) & J is_closed_on Initialize ((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 Initialize ((StepTimes a,J,s) . k) & J is_closed_on Initialize ((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),(Initialize s));
set UILI = UsedIntLoc J;
set UFLI = FinSeq-Locations ;
assume that
A1: ((StepTimes a,J,s) . k) . (intloc 0 ) = 1 and
A2: J is_halting_on Initialize ((StepTimes a,J,s) . k) and
A3: J is_closed_on Initialize ((StepTimes a,J,s) . k) and
A4: ((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 )
A6: 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 Initialize ((StepTimes a,J,s) . k) by A2, A3, A6, SFMASTR1:4;
then A8: DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . (k + 1)) = DataPart (IExec (J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),((StepTimes a,J,s) . k)) by A1, A4, A6, A2, A3, SCMFSA9A:38, SFMASTR1:3;

A9: 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 )
assume A10: x in UsedIntLoc J ; :: thesis: ((StepTimes a,J,s) . (k + 1)) . x = (IExec J,((StepTimes a,J,s) . k)) . x
not 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) in {a} \/ (UsedIntLoc J) by SFMASTR1:21;
then A11: 1 -stRWNotIn ({a} \/ (UsedIntLoc J)) <> x by A10, 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 A8, SCMFSA6A:38
.= (Exec (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )),(IExec J,((StepTimes a,J,s) . k))) . x by A2, A3, SFMASTR1:12
.= (IExec J,((StepTimes a,J,s) . k)) . x by A11, 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 A8, SCMFSA6A:38
.= (Exec (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )),(IExec J,((StepTimes a,J,s) . k))) . x by A2, A3, 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 A9, Th7; :: thesis: verum