let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for j being sequential Instruction of SCM+FSA
for f being FinSeq-Location
for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
let s be State of SCM+FSA; for j being sequential Instruction of SCM+FSA
for f being FinSeq-Location
for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
let j be sequential Instruction of SCM+FSA; for f being FinSeq-Location
for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
let f be FinSeq-Location ; for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
let Ig be good really-closed Program of SCM+FSA; ( ( Ig is parahalting or Ig is_halting_on Initialized s,p ) implies (IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f )
set I = Ig;
set Mj = Macro j;
f in FinSeq-Locations
by SCMFSA_2:def 5;
then A1:
f in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
assume A2:
( Ig is parahalting or Ig is_halting_on Initialized s,p )
; (IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
A3:
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
by A2, Th9;
thus (IExec ((Ig ";" j),p,s)) . f =
(IExec ((Macro j),p,(IExec (Ig,p,s)))) . f
by A2, Th7
.=
(IExec ((Macro j),p,(IExec (Ig,p,s)))) . f
.=
(Exec (j,(Initialized (IExec (Ig,p,s))))) . f
by SCMFSA6C:5
.=
(Exec (j,(Initialized (IExec (Ig,p,s))))) . f
.=
(DataPart (Exec (j,(Initialized (IExec (Ig,p,s)))))) . f
by A1, FUNCT_1:49
.=
(DataPart (Exec (j,(IExec (Ig,p,s))))) . f
by A3, SCMFSA6C:4
.=
(Exec (j,(IExec (Ig,p,s)))) . f
by A1, FUNCT_1:49
; verum