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