let c be read-write Int-Location ; :: thesis: for aa, bb being Int-Location
for f being FinSeq-Location holds {aa,bb,c} c= UsedIntLoc (FinSeqMin (f,aa,bb,c))
let aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location holds {aa,bb,c} c= UsedIntLoc (FinSeqMin (f,aa,bb,c))
let f be FinSeq-Location ; :: thesis: {aa,bb,c} c= UsedIntLoc (FinSeqMin (f,aa,bb,c))
set a = aa;
set b = bb;
set aux1 = 1 -stRWNotIn {aa,bb,c};
set aux2 = 2 -ndRWNotIn {aa,bb,c};
set cv = 3 -rdRWNotIn {aa,bb,c};
set i0 = c := aa;
set i10 = (1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}));
set i11 = (2 -ndRWNotIn {aa,bb,c}) := (f,c);
set I12 = if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA));
set I1B = (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ';' (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)));
set I1 = for-up ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ';' (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))));
A1: UsedIntLoc ((c := aa) ';' (for-up ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ';' (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))) = (UsedIntLoc (c := aa)) \/ (UsedIntLoc (for-up ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ';' (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))) by SF_MASTR:29;
A2: {(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ';' (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))) c= UsedIntLoc (for-up ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ';' (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))))) by Th28;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {aa,bb,c} or x in UsedIntLoc (FinSeqMin (f,aa,bb,c)) )
A3: UsedIntLoc (c := aa) = {c,aa} by SF_MASTR:14;
assume A4: x in {aa,bb,c} ; :: thesis: x in UsedIntLoc (FinSeqMin (f,aa,bb,c))

per cases ( x = aa or x = bb or x = c ) by A4, ENUMSET1:def 1;

suppose x = aa ; :: thesis: x in UsedIntLoc (FinSeqMin (f,aa,bb,c))

then x in {c,aa} by TARSKI:def 2;
hence x in UsedIntLoc (FinSeqMin (f,aa,bb,c)) by A1, A3, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = bb ; :: thesis: x in UsedIntLoc (FinSeqMin (f,aa,bb,c))

then x in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} by ENUMSET1:def 1;
then x in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ';' (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))) by XBOOLE_0:def 3;
hence x in UsedIntLoc (FinSeqMin (f,aa,bb,c)) by A1, A2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = c ; :: thesis: x in UsedIntLoc (FinSeqMin (f,aa,bb,c))

then x in {c,aa} by TARSKI:def 2;
hence x in UsedIntLoc (FinSeqMin (f,aa,bb,c)) by A1, A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;