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) \/ (UsedI*Loc p)) \/ (UsedILoc 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) \/ (UsedI*Loc p)) \/ (UsedILoc 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) \/ (UsedI*Loc p)) \/ (UsedILoc p) & x is not Int-Location implies x is FinSeq-Location )
set D1 = UsedI*Loc p;
set D2 = UsedILoc p;
assume that
A1: dom t c= Int-Locations \/ FinSeq-Locations and
A2: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis: ( x is Int-Location or x is FinSeq-Location )
( x in (dom t) \/ (UsedI*Loc p) or x in UsedILoc p ) by A2, XBOOLE_0:def 3;
then A3: ( x in dom t or x in UsedI*Loc p or x in UsedILoc p ) by XBOOLE_0:def 3;
per cases ( x in Int-Locations or x in FinSeq-Locations or x in UsedI*Loc p or x in UsedILoc 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 AMI_2:def 16; :: 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:def 5; :: thesis: verum
end;
suppose x in UsedI*Loc p ; :: thesis: ( x is Int-Location or x is FinSeq-Location )
then x in FinSeq-Locations ;
hence ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:def 5; :: thesis: verum
end;
suppose x in UsedILoc p ; :: thesis: ( x is Int-Location or x is FinSeq-Location )
then x in Int-Locations ;
hence ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def 16; :: thesis: verum
end;
end;