let f be FinSeq-Location ; :: thesis: for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (i ';' j),s) . f = (Exec j,(Exec i,(Initialize s))) . f
let s be State of SCM+FSA ; :: thesis: for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (i ';' j),s) . f = (Exec j,(Exec i,(Initialize s))) . f
let i be parahalting keeping_0 Instruction of SCM+FSA ; :: thesis: for j being parahalting Instruction of SCM+FSA holds (IExec (i ';' j),s) . f = (Exec j,(Exec i,(Initialize s))) . f
let j be parahalting Instruction of SCM+FSA ; :: thesis: (IExec (i ';' j),s) . f = (Exec j,(Exec i,(Initialize s))) . f
set Mi = Macro i;
thus (IExec (i ';' j),s) . f = (IExec ((Macro i) ';' j),s) . f
.= (Exec j,(IExec (Macro i),s)) . f by Th8
.= (Exec j,(Exec i,(Initialize s))) . f by Th6 ; :: thesis: verum