let a be Int-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) . a = (Exec j,(Exec i,(Initialize s))) . a
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) . a = (Exec j,(Exec i,(Initialize s))) . a
let i be parahalting keeping_0 Instruction of SCM+FSA ; :: thesis: for j being parahalting Instruction of SCM+FSA holds (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a
let j be parahalting Instruction of SCM+FSA ; :: thesis: (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a
set Mi = Macro i;
thus (IExec (i ';' j),s) . a = (IExec ((Macro i) ';' j),s) . a
.= (Exec j,(IExec (Macro i),s)) . a by Th7
.= (Exec j,(Exec i,(Initialize s))) . a by Th6 ; :: thesis: verum