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

A2: now

let x be Int-Location ; :: thesis: ( x in UsedIntLoc I implies ((StepTimes a,I,s) . 0 ) . x = s . x )
A3: not 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) in {a} \/ (UsedIntLoc I) by SFMASTR1:21;
assume x in UsedIntLoc I ; :: thesis: ((StepTimes a,I,s) . 0 ) . x = s . x
then A4: 1 -stRWNotIn ({a} \/ (UsedIntLoc I)) <> x by A3, 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 A4, SCMFSA_2:89
.= s . x by A1, 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 A2, Th7; :: thesis: verum