let c be read-write Int-Location; :: thesis: for aa, bb being Int-Location
for f being FinSeq-Location st c <> aa holds
not FinSeqMin (f,aa,bb,c) destroys aa
let aa, bb be Int-Location; :: thesis: for f being FinSeq-Location st c <> aa holds
not FinSeqMin (f,aa,bb,c) destroys aa
let f be FinSeq-Location ; :: thesis: ( c <> aa implies not FinSeqMin (f,aa,bb,c) destroys aa )
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 i10 = (1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}));
set i11 = (2 -ndRWNotIn {aa,bb,c}) := (f,c);
reconsider I12 = if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)) as really-closed MacroInstruction of SCM+FSA ;
set I1B = (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" I12;
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))) ";" I12));
A1: not Stop SCM+FSA destroys aa by SCMFSA8C:56;
A2: aa in {aa,bb,c} by ENUMSET1:def 1;
then 1 -stRWNotIn {aa,bb,c} <> aa by SCMFSA_M:25;
then A3: not (1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c})) destroys aa by SCMFSA7B:14;
A4: 2 -ndRWNotIn {aa,bb,c} <> aa by A2, SCMFSA_M:25;
then not (2 -ndRWNotIn {aa,bb,c}) := (f,c) destroys aa by SCMFSA7B:14;
then A5: not ((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c)) destroys aa by A3, SCMFSA8C:55;
assume A6: c <> aa ; :: thesis: not FinSeqMin (f,aa,bb,c) destroys aa
then not Macro (c := (3 -rdRWNotIn {aa,bb,c})) destroys aa by SCMFSA7B:6, SCMFSA8C:48;
then not I12 destroys aa by A4, A1, Th7;
then A7: not (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" I12 destroys aa by A5, SCMFSA8C:52;
aa in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} by ENUMSET1:def 1;
then aa in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" I12)) by XBOOLE_0:def 3;
then A8: aa <> 1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" I12))) by SCMFSA_M:25;
3 -rdRWNotIn {aa,bb,c} <> aa by A2, SCMFSA_M:25;
then not 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))) ";" I12)) destroys aa by A7, A8, Th21;
hence not FinSeqMin (f,aa,bb,c) destroys aa by A6, SCMFSA7B:6, SCMFSA8C:53; :: thesis: verum