let s be State of SCM+FSA ; :: thesis: for f being FinSeq-Location
for I being InitHalting keepInt0_1 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 f be FinSeq-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) . f = (Exec j,(IExec I,s)) . f
let I be InitHalting keepInt0_1 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)),SCM+FSA ;
A1: not f in dom (Start-At ((IC (IExec (Macro j),(IExec I,s))) + (card I)),SCM+FSA ) by SCMFSA6B:10;
A2: DataPart (Initialize (IExec I,s)) = DataPart (IExec I,s) by Th32;
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)),SCM+FSA )) . f by Th29
.= (IExec (Macro j),(IExec I,s)) . f by A1, FUNCT_4:12
.= (Exec j,(Initialize (IExec I,s))) . f by SCMFSA6C:6
.= (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, SCMFSA6C:5
.= (Exec j,(IExec I,s)) . f by A3, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum