let s be State 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,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,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,s) . 0 ) | ((UsedIntLoc I) \/ FinSeq-Locations ) = s | ((UsedIntLoc I) \/ FinSeq-Locations ) )
assume A1: s . (intloc 0 ) = 1 ; :: thesis: ((StepTimes a,I,s) . 0 ) | ((UsedIntLoc I) \/ FinSeq-Locations ) = s | ((UsedIntLoc I) \/ FinSeq-Locations )
set ST = StepTimes a,I,s;
set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc I));
set Is = Initialize s;
set UILI = UsedIntLoc I;
A2: DataPart (Initialize s) = DataPart s by A1, SCMFSA8C:27;

A3: now

let x be Int-Location ; :: thesis: ( x in UsedIntLoc I implies ((StepTimes a,I,s) . 0 ) . x = s . x )
assume A4: x in UsedIntLoc I ; :: thesis: ((StepTimes a,I,s) . 0 ) . x = s . x
not 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) in {a} \/ (UsedIntLoc I) by SFMASTR1:21;
then A5: 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) <> x by A4, XBOOLE_0:def 3;
thus ((StepTimes a,I,s) . 0 ) . x = (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialize s)) . x by SCMFSA_9:def 5
.= (Initialize s) . x by A5, SCMFSA_2:89
.= s . x by A2, SCMFSA6A:38 ; :: thesis: verum

end;

now

let x be FinSeq-Location ; :: thesis: ((StepTimes a,I,s) . 0 ) . x = s . x
thus ((StepTimes a,I,s) . 0 ) . x = (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialize s)) . x by SCMFSA_9:def 5
.= (Initialize s) . x by SCMFSA_2:89
.= s . x by SCMFSA6C:3 ; :: thesis: verum

end;

hence ((StepTimes a,I,s) . 0 ) | ((UsedIntLoc I) \/ FinSeq-Locations ) = s | ((UsedIntLoc I) \/ FinSeq-Locations ) by A3, Th7; :: thesis: verum