let f be FinSeq-Location ; :: thesis: for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . f = (Exec j,(IExec I,s)) . f
let s be State of SCM+FSA ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . f = (Exec j,(IExec I,s)) . f
let I be parahalting keeping_0 Program of SCM+FSA ; :: thesis: for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . f = (Exec j,(IExec I,s)) . f
let j be parahalting Instruction of SCM+FSA ; :: thesis: (IExec (I ';' j),s) . f = (Exec j,(IExec I,s)) . f
set Mj = Macro j;
set SA = Start-At ((IC (IExec (Macro j),(IExec I,s))) + (card I));
A1: ( not f in dom (Start-At ((IC (IExec (Macro j),(IExec I,s))) + (card I))) & f in dom (IExec (Macro j),(IExec I,s)) ) by SCMFSA6B:10, SCMFSA_2:67;
A2: DataPart (Initialize (IExec I,s)) = DataPart (IExec I,s) by Lm3;
f in FinSeq-Locations by SCMFSA_2:10;
then A3: f in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
thus (IExec (I ';' j),s) . f = ((IExec (Macro j),(IExec I,s)) +* (Start-At ((IC (IExec (Macro j),(IExec I,s))) + (card I)))) . f by SCMFSA6B:44
.= (IExec (Macro j),(IExec I,s)) . f by A1, FUNCT_4:12
.= (Exec j,(Initialize (IExec I,s))) . f by Th6
.= (DataPart (Exec j,(Initialize (IExec I,s)))) . f by A3, FUNCT_1:72, SCMFSA_2:127
.= (DataPart (Exec j,(IExec I,s))) . f by A2, Th5
.= (Exec j,(IExec I,s)) . f by A3, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum