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 Initialized s & Ig is_closed_on Initialized 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 Initialized s & Ig is_closed_on Initialized 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 Initialized s & Ig is_closed_on Initialized 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 Initialized s & Ig is_closed_on Initialized 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 Initialized s & Ig is_closed_on Initialized 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: J is_halting_on IExec (Ig,s) by A2, SCMFSA7B:25;
A4: Ig is_closed_on Initialized s by A1, SCMFSA7B:24;
A5: not a in dom (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA)) by SCMFSA6B:9;
A6: J is_closed_on IExec (Ig,s) by A2, SCMFSA7B:24;
Ig is_halting_on Initialized 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)) . a = (IExec (J,(IExec (Ig,s)))) . a by A5, FUNCT_4:12; :: thesis: verum