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 destroysdestroy aa
let aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location st c <> aa holds
not FinSeqMin f,aa,bb,c destroysdestroy aa
let f be FinSeq-Location ; :: thesis: ( c <> aa implies not FinSeqMin f,aa,bb,c destroysdestroy 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;
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: not Stop SCM+FSA destroysdestroy aa by SCMFSA8C:85;
A2: aa in {aa,bb,c} by ENUMSET1:def 1;
then 1 -stRWNotIn {aa,bb,c} <> aa by SFMASTR1:21;
then A3: not (1 -stRWNotIn {aa,bb,c}) := f,(3 -rdRWNotIn {aa,bb,c}) destroysdestroy aa by SCMFSA7B:20;
A4: 2 -ndRWNotIn {aa,bb,c} <> aa by A2, SFMASTR1:21;
then not (2 -ndRWNotIn {aa,bb,c}) := f,c destroysdestroy aa by SCMFSA7B:20;
then A5: not ((1 -stRWNotIn {aa,bb,c}) := f,(3 -rdRWNotIn {aa,bb,c})) ';' ((2 -ndRWNotIn {aa,bb,c}) := f,c) destroysdestroy aa by A3, SCMFSA8C:84;
assume A6: c <> aa ; :: thesis: not FinSeqMin f,aa,bb,c destroysdestroy aa
then not Macro (c := (3 -rdRWNotIn {aa,bb,c})) destroysdestroy aa by SCMFSA7B:12, SCMFSA8C:77;
then not if>0 (2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA ) destroysdestroy aa by A4, A1, Th15;
then A7: not (((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 )) destroysdestroy aa by A5, SCMFSA8C:81;
aa in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} by ENUMSET1:def 1;
then aa 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;
then A8: aa <> 1 -stRWNotIn ({(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 SFMASTR1:21;
3 -rdRWNotIn {aa,bb,c} <> aa by A2, SFMASTR1:21;
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)) ';' (if>0 (2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA ))) destroysdestroy aa by A7, A8, Th29;
hence not FinSeqMin f,aa,bb,c destroysdestroy aa by A6, SCMFSA7B:12, SCMFSA8C:82; :: thesis: verum