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
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
( FinSeqMin (f,aa,bb,c) is_closed_on s,p & FinSeqMin (f,aa,bb,c) is_halting_on s,p )
let c be read-write Int-Location ; :: thesis: for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
( FinSeqMin (f,aa,bb,c) is_closed_on s,p & FinSeqMin (f,aa,bb,c) is_halting_on s,p )
let aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
( FinSeqMin (f,aa,bb,c) is_closed_on s,p & FinSeqMin (f,aa,bb,c) is_halting_on s,p )
let f be FinSeq-Location ; :: thesis: for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
( FinSeqMin (f,aa,bb,c) is_closed_on s,p & FinSeqMin (f,aa,bb,c) is_halting_on s,p )
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 implies ( FinSeqMin (f,aa,bb,c) is_closed_on s,p & FinSeqMin (f,aa,bb,c) is_halting_on s,p ) )
assume A1: s . (intloc 0) = 1 ; :: thesis: ( FinSeqMin (f,aa,bb,c) is_closed_on s,p & FinSeqMin (f,aa,bb,c) is_halting_on s,p )
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)),p,s);
set p1 = p;
A2: (IExec ((Macro (c := aa)),p,s)) . (intloc 0) = (IExec ((Macro (c := aa)),p,s)) . (intloc 0)
.= (Exec ((c := aa),(Initialized s))) . (intloc 0) by SCMFSA6C:5
.= (Exec ((c := aa),(Initialized s))) . (intloc 0)
.= (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA6A:38 ;
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)),p,s),p by Th32;
A4: ( Macro (c := aa) is_closed_on Initialized s,p & Macro (c := aa) is_halting_on Initialized s,p ) by SCMFSA7B:18, SCMFSA7B:19;
then A5: FinSeqMin (f,aa,bb,c) is_closed_on Initialized s,p by A3, SFMASTR1:2;
hence FinSeqMin (f,aa,bb,c) is_closed_on s,p by A1, SFMASTR2:4; :: thesis: FinSeqMin (f,aa,bb,c) is_halting_on s,p
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)),p,s),p by A2, Th32;
then FinSeqMin (f,aa,bb,c) is_halting_on Initialized s,p by A3, A4, SFMASTR1:3;
hence FinSeqMin (f,aa,bb,c) is_halting_on s,p by A1, A5, SFMASTR2:5; :: thesis: verum