let s be State of SCM+FSA ; :: thesis: for a being Int-Location
for I being InitHalting keepInt0_1 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . a = (Exec j,(IExec I,s)) . a
let a be Int-Location ; :: thesis: for I being InitHalting keepInt0_1 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . a = (Exec j,(IExec I,s)) . a
let I be InitHalting keepInt0_1 Program of SCM+FSA ; :: thesis: for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . a = (Exec j,(IExec I,s)) . a
let j be parahalting Instruction of SCM+FSA ; :: 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))) & a in dom (IExec (Macro j),(IExec I,s)) ) by SCMFSA6B:9, SCMFSA_2:66;
A2: DataPart (Initialize (IExec I,s)) = DataPart (IExec I,s) by Th32;
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 Th29
.= (IExec (Macro j),(IExec I,s)) . a by A1, FUNCT_4:12
.= (Exec j,(Initialize (IExec I,s))) . a by SCMFSA6C:6
.= (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, SCMFSA6C:5
.= (Exec j,(IExec I,s)) . a by A3, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum