let s be State of SCM+FSA ; :: thesis: for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for a being Int-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) . a = (IExec J,(IExec Ig,s)) . a
let J be Program of SCM+FSA ; :: thesis: for Ig being good Program of SCM+FSA
for a being Int-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) . a = (IExec J,(IExec Ig,s)) . a
let Ig be good Program of SCM+FSA ; :: thesis: for a being Int-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) . a = (IExec J,(IExec Ig,s)) . a
let a be Int-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) . a = (IExec J,(IExec Ig,s)) . a )
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) . a = (IExec J,(IExec Ig,s)) . a
A3: Ig is_halting_on Initialize s by A1, SCMFSA7B:25;
A4: J is_halting_on IExec Ig,s by A2, SCMFSA7B:25;
A5: Ig is_closed_on Initialize s by A1, SCMFSA7B:24;
J is_closed_on IExec Ig,s by A2, SCMFSA7B:24;
then A6: IExec (Ig ';' J),s = (IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig))) by A3, A4, A5, Th7;
not a in dom (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig))) by SCMFSA6B:9;
hence (IExec (Ig ';' J),s) . a = (IExec J,(IExec Ig,s)) . a by A6, FUNCT_4:12; :: thesis: verum