let t be FinPartState of SCM+FSA; :: thesis: for p being Program of
for x being set st dom t c= Int-Locations \/ FinSeq-Locations & x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) & x is not Int-Location holds
x is FinSeq-Location
let p be Program of ; :: thesis: for x being set st dom t c= Int-Locations \/ FinSeq-Locations & x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) & x is not Int-Location holds
x is FinSeq-Location
let x be set ; :: thesis: ( dom t c= Int-Locations \/ FinSeq-Locations & x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) & x is not Int-Location implies x is FinSeq-Location )
set D1 = UsedInt*Loc p;
set D2 = UsedIntLoc p;
assume that
A1: dom t c= Int-Locations \/ FinSeq-Locations and
A2: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: ( x is Int-Location or x is FinSeq-Location )
( x in (dom t) \/ (UsedInt*Loc p) or x in UsedIntLoc p ) by A2, XBOOLE_0:def 3;
then A3: ( x in dom t or x in UsedInt*Loc p or x in UsedIntLoc p ) by XBOOLE_0:def 3;

per cases ( x in Int-Locations or x in FinSeq-Locations or x in UsedInt*Loc p or x in UsedIntLoc p ) by A1, A3, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ( x is Int-Location or x is FinSeq-Location )

hence ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:4; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ( x is Int-Location or x is FinSeq-Location )

hence ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:5; :: thesis: verum

end;

suppose x in UsedInt*Loc p ; :: thesis: ( x is Int-Location or x is FinSeq-Location )

hence ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:5; :: thesis: verum

end;

suppose x in UsedIntLoc p ; :: thesis: ( x is Int-Location or x is FinSeq-Location )

hence ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:4; :: thesis: verum

end;

end;