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);
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 destroys 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})) destroys aa by SCMFSA7B:20;
A4: 2 -ndRWNotIn {aa,bb,c} <> aa by A2, SFMASTR1:21;
then not (2 -ndRWNotIn {aa,bb,c}) := (f,c) destroys 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)) destroys aa by A3, SCMFSA8C:84;
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: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)) destroys 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))) destroys 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))))) destroys aa by A7, A8, Th29;
hence not FinSeqMin (f,aa,bb,c) destroys aa by A6, SCMFSA7B:12, SCMFSA8C:82; :: thesis: verum