let a be Int-Location; for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being sequential keeping_0 Instruction of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA
for i being sequential keeping_0 Instruction of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
let P be Instruction-Sequence of SCM+FSA; for i being sequential keeping_0 Instruction of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
let i be sequential keeping_0 Instruction of SCM+FSA; for j being sequential Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
let j be sequential Instruction of SCM+FSA; (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
set Mi = Macro i;
thus (IExec ((i ";" j),P,s)) . a =
(IExec (((Macro i) ";" j),P,s)) . a
.=
(Exec (j,(IExec ((Macro i),P,s)))) . a
by Th5
.=
(Exec (j,(Exec (i,(Initialized s))))) . a
by Th4
; verum