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