let s be State of SCM+FSA ; :: thesis: for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location st s . (intloc 0 ) = 1 holds
( FinSeqMin f,aa,bb,c is_closed_on s & FinSeqMin f,aa,bb,c is_halting_on s )
let c be read-write Int-Location ; :: thesis: for aa, bb being Int-Location
for f being FinSeq-Location st s . (intloc 0 ) = 1 holds
( FinSeqMin f,aa,bb,c is_closed_on s & FinSeqMin f,aa,bb,c is_halting_on s )
let aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location st s . (intloc 0 ) = 1 holds
( FinSeqMin f,aa,bb,c is_closed_on s & FinSeqMin f,aa,bb,c is_halting_on s )
let f be FinSeq-Location ; :: thesis: ( s . (intloc 0 ) = 1 implies ( FinSeqMin f,aa,bb,c is_closed_on s & FinSeqMin f,aa,bb,c is_halting_on s ) )
assume A1: s . (intloc 0 ) = 1 ; :: thesis: ( FinSeqMin f,aa,bb,c is_closed_on s & FinSeqMin f,aa,bb,c is_halting_on s )
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 )));
set s1 = IExec (Macro (c := aa)),s;
(IExec (Macro (c := aa)),s) . (intloc 0 ) = (Exec (c := aa),(Initialize s)) . (intloc 0 ) by SCMFSA6C:6
.= (Initialize s) . (intloc 0 ) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
then A3: ( 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 ))) is_closed_on IExec (Macro (c := aa)),s & 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 ))) is_halting_on IExec (Macro (c := aa)),s ) by Th32;
A4: Macro (c := aa) is_closed_on Initialize s by SCMFSA7B:24;
A5: Macro (c := aa) is_halting_on Initialize s by SCMFSA7B:25;
then A6: FinSeqMin f,aa,bb,c is_closed_on Initialize s by A3, A4, SFMASTR1:3;
hence FinSeqMin f,aa,bb,c is_closed_on s by A1, SFMASTR2:4; :: thesis: FinSeqMin f,aa,bb,c is_halting_on s
FinSeqMin f,aa,bb,c is_halting_on Initialize s by A3, A4, A5, SFMASTR1:4;
hence FinSeqMin f,aa,bb,c is_halting_on s by A1, A6, SFMASTR2:5; :: thesis: verum