let s be State of SCM+FSA ; :: thesis: for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) & ( J is parahalting or ( J is_halting_on IExec Ig,s & J is_closed_on IExec Ig,s ) ) holds
(IExec (Ig ';' J),s) . f = (IExec J,(IExec Ig,s)) . f
let J be Program of SCM+FSA ; :: thesis: for Ig being good Program of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) & ( J is parahalting or ( J is_halting_on IExec Ig,s & J is_closed_on IExec Ig,s ) ) holds
(IExec (Ig ';' J),s) . f = (IExec J,(IExec Ig,s)) . f
let Ig be good Program of SCM+FSA ; :: thesis: for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) & ( J is parahalting or ( J is_halting_on IExec Ig,s & J is_closed_on IExec Ig,s ) ) holds
(IExec (Ig ';' J),s) . f = (IExec J,(IExec Ig,s)) . f
let f be FinSeq-Location ; :: thesis: ( ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) & ( J is parahalting or ( J is_halting_on IExec Ig,s & J is_closed_on IExec Ig,s ) ) implies (IExec (Ig ';' J),s) . f = (IExec J,(IExec Ig,s)) . f )
set I = Ig;
assume that
A1: ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) and
A2: ( J is parahalting or ( J is_halting_on IExec Ig,s & J is_closed_on IExec Ig,s ) ) ; :: thesis: (IExec (Ig ';' J),s) . f = (IExec J,(IExec Ig,s)) . f
A3: J is_halting_on IExec Ig,s by A2, SCMFSA7B:25;
A4: Ig is_closed_on Initialize s by A1, SCMFSA7B:24;
A5: not f in dom (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig)),SCM+FSA ) by SCMFSA6B:10;
A6: J is_closed_on IExec Ig,s by A2, SCMFSA7B:24;
Ig is_halting_on Initialize s by A1, SCMFSA7B:25;
then IExec (Ig ';' J),s = (IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig)),SCM+FSA ) by A3, A4, A6, Th7;
hence (IExec (Ig ';' J),s) . f = (IExec J,(IExec Ig,s)) . f by A5, FUNCT_4:12; :: thesis: verum